======================================================== The given Problem was: b a -> a b c c -> a b c c b -> b c a a -> b a c ======================================================== A self-embedding rewrite structure for the given SRS is: ac (b)^k c --> bac (b)^k+1 c (#26845) pattern overlapped by closure at l-1 RP: c (b)^k c --> a (b)^k+1 c (#13520) pattern overlapped by pattern RP: c (b)^k c --> (b)^k abc (#151) pattern overlapped by closure at r0 RP: c (b)^k --> (b)^k c (#3) self-overlapping Closure at 1 OC: c b --(1)-> b c (#3) Rule OC: c c --(1)-> a b c (#2) Rule RP: (b)^k a --> a (b)^k (#2) self-overlapping Closure at -1 OC: b a --(1)-> a b (#1) Rule OC: a a --(1)-> b a c (#4) Rule Hence, the SRS is non-terminating.