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
 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)))))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [if2#](x0, x1) = -1x0 + -7x1 + 0,
      
      [if#](x0, x1, x2) = -1x1 + -6x2 + 0,
      
      [weight#](x0) = -4x0 + 0,
      
      [if2](x0, x1) = x1 + 8,
      
      [weight_undefined_error] = 8,
      
      [if](x0, x1, x2) = x2 + 8,
      
      [weight](x0) = x0 + 8,
      
      [head](x0) = x0 + 3,
      
      [tail](x0) = -4x0 + 0,
      
      [false] = 2,
      
      [true] = 0,
      
      [empty](x0) = x0 + -10,
      
      [nil] = 0,
      
      [0] = 0,
      
      [sum](x0, x1) = x1 + 0,
      
      [cons](x0, x1) = 2x0 + 4x1 + 2,
      
      [s](x0) = 0
     orientation:
      if2#(false(),x) = -7x + 1 >= -8x + 0 = weight#(sum(x,cons(0(),tail(tail(x)))))
      
      weight#(x) = -4x + 0 >= -5x + 0 = if#(empty(x),empty(tail(x)),x)
      
      if#(false(),b,x) = -1b + -6x + 0 >= -1b + -7x + 0 = if2#(b,x)
      
      sum(cons(s(n),x),cons(m,y)) = 2m + 4y + 2 >= 4y + 2 = sum(cons(n,x),cons(s(m),y))
      
      sum(cons(0(),x),y) = y + 0 >= y + 0 = sum(x,y)
      
      sum(nil(),y) = y + 0 >= y = y
      
      empty(nil()) = 0 >= 0 = true()
      
      empty(cons(n,x)) = 2n + 4x + 2 >= 2 = false()
      
      tail(nil()) = 0 >= 0 = nil()
      
      tail(cons(n,x)) = -2n + x + 0 >= x = x
      
      head(cons(n,x)) = 2n + 4x + 3 >= n = n
      
      weight(x) = x + 8 >= x + 8 = if(empty(x),empty(tail(x)),x)
      
      if(true(),b,x) = x + 8 >= 8 = weight_undefined_error()
      
      if(false(),b,x) = x + 8 >= x + 8 = if2(b,x)
      
      if2(true(),x) = x + 8 >= x + 3 = head(x)
      
      if2(false(),x) = x + 8 >= -4x + 8 = weight(sum(x,cons(0(),tail(tail(x)))))
     problem:
      DPs:
       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)))))
     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)))))
    Matrix Interpretation Processor: dim=2
     
     interpretation:
      [sum#](x0, x1) = [0 1]x0,
      
                      [1 0]  
      [if2](x0, x1) = [1 0]x1,
      
                                 [0]
      [weight_undefined_error] = [0],
      
                         [2 0]     [1 0]  
      [if](x0, x1, x2) = [0 0]x1 + [1 0]x2,
      
                     [1 0]  
      [weight](x0) = [1 0]x0,
      
                   [1 0]  
      [head](x0) = [1 0]x0,
      
                   [0 1]     [1]
      [tail](x0) = [1 1]x0 + [0],
      
                [0]
      [false] = [0],
      
               [0]
      [true] = [3],
      
                    [0 0]     [0]
      [empty](x0) = [1 2]x0 + [1],
      
              [0]
      [nil] = [1],
      
            [0]
      [0] = [0],
      
                      [2 0]  
      [sum](x0, x1) = [0 1]x1,
      
                       [1 2]     [0 0]     [0]
      [cons](x0, x1) = [0 0]x0 + [1 3]x1 + [2],
      
                [0]
      [s](x0) = [0]
     orientation:
      sum#(cons(s(n),x),cons(m,y)) = [1 3]x + [2] >= [1 3]x + [2] = sum#(cons(n,x),cons(s(m),y))
      
      sum#(cons(0(),x),y) = [1 3]x + [2] >= [0 1]x = sum#(x,y)
      
                                    [2 4]    [0 0]    [0]    [0 0]    [0]                              
      sum(cons(s(n),x),cons(m,y)) = [0 0]m + [1 3]y + [2] >= [1 3]y + [2] = sum(cons(n,x),cons(s(m),y))
      
                           [2 0]     [2 0]            
      sum(cons(0(),x),y) = [0 1]y >= [0 1]y = sum(x,y)
      
                     [2 0]          
      sum(nil(),y) = [0 1]y >= y = y
      
                     [0]    [0]         
      empty(nil()) = [3] >= [3] = true()
      
                         [0 0]    [0 0]    [0]    [0]          
      empty(cons(n,x)) = [1 2]n + [2 6]x + [5] >= [0] = false()
      
                    [2]    [0]        
      tail(nil()) = [1] >= [1] = nil()
      
                        [0 0]    [1 3]    [3]         
      tail(cons(n,x)) = [1 2]n + [1 3]x + [2] >= x = x
      
                        [1 2]          
      head(cons(n,x)) = [1 2]n >= n = n
      
                  [1 0]     [1 0]                                 
      weight(x) = [1 0]x >= [1 0]x = if(empty(x),empty(tail(x)),x)
      
                       [2 0]    [1 0]     [0]                           
      if(true(),b,x) = [0 0]b + [1 0]x >= [0] = weight_undefined_error()
      
                        [2 0]    [1 0]     [1 0]            
      if(false(),b,x) = [0 0]b + [1 0]x >= [1 0]x = if2(b,x)
      
                      [1 0]     [1 0]           
      if2(true(),x) = [1 0]x >= [1 0]x = head(x)
      
                       [1 0]     [0]                                         
      if2(false(),x) = [1 0]x >= [0] = weight(sum(x,cons(0(),tail(tail(x)))))
     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)))))
     Open