======================================================== The given Problem was: a -> b a -> b b c c a b -> a c a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b b b b b --(12)-> b b a a b b b b b c c a c c a (#193085) OC+OC at 6 OC: a a b b b b b --(11)-> b b a a b b a b b c c a c c a (#93360) OC+OC at 2 OC: a --(1)-> b b c (#2) Rule OC: c a b b b b b --(10)-> a a b b a b b c c a c c a (#36536) OC+OC at 5 OC: c a b b b b b --(9)-> a a b b a a c a c c a (#20099) OC+OC at 1 OC: c a b --(1)-> a c a (#3) Rule OC: c a b b b b --(8)-> a b b a a c a c c a (#6308) OC+OC at 1 OC: c a b --(1)-> a c a (#3) Rule OC: c a b b b --(7)-> b b a a c a c c a (#5045) OC+OC at 3 OC: c a b b b --(6)-> b b a c a b c c a (#3230) OC+OC at 0 OC: c a b b b --(4)-> a a b b c c a (#121) OC+OC at 2 OC: c a b b b --(3)-> a a a c a (#69) OC+OC at 1 OC: c a b --(1)-> a c a (#3) Rule OC: c a b b --(2)-> a a c a (#20) OC+OC at 1 OC: c a b --(1)-> a c a (#3) Rule OC: c a b --(1)-> a c a (#3) Rule OC: a --(1)-> b b c (#2) Rule OC: a a b --(2)-> b b a c a (#8) OC+OC at 2 OC: a --(1)-> b b c (#2) Rule OC: c a b --(1)-> a c a (#3) Rule OC: c a b --(1)-> a c a (#3) Rule OC: a --(1)-> b b c (#2) Rule OC: a --(1)-> b (#1) Rule Hence, the SRS is non-terminating.