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