======================================================== The given Problem was: a a a -> b b c a a b b -> c a b c -> ======================================================== A self-embedding rewrite structure for the given SRS is: (b)^k+3 --> (b)^2k aab (#13669) pattern overlapped by closure at m2 RP: (b)^k+3 --> (bbc)^k aab (#8968) pattern overlapped by pattern RP: (b)^k+3 --> (a)^k+2 b (#18) increment RP: (b)^k+2 --> (a)^k+1 b (#10) increment RP: (b)^k+1 --> (a)^k b (#9) pattern overlapped by closure at m0 RP: (b)^k+1 --> (ca)^k b (#1) self-overlapping Closure at 2 OC: b b --(1)-> c a b (#2) Rule OC: c --(1)-> (#3) Rule RP: (a)^k+2 --> (bbc)^k aa (#2) self-overlapping Closure at 3 OC: a a a --(1)-> b b c a a (#1) Rule OC: c --(1)-> (#3) Rule Hence, the SRS is non-terminating.