MAYBE

Problem:
 -(0(),y) -> 0()
 -(x,0()) -> x
 -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
 p(0()) -> 0()
 p(s(x)) -> x

Proof:
 DP Processor:
  DPs:
   -#(x,s(y)) -> p#(s(y))
   -#(x,s(y)) -> -#(x,p(s(y)))
  TRS:
   -(0(),y) -> 0()
   -(x,0()) -> x
   -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
   p(0()) -> 0()
   p(s(x)) -> x
  Usable Rule Processor:
   DPs:
    -#(x,s(y)) -> p#(s(y))
    -#(x,s(y)) -> -#(x,p(s(y)))
   TRS:
    p(s(x)) -> x
   ADG Processor:
    DPs:
     -#(x,s(y)) -> p#(s(y))
     -#(x,s(y)) -> -#(x,p(s(y)))
    TRS:
     p(s(x)) -> x
    graph:
     -#(x,s(y)) -> -#(x,p(s(y))) -> -#(x,s(y)) -> p#(s(y))
     -#(x,s(y)) -> -#(x,p(s(y))) -> -#(x,s(y)) -> -#(x,p(s(y)))
    Restore Modifier:
     DPs:
      -#(x,s(y)) -> p#(s(y))
      -#(x,s(y)) -> -#(x,p(s(y)))
     TRS:
      -(0(),y) -> 0()
      -(x,0()) -> x
      -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
      p(0()) -> 0()
      p(s(x)) -> x
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 2/4
      DPs:
       -#(x,s(y)) -> -#(x,p(s(y)))
      TRS:
       -(0(),y) -> 0()
       -(x,0()) -> x
       -(x,s(y)) -> if(greater(x,s(y)),s(-(x,p(s(y)))),0())
       p(0()) -> 0()
       p(s(x)) -> x
      Open