MAYBE
Trs:
 {     times(X, s(Y)) -> plus(X, times(Y, X)),
  plus(plus(X, Y), Z) -> plus(X, plus(Y, Z))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open