======================================================== The given Problem was: a b c -> c b a a c -> a a d a d a b -> b a d d a c -> b c c ======================================================== A self-embedding rewrite structure for the given SRS is: a (ab)^k+1 cc --> a (ab)^k+2 cc (#119220) pattern overlapped by closure at r0 RP: a (ab)^k+1 c --> aa (ba)^k+1 da (#70270) pattern overlapped by pattern RP: a (ab)^k+1 c --> aad (ab)^k+1 a (#868) pattern overlapped by closure at l-1 RP: (ab)^k+1 c --> c (ba)^k ba (#29) expand -> RP: (ab)^k+1 c --> c (ba)^k+1 (#7) increment RP: (ab)^k c --> c (ba)^k (#5) self-overlapping Closure at -2 OC: a b c --(1)-> c b a (#1) Rule OC: a c --(1)-> a a d a (#2) Rule RP: d (ab)^k+1 --> (ba)^k+1 d (#8) increment RP: d (ab)^k --> (ba)^k d (#1) self-overlapping Closure at 2 OC: d a b --(1)-> b a d (#3) Rule OC: d a c --(1)-> b c c (#4) Rule Hence, the SRS is non-terminating.