MAYBE

Problem:
 minus(x,0()) -> x
 minus(0(),y) -> 0()
 minus(s(x),s(y)) -> minus(p(s(x)),p(s(y)))
 minus(x,plus(y,z)) -> minus(minus(x,y),z)
 p(s(s(x))) -> s(p(s(x)))
 p(0()) -> s(s(0()))
 div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
 div(plus(x,y),z) -> plus(div(x,z),div(y,z))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(y,minus(s(x),s(0()))))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> p#(s(y))
   minus#(s(x),s(y)) -> p#(s(x))
   minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
   minus#(x,plus(y,z)) -> minus#(x,y)
   minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
   p#(s(s(x))) -> p#(s(x))
   div#(s(x),s(y)) -> minus#(x,y)
   div#(s(x),s(y)) -> div#(minus(x,y),s(y))
   div#(plus(x,y),z) -> div#(y,z)
   div#(plus(x,y),z) -> div#(x,z)
   div#(plus(x,y),z) -> plus#(div(x,z),div(y,z))
   plus#(s(x),y) -> minus#(s(x),s(0()))
   plus#(s(x),y) -> plus#(y,minus(s(x),s(0())))
  TRS:
   minus(x,0()) -> x
   minus(0(),y) -> 0()
   minus(s(x),s(y)) -> minus(p(s(x)),p(s(y)))
   minus(x,plus(y,z)) -> minus(minus(x,y),z)
   p(s(s(x))) -> s(p(s(x)))
   p(0()) -> s(s(0()))
   div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
   div(plus(x,y),z) -> plus(div(x,z),div(y,z))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(y,minus(s(x),s(0()))))
  Usable Rule Processor:
   DPs:
    minus#(s(x),s(y)) -> p#(s(y))
    minus#(s(x),s(y)) -> p#(s(x))
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
    minus#(x,plus(y,z)) -> minus#(x,y)
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    p#(s(s(x))) -> p#(s(x))
    div#(s(x),s(y)) -> minus#(x,y)
    div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    div#(plus(x,y),z) -> div#(y,z)
    div#(plus(x,y),z) -> div#(x,z)
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z))
    plus#(s(x),y) -> minus#(s(x),s(0()))
    plus#(s(x),y) -> plus#(y,minus(s(x),s(0())))
   TRS:
    p(s(s(x))) -> s(p(s(x)))
    minus(x,0()) -> x
    minus(0(),y) -> 0()
    minus(s(x),s(y)) -> minus(p(s(x)),p(s(y)))
    minus(x,plus(y,z)) -> minus(minus(x,y),z)
    div(s(x),s(y)) -> s(div(minus(x,y),s(y)))
    div(plus(x,y),z) -> plus(div(x,z),div(y,z))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(y,minus(s(x),s(0()))))
   Open