YES
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:
  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),
       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)))}
  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}
  EDG:
   {(sum#(cons(0(), x), y) -> sum#(x, y), 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)))
    (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(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)))
    (sum#(cons(s(n), x), cons(m, y)) -> sum#(cons(n, x), cons(s(m), y)), sum#(cons(0(), x), y) -> sum#(x, y))}
   SCCS:
    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:
     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:
      Argument Filtering:
       pi(weight#) = 0, pi(weight) = [], pi(nil) = [], pi(0) = [], pi(s) = [], pi(cons) = [1], pi(sum) = 1
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {}
      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}
      Qed
    SCC:
     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:
      Argument Filtering:
       pi(weight) = [], pi(nil) = [], pi(0) = [], pi(s) = 0, pi(cons) = [0,1], pi(sum#) = 0, pi(sum) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0, x1) = x0 + x1,
       [0] = 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}
      EDG:
       {(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)))}
       SCCS:
        Scc:
         {sum#(cons(s(n), x), cons(m, y)) -> sum#(cons(n, x), cons(s(m), y))}
        SCC:
         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:
          Argument Filtering:
           pi(weight) = [], pi(nil) = [], pi(0) = [], pi(s) = [0], pi(cons) = 0, pi(sum#) = 0, pi(sum) = []
          Usable Rules:
           {}
          Interpretation:
           [s](x0) = x0 + 1
          Strict:
           {}
          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}
          Qed