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
  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)
    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
   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
    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
     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)
     Restore Modifier:
      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
      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
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [sum#](x0, x1) = x0,
         
         [weight](x0) = x0,
         
         [nil] = 0,
         
         [0] = 1,
         
         [sum](x0, x1) = x1,
         
         [cons](x0, x1) = x0 + x1 + 1,
         
         [s](x0) = x0
        orientation:
         sum#(cons(0(),x),y) = x + 2 >= x = sum#(x,y)
         
         sum#(cons(s(n),x),cons(m,y)) = n + x + 1 >= n + x + 1 = sum#(cons(n,x),cons(s(m),y))
         
         sum(cons(s(n),x),cons(m,y)) = m + y + 1 >= m + y + 1 = sum(cons(n,x),cons(s(m),y))
         
         sum(cons(0(),x),y) = y >= y = sum(x,y)
         
         sum(nil(),y) = y >= y = y
         
         weight(cons(n,cons(m,x))) = m + n + x + 2 >= x + 2 = weight(sum(cons(n,cons(m,x)),cons(0(),x)))
         
         weight(cons(n,nil())) = n + 1 >= n = n
        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
          weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x)))
          weight(cons(n,nil())) -> n
        Open