======================================================== The given Problem was: a -> a -> b b a c -> c c a b a c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b a c c a c c --(10)-> c b a c c a c c a b (#145093) OC+OC at 2 OC: b a c c a c c --(9)-> c b c a c c a c c a b (#115017) OC+OC at 1 OC: b a c c a c c --(8)-> c a c a c c a c c a b (#96452) OC+OC at 2 OC: b a c c a c c --(7)-> c a c c a c c a c c a b (#77813) OC+OC at 5 OC: b a c c --(4)-> c a c c a b (#109) OC+OC at 2 OC: b a c --(2)-> c a b a (#7) OC+OC at 0 OC: b a c --(1)-> c c a b a (#3) Rule OC: c --(1)-> (#4) Rule OC: b a c --(2)-> c c a b (#6) OC+OC at 4 OC: b a c --(1)-> c c a b a (#3) Rule OC: a --(1)-> (#1) Rule OC: b a c c --(3)-> c c a c c a b (#105) OC+OC at 3 OC: b a c --(1)-> c c a b a (#3) Rule OC: b a c --(2)-> c c a b (#6) OC+OC at 4 OC: b a c --(1)-> c c a b a (#3) Rule OC: a --(1)-> (#1) Rule OC: c --(1)-> (#4) Rule OC: a --(1)-> b (#2) Rule OC: c --(1)-> (#4) Rule Hence, the SRS is non-terminating.