======================================================== The given Problem was: a -> a -> b a b c -> c b a c a c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c b c --(11)-> b a b c b c c b c a (#48885) OC+OC at 5 OC: a b c b c c b c --(10)-> b a b c b a c c b c a (#33072) OC+OC at 7 OC: a b c b c c --(8)-> b a b c b a c a (#1276) OC+OC at 2 OC: a b c b c c --(7)-> b a c b c b a c a (#1149) OC+OC at 3 OC: a b c --(2)-> b a c a (#7) OC+OC at 0 OC: a b c --(1)-> c b a c a (#3) Rule OC: c --(1)-> (#4) Rule OC: a b c c --(5)-> b c b a c a (#226) OC+OC at 1 OC: a b c --(4)-> b a b (#22) OC+OC at 2 OC: a b c --(3)-> b a c b (#14) OC+OC at 3 OC: a b c --(2)-> b a c a (#7) OC+OC at 0 OC: a b c --(1)-> c b a c a (#3) Rule OC: c --(1)-> (#4) Rule OC: a --(1)-> b (#2) Rule OC: c --(1)-> (#4) Rule OC: a b c --(1)-> c b a c a (#3) Rule OC: c --(1)-> (#4) Rule OC: a b c --(2)-> c b c a (#5) OC+OC at 2 OC: a b c --(1)-> c b a c a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.