======================================================== The given Problem was: a -> a -> b b b c -> a c c c a b ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c --(13)-> a c c c c c c c c c a b c b c c c a b (#239785) OC+OC at 13 OC: a b c b c --(11)-> a c c c c c c c c c a b c b b (#50876) OC+OC at 7 OC: a b c b c --(8)-> a c c c c c c a b c c b b (#11314) OC+OC at 4 OC: a b c b c --(5)-> a c c c a b c c c b b (#459) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c b c --(4)-> a c c c a b c c c b b (#243) OC+OC at 5 OC: b b c --(1)-> a c c c a b (#3) Rule OC: b b c --(3)-> b c c c b b (#27) OC+OC at 4 OC: b b c --(2)-> b c c c a b (#11) OC+OC at 0 OC: b b c --(1)-> a c c c a b (#3) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule OC: a b c --(3)-> c c c a b (#7) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(2)-> c c c a b (#4) OC+OC at 0 OC: b b c --(1)-> a c c c a b (#3) Rule OC: a --(1)-> (#1) Rule OC: a b c --(3)-> c c c a b (#7) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(2)-> c c c a b (#4) OC+OC at 0 OC: b b c --(1)-> a c c c a b (#3) Rule OC: a --(1)-> (#1) Rule OC: b b c --(2)-> b c c c a b (#11) OC+OC at 0 OC: b b c --(1)-> a c c c a b (#3) Rule OC: a --(1)-> b (#2) Rule Hence, the SRS is non-terminating.