======================================================== The given Problem was: a -> b a b c -> c c b a a c c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b c c b c c b c c --(16)-> b b a b c c b c c b c c b a a b a a (#780588) OC+OC at 3 OC: a b c c --(5)-> b b a a (#17) OC+OC at 1 OC: a b c --(3)-> b a b (#7) OC+OC at 0 OC: a b c --(2)-> c c b a b (#6) OC+OC at 4 OC: a b c --(1)-> c c b a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c c --(1)-> (#3) Rule OC: a b c --(2)-> b a a (#4) OC+OC at 0 OC: a b c --(1)-> c c b a a (#2) Rule OC: c c --(1)-> (#3) Rule OC: a b c c b c c --(11)-> b c c b c c b c c b a a b a a (#33672) OC+OC at 1 OC: a b c --(3)-> b a b (#7) OC+OC at 0 OC: a b c --(2)-> c c b a b (#6) OC+OC at 4 OC: a b c --(1)-> c c b a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c c --(1)-> (#3) Rule OC: a b c b c c --(8)-> c c b c c b c c b a a b a a (#13676) OC+OC at 6 OC: a b c b c c --(7)-> c c b c c b a b c b a a (#4820) OC+OC at 3 OC: a b c b c c --(5)-> c c b a b c c b a a (#179) OC+OC at 4 OC: a b c --(1)-> c c b a a (#2) Rule OC: a b c c --(4)-> b c c b a a (#28) OC+OC at 1 OC: a b c --(3)-> b a b (#7) OC+OC at 0 OC: a b c --(2)-> c c b a b (#6) OC+OC at 4 OC: a b c --(1)-> c c b a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: c c --(1)-> (#3) Rule OC: a b c --(1)-> c c b a a (#2) Rule OC: a b c --(2)-> c c b a b (#6) OC+OC at 4 OC: a b c --(1)-> c c b a a (#2) Rule OC: a --(1)-> b (#1) Rule OC: a b c --(1)-> c c b a a (#2) Rule Hence, the SRS is non-terminating.