========================================================
The given Problem was:
a a b -> b b c a a
a c -> a a
========================================================
A self-embedding rewrite structure for the given SRS is:
a a b c a b b c b b --(11)-> b b c b b c b b c a b b c a a b c a b b c b b c a a (#352242)
OC+OC at 18
OC: a a b c a b b --(8)-> b b c b b c b b c a b b c a a b c a a (#25589)
OC+OC at 10
OC: a a b c a b b --(6)-> b b c b b c b b c a a c b b c a a (#4242)
OC+OC at 12
OC: a a b c a b --(5)-> b b c b b c b b c a a c a a (#1653)
OC+OC at 6
OC: a a b c a b --(4)-> b b c b b c a a b c a a (#651)
OC+OC at 3
OC: a a b c a b --(3)-> b b c a a b b c a a (#67)
OC+OC at 4
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a c a b --(2)-> a b b c a a (#7)
OC+OC at 1
OC: a c --(1)-> a a (#2)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a c b --(2)-> b b c a a (#6)
OC+OC at 0
OC: a c --(1)-> a a (#2)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a c b b --(3)-> b b c b b c a a (#31)
OC+OC at 0
OC: a c --(1)-> a a (#2)
Rule
OC: a a b b --(2)-> b b c b b c a a (#25)
OC+OC at 3
OC: a a b --(1)-> b b c a a (#1)
Rule
OC: a a b --(1)-> b b c a a (#1)
Rule
Hence, the SRS is non-terminating.