======================================================== The given Problem was: a -> a a -> b b c b -> c b -> b a c ======================================================== A self-embedding rewrite structure for the given SRS is: c b b b b b b --(16)-> b b b c b b b b b b c c c (#619877) OC+OC at 4 OC: c b b --(4)-> b b b c c (#146) OC+OC at 1 OC: c b b --(3)-> b a a c (#12) OC+OC at 2 OC: c b --(1)-> b a c (#4) Rule OC: c b --(2)-> a c (#6) OC+OC at 0 OC: c b --(1)-> b a c (#4) Rule OC: b --(1)-> (#3) Rule OC: a a --(1)-> b b c (#2) Rule OC: c b b b b --(12)-> b b b b b b c c c (#42101) OC+OC at 4 OC: c b b b b --(11)-> b b b b a a c c (#21824) OC+OC at 5 OC: c b b b b --(9)-> b b b b a c b c (#4395) OC+OC at 6 OC: c b b b --(7)-> b b b b a c c (#1957) OC+OC at 3 OC: c b b b --(6)-> b b b c b c (#379) OC+OC at 4 OC: c b b --(4)-> b b b c c (#146) OC+OC at 1 OC: c b b --(3)-> b a a c (#12) OC+OC at 2 OC: c b --(1)-> b a c (#4) Rule OC: c b --(2)-> a c (#6) OC+OC at 0 OC: c b --(1)-> b a c (#4) Rule OC: b --(1)-> (#3) Rule OC: a a --(1)-> b b c (#2) Rule OC: c b --(2)-> b c (#5) OC+OC at 1 OC: c b --(1)-> b a c (#4) Rule OC: a --(1)-> (#1) Rule OC: c b --(1)-> b a c (#4) Rule OC: c b --(2)-> b c (#5) OC+OC at 1 OC: c b --(1)-> b a c (#4) Rule OC: a --(1)-> (#1) Rule OC: c b --(2)-> a c (#6) OC+OC at 0 OC: c b --(1)-> b a c (#4) Rule OC: b --(1)-> (#3) Rule OC: a a --(1)-> b b c (#2) Rule Hence, the SRS is non-terminating.