YES

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

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   plus#(s(x),y) -> plus#(x,y)
   plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
  TDG Processor:
   DPs:
    minus#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    plus#(s(x),y) -> plus#(x,y)
    plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
   TRS:
    minus(x,0()) -> x
    minus(s(x),s(y)) -> minus(x,y)
    quot(0(),s(y)) -> 0()
    quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
   graph:
    plus#(s(x),y) -> plus#(x,y) ->
    plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
    plus#(s(x),y) -> plus#(x,y) ->
    plus#(s(x),y) -> plus#(x,y)
    plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) ->
    plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
    plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0()))) ->
    plus#(s(x),y) -> plus#(x,y)
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    quot#(s(x),s(y)) -> quot#(minus(x,y),s(y)) ->
    quot#(s(x),s(y)) -> minus#(x,y)
    quot#(s(x),s(y)) -> minus#(x,y) ->
    minus#(s(x),s(y)) -> minus#(x,y)
    minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 8/25
    DPs:
     quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [quot#](x0, x1) = x0,
      
      [plus](x0, x1) = 2x0 + 2x1 + 4,
      
      [quot](x0, x1) = 4x0 + 3x1 + 3,
      
      [s](x0) = x0 + 2,
      
      [minus](x0, x1) = x0,
      
      [0] = 0
     orientation:
      quot#(s(x),s(y)) = x + 2 >= x = quot#(minus(x,y),s(y))
      
      minus(x,0()) = x >= x = x
      
      minus(s(x),s(y)) = x + 2 >= x = minus(x,y)
      
      quot(0(),s(y)) = 3y + 9 >= 0 = 0()
      
      quot(s(x),s(y)) = 4x + 3y + 17 >= 4x + 3y + 11 = s(quot(minus(x,y),s(y)))
      
      plus(0(),y) = 2y + 4 >= y = y
      
      plus(s(x),y) = 2x + 2y + 8 >= 2x + 2y + 6 = s(plus(x,y))
      
      plus(minus(x,s(0())),minus(y,s(s(z)))) = 2x + 2y + 4 >= 2x + 2y + 4 = plus(minus(y,s(s(z))),minus(x,s(0())))
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
     Qed
    
    DPs:
     minus#(s(x),s(y)) -> minus#(x,y)
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [minus#](x0, x1) = x0,
      
      [plus](x0, x1) = x0 + x1,
      
      [quot](x0, x1) = x0,
      
      [s](x0) = x0 + 2,
      
      [minus](x0, x1) = x0,
      
      [0] = 0
     orientation:
      minus#(s(x),s(y)) = x + 2 >= x = minus#(x,y)
      
      minus(x,0()) = x >= x = x
      
      minus(s(x),s(y)) = x + 2 >= x = minus(x,y)
      
      quot(0(),s(y)) = 0 >= 0 = 0()
      
      quot(s(x),s(y)) = x + 2 >= x + 2 = s(quot(minus(x,y),s(y)))
      
      plus(0(),y) = y >= y = y
      
      plus(s(x),y) = x + y + 2 >= x + y + 2 = s(plus(x,y))
      
      plus(minus(x,s(0())),minus(y,s(s(z)))) = x + y >= x + y = plus(minus(y,s(s(z))),minus(x,s(0())))
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
     Qed
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
     plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
    Matrix Interpretation Processor: dim=3
     
     interpretation:
      [plus#](x0, x1) = [1 0 1]x0 + [0 1 0]x1,
      
                              
      [plus](x0, x1) = x0 + x1
                              ,
      
                       [1 0 0]     [0 0 1]     [1]
      [quot](x0, x1) = [0 0 0]x0 + [0 1 0]x1 + [0]
                       [0 0 0]     [0 0 0]     [0],
      
                     [1]
      [s](x0) = x0 + [0]
                     [0],
      
                        [1 0 0]     [0 0 0]     [0]
      [minus](x0, x1) = [1 1 1]x0 + [1 0 0]x1 + [1]
                        [0 1 1]     [0 0 0]     [0],
      
            [0]
      [0] = [0]
            [0]
     orientation:
      plus#(s(x),y) = [1 0 1]x + [0 1 0]y + [1] >= [1 0 1]x + [0 1 0]y = plus#(x,y)
      
      plus#(minus(x,s(0())),minus(y,s(s(z)))) = [1 1 1]x + [1 1 1]y + [1 0 0]z + [3] >= [1 1 1]x + [1 1 1]y + [2] = plus#(minus(y,s(s(z))),minus(x,s(0())))
      
                     [1 0 0]    [0]         
      minus(x,0()) = [1 1 1]x + [1] >= x = x
                     [0 1 1]    [0]         
      
                         [1 0 0]    [0 0 0]    [1]    [1 0 0]    [0 0 0]    [0]             
      minus(s(x),s(y)) = [1 1 1]x + [1 0 0]y + [3] >= [1 1 1]x + [1 0 0]y + [1] = minus(x,y)
                         [0 1 1]    [0 0 0]    [0]    [0 1 1]    [0 0 0]    [0]             
      
                       [0 0 1]    [1]    [0]      
      quot(0(),s(y)) = [0 1 0]y + [0] >= [0] = 0()
                       [0 0 0]    [0]    [0]      
      
                        [1 0 0]    [0 0 1]    [2]    [1 0 0]    [0 0 1]    [2]                           
      quot(s(x),s(y)) = [0 0 0]x + [0 1 0]y + [0] >= [0 0 0]x + [0 1 0]y + [0] = s(quot(minus(x,y),s(y)))
                        [0 0 0]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                           
      
                              
      plus(0(),y) = y >= y = y
                              
      
                             [1]            [1]               
      plus(s(x),y) = x + y + [0] >= x + y + [0] = s(plus(x,y))
                             [0]            [0]               
      
                                               [1 0 0]    [1 0 0]    [0 0 0]    [0]    [1 0 0]    [1 0 0]    [0 0 0]    [0]                                         
      plus(minus(x,s(0())),minus(y,s(s(z)))) = [1 1 1]x + [1 1 1]y + [1 0 0]z + [5] >= [1 1 1]x + [1 1 1]y + [1 0 0]z + [5] = plus(minus(y,s(s(z))),minus(x,s(0())))
                                               [0 1 1]    [0 1 1]    [0 0 0]    [0]    [0 1 1]    [0 1 1]    [0 0 0]    [0]                                         
     problem:
      DPs:
       
      TRS:
       minus(x,0()) -> x
       minus(s(x),s(y)) -> minus(x,y)
       quot(0(),s(y)) -> 0()
       quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
     Qed