======================================================== The given Problem was: c b -> b a a c -> a b c b b -> b c c a -> c c c ======================================================== A self-embedding rewrite structure for the given SRS is: b (c)^k+1 bc --> b (c)^2k+3 bc (#226430) pattern overlapped by pattern RP: b (c)^k+1 bc --> bc (a)^k+1 bc (#4149) pattern overlapped by closure at r0 RP: b (c)^k+1 b --> bc (a)^k a (#425) expand -> RP: b (c)^k+1 b --> bc (a)^k+1 (#131) pattern overlapped by closure at l-1 RP: (c)^k+1 b --> b (a)^k+1 (#8) increment RP: (c)^k b --> b (a)^k (#2) self-overlapping Closure at -1 OC: c b --(1)-> b a (#1) Rule OC: b b --(1)-> b c (#3) Rule OC: a c --(1)-> a b c (#2) Rule RP: c (a)^k+1 --> (c)^2k+3 (#11) increment RP: c (a)^k --> (c)^2k+1 (#3) self-overlapping Closure at 2 OC: c a --(1)-> c c c (#4) Rule Hence, the SRS is non-terminating.