YES
Time: 0.232551
TRS:
 {       plus(0(), Y) -> Y,
         plus(s X, Y) -> s plus(X, Y),
          min(X, 0()) -> X,
        min(s X, s Y) -> min(X, Y),
  min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
       quot(0(), s Y) -> 0(),
       quot(s X, s Y) -> s quot(min(X, Y), s Y)}
 DP:
  DP:
   {       plus#(s X, Y) -> plus#(X, Y),
          min#(s X, s Y) -> min#(X, Y),
    min#(min(X, Y), Z()) -> plus#(Y, Z()),
    min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())),
         quot#(s X, s Y) -> min#(X, Y),
         quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
  TRS:
  {       plus(0(), Y) -> Y,
          plus(s X, Y) -> s plus(X, Y),
           min(X, 0()) -> X,
         min(s X, s Y) -> min(X, Y),
   min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
        quot(0(), s Y) -> 0(),
        quot(s X, s Y) -> s quot(min(X, Y), s Y)}
  EDG:
   {(min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y))
    (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> quot#(min(X, Y), s Y))
    (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> min#(X, Y))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(s X, s Y) -> min#(X, Y))
    (min#(min(X, Y), Z()) -> plus#(Y, Z()), plus#(s X, Y) -> plus#(X, Y))
    (quot#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y))
    (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (plus#(s X, Y) -> plus#(X, Y), plus#(s X, Y) -> plus#(X, Y))}
   STATUS:
    arrows: 0.638889
    SCCS (3):
     Scc:
      {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
     Scc:
      {      min#(s X, s Y) -> min#(X, Y),
       min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
     Scc:
      {plus#(s X, Y) -> plus#(X, Y)}
     
     SCC (1):
      Strict:
       {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
      Weak:
      {       plus(0(), Y) -> Y,
              plus(s X, Y) -> s plus(X, Y),
               min(X, 0()) -> X,
             min(s X, s Y) -> min(X, Y),
       min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
            quot(0(), s Y) -> 0(),
            quot(s X, s Y) -> s quot(min(X, Y), s Y)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [plus](x0, x1) = 0,
        
        [min](x0, x1) = x0,
        
        [quot](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [Z] = 0,
        
        [quot#](x0, x1) = x0 + 1
       Strict:
        quot#(s X, s Y) -> quot#(min(X, Y), s Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
       Weak:
        quot(s X, s Y) -> s quot(min(X, Y), s Y)
        2 + 1Y + 0X >= 3 + 1Y + 0X
        quot(0(), s Y) -> 0()
        2 + 1Y >= 0
        min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
        0 + 0Y + 1X >= 0 + 0Y + 1X
        min(s X, s Y) -> min(X, Y)
        1 + 0Y + 1X >= 0 + 0Y + 1X
        min(X, 0()) -> X
        0 + 1X >= 1X
        plus(s X, Y) -> s plus(X, Y)
        0 + 0Y + 0X >= 1 + 0Y + 0X
        plus(0(), Y) -> Y
        0 + 0Y >= 1Y
      Qed
    
    SCC (2):
     Strict:
      {      min#(s X, s Y) -> min#(X, Y),
       min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
     Weak:
     {       plus(0(), Y) -> Y,
             plus(s X, Y) -> s plus(X, Y),
              min(X, 0()) -> X,
            min(s X, s Y) -> min(X, Y),
      min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
           quot(0(), s Y) -> 0(),
           quot(s X, s Y) -> s quot(min(X, Y), s Y)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [plus](x0, x1) = 0,
       
       [min](x0, x1) = x0 + x1 + 1,
       
       [quot](x0, x1) = 0,
       
       [s](x0) = x0,
       
       [0] = 1,
       
       [Z] = 0,
       
       [min#](x0, x1) = x0
      Strict:
       min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))
       1 + 1Y + 1X >= 0 + 0Y + 1X
       min#(s X, s Y) -> min#(X, Y)
       0 + 0Y + 1X >= 0 + 0Y + 1X
      Weak:
       quot(s X, s Y) -> s quot(min(X, Y), s Y)
       0 + 0Y + 0X >= 0 + 0Y + 0X
       quot(0(), s Y) -> 0()
       0 + 0Y >= 1
       min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
       2 + 1Y + 1X >= 1 + 0Y + 1X
       min(s X, s Y) -> min(X, Y)
       1 + 1Y + 1X >= 1 + 1Y + 1X
       min(X, 0()) -> X
       2 + 1X >= 1X
       plus(s X, Y) -> s plus(X, Y)
       0 + 0Y + 0X >= 0 + 0Y + 0X
       plus(0(), Y) -> Y
       0 + 0Y >= 1Y
     SCCS (1):
      Scc:
       {min#(s X, s Y) -> min#(X, Y)}
      
      SCC (1):
       Strict:
        {min#(s X, s Y) -> min#(X, Y)}
       Weak:
       {       plus(0(), Y) -> Y,
               plus(s X, Y) -> s plus(X, Y),
                min(X, 0()) -> X,
              min(s X, s Y) -> min(X, Y),
        min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
             quot(0(), s Y) -> 0(),
             quot(s X, s Y) -> s quot(min(X, Y), s Y)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [plus](x0, x1) = x0 + 1,
         
         [min](x0, x1) = x0 + 1,
         
         [quot](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [Z] = 1,
         
         [min#](x0, x1) = x0 + 1
        Strict:
         min#(s X, s Y) -> min#(X, Y)
         2 + 0Y + 1X >= 1 + 0Y + 1X
        Weak:
         quot(s X, s Y) -> s quot(min(X, Y), s Y)
         2 + 1Y + 0X >= 3 + 1Y + 0X
         quot(0(), s Y) -> 0()
         2 + 1Y >= 1
         min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
         2 + 0Y + 0X >= 2 + 1Y + 0X
         min(s X, s Y) -> min(X, Y)
         2 + 1Y + 0X >= 1 + 1Y + 0X
         min(X, 0()) -> X
         2 + 0X >= 1X
         plus(s X, Y) -> s plus(X, Y)
         2 + 0Y + 1X >= 2 + 0Y + 1X
         plus(0(), Y) -> Y
         2 + 0Y >= 1Y
       Qed
   
   SCC (1):
    Strict:
     {plus#(s X, Y) -> plus#(X, Y)}
    Weak:
    {       plus(0(), Y) -> Y,
            plus(s X, Y) -> s plus(X, Y),
             min(X, 0()) -> X,
           min(s X, s Y) -> min(X, Y),
     min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
          quot(0(), s Y) -> 0(),
          quot(s X, s Y) -> s quot(min(X, Y), s Y)}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [plus](x0, x1) = x0 + 1,
      
      [min](x0, x1) = 0,
      
      [quot](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [0] = 1,
      
      [Z] = 0,
      
      [plus#](x0, x1) = x0
     Strict:
      plus#(s X, Y) -> plus#(X, Y)
      1 + 0Y + 1X >= 0 + 0Y + 1X
     Weak:
      quot(s X, s Y) -> s quot(min(X, Y), s Y)
      2 + 1Y + 0X >= 3 + 1Y + 0X
      quot(0(), s Y) -> 0()
      2 + 1Y >= 1
      min(min(X, Y), Z()) -> min(X, plus(Y, Z()))
      0 + 0Y + 0X >= 0 + 0Y + 0X
      min(s X, s Y) -> min(X, Y)
      0 + 0Y + 0X >= 0 + 0Y + 0X
      min(X, 0()) -> X
      0 + 0X >= 1X
      plus(s X, Y) -> s plus(X, Y)
      2 + 0Y + 1X >= 2 + 0Y + 1X
      plus(0(), Y) -> Y
      2 + 0Y >= 1Y
    Qed