YES

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()))))
  TDG 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) -> 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()))
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(x,plus(y,z)) -> minus#(x,y)
    plus#(s(x),y) -> minus#(s(x),s(0())) ->
    minus#(s(x),s(y)) -> minus#(p(s(x)),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)) -> p#(s(y))
    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) -> plus#(div(x,z),div(y,z)) ->
    plus#(s(x),y) -> minus#(s(x),s(0()))
    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#(y,z) -> div#(plus(x,y),z) -> div#(x,z)
    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#(s(x),s(y)) -> div#(minus(x,y),s(y))
    div#(plus(x,y),z) -> div#(y,z) -> div#(s(x),s(y)) -> minus#(x,y)
    div#(plus(x,y),z) -> div#(x,z) ->
    div#(plus(x,y),z) -> plus#(div(x,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) -> div#(y,z)
    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#(s(x),s(y)) -> minus#(x,y)
    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)) -> 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) -> div#(y,z)
    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#(s(x),s(y)) -> minus#(x,y)
    div#(s(x),s(y)) -> minus#(x,y) ->
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z)
    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#(s(x),s(y)) -> minus#(p(s(x)),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)) -> p#(s(y))
    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#(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#(x,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#(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)) -> p#(s(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#(minus(x,y),z) ->
    minus#(x,plus(y,z)) -> minus#(x,y)
    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#(s(x),s(y)) -> p#(s(x))
    minus#(x,plus(y,z)) -> minus#(minus(x,y),z) ->
    minus#(s(x),s(y)) -> p#(s(y))
    minus#(x,plus(y,z)) -> minus#(x,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#(x,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#(x,y) ->
    minus#(s(x),s(y)) -> p#(s(x))
    minus#(x,plus(y,z)) -> minus#(x,y) -> minus#(s(x),s(y)) -> p#(s(y))
   SCC Processor:
    #sccs: 4
    #rules: 8
    #arcs: 47/169
    DPs:
     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)
    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:
      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)
     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)))
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       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)))
      interpretation:
       [div#](x0, x1) = x0 + 0,
       
       [plus](x0, x1) = x0 + x1 + 0,
       
       [p](x0) = x0 + 0,
       
       [s](x0) = 1x0 + 1,
       
       [minus](x0, x1) = x0 + 0,
       
       [0] = 7
      orientation:
       div#(plus(x,y),z) = x + y + 0 >= y + 0 = div#(y,z)
       
       div#(s(x),s(y)) = 1x + 1 >= x + 0 = div#(minus(x,y),s(y))
       
       div#(plus(x,y),z) = x + y + 0 >= x + 0 = div#(x,z)
       
       minus(x,0()) = x + 0 >= x = x
       
       minus(0(),y) = 7 >= 7 = 0()
       
       minus(s(x),s(y)) = 1x + 1 >= 1x + 1 = minus(p(s(x)),p(s(y)))
       
       minus(x,plus(y,z)) = x + 0 >= x + 0 = minus(minus(x,y),z)
       
       p(s(s(x))) = 2x + 2 >= 2x + 2 = s(p(s(x)))
      problem:
       DPs:
        div#(plus(x,y),z) -> div#(y,z)
        div#(plus(x,y),z) -> div#(x,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)))
      Restore Modifier:
       DPs:
        div#(plus(x,y),z) -> div#(y,z)
        div#(plus(x,y),z) -> div#(x,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()))))
       Subterm Criterion Processor:
        simple projection:
         pi(div#) = 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
    
    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()))))
    Bounds Processor:
     bound: 2
     enrichment: top-dp
     automaton:
      final states: {9}
      transitions:
       p0(8) -> 8*
       plus0(8,8) -> 8*
       div0(8,8) -> 8*
       plus{#,1}(8,17) -> 9*
       minus1(16,15) -> 17*
       s1(14) -> 15*
       s1(16) -> 16*
       s1(8) -> 16*
       01() -> 14*
       plus{#,2}(17,21) -> 9*
       minus2(20,19) -> 21*
       s2(20) -> 20*
       s2(18) -> 19*
       s2(8) -> 20*
       02() -> 18*
       plus{#,0}(8,8) -> 9*
       p2(20) -> 20*
       p2(19) -> 19*
       s0(8) -> 8*
       p1(15) -> 15*
       p1(16) -> 16*
       minus0(8,8) -> 8*
       00() -> 8*
     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
    
    DPs:
     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)
    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()))))
    CDG Processor:
     DPs:
      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)
     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:
      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#(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)) -> 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: 2
      #rules: 3
      #arcs: 7/9
      DPs:
       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()))))
      Subterm Criterion Processor:
       simple projection:
        pi(minus#) = 1
       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
      
      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()))))
      Usable Rule Processor:
       DPs:
        minus#(s(x),s(y)) -> minus#(p(s(x)),p(s(y)))
       TRS:
        p(s(s(x))) -> s(p(s(x)))
       Semantic Labeling Processor:
        dimension: 2
        usable rules:
         
        interpretation:
                   [1 0]  
         [p](x0) = [1 0]x0,
         
                   [1 1]     [0]
         [s](x0) = [1 1]x0 + [1]
         labeled:
          minus#
          s
          p
         usable (for model):
          minus#
          s
          p
         argument filtering:
          pi(s) = 0
          pi(p) = 0
          pi(minus#) = []
        precedence:
         minus# ~ p ~ s
        problem:
         DPs:
          
         TRS:
          p(s(s(x))) -> s(p(s(x)))
        Qed
    
    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