======================================================== The given Problem was: a -> a -> b b b c -> a c c c a a ======================================================== A self-embedding rewrite structure for the given SRS is: b b c b c c --(18)-> c c c c c c a c c c b b c b c c c a (#1082343) OC+OC at 13 OC: b b c b c --(15)-> c c c c c c a c c c b b c b b (#297214) OC+OC at 6 OC: b b c b c --(11)-> c c c c c c a b c c b b (#32945) OC+OC at 3 OC: b b c b c --(7)-> c c c a b c c c b b (#1206) OC+OC at 4 OC: b b c --(2)-> c c c a a (#4) OC+OC at 0 OC: b b c --(1)-> a c c c a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b c --(5)-> b c c c b b (#96) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(4)-> b c c c b b (#81) OC+OC at 5 OC: b b c --(3)-> b c c c b a (#43) OC+OC at 0 OC: b b c --(2)-> a c c c b a (#15) OC+OC at 4 OC: b b c --(1)-> a c c c a a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule OC: a b c --(4)-> c c c a b (#38) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(3)-> c c c a b (#13) OC+OC at 4 OC: b b c --(2)-> c c c a a (#4) OC+OC at 0 OC: b b c --(1)-> a c c c a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> b (#2) Rule OC: a b c --(4)-> a c c c b b (#78) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(3)-> a c c c b b (#44) OC+OC at 5 OC: b b c --(2)-> a c c c b a (#15) OC+OC at 4 OC: b b c --(1)-> a c c c a a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule OC: b b c --(3)-> b c c c a (#10) OC+OC at 0 OC: b b c --(2)-> a c c c a (#5) OC+OC at 4 OC: b b c --(1)-> a c c c a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> b (#2) Rule Hence, the SRS is non-terminating.