======================================================== The given Problem was: a a a -> c c b b b b -> c c c c c c -> a b b ======================================================== A self-embedding rewrite structure for the given SRS is: a a a b b b b --(19)-> a a a b b b b (#130499) OC+OC at 2 OC: a a a b b b b --(18)-> a a c c c b b (#86868) OC+OC at 2 OC: a a a b b b b --(17)-> a a b b b b b (#59834) OC+OC at 1 OC: a a a b b b b --(15)-> a b b b b b b (#30043) OC+OC at 0 OC: a a a b b b b --(14)-> c c c b b b b (#20427) OC+OC at 1 OC: a a a b b b b --(13)-> c a a a b b b (#13657) OC+OC at 3 OC: a a a b b b b --(11)-> c a a b b b b (#6502) OC+OC at 2 OC: a a a b b b b --(9)-> c a b b b b b (#3237) OC+OC at 1 OC: a a a b b b b --(8)-> c c c c b b b (#366) OC+OC at 2 OC: a a a --(1)-> c c b (#1) Rule OC: b b b b b --(7)-> c c b b b (#223) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c b b --(6)-> c c b b b (#214) OC+OC at 0 OC: c c c b b --(5)-> a a a b b (#48) OC+OC at 1 OC: c c c --(1)-> a b b (#3) Rule OC: b b b b --(4)-> a a b b (#15) OC+OC at 1 OC: b b b --(2)-> a b b (#4) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule OC: b b b --(2)-> a b b (#4) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule OC: a a a --(1)-> c c b (#1) Rule OC: c c c --(1)-> a b b (#3) Rule OC: b b b --(2)-> a b b (#4) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule OC: b b b --(2)-> a b b (#4) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule OC: a a a --(1)-> c c b (#1) Rule OC: c c c --(1)-> a b b (#3) Rule OC: b b b --(2)-> a b b (#4) OC+OC at 0 OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule OC: b b b --(1)-> c c c (#2) Rule OC: c c c --(1)-> a b b (#3) Rule Hence, the SRS is non-terminating.