======================================================== The given Problem was: a a a a -> b a a a b b -> a a b ======================================================== A self-embedding rewrite structure for the given SRS is: (a)^k+4 --> (a)^2k baaa (#1032) pattern overlapped by pattern RP: (a)^k+4 --> (b)^k+1 aaa (#41) increment RP: (a)^k+3 --> (b)^k aaa (#2) self-overlapping Closure at 1 OC: a a a a --(1)-> b a a a (#1) Rule RP: (b)^k+1 --> (a)^2k b (#1) self-overlapping Closure at 2 OC: b b --(1)-> a a b (#2) Rule Hence, the SRS is non-terminating.