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

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

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

(0) Obligation:

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

Begin(b(x)) → Wait(Right1(x))
Begin(b(s(x))) → Wait(Right2(x))
Begin(s(x)) → Wait(Right3(x))
Begin(b(x)) → Wait(Right4(x))
Begin(b(s(x))) → Wait(Right5(x))
Begin(s(x)) → Wait(Right6(x))
Begin(u(x)) → Wait(Right7(x))
Begin(s(x)) → Wait(Right8(x))
Begin(u(x)) → Wait(Right9(x))
Begin(u(x)) → Wait(Right10(x))
Right1(s(End(x))) → Left(b(s(s(s(End(x))))))
Right2(s(End(x))) → Left(b(t(End(x))))
Right3(s(b(End(x)))) → Left(b(t(End(x))))
Right4(t(End(x))) → Left(b(s(End(x))))
Right5(t(End(x))) → Left(u(t(b(End(x)))))
Right6(t(b(End(x)))) → Left(u(t(b(End(x)))))
Right7(b(End(x))) → Left(b(s(End(x))))
Right8(t(End(x))) → Left(t(t(End(x))))
Right9(t(End(x))) → Left(u(t(End(x))))
Right10(s(End(x))) → Left(s(s(End(x))))
Right1(s(x)) → As(Right1(x))
Right2(s(x)) → As(Right2(x))
Right3(s(x)) → As(Right3(x))
Right4(s(x)) → As(Right4(x))
Right5(s(x)) → As(Right5(x))
Right6(s(x)) → As(Right6(x))
Right7(s(x)) → As(Right7(x))
Right8(s(x)) → As(Right8(x))
Right9(s(x)) → As(Right9(x))
Right10(s(x)) → As(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))
Right1(t(x)) → At(Right1(x))
Right2(t(x)) → At(Right2(x))
Right3(t(x)) → At(Right3(x))
Right4(t(x)) → At(Right4(x))
Right5(t(x)) → At(Right5(x))
Right6(t(x)) → At(Right6(x))
Right7(t(x)) → At(Right7(x))
Right8(t(x)) → At(Right8(x))
Right9(t(x)) → At(Right9(x))
Right10(t(x)) → At(Right10(x))
Right1(u(x)) → Au(Right1(x))
Right2(u(x)) → Au(Right2(x))
Right3(u(x)) → Au(Right3(x))
Right4(u(x)) → Au(Right4(x))
Right5(u(x)) → Au(Right5(x))
Right6(u(x)) → Au(Right6(x))
Right7(u(x)) → Au(Right7(x))
Right8(u(x)) → Au(Right8(x))
Right9(u(x)) → Au(Right9(x))
Right10(u(x)) → Au(Right10(x))
As(Left(x)) → Left(s(x))
Ab(Left(x)) → Left(b(x))
At(Left(x)) → Left(t(x))
Au(Left(x)) → Left(u(x))
Wait(Left(x)) → Begin(x)
s(b(x)) → b(s(s(s(x))))
s(b(s(x))) → b(t(x))
t(b(x)) → b(s(x))
t(b(s(x))) → u(t(b(x)))
b(u(x)) → b(s(x))
t(s(x)) → t(t(x))
t(u(x)) → u(t(x))
s(u(x)) → s(s(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 u t End → Wait Left u t End

Wait Left u t End → Wait Left u t End
by OverlapClosure OC 2
Wait Left u → Wait Right9
by OverlapClosure OC 2
Wait Left → Begin
by original rule (OC 1)
Begin u → Wait Right9
by original rule (OC 1)
Right9 t End → Left u t End
by original rule (OC 1)

(2) NO