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

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

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

(0) Obligation:

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

Begin(a(x)) → Wait(Right1(x))
Begin(a(x)) → Wait(Right2(x))
Begin(l1(x)) → Wait(Right3(x))
Begin(a(l2(x))) → Wait(Right4(x))
Begin(l2(x)) → Wait(Right5(x))
Begin(b(x)) → Wait(Right6(x))
Begin(b(x)) → Wait(Right7(x))
Begin(l1(x)) → Wait(Right8(x))
Begin(l2(x)) → Wait(Right9(x))
Begin(a(x)) → Wait(Right10(x))
Right1(r1(End(x))) → Left(a(a(a(r1(End(x))))))
Right2(r2(End(x))) → Left(a(a(a(r2(End(x))))))
Right3(a(End(x))) → Left(l1(a(a(a(End(x))))))
Right4(a(End(x))) → Left(l2(a(a(End(x)))))
Right5(a(a(End(x)))) → Left(l2(a(a(End(x)))))
Right6(r1(End(x))) → Left(l1(b(End(x))))
Right7(r2(End(x))) → Left(l2(a(b(End(x)))))
Right8(b(End(x))) → Left(b(r2(End(x))))
Right9(b(End(x))) → Left(b(r1(End(x))))
Right10(a(End(x))) → Left(End(x))
Right1(r1(x)) → Ar1(Right1(x))
Right2(r1(x)) → Ar1(Right2(x))
Right3(r1(x)) → Ar1(Right3(x))
Right4(r1(x)) → Ar1(Right4(x))
Right5(r1(x)) → Ar1(Right5(x))
Right6(r1(x)) → Ar1(Right6(x))
Right7(r1(x)) → Ar1(Right7(x))
Right8(r1(x)) → Ar1(Right8(x))
Right9(r1(x)) → Ar1(Right9(x))
Right10(r1(x)) → Ar1(Right10(x))
Right1(a(x)) → Aa(Right1(x))
Right2(a(x)) → Aa(Right2(x))
Right3(a(x)) → Aa(Right3(x))
Right4(a(x)) → Aa(Right4(x))
Right5(a(x)) → Aa(Right5(x))
Right6(a(x)) → Aa(Right6(x))
Right7(a(x)) → Aa(Right7(x))
Right8(a(x)) → Aa(Right8(x))
Right9(a(x)) → Aa(Right9(x))
Right10(a(x)) → Aa(Right10(x))
Right1(r2(x)) → Ar2(Right1(x))
Right2(r2(x)) → Ar2(Right2(x))
Right3(r2(x)) → Ar2(Right3(x))
Right4(r2(x)) → Ar2(Right4(x))
Right5(r2(x)) → Ar2(Right5(x))
Right6(r2(x)) → Ar2(Right6(x))
Right7(r2(x)) → Ar2(Right7(x))
Right8(r2(x)) → Ar2(Right8(x))
Right9(r2(x)) → Ar2(Right9(x))
Right10(r2(x)) → Ar2(Right10(x))
Right1(l1(x)) → Al1(Right1(x))
Right2(l1(x)) → Al1(Right2(x))
Right3(l1(x)) → Al1(Right3(x))
Right4(l1(x)) → Al1(Right4(x))
Right5(l1(x)) → Al1(Right5(x))
Right6(l1(x)) → Al1(Right6(x))
Right7(l1(x)) → Al1(Right7(x))
Right8(l1(x)) → Al1(Right8(x))
Right9(l1(x)) → Al1(Right9(x))
Right10(l1(x)) → Al1(Right10(x))
Right1(l2(x)) → Al2(Right1(x))
Right2(l2(x)) → Al2(Right2(x))
Right3(l2(x)) → Al2(Right3(x))
Right4(l2(x)) → Al2(Right4(x))
Right5(l2(x)) → Al2(Right5(x))
Right6(l2(x)) → Al2(Right6(x))
Right7(l2(x)) → Al2(Right7(x))
Right8(l2(x)) → Al2(Right8(x))
Right9(l2(x)) → Al2(Right9(x))
Right10(l2(x)) → Al2(Right10(x))
Right1(b(x)) → Ab(Right1(x))
Right2(b(x)) → Ab(Right2(x))
Right3(b(x)) → Ab(Right3(x))
Right4(b(x)) → Ab(Right4(x))
Right5(b(x)) → Ab(Right5(x))
Right6(b(x)) → Ab(Right6(x))
Right7(b(x)) → Ab(Right7(x))
Right8(b(x)) → Ab(Right8(x))
Right9(b(x)) → Ab(Right9(x))
Right10(b(x)) → Ab(Right10(x))
Ar1(Left(x)) → Left(r1(x))
Aa(Left(x)) → Left(a(x))
Ar2(Left(x)) → Left(r2(x))
Al1(Left(x)) → Left(l1(x))
Al2(Left(x)) → Left(l2(x))
Ab(Left(x)) → Left(b(x))
Wait(Left(x)) → Begin(x)
r1(a(x)) → a(a(a(r1(x))))
r2(a(x)) → a(a(a(r2(x))))
a(l1(x)) → l1(a(a(a(x))))
a(a(l2(x))) → l2(a(a(x)))
r1(b(x)) → l1(b(x))
r2(b(x)) → l2(a(b(x)))
b(l1(x)) → b(r2(x))
b(l2(x)) → b(r1(x))
a(a(x)) → 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:
Wait Left l2 a a End → Wait Left l2 a a End

Wait Left l2 a a End → Wait Left l2 a a End
by OverlapClosure OC 2
Wait Left l2 → Wait Right5
by OverlapClosure OC 2
Wait Left → Begin
by original rule (OC 1)
Begin l2 → Wait Right5
by original rule (OC 1)
Right5 a a End → Left l2 a a End
by original rule (OC 1)

(2) NO