YES

Problem:
 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
 empty(nil()) -> true()
 empty(cons(n,x)) -> false()
 tail(nil()) -> nil()
 tail(cons(n,x)) -> x
 head(cons(n,x)) -> n
 weight(x) -> if(empty(x),empty(tail(x)),x)
 if(true(),b,x) -> weight_undefined_error()
 if(false(),b,x) -> if2(b,x)
 if2(true(),x) -> head(x)
 if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))

Proof:
 DP Processor:
  DPs:
   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#(x) -> tail#(x)
   weight#(x) -> empty#(tail(x))
   weight#(x) -> empty#(x)
   weight#(x) -> if#(empty(x),empty(tail(x)),x)
   if#(false(),b,x) -> if2#(b,x)
   if2#(true(),x) -> head#(x)
   if2#(false(),x) -> tail#(x)
   if2#(false(),x) -> tail#(tail(x))
   if2#(false(),x) -> sum#(x,cons(0(),tail(tail(x))))
   if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(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
   empty(nil()) -> true()
   empty(cons(n,x)) -> false()
   tail(nil()) -> nil()
   tail(cons(n,x)) -> x
   head(cons(n,x)) -> n
   weight(x) -> if(empty(x),empty(tail(x)),x)
   if(true(),b,x) -> weight_undefined_error()
   if(false(),b,x) -> if2(b,x)
   if2(true(),x) -> head(x)
   if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
  TDG Processor:
   DPs:
    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#(x) -> tail#(x)
    weight#(x) -> empty#(tail(x))
    weight#(x) -> empty#(x)
    weight#(x) -> if#(empty(x),empty(tail(x)),x)
    if#(false(),b,x) -> if2#(b,x)
    if2#(true(),x) -> head#(x)
    if2#(false(),x) -> tail#(x)
    if2#(false(),x) -> tail#(tail(x))
    if2#(false(),x) -> sum#(x,cons(0(),tail(tail(x))))
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(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
    empty(nil()) -> true()
    empty(cons(n,x)) -> false()
    tail(nil()) -> nil()
    tail(cons(n,x)) -> x
    head(cons(n,x)) -> n
    weight(x) -> if(empty(x),empty(tail(x)),x)
    if(true(),b,x) -> weight_undefined_error()
    if(false(),b,x) -> if2(b,x)
    if2(true(),x) -> head(x)
    if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
   graph:
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x))))) ->
    weight#(x) -> if#(empty(x),empty(tail(x)),x)
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x))))) ->
    weight#(x) -> empty#(x)
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x))))) ->
    weight#(x) -> empty#(tail(x))
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x))))) ->
    weight#(x) -> tail#(x)
    if2#(false(),x) -> sum#(x,cons(0(),tail(tail(x)))) ->
    sum#(cons(0(),x),y) -> sum#(x,y)
    if2#(false(),x) -> sum#(x,cons(0(),tail(tail(x)))) ->
    sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
    if#(false(),b,x) -> if2#(b,x) ->
    if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x)))))
    if#(false(),b,x) -> if2#(b,x) ->
    if2#(false(),x) -> sum#(x,cons(0(),tail(tail(x))))
    if#(false(),b,x) -> if2#(b,x) -> if2#(false(),x) -> tail#(tail(x))
    if#(false(),b,x) -> if2#(b,x) -> if2#(false(),x) -> tail#(x)
    if#(false(),b,x) -> if2#(b,x) ->
    if2#(true(),x) -> head#(x)
    weight#(x) -> if#(empty(x),empty(tail(x)),x) ->
    if#(false(),b,x) -> if2#(b,x)
    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))
    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))
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 16/144
    DPs:
     if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x)))))
     weight#(x) -> if#(empty(x),empty(tail(x)),x)
     if#(false(),b,x) -> if2#(b,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
     empty(nil()) -> true()
     empty(cons(n,x)) -> false()
     tail(nil()) -> nil()
     tail(cons(n,x)) -> x
     head(cons(n,x)) -> n
     weight(x) -> if(empty(x),empty(tail(x)),x)
     if(true(),b,x) -> weight_undefined_error()
     if(false(),b,x) -> if2(b,x)
     if2(true(),x) -> head(x)
     if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
    Usable Rule Processor:
     DPs:
      if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(x)))))
      weight#(x) -> if#(empty(x),empty(tail(x)),x)
      if#(false(),b,x) -> if2#(b,x)
     TRS:
      tail(nil()) -> nil()
      tail(cons(n,x)) -> x
      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
      empty(nil()) -> true()
      empty(cons(n,x)) -> false()
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       tail(nil()) -> nil()
       tail(cons(n,x)) -> x
       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
       empty(nil()) -> true()
       empty(cons(n,x)) -> false()
      interpretation:
       [if2#](x0, x1) = -3x0 + -4x1 + 0,
       
       [if#](x0, x1, x2) = x1 + -4x2 + 0,
       
       [weight#](x0) = -4x0 + 0,
       
       [tail](x0) = -4x0 + 0,
       
       [false] = 5,
       
       [true] = 0,
       
       [empty](x0) = x0,
       
       [nil] = 0,
       
       [0] = 1,
       
       [sum](x0, x1) = -2x0 + x1 + 0,
       
       [cons](x0, x1) = 4x0 + 5x1 + 5,
       
       [s](x0) = x0
      orientation:
       if2#(false(),x) = -4x + 2 >= -6x + 1 = weight#(sum(x,cons(0(),tail(tail(x)))))
       
       weight#(x) = -4x + 0 >= -4x + 0 = if#(empty(x),empty(tail(x)),x)
       
       if#(false(),b,x) = b + -4x + 0 >= -3b + -4x + 0 = if2#(b,x)
       
       tail(nil()) = 0 >= 0 = nil()
       
       tail(cons(n,x)) = n + 1x + 1 >= x = x
       
       sum(cons(s(n),x),cons(m,y)) = 4m + 2n + 3x + 5y + 5 >= 4m + 2n + 3x + 5y + 5 = sum(cons(n,x),cons(s(m),y))
       
       sum(cons(0(),x),y) = 3x + y + 3 >= -2x + y + 0 = sum(x,y)
       
       sum(nil(),y) = y + 0 >= y = y
       
       empty(nil()) = 0 >= 0 = true()
       
       empty(cons(n,x)) = 4n + 5x + 5 >= 5 = false()
      problem:
       DPs:
        weight#(x) -> if#(empty(x),empty(tail(x)),x)
        if#(false(),b,x) -> if2#(b,x)
       TRS:
        tail(nil()) -> nil()
        tail(cons(n,x)) -> x
        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
        empty(nil()) -> true()
        empty(cons(n,x)) -> false()
      Restore Modifier:
       DPs:
        weight#(x) -> if#(empty(x),empty(tail(x)),x)
        if#(false(),b,x) -> if2#(b,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
        empty(nil()) -> true()
        empty(cons(n,x)) -> false()
        tail(nil()) -> nil()
        tail(cons(n,x)) -> x
        head(cons(n,x)) -> n
        weight(x) -> if(empty(x),empty(tail(x)),x)
        if(true(),b,x) -> weight_undefined_error()
        if(false(),b,x) -> if2(b,x)
        if2(true(),x) -> head(x)
        if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 3/4
        
    
    DPs:
     sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
     sum#(cons(0(),x),y) -> sum#(x,y)
    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
     empty(nil()) -> true()
     empty(cons(n,x)) -> false()
     tail(nil()) -> nil()
     tail(cons(n,x)) -> x
     head(cons(n,x)) -> n
     weight(x) -> if(empty(x),empty(tail(x)),x)
     if(true(),b,x) -> weight_undefined_error()
     if(false(),b,x) -> if2(b,x)
     if2(true(),x) -> head(x)
     if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
    Usable Rule Processor:
     DPs:
      sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
      sum#(cons(0(),x),y) -> sum#(x,y)
     TRS:
      
     Semantic Labeling Processor:
      dimension: 1
      usable rules:
       
      interpretation:
       [0] = 0,
       
       [cons](x0, x1) = x1,
       
       [s](x0) = x0
       labeled:
        s
       usable (for model):
        s
       argument filtering:
        pi(s) = []
        pi(cons) = [1]
        pi(0) = []
        pi(sum#) = 0
      precedence:
       sum# ~ 0 ~ cons ~ s
      problem:
       DPs:
        sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
       TRS:
        
      Restore Modifier:
       DPs:
        sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
       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
        empty(nil()) -> true()
        empty(cons(n,x)) -> false()
        tail(nil()) -> nil()
        tail(cons(n,x)) -> x
        head(cons(n,x)) -> n
        weight(x) -> if(empty(x),empty(tail(x)),x)
        if(true(),b,x) -> weight_undefined_error()
        if(false(),b,x) -> if2(b,x)
        if2(true(),x) -> head(x)
        if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
       Usable Rule Processor:
        DPs:
         sum#(cons(s(n),x),cons(m,y)) -> sum#(cons(n,x),cons(s(m),y))
        TRS:
         
        Semantic Labeling Processor:
         dimension: 1
         usable rules:
          
         interpretation:
          [cons](x0, x1) = x0 + x1 + 1,
          
          [s](x0) = 1
          labeled:
           cons
          usable (for model):
           cons
           s
          argument filtering:
           pi(s) = [0]
           pi(cons) = 0
           pi(sum#) = 0
         precedence:
          sum# ~ cons ~ s
         problem:
          DPs:
           
          TRS:
           
         Qed