NO
0 QTRS
↳1 NonTerminationProof (⇒, 0 ms)
↳2 NO
a(b(a(b(x)))) → b(a(b(a(a(b(x))))))
a b a b a b → b a b a b a b a a b
a b a b → b a b a a bby original rule (OC 1)