MAYBE
Time: 0.005638
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))}
    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))}
     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))}
      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))}
          Open
         
         
         
         
         
         
         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))}
          Open