========================================================
The given Problem was:
b a -> a b
c c -> a b c
c b -> b c
a a -> b a c
========================================================
A self-embedding rewrite structure for the given SRS is:
ac (b)^k c --> bac (b)^k+1 c (#26845)
pattern overlapped by closure at l-1
RP: c (b)^k c --> a (b)^k+1 c (#13520)
pattern overlapped by pattern
RP: c (b)^k c --> (b)^k abc (#151)
pattern overlapped by closure at r0
RP: c (b)^k --> (b)^k c (#3)
self-overlapping Closure at 1
OC: c b --(1)-> b c (#3)
Rule
OC: c c --(1)-> a b c (#2)
Rule
RP: (b)^k a --> a (b)^k (#2)
self-overlapping Closure at -1
OC: b a --(1)-> a b (#1)
Rule
OC: a a --(1)-> b a c (#4)
Rule
Hence, the SRS is non-terminating.