======================================================== The given Problem was: a -> a a a -> b b c -> c a c b c -> ======================================================== A self-embedding rewrite structure for the given SRS is: b c c c c c --(13)-> b c c c c c b (#12478) OC+OC at 5 OC: b c c c c c --(12)-> b c c c c a c b (#11712) OC+OC at 2 OC: b c c c --(9)-> b c b (#1246) OC+OC at 0 OC: b c c c --(8)-> a a a c b (#468) OC+OC at 2 OC: b c c c --(7)-> a a c a c b (#339) OC+OC at 3 OC: b c c --(5)-> a a c b (#61) OC+OC at 0 OC: b c c --(4)-> c a a c b (#22) OC+OC at 2 OC: b c --(2)-> c a b (#7) OC+OC at 2 OC: b c --(1)-> c a c b (#3) Rule OC: c --(1)-> (#4) Rule OC: b c --(2)-> a c b (#6) OC+OC at 0 OC: b c --(1)-> c a c b (#3) Rule OC: c --(1)-> (#4) Rule OC: c --(1)-> (#4) Rule OC: b c --(2)-> a c b (#6) OC+OC at 0 OC: b c --(1)-> c a c b (#3) Rule OC: c --(1)-> (#4) Rule OC: c --(1)-> (#4) Rule OC: a a a --(1)-> b (#2) Rule OC: b c c --(3)-> c c c a c b (#35) OC+OC at 2 OC: b c --(2)-> c c b (#5) OC+OC at 1 OC: b c --(1)-> c a c b (#3) Rule OC: a --(1)-> (#1) Rule OC: b c --(1)-> c a c b (#3) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.