0 QTRS
↳1 NonTerminationProof (⇒, 135 ms)
↳2 NO
Begin(1(x)) → Wait(Right1(x))
Begin(2(x)) → Wait(Right2(x))
Begin(2(x)) → Wait(Right3(x))
Begin(3(x)) → Wait(Right4(x))
Begin(4(x)) → Wait(Right5(x))
Begin(4(x)) → Wait(Right6(x))
Begin(5(x)) → Wait(Right7(x))
Begin(6(x)) → Wait(Right8(x))
Begin(6(x)) → Wait(Right9(x))
Right1(1(End(x))) → Left(4(3(End(x))))
Right2(1(End(x))) → Left(2(1(End(x))))
Right3(2(End(x))) → Left(1(1(1(End(x)))))
Right4(3(End(x))) → Left(5(6(End(x))))
Right5(3(End(x))) → Left(1(1(End(x))))
Right6(4(End(x))) → Left(3(End(x)))
Right7(5(End(x))) → Left(6(2(End(x))))
Right8(5(End(x))) → Left(1(2(End(x))))
Right9(6(End(x))) → Left(2(1(End(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))
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))
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))
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))
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))
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))
A1(Left(x)) → Left(1(x))
A4(Left(x)) → Left(4(x))
A3(Left(x)) → Left(3(x))
A2(Left(x)) → Left(2(x))
A5(Left(x)) → Left(5(x))
A6(Left(x)) → Left(6(x))
Wait(Left(x)) → Begin(x)
1(1(x)) → 4(3(x))
1(2(x)) → 2(1(x))
2(2(x)) → 1(1(1(x)))
3(3(x)) → 5(6(x))
3(4(x)) → 1(1(x))
4(4(x)) → 3(x)
5(5(x)) → 6(2(x))
5(6(x)) → 1(2(x))
6(6(x)) → 2(1(x))
Wait Left 2 1 End → Wait Left 2 1 End
Wait Left 2 → Wait Right2
by OverlapClosure OC 2Wait Left → Begin
by original rule (OC 1)Begin 2 → Wait Right2
by original rule (OC 1)
Right2 1 End → Left 2 1 End
by original rule (OC 1)