======================================================== The given Problem was: b c -> d c b d -> d b a d -> a b b ======================================================== A self-embedding rewrite structure for the given SRS is: a (b)^k dc --> a (b)^k+1 dc (#1249) pattern overlapped by closure at r0 RP: a (b)^k d --> a (b)^k+1 b (#190) expand -> RP: a (b)^k d --> a (b)^k+2 (#66) pattern overlapped by closure at l-1 RP: (b)^k d --> d (b)^k (#2) self-overlapping Closure at -1 OC: b d --(1)-> d b (#2) Rule OC: a d --(1)-> a b b (#3) Rule OC: b c --(1)-> d c (#1) Rule Hence, the SRS is non-terminating.