MAYBE
Time: 1.227242
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 cons(n, x) -> false(),
                    empty nil() -> true(),
                tail cons(n, x) -> x,
                     tail nil() -> nil(),
                head cons(n, x) -> n,
               if(true(), b, x) -> weight_undefined_error(),
              if(false(), b, x) -> if2(b, x),
                       weight x -> if(empty x, empty tail x, x),
                 if2(true(), x) -> head x,
                if2(false(), x) -> weight sum(x, cons(0(), tail tail x))}
 DP:
  DP:
   {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
             sum#(cons(0(), x), y) -> sum#(x, y),
                if#(false(), b, x) -> if2#(b, x),
                         weight# x -> empty# x,
                         weight# x -> empty# tail x,
                         weight# x -> tail# x,
                         weight# x -> if#(empty x, empty tail x, x),
                   if2#(true(), x) -> head# x,
                  if2#(false(), x) -> sum#(x, cons(0(), tail tail x)),
                  if2#(false(), x) -> tail# x,
                  if2#(false(), x) -> 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 cons(n, x) -> false(),
                     empty nil() -> true(),
                 tail cons(n, x) -> x,
                      tail nil() -> nil(),
                 head cons(n, x) -> n,
                if(true(), b, x) -> weight_undefined_error(),
               if(false(), b, x) -> if2(b, x),
                        weight x -> if(empty x, empty tail x, x),
                  if2(true(), x) -> head x,
                 if2(false(), x) -> weight sum(x, cons(0(), tail tail x))}
  UR:
   {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 cons(n, x) -> false(),
                      empty nil() -> true(),
                  tail cons(n, x) -> x,
                       tail nil() -> nil(),
                          a(z, w) -> z,
                          a(z, w) -> w}
   EDG:
    {(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 -> tail# 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 -> empty# 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(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)))
     (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#(true(), x) -> head# 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# x)
     (if#(false(), b, x) -> if2#(b, x), if2#(false(), x) -> tail# tail x)
     (if#(false(), b, x) -> if2#(b, x), if2#(false(), x) -> weight# sum(x, cons(0(), tail tail x)))
     (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))
     (weight# x -> if#(empty x, empty tail x, x), if#(false(), b, x) -> if2#(b, x))}
    STATUS:
     arrows: 0.888889
     SCCS (2):
      Scc:
       {if#(false(), b, x) -> if2#(b, x),
                 weight# x -> if#(empty x, empty tail x, x),
          if2#(false(), x) -> weight# sum(x, cons(0(), tail tail x))}
      Scc:
       {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 (3):
       Strict:
        {if#(false(), b, x) -> if2#(b, x),
                  weight# x -> if#(empty x, empty tail x, x),
           if2#(false(), x) -> weight# sum(x, cons(0(), tail tail x))}
       Weak:
       {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 cons(n, x) -> false(),
                          empty nil() -> true(),
                      tail cons(n, x) -> x,
                           tail nil() -> nil(),
                      head cons(n, x) -> n,
                     if(true(), b, x) -> weight_undefined_error(),
                    if(false(), b, x) -> if2(b, x),
                             weight x -> if(empty x, empty tail x, x),
                       if2(true(), x) -> head x,
                      if2(false(), x) -> weight sum(x, cons(0(), tail tail x))}
       Fail
      
      
      
      
      
      
      SCC (2):
       Strict:
        {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y)),
                  sum#(cons(0(), x), y) -> sum#(x, y)}
       Weak:
       {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 cons(n, x) -> false(),
                          empty nil() -> true(),
                      tail cons(n, x) -> x,
                           tail nil() -> nil(),
                      head cons(n, x) -> n,
                     if(true(), b, x) -> weight_undefined_error(),
                    if(false(), b, x) -> if2(b, x),
                             weight x -> if(empty x, empty tail x, x),
                       if2(true(), x) -> head x,
                      if2(false(), x) -> weight sum(x, cons(0(), tail tail x))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1 + 1,
         
         [sum](x0, x1) = 0,
         
         [cons](x0, x1) = x0 + 1,
         
         [if2](x0, x1) = x0 + 1,
         
         [s](x0) = 0,
         
         [empty](x0) = x0 + 1,
         
         [tail](x0) = x0 + 1,
         
         [head](x0) = x0 + 1,
         
         [weight](x0) = 0,
         
         [0] = 0,
         
         [nil] = 1,
         
         [true] = 1,
         
         [false] = 1,
         
         [weight_undefined_error] = 0,
         
         [sum#](x0, x1) = x0
        Strict:
         sum#(cons(0(), x), y) -> sum#(x, y)
         1 + 1x + 0y >= 0 + 1x + 0y
         sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))
         1 + 0n + 1x + 0m + 0y >= 1 + 0n + 1x + 0m + 0y
        Weak:
         if2(false(), x) -> weight sum(x, cons(0(), tail tail x))
         2 + 0x >= 0 + 0x
         if2(true(), x) -> head x
         2 + 0x >= 1 + 1x
         weight x -> if(empty x, empty tail x, x)
         0 + 0x >= 4 + 2x
         if(false(), b, x) -> if2(b, x)
         2 + 0x + 1b >= 1 + 0x + 1b
         if(true(), b, x) -> weight_undefined_error()
         2 + 0x + 1b >= 0
         head cons(n, x) -> n
         2 + 0n + 1x >= 1n
         tail nil() -> nil()
         2 >= 1
         tail cons(n, x) -> x
         2 + 0n + 1x >= 1x
         empty nil() -> true()
         2 >= 1
         empty cons(n, x) -> false()
         2 + 0n + 1x >= 1
         sum(nil(), y) -> y
         0 + 0y >= 1y
         sum(cons(0(), x), y) -> sum(x, y)
         0 + 0x + 0y >= 0 + 0x + 0y
         sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y))
         0 + 0n + 0x + 0m + 0y >= 0 + 0n + 0x + 0m + 0y
       SCCS (1):
        Scc:
         {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))}
        
        SCC (1):
         Strict:
          {sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))}
         Weak:
         {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 cons(n, x) -> false(),
                            empty nil() -> true(),
                        tail cons(n, x) -> x,
                             tail nil() -> nil(),
                        head cons(n, x) -> n,
                       if(true(), b, x) -> weight_undefined_error(),
                      if(false(), b, x) -> if2(b, x),
                               weight x -> if(empty x, empty tail x, x),
                         if2(true(), x) -> head x,
                        if2(false(), x) -> weight sum(x, cons(0(), tail tail x))}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [if](x0, x1, x2) = x0 + 1,
           
           [sum](x0, x1) = x0 + 1,
           
           [cons](x0, x1) = x0,
           
           [if2](x0, x1) = x0 + 1,
           
           [s](x0) = x0 + 1,
           
           [empty](x0) = 0,
           
           [tail](x0) = 0,
           
           [head](x0) = 0,
           
           [weight](x0) = 0,
           
           [0] = 1,
           
           [nil] = 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [weight_undefined_error] = 0,
           
           [sum#](x0, x1) = x0
          Strict:
           sum#(cons(s n, x), cons(m, y)) -> sum#(cons(n, x), cons(s m, y))
           1 + 1n + 0x + 0m + 0y >= 0 + 1n + 0x + 0m + 0y
          Weak:
           if2(false(), x) -> weight sum(x, cons(0(), tail tail x))
           2 + 0x >= 0 + 0x
           if2(true(), x) -> head x
           2 + 0x >= 0 + 0x
           weight x -> if(empty x, empty tail x, x)
           0 + 0x >= 1 + 0x
           if(false(), b, x) -> if2(b, x)
           2 + 0x + 0b >= 1 + 0x + 1b
           if(true(), b, x) -> weight_undefined_error()
           2 + 0x + 0b >= 0
           head cons(n, x) -> n
           0 + 0n + 0x >= 1n
           tail nil() -> nil()
           0 >= 1
           tail cons(n, x) -> x
           0 + 0n + 0x >= 1x
           empty nil() -> true()
           0 >= 1
           empty cons(n, x) -> false()
           0 + 0n + 0x >= 1
           sum(nil(), y) -> y
           2 + 0y >= 1y
           sum(cons(0(), x), y) -> sum(x, y)
           2 + 0x + 0y >= 1 + 1x + 0y
           sum(cons(s n, x), cons(m, y)) -> sum(cons(n, x), cons(s m, y))
           2 + 1n + 0x + 0m + 0y >= 1 + 1n + 0x + 0m + 0y
         Qed