YES
Time: 0.028065
TRS:
 {        minus(x, 0()) -> x,
  minus(minus(x, y), z) -> minus(x, plus(y, z)),
        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)}
 DP:
  DP:
   {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
    minus#(minus(x, y), z) -> plus#(y, z),
          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)}
  TRS:
  {        minus(x, 0()) -> x,
   minus(minus(x, y), z) -> minus(x, plus(y, z)),
         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)}
  UR:
   {        minus(x, 0()) -> x,
    minus(minus(x, y), z) -> minus(x, plus(y, z)),
          minus(s x, s y) -> minus(x, y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (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))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (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#(minus(x, y), z) -> plus#(y, z))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))}
    STATUS:
     arrows: 0.638889
     SCCS (3):
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {plus#(s x, y) -> plus#(x, y)}
      
      SCC (1):
       Strict:
        {quot#(s x, s y) -> quot#(minus(x, y), s y)}
       Weak:
       {        minus(x, 0()) -> x,
        minus(minus(x, y), z) -> minus(x, plus(y, z)),
              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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [minus](x0, x1) = x0,
         
         [quot](x0, x1) = x0 + 1,
         
         [plus](x0, x1) = 0,
         
         [s](x0) = x0 + 1,
         
         [0] = 0,
         
         [quot#](x0, x1) = x0 + 1
        Strict:
         quot#(s x, s y) -> quot#(minus(x, y), s y)
         2 + 1x + 0y >= 1 + 1x + 0y
        Weak:
         plus(s x, y) -> s plus(x, y)
         0 + 0x + 0y >= 1 + 0x + 0y
         plus(0(), y) -> y
         0 + 0y >= 1y
         quot(s x, s y) -> s quot(minus(x, y), s y)
         2 + 0x + 1y >= 3 + 0x + 1y
         quot(0(), s y) -> 0()
         2 + 1y >= 0
         minus(s x, s y) -> minus(x, y)
         1 + 1x + 0y >= 0 + 1x + 0y
         minus(minus(x, y), z) -> minus(x, plus(y, z))
         0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z
         minus(x, 0()) -> x
         0 + 1x >= 1x
       Qed
     
     SCC (2):
      Strict:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {        minus(x, 0()) -> x,
       minus(minus(x, y), z) -> minus(x, plus(y, z)),
             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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [minus](x0, x1) = x0 + x1 + 1,
        
        [quot](x0, x1) = x0 + 1,
        
        [plus](x0, x1) = 1,
        
        [s](x0) = x0,
        
        [0] = 1,
        
        [minus#](x0, x1) = x0
       Strict:
        minus#(s x, s y) -> minus#(x, y)
        0 + 1x + 0y >= 0 + 1x + 0y
        minus#(minus(x, y), z) -> minus#(x, plus(y, z))
        1 + 1x + 1y + 0z >= 0 + 1x + 0y + 0z
       Weak:
        plus(s x, y) -> s plus(x, y)
        1 + 0x + 0y >= 1 + 0x + 0y
        plus(0(), y) -> y
        1 + 0y >= 1y
        quot(s x, s y) -> s quot(minus(x, y), s y)
        1 + 1x + 0y >= 2 + 1x + 1y
        quot(0(), s y) -> 0()
        2 + 0y >= 1
        minus(s x, s y) -> minus(x, y)
        1 + 1x + 1y >= 1 + 1x + 1y
        minus(minus(x, y), z) -> minus(x, plus(y, z))
        2 + 1x + 1y + 1z >= 2 + 1x + 0y + 0z
        minus(x, 0()) -> x
        2 + 1x >= 1x
      SCCS (1):
       Scc:
        {minus#(s x, s y) -> minus#(x, y)}
       
       SCC (1):
        Strict:
         {minus#(s x, s y) -> minus#(x, y)}
        Weak:
        {        minus(x, 0()) -> x,
         minus(minus(x, y), z) -> minus(x, plus(y, z)),
               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)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [minus](x0, x1) = x0 + x1 + 1,
          
          [quot](x0, x1) = x0 + 1,
          
          [plus](x0, x1) = 1,
          
          [s](x0) = x0 + 1,
          
          [0] = 1,
          
          [minus#](x0, x1) = x0
         Strict:
          minus#(s x, s y) -> minus#(x, y)
          1 + 0x + 1y >= 0 + 0x + 1y
         Weak:
          plus(s x, y) -> s plus(x, y)
          1 + 0x + 0y >= 2 + 0x + 0y
          plus(0(), y) -> y
          1 + 0y >= 1y
          quot(s x, s y) -> s quot(minus(x, y), s y)
          2 + 0x + 1y >= 3 + 0x + 1y
          quot(0(), s y) -> 0()
          2 + 1y >= 1
          minus(s x, s y) -> minus(x, y)
          3 + 1x + 1y >= 1 + 1x + 1y
          minus(minus(x, y), z) -> minus(x, plus(y, z))
          2 + 1x + 1y + 1z >= 2 + 1x + 0y + 0z
          minus(x, 0()) -> x
          2 + 1x >= 1x
        Qed
    
    SCC (1):
     Strict:
      {plus#(s x, y) -> plus#(x, y)}
     Weak:
     {        minus(x, 0()) -> x,
      minus(minus(x, y), z) -> minus(x, plus(y, z)),
            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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [minus](x0, x1) = x0 + 1,
       
       [quot](x0, x1) = x0 + 1,
       
       [plus](x0, x1) = 1,
       
       [s](x0) = x0 + 1,
       
       [0] = 1,
       
       [plus#](x0, x1) = x0
      Strict:
       plus#(s x, y) -> plus#(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
      Weak:
       plus(s x, y) -> s plus(x, y)
       1 + 0x + 0y >= 2 + 0x + 0y
       plus(0(), y) -> y
       1 + 0y >= 1y
       quot(s x, s y) -> s quot(minus(x, y), s y)
       2 + 0x + 1y >= 3 + 0x + 1y
       quot(0(), s y) -> 0()
       2 + 1y >= 1
       minus(s x, s y) -> minus(x, y)
       2 + 0x + 1y >= 1 + 0x + 1y
       minus(minus(x, y), z) -> minus(x, plus(y, z))
       1 + 0x + 0y + 1z >= 2 + 0x + 0y + 0z
       minus(x, 0()) -> x
       2 + 0x >= 1x
     Qed