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()))))
  EDG 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()))))
   graph:
    plus#(s(x),y) -> plus#(y,minus(s(x),s(0()))) ->
    plus#(s(x),y) -> minus#(s(x),s(0()))
    plus#(s(x),y) -> plus#(y,minus(s(x),s(0()))) ->
    plus#(s(x),y) -> plus#(y,minus(s(x),s(0())))
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(s(x),s(y)) -> p#(s(y))
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(s(x),s(y)) -> p#(s(x))
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z)) ->
    plus#(s(x),y) -> minus#(s(x),s(0()))
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z)) ->
    plus#(s(x),y) -> plus#(y,minus(s(x),s(0())))
    div#(plus(x,y),z) -> div#(y,z) -> div#(s(x),s(y)) -> minus#(x,y)
    div#(plus(x,y),z) -> div#(y,z) ->
    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#(y,z)
    div#(plus(x,y),z) -> div#(y,z) -> div#(plus(x,y),z) -> div#(x,z)
    div#(plus(x,y),z) -> div#(y,z) ->
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z))
    div#(plus(x,y),z) -> div#(x,z) -> div#(s(x),s(y)) -> minus#(x,y)
    div#(plus(x,y),z) -> div#(x,z) ->
    div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    div#(plus(x,y),z) -> div#(x,z) -> div#(plus(x,y),z) -> div#(y,z)
    div#(plus(x,y),z) -> div#(x,z) -> div#(plus(x,y),z) -> div#(x,z)
    div#(plus(x,y),z) -> div#(x,z) ->
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z))
    div#(s(x),s(y)) -> div#(minus(x,y),s(y)) ->
    div#(s(x),s(y)) -> minus#(x,y)
    div#(s(x),s(y)) -> div#(minus(x,y),s(y)) ->
    div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    div#(s(x),s(y)) -> div#(minus(x,y),s(y)) ->
    div#(plus(x,y),z) -> div#(y,z)
    div#(s(x),s(y)) -> div#(minus(x,y),s(y)) ->
    div#(plus(x,y),z) -> div#(x,z)
    div#(s(x),s(y)) -> div#(minus(x,y),s(y)) ->
    div#(plus(x,y),z) -> plus#(div(x,z),div(y,z))
    div#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> p#(s(y))
    div#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> p#(s(x))
    div#(s(x),s(y)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
    div#(s(x),s(y)) -> minus#(x,y) ->
    minus#(x,plus(y,z)) -> minus#(x,y)
    div#(s(x),s(y)) -> minus#(x,y) ->
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    minus#(s(x),s(y)) -> p#(s(y)) -> p#(s(s(x))) -> p#(s(x))
    minus#(s(x),s(y)) -> p#(s(x)) ->
    p#(s(s(x))) -> p#(s(x))
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y))) ->
    minus#(s(x),s(y)) -> p#(s(y))
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y))) ->
    minus#(s(x),s(y)) -> p#(s(x))
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y))) ->
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y))) ->
    minus#(x,plus(y,z)) -> minus#(x,y)
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y))) ->
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(s(x),s(y)) -> p#(s(y))
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(s(x),s(y)) -> p#(s(x))
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(x,plus(y,z)) -> minus#(x,y)
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    minus#(x,plus(y,z)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> p#(s(y))
    minus#(x,plus(y,z)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> p#(s(x))
    minus#(x,plus(y,z)) -> minus#(x,y) ->
    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#(x,y)
    minus#(x,plus(y,z)) -> minus#(x,y) -> minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
   SCC Processor:
    #sccs: 4
    #rules: 8
    #arcs: 45/169
    DPs:
     div#(plus(x,y),z) -> div#(y,z)
     div#(plus(x,y),z) -> div#(x,z)
     div#(s(x),s(y)) -> div#(minus(x,y),s(y))
    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()))))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [div#](x0, x1) = x0 + 1,
      
      [div](x0, x1) = x0,
      
      [plus](x0, x1) = x0 + x1 + 1,
      
      [p](x0) = 0,
      
      [s](x0) = x0,
      
      [minus](x0, x1) = x0,
      
      [0] = 0
     orientation:
      div#(plus(x,y),z) = x + y + 2 >= y + 1 = div#(y,z)
      
      div#(plus(x,y),z) = x + y + 2 >= x + 1 = div#(x,z)
      
      div#(s(x),s(y)) = x + 1 >= x + 1 = div#(minus(x,y),s(y))
      
      minus(x,0()) = x >= x = x
      
      minus(0(),y) = 0 >= 0 = 0()
      
      minus(s(x),s(y)) = x >= 0 = minus(p(s(x)),p(s(y)))
      
      minus(x,plus(y,z)) = x >= x = minus(minus(x,y),z)
      
      p(s(s(x))) = 0 >= 0 = s(p(s(x)))
      
      p(0()) = 0 >= 0 = s(s(0()))
      
      div(s(x),s(y)) = x >= x = s(div(minus(x,y),s(y)))
      
      div(plus(x,y),z) = x + y + 1 >= x + y + 1 = plus(div(x,z),div(y,z))
      
      plus(0(),y) = y + 1 >= y = y
      
      plus(s(x),y) = x + y + 1 >= x + y + 1 = s(plus(y,minus(s(x),s(0()))))
     problem:
      DPs:
       div#(s(x),s(y)) -> div#(minus(x,y),s(y))
      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()))))
     Open
    
    DPs:
     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()))))
    Open
    
    DPs:
     minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
     minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
     minus#(x,plus(y,z)) -> minus#(x,y)
    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()))))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [minus#](x0, x1) = x0 + x1 + 1,
      
      [div](x0, x1) = x0,
      
      [plus](x0, x1) = x0 + x1 + 1,
      
      [p](x0) = 0,
      
      [s](x0) = 0,
      
      [minus](x0, x1) = x0 + x1 + 1,
      
      [0] = 0
     orientation:
      minus#(s(x),s(y)) = 1 >= 1 = minus#(p(s(x)),p(s(y)))
      
      minus#(x,plus(y,z)) = x + y + z + 2 >= x + y + z + 2 = minus#(minus(x,y),z)
      
      minus#(x,plus(y,z)) = x + y + z + 2 >= x + y + 1 = minus#(x,y)
      
      minus(x,0()) = x + 1 >= x = x
      
      minus(0(),y) = y + 1 >= 0 = 0()
      
      minus(s(x),s(y)) = 1 >= 1 = minus(p(s(x)),p(s(y)))
      
      minus(x,plus(y,z)) = x + y + z + 2 >= x + y + z + 2 = minus(minus(x,y),z)
      
      p(s(s(x))) = 0 >= 0 = s(p(s(x)))
      
      p(0()) = 0 >= 0 = s(s(0()))
      
      div(s(x),s(y)) = 0 >= 0 = s(div(minus(x,y),s(y)))
      
      div(plus(x,y),z) = x + y + 1 >= x + y + 1 = plus(div(x,z),div(y,z))
      
      plus(0(),y) = y + 1 >= y = y
      
      plus(s(x),y) = y + 1 >= 0 = s(plus(y,minus(s(x),s(0()))))
     problem:
      DPs:
       minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
       minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
      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()))))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [minus#](x0, x1) = x1,
       
       [div](x0, x1) = x0,
       
       [plus](x0, x1) = x1 + 1,
       
       [p](x0) = 0,
       
       [s](x0) = 0,
       
       [minus](x0, x1) = x0,
       
       [0] = 0
      orientation:
       minus#(s(x),s(y)) = 0 >= 0 = minus#(p(s(x)),p(s(y)))
       
       minus#(x,plus(y,z)) = z + 1 >= z = minus#(minus(x,y),z)
       
       minus(x,0()) = x >= x = x
       
       minus(0(),y) = 0 >= 0 = 0()
       
       minus(s(x),s(y)) = 0 >= 0 = minus(p(s(x)),p(s(y)))
       
       minus(x,plus(y,z)) = x >= x = minus(minus(x,y),z)
       
       p(s(s(x))) = 0 >= 0 = s(p(s(x)))
       
       p(0()) = 0 >= 0 = s(s(0()))
       
       div(s(x),s(y)) = 0 >= 0 = s(div(minus(x,y),s(y)))
       
       div(plus(x,y),z) = y + 1 >= y + 1 = plus(div(x,z),div(y,z))
       
       plus(0(),y) = y + 1 >= y = y
       
       plus(s(x),y) = y + 1 >= 0 = s(plus(y,minus(s(x),s(0()))))
      problem:
       DPs:
        minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
       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()))))
      Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    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()))))
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      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()))))
     Qed