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