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)))))
  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#(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:
    f21(x,y) -> x
    f21(x,y) -> y
    tail(nil()) -> nil()
    tail(cons(n,x)) -> x
    empty(nil()) -> true()
    empty(cons(n,x)) -> false()
    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#(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:
     f21(x,y) -> x
     f21(x,y) -> y
     tail(nil()) -> nil()
     tail(cons(n,x)) -> x
     empty(nil()) -> true()
     empty(cons(n,x)) -> false()
     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:
     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))
    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#(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)))))
     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)))))
      Open
      
      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)))))
      Open