======================================================== The given Problem was: a -> a b -> b c a c a c -> b a a ======================================================== A self-embedding rewrite structure for the given SRS is: c a c b b c b c --(15)-> b b b b c a c b b c b c a (#562424) OC+OC at 3 OC: c a c b b c b c --(14)-> b b b a b c b b c b c a (#231682) OC+OC at 6 OC: c a c b b --(7)-> b b b a b c c a (#1321) OC+OC at 4 OC: c a c b b --(5)-> b b b a a b c a (#264) OC+OC at 5 OC: c a c b --(4)-> b b b a a a (#226) OC+OC at 1 OC: c a c b --(2)-> b a b c a (#16) OC+OC at 2 OC: c a c --(1)-> b a a (#3) Rule OC: a b --(1)-> b c a (#2) Rule OC: a b c --(2)-> b b a a (#11) OC+OC at 1 OC: a b --(1)-> b c a (#2) Rule OC: c a c --(1)-> b a a (#3) Rule OC: a b --(1)-> b c a (#2) Rule OC: a b --(2)-> b c (#4) OC+OC at 2 OC: a b --(1)-> b c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c a c b c --(7)-> b b c b c a (#594) OC+OC at 3 OC: c a c b c --(6)-> b b c a b (#262) OC+OC at 1 OC: c a c b c --(5)-> b a b b (#51) OC+OC at 4 OC: c a c b c --(4)-> b a b b a (#42) OC+OC at 2 OC: c a c --(1)-> b a a (#3) Rule OC: a b c --(3)-> b b a (#10) OC+OC at 1 OC: a b --(1)-> b c a (#2) Rule OC: c a c --(2)-> b a (#5) OC+OC at 1 OC: c a c --(1)-> b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> b c a (#2) Rule OC: a b --(1)-> b c a (#2) Rule OC: a b --(1)-> b c a (#2) Rule Hence, the SRS is non-terminating.