======================================================== The given Problem was: a -> a b -> c a c c -> b b c b a ======================================================== A self-embedding rewrite structure for the given SRS is: a b b b c b b b c --(18)-> b b c b c b b c b a b b b c b b b c b (#274702) OC+OC at 15 OC: a b b b c b b b c --(17)-> b b c b c b b c b a b b b c b a b b c b (#236184) OC+OC at 11 OC: a b b b c --(10)-> b b c b c b b c b a b a (#2478) OC+OC at 5 OC: a b b b c --(9)-> b b c b c c c b a (#826) OC+OC at 5 OC: a b b b c --(7)-> b b c b c a b c b a (#702) OC+OC at 4 OC: a b b b c --(6)-> b b c b a b b c b a (#290) OC+OC at 5 OC: a b b --(3)-> b b c b a a (#29) 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 b c b a (#3) Rule OC: a b c --(3)-> b b c b a (#12) OC+OC at 0 OC: a b --(2)-> c (#4) OC+OC at 1 OC: a b --(1)-> c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b b c b a (#3) Rule OC: a b --(1)-> c a (#2) Rule OC: a b --(2)-> c (#4) OC+OC at 1 OC: a b --(1)-> c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(1)-> b b c b a (#3) Rule OC: a b b b c --(7)-> b b c b a b b c b (#291) OC+OC at 5 OC: a b b --(3)-> b b c b a a (#29) 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 b c b a (#3) Rule OC: a b c --(4)-> b b c b (#11) OC+OC at 0 OC: a b --(2)-> c (#4) OC+OC at 1 OC: a b --(1)-> c a (#2) Rule OC: a --(1)-> (#1) Rule OC: c c --(2)-> b b c b (#8) OC+OC at 4 OC: c c --(1)-> b b c b a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.