======================================================== The given Problem was: a -> a -> b a b c -> c c b a a c -> ======================================================== A self-embedding rewrite structure for the given SRS is: a b c b c c b c c --(11)-> c c b a b c b c c b c c b a a (#466003) OC+OC at 5 OC: a b c b c c b c c --(10)-> c c b a b c c b c c b c c b a a (#335292) OC+OC at 4 OC: a b c --(1)-> c c b a a (#3) Rule OC: a b c c b c c --(9)-> b c c b c c b c c b a a (#15565) OC+OC at 4 OC: a b c c --(6)-> b c c b a (#120) OC+OC at 1 OC: a b c --(4)-> b a b (#22) OC+OC at 0 OC: a b c --(3)-> c b a b (#13) OC+OC at 3 OC: a b c --(2)-> c b a a (#7) OC+OC at 0 OC: a b c --(1)-> c c b a a (#3) Rule OC: c --(1)-> (#4) Rule OC: a --(1)-> b (#2) Rule OC: c --(1)-> (#4) Rule OC: a b c --(2)-> c c b a (#5) OC+OC at 3 OC: a b c --(1)-> c c b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b c c --(3)-> c c b c c b a a (#122) OC+OC at 3 OC: a b c --(2)-> c c b a b (#10) OC+OC at 4 OC: a b c --(1)-> c c b a a (#3) Rule OC: a --(1)-> b (#2) Rule OC: a b c --(1)-> c c b a a (#3) Rule OC: c --(1)-> (#4) Rule Hence, the SRS is non-terminating.