======================================================== The given Problem was: a -> b c a b b -> c a a a c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b b c b c b --(17)-> c a b b b b c b c b c (#78147) OC+OC at 5 OC: a b b b b c b c b --(16)-> c a b b b a b c b c (#36936) OC+OC at 8 OC: a b b b b c b c b --(15)-> c a b b b a b c a (#18188) OC+OC at 6 OC: a b b b b c b c b --(14)-> c a b b b a a a (#15790) OC+OC at 2 OC: a b b b b c b c b --(12)-> c a a c b b a a a (#4752) OC+OC at 3 OC: a b b --(1)-> c a a a (#2) Rule OC: a b b c b c b --(11)-> c b b a a a (#1152) OC+OC at 1 OC: a b b c b c b --(9)-> c a c b a a a (#727) OC+OC at 2 OC: a b b c --(3)-> c a a b (#8) OC+OC at 3 OC: a b b --(1)-> c a a a (#2) Rule OC: a c --(2)-> b (#4) OC+OC at 1 OC: a --(1)-> b c (#1) Rule OC: c c --(1)-> (#3) Rule OC: a b b c b --(6)-> c b a a a (#64) OC+OC at 1 OC: a b b c b --(4)-> c a c a a a (#41) OC+OC at 2 OC: a b b c --(3)-> c a a b (#8) OC+OC at 3 OC: a b b --(1)-> c a a a (#2) Rule OC: a c --(2)-> b (#4) OC+OC at 1 OC: a --(1)-> b c (#1) Rule OC: c c --(1)-> (#3) Rule OC: a b b --(1)-> c a a a (#2) Rule OC: a c --(2)-> b (#4) OC+OC at 1 OC: a --(1)-> b c (#1) Rule OC: c c --(1)-> (#3) Rule OC: a c --(2)-> b (#4) OC+OC at 1 OC: a --(1)-> b c (#1) Rule OC: c c --(1)-> (#3) Rule OC: a c --(2)-> b (#4) OC+OC at 1 OC: a --(1)-> b c (#1) Rule OC: c c --(1)-> (#3) Rule OC: a --(1)-> b c (#1) Rule OC: a --(1)-> b c (#1) Rule OC: a --(1)-> b c (#1) Rule Hence, the SRS is non-terminating.