======================================================== The given Problem was: a -> b a c -> c b b -> a a a c c ======================================================== A self-embedding rewrite structure for the given SRS is: c b b b b b b --(13)-> a a a c b b b b b b c c c (#160483) OC+OC at 5 OC: c b b b b b b --(12)-> a a a c b a b b b b c c c (#71727) OC+OC at 4 OC: c b b --(1)-> a a a c c (#3) Rule OC: c b b b b --(11)-> b a b b b b c c c (#18497) OC+OC at 3 OC: c b b b b --(7)-> b a b c b b c (#363) OC+OC at 4 OC: c b b --(3)-> b a b c c (#8) OC+OC at 0 OC: c b b --(2)-> a a b c c (#6) OC+OC at 2 OC: c b b --(1)-> a a a c c (#3) Rule OC: a --(1)-> b (#1) Rule OC: a --(1)-> b (#1) Rule OC: c b b --(4)-> b b c (#19) OC+OC at 2 OC: c b b --(3)-> b b a c c (#10) OC+OC at 0 OC: c b b --(2)-> a b a c c (#5) OC+OC at 1 OC: c b b --(1)-> a a a c c (#3) Rule OC: a --(1)-> b (#1) Rule OC: a --(1)-> b (#1) Rule OC: a c --(1)-> (#2) Rule OC: c b b --(4)-> b b b c c (#16) OC+OC at 0 OC: c b b --(3)-> a b b c c (#9) OC+OC at 1 OC: c b b --(2)-> a a b c c (#6) OC+OC at 2 OC: c b b --(1)-> a a a c c (#3) Rule OC: a --(1)-> b (#1) Rule OC: a --(1)-> b (#1) Rule OC: a --(1)-> b (#1) Rule OC: a --(1)-> b (#1) Rule Hence, the SRS is non-terminating.