======================================================== The given Problem was: a b -> a c -> c c b b b c -> a a ======================================================== A self-embedding rewrite structure for the given SRS is: b c c c c --(24)-> c c b c c c c b b c b b b b b b b (#755977) OC+OC at 5 OC: b c c c c --(23)-> c c b c c a c c b b b b b b b (#530387) OC+OC at 5 OC: b c c c c --(21)-> c c b c c b c c b b b b b (#277168) OC+OC at 6 OC: b c c c c --(18)-> c c b c c b b c b c b b b (#110822) OC+OC at 9 OC: b c c c c --(15)-> c c b c c b b c b b c b b c b b b (#43967) OC+OC at 3 OC: b c c c c --(14)-> c c b a c c b b c b b c b b b (#17127) OC+OC at 4 OC: b c c c c --(13)-> c c b a a c c b b c b b b (#6651) OC+OC at 5 OC: b c c c c --(12)-> c c b a a a c c b b b (#2655) OC+OC at 6 OC: b c c c c --(11)-> c c b a a a a c b (#1111) OC+OC at 5 OC: b c c c c --(10)-> c c b a a b c c b (#371) OC+OC at 6 OC: b c c --(4)-> c c b a a b b (#35) OC+OC at 3 OC: b c c --(3)-> c c b b c b b (#24) OC+OC at 0 OC: b c c --(2)-> a c c b b (#6) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule OC: b c --(1)-> a a (#3) Rule OC: b c c --(6)-> c c b (#55) OC+OC at 3 OC: b c c --(3)-> c c b b c b b (#24) OC+OC at 0 OC: b c c --(2)-> a c c b b (#6) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule OC: b c b b --(3)-> (#5) OC+OC at 0 OC: b c b --(2)-> a (#4) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a b --(1)-> (#1) Rule OC: a b --(1)-> (#1) Rule OC: b c --(1)-> a a (#3) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule OC: b c b b --(3)-> (#5) OC+OC at 0 OC: b c b --(2)-> a (#4) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a b --(1)-> (#1) Rule OC: a b --(1)-> (#1) Rule OC: b c b c --(3)-> c c b b (#8) OC+OC at 0 OC: b c b --(2)-> a (#4) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a b --(1)-> (#1) Rule OC: a c --(1)-> c c b b (#2) Rule OC: b c c --(2)-> a c c b b (#6) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a c --(1)-> c c b b (#2) Rule OC: a c --(1)-> c c b b (#2) Rule Hence, the SRS is non-terminating.