======================================================== The given Problem was: a -> a b -> c c c -> b c b a a ======================================================== A self-embedding rewrite structure for the given SRS is: c c b c b c b c --(27)-> b c b b c b b c b c c b c b c b c (#885657) OC+OC at 16 OC: c c b c b c b c --(26)-> b c b b c b b c b c c b c b c b a b (#818022) OC+OC at 13 OC: c c b c b c b c --(24)-> b c b b c b b c b c c b c c c b (#301536) OC+OC at 13 OC: c c b c b c b c --(23)-> b c b b c b b c b c c b c a b c b (#165772) OC+OC at 14 OC: c c b c b c --(19)-> b c b b c b b c b c c b c a a (#155834) OC+OC at 6 OC: c c b c b c --(13)-> b c b b c b c c b c b a a (#10950) OC+OC at 3 OC: c c b c b c --(7)-> b c b c c b c c b a a (#473) OC+OC at 6 OC: c c b c b c --(6)-> b c b c c b a b c b a a (#203) OC+OC at 7 OC: c c b c --(4)-> b c b c c b a a (#64) OC+OC at 3 OC: c c b c --(3)-> b c b a b c b a a (#20) OC+OC at 4 OC: c c --(1)-> b c b a a (#3) Rule OC: a b c --(2)-> b c b a a (#6) OC+OC at 0 OC: a b --(1)-> c (#2) Rule OC: c c --(1)-> b c b a a (#3) Rule OC: a b --(1)-> c (#2) Rule OC: a b c --(2)-> b c b a a (#6) OC+OC at 0 OC: a b --(1)-> c (#2) Rule OC: c c --(1)-> b c b a a (#3) Rule OC: a b --(1)-> c (#2) Rule OC: c c b c --(6)-> b c b c c b (#67) OC+OC at 3 OC: c c b c --(5)-> b c b a b c b (#21) OC+OC at 4 OC: c c --(1)-> b c b a a (#3) Rule OC: a b c --(4)-> b c b (#10) OC+OC at 3 OC: a b c --(3)-> b c b a (#7) OC+OC at 0 OC: a b --(1)-> c (#2) Rule OC: c c --(2)-> b c b a (#4) OC+OC at 3 OC: c c --(1)-> b c b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> c (#2) Rule OC: c c b c b --(6)-> b c b c c b c (#102) OC+OC at 3 OC: c c b c b --(5)-> b c b a b c b c (#45) OC+OC at 4 OC: c c --(1)-> b c b a a (#3) Rule OC: a b c b --(4)-> b c b c (#15) OC+OC at 0 OC: a b --(1)-> c (#2) Rule OC: c c b --(3)-> b c b c (#9) OC+OC at 3 OC: c c --(2)-> b c b a (#4) OC+OC at 3 OC: c c --(1)-> b c b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> c (#2) Rule OC: a b --(1)-> c (#2) Rule OC: a b c --(4)-> b c b (#10) OC+OC at 3 OC: a b c --(3)-> b c b a (#7) OC+OC at 0 OC: a b --(1)-> c (#2) Rule OC: c c --(2)-> b c b a (#4) OC+OC at 3 OC: c c --(1)-> b c b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> c (#2) Rule OC: c c --(2)-> b c b a (#4) OC+OC at 3 OC: c c --(1)-> b c b a a (#3) Rule OC: a --(1)-> (#1) Rule OC: a b --(1)-> c (#2) Rule Hence, the SRS is non-terminating.