MAYBE

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

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