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