======================================================== The given Problem was: b b -> b a a b -> b c c a c -> a a c a -> b a a ======================================================== A self-embedding rewrite structure for the given SRS is: ba (c)^k ba --> ba (c)^2k+1 baa (#42933) pattern overlapped by closure at r0 RP: ba (c)^k b --> ba (c)^2k+1 c (#4994) expand -> RP: ba (c)^k b --> ba (c)^2k+2 (#2131) pattern overlapped by closure at l-1 RP: a (c)^k b --> b (c)^2k+2 (#619) pattern overlapped by pattern RP: a (c)^k --> (a)^k+1 (#2) self-overlapping Closure at 1 OC: a c --(1)-> a a (#3) Rule RP: (a)^k+1 b --> b (c)^2k+2 (#19) increment RP: (a)^k b --> b (c)^2k (#3) self-overlapping Closure at -1 OC: a b --(1)-> b c c (#2) Rule OC: b b --(1)-> b a (#1) Rule OC: c a --(1)-> b a a (#4) Rule Hence, the SRS is non-terminating.