======================================================== The given Problem was: c c -> b b a b -> a c b b a -> b b b c -> c a a ======================================================== A self-embedding rewrite structure for the given SRS is: abb (a)^k cb --> abb (a)^2k+4 cb (#102984) pattern overlapped by closure at l-2 RP: b (a)^k cb --> c (a)^2k+2 cb (#6446) pattern overlapped by pattern RP: b (a)^k --> (b)^k+1 (#1) self-overlapping Closure at 1 OC: b a --(1)-> b b (#3) Rule RP: (b)^k+1 cb --> c (a)^2k+2 cb (#294) pattern overlapped by closure at r0 RP: (b)^k+1 c --> c (a)^2k+1 a (#16) expand -> RP: (b)^k+1 c --> c (a)^2k+2 (#9) increment RP: (b)^k c --> c (a)^2k (#2) self-overlapping Closure at -1 OC: b c --(1)-> c a a (#4) Rule OC: a b --(1)-> a c b (#2) Rule OC: a b c --(3)-> a b b a a (#31) OC+OC at 1 OC: a b c --(2)-> a c c a a (#11) OC+OC at 2 OC: a b --(1)-> a c b (#2) Rule OC: b c --(1)-> c a a (#4) Rule OC: c c --(1)-> b b (#1) Rule Hence, the SRS is non-terminating.