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

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

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

(0) Obligation:

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

Begin(1(x)) → Wait(Right1(x))
Begin(9(x)) → Wait(Right2(x))
Begin(5(x)) → Wait(Right3(x))
Begin(4(x)) → Wait(Right4(x))
Begin(6(x)) → Wait(Right5(x))
Begin(8(x)) → Wait(Right6(x))
Begin(8(4(x))) → Wait(Right7(x))
Begin(4(x)) → Wait(Right8(x))
Begin(1(x)) → Wait(Right9(x))
Begin(9(x)) → Wait(Right10(x))
Begin(5(x)) → Wait(Right11(x))
Right1(3(End(x))) → Left(4(1(End(x))))
Right2(5(End(x))) → Left(2(6(5(End(x)))))
Right3(3(End(x))) → Left(8(9(7(End(x)))))
Right4(8(End(x))) → Left(6(End(x)))
Right5(2(End(x))) → Left(4(3(End(x))))
Right6(3(End(x))) → Left(3(2(7(End(x)))))
Right7(8(End(x))) → Left(1(9(End(x))))
Right8(8(8(End(x)))) → Left(1(9(End(x))))
Right9(7(End(x))) → Left(6(9(End(x))))
Right10(3(End(x))) → Left(9(3(End(x))))
Right11(7(End(x))) → Left(1(0(End(x))))
Right1(3(x)) → A3(Right1(x))
Right2(3(x)) → A3(Right2(x))
Right3(3(x)) → A3(Right3(x))
Right4(3(x)) → A3(Right4(x))
Right5(3(x)) → A3(Right5(x))
Right6(3(x)) → A3(Right6(x))
Right7(3(x)) → A3(Right7(x))
Right8(3(x)) → A3(Right8(x))
Right9(3(x)) → A3(Right9(x))
Right10(3(x)) → A3(Right10(x))
Right11(3(x)) → A3(Right11(x))
Right1(1(x)) → A1(Right1(x))
Right2(1(x)) → A1(Right2(x))
Right3(1(x)) → A1(Right3(x))
Right4(1(x)) → A1(Right4(x))
Right5(1(x)) → A1(Right5(x))
Right6(1(x)) → A1(Right6(x))
Right7(1(x)) → A1(Right7(x))
Right8(1(x)) → A1(Right8(x))
Right9(1(x)) → A1(Right9(x))
Right10(1(x)) → A1(Right10(x))
Right11(1(x)) → A1(Right11(x))
Right1(4(x)) → A4(Right1(x))
Right2(4(x)) → A4(Right2(x))
Right3(4(x)) → A4(Right3(x))
Right4(4(x)) → A4(Right4(x))
Right5(4(x)) → A4(Right5(x))
Right6(4(x)) → A4(Right6(x))
Right7(4(x)) → A4(Right7(x))
Right8(4(x)) → A4(Right8(x))
Right9(4(x)) → A4(Right9(x))
Right10(4(x)) → A4(Right10(x))
Right11(4(x)) → A4(Right11(x))
Right1(5(x)) → A5(Right1(x))
Right2(5(x)) → A5(Right2(x))
Right3(5(x)) → A5(Right3(x))
Right4(5(x)) → A5(Right4(x))
Right5(5(x)) → A5(Right5(x))
Right6(5(x)) → A5(Right6(x))
Right7(5(x)) → A5(Right7(x))
Right8(5(x)) → A5(Right8(x))
Right9(5(x)) → A5(Right9(x))
Right10(5(x)) → A5(Right10(x))
Right11(5(x)) → A5(Right11(x))
Right1(9(x)) → A9(Right1(x))
Right2(9(x)) → A9(Right2(x))
Right3(9(x)) → A9(Right3(x))
Right4(9(x)) → A9(Right4(x))
Right5(9(x)) → A9(Right5(x))
Right6(9(x)) → A9(Right6(x))
Right7(9(x)) → A9(Right7(x))
Right8(9(x)) → A9(Right8(x))
Right9(9(x)) → A9(Right9(x))
Right10(9(x)) → A9(Right10(x))
Right11(9(x)) → A9(Right11(x))
Right1(2(x)) → A2(Right1(x))
Right2(2(x)) → A2(Right2(x))
Right3(2(x)) → A2(Right3(x))
Right4(2(x)) → A2(Right4(x))
Right5(2(x)) → A2(Right5(x))
Right6(2(x)) → A2(Right6(x))
Right7(2(x)) → A2(Right7(x))
Right8(2(x)) → A2(Right8(x))
Right9(2(x)) → A2(Right9(x))
Right10(2(x)) → A2(Right10(x))
Right11(2(x)) → A2(Right11(x))
Right1(6(x)) → A6(Right1(x))
Right2(6(x)) → A6(Right2(x))
Right3(6(x)) → A6(Right3(x))
Right4(6(x)) → A6(Right4(x))
Right5(6(x)) → A6(Right5(x))
Right6(6(x)) → A6(Right6(x))
Right7(6(x)) → A6(Right7(x))
Right8(6(x)) → A6(Right8(x))
Right9(6(x)) → A6(Right9(x))
Right10(6(x)) → A6(Right10(x))
Right11(6(x)) → A6(Right11(x))
Right1(8(x)) → A8(Right1(x))
Right2(8(x)) → A8(Right2(x))
Right3(8(x)) → A8(Right3(x))
Right4(8(x)) → A8(Right4(x))
Right5(8(x)) → A8(Right5(x))
Right6(8(x)) → A8(Right6(x))
Right7(8(x)) → A8(Right7(x))
Right8(8(x)) → A8(Right8(x))
Right9(8(x)) → A8(Right9(x))
Right10(8(x)) → A8(Right10(x))
Right11(8(x)) → A8(Right11(x))
Right1(7(x)) → A7(Right1(x))
Right2(7(x)) → A7(Right2(x))
Right3(7(x)) → A7(Right3(x))
Right4(7(x)) → A7(Right4(x))
Right5(7(x)) → A7(Right5(x))
Right6(7(x)) → A7(Right6(x))
Right7(7(x)) → A7(Right7(x))
Right8(7(x)) → A7(Right8(x))
Right9(7(x)) → A7(Right9(x))
Right10(7(x)) → A7(Right10(x))
Right11(7(x)) → A7(Right11(x))
Right1(0(x)) → A0(Right1(x))
Right2(0(x)) → A0(Right2(x))
Right3(0(x)) → A0(Right3(x))
Right4(0(x)) → A0(Right4(x))
Right5(0(x)) → A0(Right5(x))
Right6(0(x)) → A0(Right6(x))
Right7(0(x)) → A0(Right7(x))
Right8(0(x)) → A0(Right8(x))
Right9(0(x)) → A0(Right9(x))
Right10(0(x)) → A0(Right10(x))
Right11(0(x)) → A0(Right11(x))
A3(Left(x)) → Left(3(x))
A1(Left(x)) → Left(1(x))
A4(Left(x)) → Left(4(x))
A5(Left(x)) → Left(5(x))
A9(Left(x)) → Left(9(x))
A2(Left(x)) → Left(2(x))
A6(Left(x)) → Left(6(x))
A8(Left(x)) → Left(8(x))
A7(Left(x)) → Left(7(x))
A0(Left(x)) → Left(0(x))
Wait(Left(x)) → Begin(x)
3(1(x)) → 4(1(x))
5(9(x)) → 2(6(5(x)))
3(5(x)) → 8(9(7(x)))
9(x) → 3(2(3(x)))
8(4(x)) → 6(x)
2(6(x)) → 4(3(x))
3(8(x)) → 3(2(7(x)))
9(x) → 5(0(2(x)))
8(8(4(x))) → 1(9(x))
7(1(x)) → 6(9(x))
3(9(x)) → 9(3(x))
7(5(x)) → 1(0(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 9 3 End → Wait Left 9 3 End

Wait Left 9 3 End → Wait Left 9 3 End
by OverlapClosure OC 2
Wait Left 9 → Wait Right10
by OverlapClosure OC 2
Wait Left → Begin
by original rule (OC 1)
Begin 9 → Wait Right10
by original rule (OC 1)
Right10 3 End → Left 9 3 End
by original rule (OC 1)

(2) NO