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) = x0 + -3x1 + -16,
       
       [if#](x0, x1, x2) = x1 + -2x2 + -16,
       
       [weight#](x0) = x0 + 2,
       
       [tail](x0) = -3x0 + 0,
       
       [false] = 4,
       
       [true] = 1,
       
       [empty](x0) = 1x0 + 0,
       
       [nil] = 0,
       
       [0] = 3,
       
       [sum](x0, x1) = -8x0 + x1 + -16,
       
       [cons](x0, x1) = x0 + 3x1 + 3,
       
       [s](x0) = x0
      orientation:
       if2#(false(),x) = -3x + 4 >= -3x + 3 = weight#(sum(x,cons(0(),tail(tail(x)))))
       
       weight#(x) = x + 2 >= -2x + 1 = if#(empty(x),empty(tail(x)),x)
       
       if#(false(),b,x) = b + -2x + -16 >= b + -3x + -16 = if2#(b,x)
       
       tail(nil()) = 0 >= 0 = nil()
       
       tail(cons(n,x)) = -3n + x + 0 >= x = x
       
       sum(cons(s(n),x),cons(m,y)) = m + -8n + -5x + 3y + 3 >= m + -8n + -5x + 3y + 3 = sum(cons(n,x),cons(s(m),y))
       
       sum(cons(0(),x),y) = -5x + y + -5 >= -8x + y + -16 = sum(x,y)
       
       sum(nil(),y) = y + -8 >= y = y
       
       empty(nil()) = 1 >= 1 = true()
       
       empty(cons(n,x)) = 1n + 4x + 4 >= 4 = false()
      problem:
       DPs:
        if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(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:
        if2#(false(),x) -> weight#(sum(x,cons(0(),tail(tail(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)))))
    Subterm Criterion Processor:
     simple projection:
      pi(cons) = [1,1]
      pi(sum#) = [0,0]
     problem:
      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)))))
     Subterm Criterion Processor:
      simple projection:
       pi(cons) = 0
       pi(sum#) = 0
      problem:
       DPs:
        
       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)))))
      Qed