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

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

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

(0) Obligation:

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

B(x) → W(M(M(V(x))))
M(x) → x
M(V(P(x))) → V(XP(x))
M(V(Q(x))) → V(XQ(x))
M(V(p(x))) → V(Xp(x))
M(V(q(x))) → V(Xq(x))
XP(P(x)) → P(XP(x))
XP(Q(x)) → Q(XP(x))
XP(p(x)) → p(XP(x))
XP(q(x)) → q(XP(x))
XQ(P(x)) → P(XQ(x))
XQ(Q(x)) → Q(XQ(x))
XQ(p(x)) → p(XQ(x))
XQ(q(x)) → q(XQ(x))
Xp(P(x)) → P(Xp(x))
Xp(Q(x)) → Q(Xp(x))
Xp(p(x)) → p(Xp(x))
Xp(q(x)) → q(Xp(x))
Xq(P(x)) → P(Xq(x))
Xq(Q(x)) → Q(Xq(x))
Xq(p(x)) → p(Xq(x))
Xq(q(x)) → q(Xq(x))
XP(E(x)) → P(E(x))
XQ(E(x)) → Q(E(x))
Xp(E(x)) → p(E(x))
Xq(E(x)) → q(E(x))
W(V(x)) → R(L(x))
L(P(x)) → YP(L(x))
L(Q(x)) → YQ(L(x))
L(p(x)) → Yp(L(x))
L(q(x)) → Yq(L(x))
L(P(x)) → D(Q(Q(p(x))))
L(p(p(x))) → D(q(q(x)))
L(p(Q(Q(x)))) → D(Q(Q(p(x))))
L(Q(p(q(x)))) → D(q(p(Q(x))))
L(q(q(p(x)))) → D(p(q(q(x))))
L(q(Q(x))) → D(x)
L(Q(q(x))) → D(x)
L(p(P(x))) → D(x)
L(P(p(x))) → D(x)
YP(D(x)) → D(P(x))
YQ(D(x)) → D(Q(x))
Yp(D(x)) → D(p(x))
Yq(D(x)) → D(q(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:
W V q q p E → W V q q p E

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

(2) NO