======================================================== The given Problem was: a l -> l a r a -> a r b l -> b a r r b -> l b ======================================================== A self-embedding rewrite structure for the given SRS is: b (a)^k lb --> b (a)^k+1 lb (#9734) pattern overlapped by closure at r0 RP: b (a)^k l --> b (a)^k+1 r (#7233) pattern overlapped by pattern RP: b (a)^k l --> bar (a)^k (#130) pattern overlapped by closure at l-1 RP: (a)^k l --> l (a)^k (#2) self-overlapping Closure at -1 OC: a l --(1)-> l a (#1) Rule OC: b l --(1)-> b a r (#3) Rule RP: r (a)^k --> (a)^k r (#3) self-overlapping Closure at 1 OC: r a --(1)-> a r (#2) Rule OC: r b --(1)-> l b (#4) Rule Hence, the SRS is non-terminating.