MAYBE

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
 weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x)))
 weight(cons(n,nil())) -> n

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#(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
  ADG 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#(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
   graph:
    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))) -> 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)) ->
    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)
    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)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 8/16
    DPs:
     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
    Open
    
    DPs:
     sum#(cons(0(),x),y) -> sum#(x,y)
     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
     weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x)))
     weight(cons(n,nil())) -> n
    Open