======================================================== The given Problem was: a -> a b -> a b -> b c a a c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b --(12)-> b c a b b b b (#9297) OC+OC at 6 OC: a b b b b --(11)-> b c a b b b c c (#3652) OC+OC at 7 OC: a b b b b --(10)-> b c a b b b c a c (#2853) OC+OC at 3 OC: a b --(1)-> b c a a (#3) Rule OC: a b b b --(9)-> b b b c a c (#820) OC+OC at 2 OC: a b b b --(7)-> b b a b c (#244) OC+OC at 1 OC: a b b b --(6)-> b c c a b c (#89) OC+OC at 6 OC: a b b b --(5)-> b c c a b c a (#79) OC+OC at 4 OC: a b b --(3)-> b c c a a (#34) OC+OC at 2 OC: a b b --(2)-> b c a b c a a (#13) OC+OC at 3 OC: a b --(1)-> b c a a (#3) Rule OC: a b --(1)-> b c a a (#3) Rule OC: a b --(1)-> (#2) Rule OC: a b --(2)-> b c a (#5) OC+OC at 2 OC: a b --(1)-> b c a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a b --(2)-> b c a (#5) OC+OC at 2 OC: a b --(1)-> b c a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule Hence, the SRS is non-terminating.