======================================================== The given Problem was: a a -> b a b -> c a c c -> b a b ======================================================== A self-embedding rewrite structure for the given SRS is: c c b b b a b b --(17)-> b c c b b b a b b b a (#36495) OC+OC at 3 OC: c c b --(3)-> b c c a (#9) OC+OC at 2 OC: c c --(2)-> b c a (#6) OC+OC at 1 OC: c c --(1)-> b a b (#3) Rule OC: a b --(1)-> c a (#2) Rule OC: a b --(1)-> c a (#2) Rule OC: a b b a b b --(14)-> b b b a b b b a (#6876) OC+OC at 2 OC: a b b a b b --(13)-> b b c c b b a (#4030) OC+OC at 4 OC: a b b a b b --(12)-> b b c c a a b a (#3836) OC+OC at 3 OC: a b b a b b --(11)-> b b c a b a b a (#1356) OC+OC at 4 OC: a b b a --(8)-> b b c a a (#212) OC+OC at 1 OC: a b b a --(6)-> b c c a (#86) OC+OC at 2 OC: a b b a --(5)-> b c a b (#28) OC+OC at 3 OC: a b b --(4)-> b c a a (#23) OC+OC at 0 OC: a b b --(2)-> c c a (#5) OC+OC at 1 OC: a b --(1)-> c a (#2) Rule OC: a b --(1)-> c a (#2) Rule OC: c c --(2)-> b c a (#6) OC+OC at 1 OC: c c --(1)-> b a b (#3) Rule OC: a b --(1)-> c a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: a b --(1)-> c a (#2) Rule OC: c c --(2)-> b c a (#6) OC+OC at 1 OC: c c --(1)-> b a b (#3) Rule OC: a b --(1)-> c a (#2) Rule OC: a b b --(3)-> b a b a (#16) OC+OC at 0 OC: a b b --(2)-> c c a (#5) OC+OC at 1 OC: a b --(1)-> c a (#2) Rule OC: a b --(1)-> c a (#2) Rule OC: c c --(1)-> b a b (#3) Rule OC: a b --(1)-> c a (#2) Rule OC: a a --(1)-> b (#1) Rule OC: c c --(1)-> b a b (#3) Rule Hence, the SRS is non-terminating.