NO
0 QTRS
↳1 NonTerminationProof (⇒, 1098 ms)
↳2 NO
a(x) → x
a(b(x)) → x
b(b(x)) → c(x)
c(a(x)) → a(a(b(c(x))))
c a a a a a → c a a a a a b c b c
c a a a a a → c a a a c a b c
by OverlapClosure OC 2c a a → c c
by OverlapClosure OC 3c a a → b b c
by OverlapClosure OC 2c a → b c
by OverlapClosure OC 3c a → a b c
by OverlapClosure OC 3c a → a a b c
by original rule (OC 1)a →
by original rule (OC 1)a →
by original rule (OC 1)c a → b c
by OverlapClosure OC 3c a → a b c
by OverlapClosure OC 3c a → a a b c
by original rule (OC 1)a →
by original rule (OC 1)a →
by original rule (OC 1)b b → c
by original rule (OC 1)c a a a → a a a c a b c
by OverlapClosure OC 3c a a a → a a a a b c a b c
by OverlapClosure OC 3c a a a → a a c a a b c
by OverlapClosure OC 2c a a → a a c c
by OverlapClosure OC 3c a a → a a b b c
by OverlapClosure OC 2c a → a a b c
by original rule (OC 1)c a → b c
by OverlapClosure OC 3c a → a b c
by OverlapClosure OC 3c a → a a b c
by original rule (OC 1)a →
by original rule (OC 1)a →
by original rule (OC 1)b b → c
by original rule (OC 1)c a → a a b c
by original rule (OC 1)c a → a a b c
by original rule (OC 1)a b →
by original rule (OC 1)
c a → a a b c
by original rule (OC 1)