======================================================== The given Problem was: a a b -> c c a a a a c -> b a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b b a b b --(10)-> c c b b a a b b a b b a a a a (#10376) OC+OC at 10 OC: a a b b a b b --(9)-> c c b b a a b b a b a c a a a (#6839) OC+OC at 7 OC: a a b b a b b --(8)-> c c b b a a b a c b a c a a a (#4752) OC+OC at 6 OC: a a b b a b b --(7)-> c c b b a a a c c b a c a a a (#1483) OC+OC at 7 OC: a a b b --(4)-> c c b b a a a a (#37) OC+OC at 3 OC: a a b b --(3)-> c c b a c a a a (#24) OC+OC at 2 OC: a a b b --(2)-> c c a c c a a a (#17) OC+OC at 3 OC: a a b --(1)-> c c a a a (#1) Rule OC: a a b --(1)-> c c a a a (#1) Rule OC: a c --(1)-> b a (#2) Rule OC: a c --(1)-> b a (#2) Rule OC: a a b b --(3)-> c c b a c a a a (#24) OC+OC at 2 OC: a a b b --(2)-> c c a c c a a a (#17) OC+OC at 3 OC: a a b --(1)-> c c a a a (#1) Rule OC: a a b --(1)-> c c a a a (#1) Rule OC: a c --(1)-> b a (#2) Rule OC: a c --(1)-> b a (#2) Rule OC: a c --(1)-> b a (#2) Rule OC: a c --(1)-> b a (#2) Rule Hence, the SRS is non-terminating.