0 QTRS
↳1 NonTerminationProof (⇒, 67 ms)
↳2 NO
Begin(r(x)) → Wait(Right1(x))
Begin(s(x)) → Wait(Right2(x))
Begin(n(x)) → Wait(Right3(x))
Begin(b(x)) → Wait(Right4(x))
Begin(u(x)) → Wait(Right5(x))
Begin(u(x)) → Wait(Right6(x))
Begin(u(x)) → Wait(Right7(x))
Begin(r(u(x))) → Wait(Right8(x))
Begin(u(x)) → Wait(Right9(x))
Begin(s(u(x))) → Wait(Right10(x))
Begin(u(x)) → Wait(Right11(x))
Begin(n(u(x))) → Wait(Right12(x))
Begin(u(x)) → Wait(Right13(x))
Begin(u(x)) → Wait(Right14(x))
Begin(s(x)) → Wait(Right15(x))
Begin(r(x)) → Wait(Right16(x))
Begin(n(x)) → Wait(Right17(x))
Begin(n(x)) → Wait(Right18(x))
Right1(r(End(x))) → Left(s(r(End(x))))
Right2(r(End(x))) → Left(s(r(End(x))))
Right3(r(End(x))) → Left(s(r(End(x))))
Right4(r(End(x))) → Left(u(s(b(End(x)))))
Right5(r(End(x))) → Left(u(r(End(x))))
Right6(s(End(x))) → Left(u(s(End(x))))
Right7(n(End(x))) → Left(u(n(End(x))))
Right8(t(End(x))) → Left(t(c(r(End(x)))))
Right9(t(r(End(x)))) → Left(t(c(r(End(x)))))
Right10(t(End(x))) → Left(t(c(r(End(x)))))
Right11(t(s(End(x)))) → Left(t(c(r(End(x)))))
Right12(t(End(x))) → Left(t(c(r(End(x)))))
Right13(t(n(End(x)))) → Left(t(c(r(End(x)))))
Right14(c(End(x))) → Left(u(c(End(x))))
Right15(c(End(x))) → Left(s(c(End(x))))
Right16(c(End(x))) → Left(r(c(End(x))))
Right17(c(End(x))) → Left(n(c(End(x))))
Right18(c(End(x))) → Left(n(End(x)))
Right1(r(x)) → Ar(Right1(x))
Right2(r(x)) → Ar(Right2(x))
Right3(r(x)) → Ar(Right3(x))
Right4(r(x)) → Ar(Right4(x))
Right5(r(x)) → Ar(Right5(x))
Right6(r(x)) → Ar(Right6(x))
Right7(r(x)) → Ar(Right7(x))
Right8(r(x)) → Ar(Right8(x))
Right9(r(x)) → Ar(Right9(x))
Right10(r(x)) → Ar(Right10(x))
Right11(r(x)) → Ar(Right11(x))
Right12(r(x)) → Ar(Right12(x))
Right13(r(x)) → Ar(Right13(x))
Right14(r(x)) → Ar(Right14(x))
Right15(r(x)) → Ar(Right15(x))
Right16(r(x)) → Ar(Right16(x))
Right17(r(x)) → Ar(Right17(x))
Right18(r(x)) → Ar(Right18(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))
Right11(s(x)) → As(Right11(x))
Right12(s(x)) → As(Right12(x))
Right13(s(x)) → As(Right13(x))
Right14(s(x)) → As(Right14(x))
Right15(s(x)) → As(Right15(x))
Right16(s(x)) → As(Right16(x))
Right17(s(x)) → As(Right17(x))
Right18(s(x)) → As(Right18(x))
Right1(n(x)) → An(Right1(x))
Right2(n(x)) → An(Right2(x))
Right3(n(x)) → An(Right3(x))
Right4(n(x)) → An(Right4(x))
Right5(n(x)) → An(Right5(x))
Right6(n(x)) → An(Right6(x))
Right7(n(x)) → An(Right7(x))
Right8(n(x)) → An(Right8(x))
Right9(n(x)) → An(Right9(x))
Right10(n(x)) → An(Right10(x))
Right11(n(x)) → An(Right11(x))
Right12(n(x)) → An(Right12(x))
Right13(n(x)) → An(Right13(x))
Right14(n(x)) → An(Right14(x))
Right15(n(x)) → An(Right15(x))
Right16(n(x)) → An(Right16(x))
Right17(n(x)) → An(Right17(x))
Right18(n(x)) → An(Right18(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))
Right11(b(x)) → Ab(Right11(x))
Right12(b(x)) → Ab(Right12(x))
Right13(b(x)) → Ab(Right13(x))
Right14(b(x)) → Ab(Right14(x))
Right15(b(x)) → Ab(Right15(x))
Right16(b(x)) → Ab(Right16(x))
Right17(b(x)) → Ab(Right17(x))
Right18(b(x)) → Ab(Right18(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))
Right11(u(x)) → Au(Right11(x))
Right12(u(x)) → Au(Right12(x))
Right13(u(x)) → Au(Right13(x))
Right14(u(x)) → Au(Right14(x))
Right15(u(x)) → Au(Right15(x))
Right16(u(x)) → Au(Right16(x))
Right17(u(x)) → Au(Right17(x))
Right18(u(x)) → Au(Right18(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))
Right11(t(x)) → At(Right11(x))
Right12(t(x)) → At(Right12(x))
Right13(t(x)) → At(Right13(x))
Right14(t(x)) → At(Right14(x))
Right15(t(x)) → At(Right15(x))
Right16(t(x)) → At(Right16(x))
Right17(t(x)) → At(Right17(x))
Right18(t(x)) → At(Right18(x))
Right1(c(x)) → Ac(Right1(x))
Right2(c(x)) → Ac(Right2(x))
Right3(c(x)) → Ac(Right3(x))
Right4(c(x)) → Ac(Right4(x))
Right5(c(x)) → Ac(Right5(x))
Right6(c(x)) → Ac(Right6(x))
Right7(c(x)) → Ac(Right7(x))
Right8(c(x)) → Ac(Right8(x))
Right9(c(x)) → Ac(Right9(x))
Right10(c(x)) → Ac(Right10(x))
Right11(c(x)) → Ac(Right11(x))
Right12(c(x)) → Ac(Right12(x))
Right13(c(x)) → Ac(Right13(x))
Right14(c(x)) → Ac(Right14(x))
Right15(c(x)) → Ac(Right15(x))
Right16(c(x)) → Ac(Right16(x))
Right17(c(x)) → Ac(Right17(x))
Right18(c(x)) → Ac(Right18(x))
Ar(Left(x)) → Left(r(x))
As(Left(x)) → Left(s(x))
An(Left(x)) → Left(n(x))
Ab(Left(x)) → Left(b(x))
Au(Left(x)) → Left(u(x))
At(Left(x)) → Left(t(x))
Ac(Left(x)) → Left(c(x))
Wait(Left(x)) → Begin(x)
r(r(x)) → s(r(x))
r(s(x)) → s(r(x))
r(n(x)) → s(r(x))
r(b(x)) → u(s(b(x)))
r(u(x)) → u(r(x))
s(u(x)) → u(s(x))
n(u(x)) → u(n(x))
t(r(u(x))) → t(c(r(x)))
t(s(u(x))) → t(c(r(x)))
t(n(u(x))) → t(c(r(x)))
c(u(x)) → u(c(x))
c(s(x)) → s(c(x))
c(r(x)) → r(c(x))
c(n(x)) → n(c(x))
c(n(x)) → n(x)
Wait Left n c End → Wait Left n c End
Wait Left n → Wait Right17
by OverlapClosure OC 2Wait Left → Begin
by original rule (OC 1)Begin n → Wait Right17
by original rule (OC 1)
Right17 c End → Left n c End
by original rule (OC 1)