======================================================== The given Problem was: a -> a b -> b a a c a a c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b c b --(13)-> b a a c a b b c b a c a a a c a a (#93597) OC+OC at 8 OC: a b b c b --(11)-> b a a c a b b c a b a c a a (#9946) OC+OC at 7 OC: a b b c b --(10)-> b a a c a b b a c a b a c a a (#5841) OC+OC at 10 OC: a b b c --(8)-> b a a c a b b a c a a (#982) OC+OC at 6 OC: a b b c --(6)-> b a a c a b a b (#82) OC+OC at 6 OC: a b b c --(5)-> b a a c a b a a b (#69) OC+OC at 8 OC: a b b --(4)-> b a a c a b a a c (#27) OC+OC at 9 OC: a b b --(3)-> b a a c a b a a c a (#11) OC+OC at 5 OC: a b --(1)-> b a a c a a (#2) Rule OC: a b --(2)-> b a a c a (#6) OC+OC at 4 OC: a b --(1)-> b a a c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#3) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a c a a (#4) OC+OC at 1 OC: a b --(1)-> b a a c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a c a a (#4) OC+OC at 1 OC: a b --(1)-> b a a c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: a b --(2)-> b a c a a (#4) OC+OC at 1 OC: a b --(1)-> b a a c a a (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.