YES
Time: 0.033700
TRS:
 {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
           sum(cons(0(), x), y) -> sum(x, y),
                  sum(nil(), y) -> y,
     weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
          weight cons(n, nil()) -> n}
 DP:
  DP:
   {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
             sum#(cons(0(), x), y) -> sum#(x, y),
       weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)),
       weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
  TRS:
  {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
            sum(cons(0(), x), y) -> sum(x, y),
                   sum(nil(), y) -> y,
      weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
           weight cons(n, nil()) -> n}
  EDG:
   {(sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(0(), x), y) -> sum#(x, y))
    (sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
    (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)))
    (weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x)), weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)))
    (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
    (weight# cons(n, cons(m, x)) -> sum#(cons(n, cons(m, x)), cons(0(), x)), sum#(cons(0(), x), y) -> sum#(x, y))
    (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)))
    (sum#(cons(0(), x), y) -> sum#(x, y), sum#(cons(0(), x), y) -> sum#(x, y))}
   STATUS:
    arrows: 0.500000
    SCCS (2):
     Scc:
      {weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
     Scc:
      {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
                sum#(cons(0(), x), y) -> sum#(x, y)}
     
     SCC (1):
      Strict:
       {weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))}
      Weak:
      {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
                sum(cons(0(), x), y) -> sum(x, y),
                       sum(nil(), y) -> y,
          weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
               weight cons(n, nil()) -> n}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [sum](x0, x1) = x0,
        
        [cons](x0, x1) = x0 + 1,
        
        [s](x0) = 0,
        
        [weight](x0) = x0,
        
        [0] = 0,
        
        [nil] = 0,
        
        [weight#](x0) = x0
       Strict:
        weight# cons(n, cons(m, x)) -> weight# sum(cons(n, cons(m, x)), cons(0(), x))
        2 + 0n + 1x + 0m >= 1 + 0n + 1x + 0m
       Weak:
        weight cons(n, nil()) -> n
        1 + 0n >= 1n
        weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x))
        2 + 0n + 1x + 0m >= 1 + 0n + 1x + 0m
        sum(nil(), y) -> y
        0 + 1y >= 1y
        sum(cons(0(), x), y) -> sum(x, y)
        0 + 0x + 1y >= 0 + 0x + 1y
        sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y))
        1 + 0n + 0x + 0m + 1y >= 1 + 0n + 0x + 0m + 1y
      Qed
    
    SCC (2):
     Strict:
      {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
                sum#(cons(0(), x), y) -> sum#(x, y)}
     Weak:
     {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
               sum(cons(0(), x), y) -> sum(x, y),
                      sum(nil(), y) -> y,
         weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
              weight cons(n, nil()) -> n}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [sum](x0, x1) = 0,
       
       [cons](x0, x1) = x0 + x1,
       
       [s](x0) = x0,
       
       [weight](x0) = 0,
       
       [0] = 1,
       
       [nil] = 0,
       
       [sum#](x0, x1) = x0
      Strict:
       sum#(cons(0(), x), y) -> sum#(x, y)
       1 + 1x + 0y >= 0 + 1x + 0y
       sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))
       0 + 1n + 1x + 0m + 0y >= 0 + 1n + 1x + 0m + 0y
      Weak:
       weight cons(n, nil()) -> n
       0 + 0n >= 1n
       weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x))
       0 + 0n + 0x + 0m >= 0 + 0n + 0x + 0m
       sum(nil(), y) -> y
       0 + 0y >= 1y
       sum(cons(0(), x), y) -> sum(x, y)
       0 + 0x + 0y >= 0 + 0x + 0y
       sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y))
       0 + 0n + 0x + 0m + 0y >= 0 + 0n + 0x + 0m + 0y
     SCCS (1):
      Scc:
       {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))}
      
      SCC (1):
       Strict:
        {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))}
       Weak:
       {sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y)),
                 sum(cons(0(), x), y) -> sum(x, y),
                        sum(nil(), y) -> y,
           weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x)),
                weight cons(n, nil()) -> n}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [sum](x0, x1) = x0 + 1,
         
         [cons](x0, x1) = x0,
         
         [s](x0) = x0 + 1,
         
         [weight](x0) = 0,
         
         [0] = 0,
         
         [nil] = 1,
         
         [sum#](x0, x1) = x0
        Strict:
         sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))
         1 + 1n + 0x + 0m + 0y >= 0 + 1n + 0x + 0m + 0y
        Weak:
         weight cons(n, nil()) -> n
         0 + 0n >= 1n
         weight cons(n, cons(m, x)) -> weight sum(cons(n, cons(m, x)), cons(0(), x))
         0 + 0n + 0x + 0m >= 0 + 0n + 0x + 0m
         sum(nil(), y) -> y
         2 + 0y >= 1y
         sum(cons(0(), x), y) -> sum(x, y)
         1 + 0x + 0y >= 1 + 1x + 0y
         sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y))
         2 + 1n + 0x + 0m + 0y >= 1 + 1n + 0x + 0m + 0y
       Qed