======================================================== The given Problem was: a -> a b -> b b c a b -> b c c -> a ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b c b b --(11)-> a b b b c b b c a (#38179) OC+OC at 5 OC: a b b b c b --(10)-> a b b b c a (#4016) OC+OC at 1 OC: a b b --(6)-> a a (#133) OC+OC at 0 OC: a b b --(5)-> b c c a (#57) OC+OC at 2 OC: a b b --(4)-> b c b c a (#34) OC+OC at 2 OC: a b --(2)-> b c a (#7) OC+OC at 0 OC: a b --(1)-> b b c a (#2) Rule OC: b --(1)-> (#3) Rule OC: a b --(2)-> b c a (#7) OC+OC at 0 OC: a b --(1)-> b b c a (#2) Rule OC: b --(1)-> (#3) Rule OC: b --(1)-> (#3) Rule OC: b c c --(1)-> a (#4) Rule OC: a b c b --(4)-> b b b c a (#63) OC+OC at 1 OC: a b c --(3)-> b a (#13) OC+OC at 1 OC: a b --(2)-> b b c (#6) OC+OC at 3 OC: a b --(1)-> b b c a (#2) Rule OC: a --(1)-> (#1) Rule OC: b c c --(1)-> a (#4) Rule OC: a b --(1)-> b b c a (#2) Rule OC: a b --(1)-> b b c a (#2) Rule Hence, the SRS is non-terminating.