======================================================== The given Problem was: a -> a b -> b c a a b -> a c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b c --(12)-> a b b c a a (#51900) OC+OC at 1 OC: a b b c --(11)-> a c c b c a a (#50217) OC+OC at 3 OC: a b b c --(10)-> a c c a b (#3486) OC+OC at 4 OC: a b b --(9)-> a c c a c (#3258) OC+OC at 2 OC: a b b --(5)-> a c a b c (#200) OC+OC at 0 OC: a b b --(4)-> b c a b c (#131) OC+OC at 5 OC: a b b --(3)-> b c a b c a (#116) OC+OC at 3 OC: a b --(1)-> b c a a (#2) Rule OC: a b --(2)-> b c a (#9) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: b --(1)-> a (#3) Rule OC: a b --(4)-> c a (#16) OC+OC at 0 OC: a b --(2)-> b c a (#9) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: b --(2)-> (#5) OC+OC at 0 OC: b --(1)-> a (#3) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a b --(1)-> b c a a (#2) Rule OC: c c --(1)-> b (#4) Rule Hence, the SRS is non-terminating.