======================================================== The given Problem was: a -> a a b -> c c c c -> b a c b -> ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b a b --(17)-> b b a a b a b a b (#675966) OC+OC at 6 OC: a a b a b a b --(16)-> b b a a b a c b (#284617) OC+OC at 4 OC: a a b a b --(12)-> b b a a a (#39015) OC+OC at 0 OC: a a b a b --(7)-> c a b a (#398) OC+OC at 1 OC: a a b --(3)-> c a (#32) OC+OC at 1 OC: a a b --(2)-> c c b a (#10) OC+OC at 2 OC: a a b --(1)-> c c c (#2) Rule OC: c --(1)-> b a (#3) Rule OC: c b --(1)-> (#4) Rule OC: a a b --(4)-> a b a (#114) OC+OC at 0 OC: a a b --(3)-> c b a b a (#63) OC+OC at 3 OC: a a b --(2)-> c b a c (#9) OC+OC at 1 OC: a a b --(1)-> c c c (#2) Rule OC: c --(1)-> b a (#3) Rule OC: c --(1)-> b a (#3) Rule OC: c b --(1)-> (#4) Rule OC: c a b --(5)-> b b a a (#252) OC+OC at 3 OC: c a b --(4)-> b b a c b a (#141) OC+OC at 1 OC: c --(1)-> b a (#3) Rule OC: a a b --(3)-> b a c b a (#51) OC+OC at 3 OC: a a b --(2)-> b a c c (#8) OC+OC at 0 OC: a a b --(1)-> c c c (#2) Rule OC: c --(1)-> b a (#3) Rule OC: c --(1)-> b a (#3) Rule OC: c b --(1)-> (#4) Rule OC: a a b --(4)-> b a c b (#53) OC+OC at 3 OC: a a b --(2)-> b a c c (#8) OC+OC at 0 OC: a a b --(1)-> c c c (#2) Rule OC: c --(1)-> b a (#3) Rule OC: c --(2)-> b (#5) OC+OC at 1 OC: c --(1)-> b a (#3) Rule OC: a --(1)-> (#1) Rule OC: c --(1)-> b a (#3) Rule Hence, the SRS is non-terminating.