======================================================== The given Problem was: a -> a b -> b c a a c b -> c c -> b ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b --(13)-> b c a b b b b a a (#10653) OC+OC at 6 OC: a b b b b --(12)-> b c a b b b c c a a (#4996) OC+OC at 7 OC: a b b b b --(11)-> b c a b b b c a c a a (#3815) OC+OC at 3 OC: a b --(1)-> b c a a (#2) Rule OC: a b b b --(10)-> b b b c a c a a (#1115) OC+OC at 1 OC: a b b b --(9)-> b c c b c a c a a (#1079) OC+OC at 3 OC: a b b b --(7)-> b c c a b c a a (#359) OC+OC at 1 OC: a b b b --(6)-> b c b c c a b c a a (#212) OC+OC at 4 OC: a b b b --(5)-> b c b c a c a b c a a (#201) OC+OC at 7 OC: a b b --(4)-> b c b c a c a a (#71) OC+OC at 2 OC: a b b --(2)-> b c a b c a a (#7) OC+OC at 3 OC: a b --(1)-> b c a a (#2) Rule OC: a b --(1)-> b c a a (#2) Rule OC: a b --(2)-> b c a (#5) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: c b --(1)-> (#3) Rule OC: a b --(2)-> b c a (#5) OC+OC at 2 OC: a b --(1)-> b c a a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b (#4) Rule Hence, the SRS is non-terminating.