======================================================== The given Problem was: a -> a -> b b b c -> c c a a a c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c --(12)-> c c a b c b c c a (#252393) OC+OC at 4 OC: a b c b c c --(11)-> c c a b c c b c c a (#121916) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c b c c --(10)-> c c a b c c b c c a (#46782) OC+OC at 4 OC: b b c --(2)-> c c a b a (#19) OC+OC at 3 OC: b b c --(1)-> c c a a a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a b c c --(8)-> c c b c c a (#7247) OC+OC at 3 OC: a b c --(4)-> c c b a b (#176) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(3)-> c c b a b (#81) OC+OC at 4 OC: b b c --(2)-> c c b a a (#18) OC+OC at 2 OC: b b c --(1)-> c c a a a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a --(1)-> b (#2) Rule OC: a b c --(4)-> c c a (#50) OC+OC at 2 OC: a b c --(3)-> c c a a (#10) OC+OC at 0 OC: a --(1)-> b (#2) Rule OC: b b c --(2)-> c c a a (#5) OC+OC at 2 OC: b b c --(1)-> c c a a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: c --(1)-> (#4) Rule Hence, the SRS is non-terminating.