MAYBE
MAYBE
TRS:
 {
          minus(x, 0()) -> x,
  minus(minus(x, y), z) -> minus(x, plus(y, z)),
          minus(0(), y) -> 0(),
      minus(s(x), s(y)) -> minus(x, y),
           plus(0(), y) -> y,
          plus(s(x), y) -> plus(x, s(y)),
          plus(s(x), y) -> s(plus(y, x)),
              zero(0()) -> true(),
             zero(s(x)) -> false(),
                 p(0()) -> 0(),
                p(s(x)) -> x,
     quot(0(), s(y), z) -> z,
    quot(s(x), s(y), z) -> quot(minus(p(ack(0(), x)), y), s(y), s(z)),
              div(x, y) -> quot(x, y, 0()),
            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))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            minus(x, 0()) -> x,
    minus(minus(x, y), z) -> minus(x, plus(y, z)),
            minus(0(), y) -> 0(),
        minus(s(x), s(y)) -> minus(x, y),
             plus(0(), y) -> y,
            plus(s(x), y) -> plus(x, s(y)),
            plus(s(x), y) -> s(plus(y, x)),
                zero(0()) -> true(),
               zero(s(x)) -> false(),
                   p(0()) -> 0(),
                  p(s(x)) -> x,
       quot(0(), s(y), z) -> z,
      quot(s(x), s(y), z) -> quot(minus(p(ack(0(), x)), y), s(y), s(z)),
                div(x, y) -> quot(x, y, 0()),
              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))
   }
  Fail