======================================================== The given Problem was: a -> a a b -> b a b a b b b -> a ======================================================== A self-embedding rewrite structure for the given SRS is: a a b a b a b a b a b a b --(15)-> a a b a b a b a b a b a b (#2967853) OC+OC at 10 OC: a a b a b a b a b a b --(13)-> a a b a b a b a b a a (#1348281) OC+OC at 2 OC: a a b a b a b a b a b --(12)-> a a a a b b a b a a (#606062) OC+OC at 5 OC: a a b a b a b a b a b --(11)-> a a a a b a a b a (#285337) OC+OC at 0 OC: a a b a b a b a b a b --(10)-> b b b a a a b a a b a (#67888) OC+OC at 2 OC: a a b --(2)-> b b a (#5) OC+OC at 1 OC: a a b --(1)-> b a b a (#2) Rule OC: a --(1)-> (#1) Rule OC: a a b a b a b a b --(8)-> b a a a b a a b a (#37518) OC+OC at 2 OC: a a b a b a b a b --(7)-> b a b b b a b a a b a (#8530) OC+OC at 3 OC: a a b --(1)-> b a b a (#2) Rule OC: a a b a b a b --(6)-> b b a b a a b a (#4061) OC+OC at 1 OC: a a b a b a b --(5)-> b a a b a b a (#232) OC+OC at 3 OC: a a b a b --(4)-> b a a a (#102) OC+OC at 2 OC: a a b a b --(3)-> b a b b b a (#25) OC+OC at 3 OC: a a b --(1)-> b a b a (#2) Rule OC: a a b --(2)-> b b a (#5) OC+OC at 1 OC: a a b --(1)-> b a b a (#2) Rule OC: a --(1)-> (#1) Rule OC: b b b --(1)-> a (#3) Rule OC: a a b --(1)-> b a b a (#2) Rule OC: a a b --(1)-> b a b a (#2) Rule OC: b b b --(1)-> a (#3) Rule OC: b b b --(1)-> a (#3) Rule OC: a a b --(1)-> b a b a (#2) Rule OC: a a b --(1)-> b a b a (#2) Rule OC: a a b --(2)-> b a b (#6) OC+OC at 3 OC: a a b --(1)-> b a b a (#2) Rule OC: a --(1)-> (#1) Rule Hence, the SRS is non-terminating.