MAYBE
Trs:
 {           double(0()) -> 0(),
            double(s(x)) -> s(s(double(x))),
       minus(s(x), s(y)) -> minus(x, y),
           minus(x, 0()) -> x,
            plus(0(), y) -> y,
  plus(s(plus(x, y)), z) -> s(plus(plus(x, y), z)),
           plus(s(x), y) -> plus(x, s(y)),
           plus(s(x), y) -> s(plus(minus(x, y), double(y))),
           plus(s(x), y) -> s(plus(x, y))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open