======================================================== The given Problem was: a -> a b -> b b a a c a b -> c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b b --(9)-> b b a b c b b a a c (#6235) OC+OC at 3 OC: a b c b b --(8)-> b b a b b c b b a a c (#2388) OC+OC at 3 OC: a b c --(3)-> b b a a (#10) OC+OC at 4 OC: a b --(2)-> b b a a c (#7) OC+OC at 5 OC: a b --(1)-> b b a a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> (#4) Rule OC: a b b --(5)-> b b c b b a a c (#42) OC+OC at 2 OC: a b b --(4)-> b b a c b b a a c (#20) OC+OC at 4 OC: a b --(2)-> b b a c a (#5) OC+OC at 2 OC: a b --(1)-> b b a a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b b a a c (#7) OC+OC at 5 OC: a b --(1)-> b b a a c a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: b --(1)-> (#3) Rule Hence, the SRS is non-terminating.