======================================================== The given Problem was: a b -> a c -> c b c b b c -> a a ======================================================== A self-embedding rewrite structure for the given SRS is: b c c c b c --(24)-> c b c c c b c b b b (#2264942) OC+OC at 4 OC: b c c c b c --(23)-> c b c c a c b b (#742970) OC+OC at 3 OC: b c c c b c --(20)-> c b c a c c b b (#479612) OC+OC at 4 OC: b c c c b c --(16)-> c b c a a c b c b b (#111155) OC+OC at 5 OC: b c c c b c --(15)-> c b c a a a c b (#36176) OC+OC at 3 OC: b c c c b c --(14)-> c b c b c a c b (#23018) OC+OC at 0 OC: b c c c b c --(13)-> a c c a c b (#2646) OC+OC at 1 OC: b c --(1)-> a a (#3) Rule OC: a c c b c --(12)-> c c a c b (#2261) OC+OC at 1 OC: a c c b c --(9)-> c a c c b (#1488) OC+OC at 2 OC: a c c b c --(5)-> c a a c b c b (#146) OC+OC at 3 OC: a c --(2)-> c a a b (#7) OC+OC at 1 OC: a c --(1)-> c b c b (#2) Rule OC: b c --(1)-> a a (#3) Rule OC: b c b c --(3)-> c b c b (#10) 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 b c b (#2) Rule OC: a c b --(4)-> c (#16) OC+OC at 1 OC: a c --(1)-> c b c 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: a c --(3)-> c a (#11) OC+OC at 1 OC: a c --(1)-> c b c b (#2) Rule 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 b c b (#2) Rule OC: b c --(1)-> a a (#3) Rule OC: a c --(1)-> c b c b (#2) Rule OC: a c b --(4)-> c (#16) OC+OC at 1 OC: a c --(1)-> c b c 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: a c --(3)-> c a (#11) OC+OC at 1 OC: a c --(1)-> c b c b (#2) Rule 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 b c b (#2) Rule Hence, the SRS is non-terminating.