NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z113-shift.srs

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 NonTerminationProof (⇒, 2386 ms)
↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

B(x) → W(M(V(x)))
M(x) → x
M(V(1(x))) → V(X1(x))
M(V(4(x))) → V(X4(x))
M(V(3(x))) → V(X3(x))
M(V(2(x))) → V(X2(x))
M(V(5(x))) → V(X5(x))
M(V(6(x))) → V(X6(x))
X1(1(x)) → 1(X1(x))
X1(4(x)) → 4(X1(x))
X1(3(x)) → 3(X1(x))
X1(2(x)) → 2(X1(x))
X1(5(x)) → 5(X1(x))
X1(6(x)) → 6(X1(x))
X4(1(x)) → 1(X4(x))
X4(4(x)) → 4(X4(x))
X4(3(x)) → 3(X4(x))
X4(2(x)) → 2(X4(x))
X4(5(x)) → 5(X4(x))
X4(6(x)) → 6(X4(x))
X3(1(x)) → 1(X3(x))
X3(4(x)) → 4(X3(x))
X3(3(x)) → 3(X3(x))
X3(2(x)) → 2(X3(x))
X3(5(x)) → 5(X3(x))
X3(6(x)) → 6(X3(x))
X2(1(x)) → 1(X2(x))
X2(4(x)) → 4(X2(x))
X2(3(x)) → 3(X2(x))
X2(2(x)) → 2(X2(x))
X2(5(x)) → 5(X2(x))
X2(6(x)) → 6(X2(x))
X5(1(x)) → 1(X5(x))
X5(4(x)) → 4(X5(x))
X5(3(x)) → 3(X5(x))
X5(2(x)) → 2(X5(x))
X5(5(x)) → 5(X5(x))
X5(6(x)) → 6(X5(x))
X6(1(x)) → 1(X6(x))
X6(4(x)) → 4(X6(x))
X6(3(x)) → 3(X6(x))
X6(2(x)) → 2(X6(x))
X6(5(x)) → 5(X6(x))
X6(6(x)) → 6(X6(x))
X1(E(x)) → 1(E(x))
X4(E(x)) → 4(E(x))
X3(E(x)) → 3(E(x))
X2(E(x)) → 2(E(x))
X5(E(x)) → 5(E(x))
X6(E(x)) → 6(E(x))
W(V(x)) → R(L(x))
L(1(x)) → Y1(L(x))
L(4(x)) → Y4(L(x))
L(3(x)) → Y3(L(x))
L(2(x)) → Y2(L(x))
L(5(x)) → Y5(L(x))
L(6(x)) → Y6(L(x))
L(1(1(x))) → D(4(3(x)))
L(1(2(x))) → D(2(1(x)))
L(2(2(x))) → D(1(1(1(x))))
L(3(3(x))) → D(5(6(x)))
L(3(4(x))) → D(1(1(x)))
L(4(4(x))) → D(3(x))
L(5(5(x))) → D(6(2(x)))
L(5(6(x))) → D(1(2(x)))
L(6(6(x))) → D(2(1(x)))
Y1(D(x)) → D(1(x))
Y4(D(x)) → D(4(x))
Y3(D(x)) → D(3(x))
Y2(D(x)) → D(2(x))
Y5(D(x)) → D(5(x))
Y6(D(x)) → D(6(x))
R(D(x)) → B(x)

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:
B 2 1 E → B 2 1 E

B 2 1 E → B 2 1 E
by OverlapClosure OC 3
B 2 1 E → R D 2 1 E
by OverlapClosure OC 3
B 2 1 E → R L 1 2 E
by OverlapClosure OC 2
B 2 1 → R L 1 X2
by OverlapClosure OC 2
B 2 → R L X2
by OverlapClosure OC 3
B 2 → W V X2
by OverlapClosure OC 2
B → W M V
by original rule (OC 1)
M V 2 → V X2
by original rule (OC 1)
W V → R L
by original rule (OC 1)
X2 1 → 1 X2
by original rule (OC 1)
X2 E → 2 E
by original rule (OC 1)
L 1 2 → D 2 1
by original rule (OC 1)
R D → B
by original rule (OC 1)

(2) NO