======================================================== The given Problem was: a a -> b a b c c c a -> c b -> a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b a b a a b --(22)-> b a b b a b a a b a b a b a a b c c (#176286) OC+OC at 13 OC: a a b a b a b a a b --(21)-> b a b b a b a a b a b a b c b a b c c (#169940) OC+OC at 14 OC: a a b a b a b a a b --(20)-> b a b b a b a a b a b a b c a a (#68243) OC+OC at 14 OC: a a b a b a b a a b --(19)-> b a b b a b a a b a b a b c c b a (#65459) OC+OC at 10 OC: a a b a b a b a a b --(18)-> b a b b a b a a b a a a b a (#24702) OC+OC at 10 OC: a a b a b a b a a b --(17)-> b a b b a b a a b a c b a b a (#13954) OC+OC at 11 OC: a a b a b a --(13)-> b a b b a b a a b a c c (#10950) OC+OC at 3 OC: a a b a b a --(7)-> b a b a a b a a b c c (#258) OC+OC at 3 OC: a a b a b a --(6)-> b a b c b a b a a b c c (#122) OC+OC at 4 OC: a a --(1)-> b a b c c (#1) Rule OC: c b a b a --(5)-> b a b a a b c c (#80) OC+OC at 3 OC: c b a b a --(4)-> b a b c b a b c c (#28) OC+OC at 0 OC: c b --(1)-> a (#3) Rule OC: a a b a --(3)-> b a b c b a b c c (#19) OC+OC at 4 OC: a a --(1)-> b a b c c (#1) Rule OC: c b a --(2)-> b a b c c (#5) OC+OC at 0 OC: c b --(1)-> a (#3) Rule OC: a a --(1)-> b a b c c (#1) Rule OC: c b --(1)-> a (#3) Rule OC: c b --(1)-> a (#3) Rule OC: a a b a a b --(6)-> b a b a a b a (#97) OC+OC at 3 OC: a a b a a b --(5)-> b a b c b a b a (#46) OC+OC at 4 OC: a a --(1)-> b a b c c (#1) Rule OC: c b a a b --(4)-> b a b a (#16) OC+OC at 0 OC: c b --(1)-> a (#3) Rule OC: a a a b --(3)-> b a b a (#9) OC+OC at 3 OC: a a a --(2)-> b a b c (#4) OC+OC at 4 OC: a a --(1)-> b a b c c (#1) Rule OC: c a --(1)-> (#2) Rule OC: c b --(1)-> a (#3) Rule OC: c b --(1)-> a (#3) Rule OC: c b a a b --(4)-> b a b a (#16) OC+OC at 0 OC: c b --(1)-> a (#3) Rule OC: a a a b --(3)-> b a b a (#9) OC+OC at 3 OC: a a a --(2)-> b a b c (#4) OC+OC at 4 OC: a a --(1)-> b a b c c (#1) Rule OC: c a --(1)-> (#2) Rule OC: c b --(1)-> a (#3) Rule OC: c b --(1)-> a (#3) Rule OC: a a --(1)-> b a b c c (#1) Rule OC: c b --(1)-> a (#3) Rule OC: a a --(1)-> b a b c c (#1) Rule OC: c b --(1)-> a (#3) Rule Hence, the SRS is non-terminating.