========================================================
The given Problem was:
a b c -> c b a
a c -> a a d a
d a b -> b a d
d a c -> b c c
========================================================
A self-embedding rewrite structure for the given SRS is:
a (ab)^k+1 cc --> a (ab)^k+2 cc (#119220)
pattern overlapped by closure at r0
RP: a (ab)^k+1 c --> aa (ba)^k+1 da (#70270)
pattern overlapped by pattern
RP: a (ab)^k+1 c --> aad (ab)^k+1 a (#868)
pattern overlapped by closure at l-1
RP: (ab)^k+1 c --> c (ba)^k ba (#29)
expand ->
RP: (ab)^k+1 c --> c (ba)^k+1 (#7)
increment
RP: (ab)^k c --> c (ba)^k (#5)
self-overlapping Closure at -2
OC: a b c --(1)-> c b a (#1)
Rule
OC: a c --(1)-> a a d a (#2)
Rule
RP: d (ab)^k+1 --> (ba)^k+1 d (#8)
increment
RP: d (ab)^k --> (ba)^k d (#1)
self-overlapping Closure at 2
OC: d a b --(1)-> b a d (#3)
Rule
OC: d a c --(1)-> b c c (#4)
Rule
Hence, the SRS is non-terminating.