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
  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#(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))) -> 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(0(),x),y) -> sum#(x,y)
    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))
    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))
   EDG 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))) -> 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: 1
     #rules: 2
     #arcs: 6/16
     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