======================================================== The given Problem was: a a a -> b c c b -> a a a a c ======================================================== A self-embedding rewrite structure for the given SRS is: c b b b --(15)-> b c b b b c a c c a a c c a c c c (#55888) OC+OC at 4 OC: c b b b --(13)-> b c b b c b c a a c c a c c c (#20920) OC+OC at 3 OC: c b b b --(9)-> b c b c b b c a c c c (#890) OC+OC at 5 OC: c b b b --(7)-> b c b c b c b c c (#433) OC+OC at 4 OC: c b b b --(6)-> b c b c a a a b c c (#105) OC+OC at 6 OC: c b b --(4)-> b c b c a a c (#44) OC+OC at 2 OC: c b b --(3)-> b c a a a a a c (#8) OC+OC at 3 OC: c b --(2)-> b c a c (#4) OC+OC at 0 OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b --(2)-> a b c c (#5) OC+OC at 1 OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b --(2)-> b c a c (#4) OC+OC at 0 OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b b --(4)-> b c b c a a c (#44) OC+OC at 2 OC: c b b --(3)-> b c a a a a a c (#8) OC+OC at 3 OC: c b --(2)-> b c a c (#4) OC+OC at 0 OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule OC: c b --(2)-> b c a c (#4) OC+OC at 0 OC: c b --(1)-> a a a a c (#2) Rule OC: a a a --(1)-> b c (#1) Rule Hence, the SRS is non-terminating.