0 QTRS
↳1 NonTerminationProof (⇒, 46 ms)
↳2 NO
Begin(f(x)) → Wait(Right1(x))
Begin(f(x)) → Wait(Right2(x))
Begin(f(x)) → Wait(Right3(x))
Begin(n(x)) → Wait(Right4(x))
Begin(o(x)) → Wait(Right5(x))
Right1(n(End(x))) → Left(f(n(End(x))))
Right2(o(End(x))) → Left(f(o(End(x))))
Right3(c(End(x))) → Left(f(c(End(x))))
Right4(c(End(x))) → Left(n(c(End(x))))
Right5(c(End(x))) → Left(o(c(End(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))
Right1(f(x)) → Af(Right1(x))
Right2(f(x)) → Af(Right2(x))
Right3(f(x)) → Af(Right3(x))
Right4(f(x)) → Af(Right4(x))
Right5(f(x)) → Af(Right5(x))
Right1(o(x)) → Ao(Right1(x))
Right2(o(x)) → Ao(Right2(x))
Right3(o(x)) → Ao(Right3(x))
Right4(o(x)) → Ao(Right4(x))
Right5(o(x)) → Ao(Right5(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))
An(Left(x)) → Left(n(x))
Af(Left(x)) → Left(f(x))
Ao(Left(x)) → Left(o(x))
Ac(Left(x)) → Left(c(x))
Wait(Left(x)) → Begin(x)
n(f(x)) → f(n(x))
o(f(x)) → f(o(x))
c(f(x)) → f(c(x))
c(n(x)) → n(c(x))
c(o(x)) → o(c(x))
Wait Left o c End → Wait Left o c End
Wait Left o → Wait Right5
by OverlapClosure OC 2Wait Left → Begin
by original rule (OC 1)Begin o → Wait Right5
by original rule (OC 1)
Right5 c End → Left o c End
by original rule (OC 1)