MAYBE
TRS:
 {             min(0(), y) -> 0(),
            min(s(x), 0()) -> 0(),
           min(s(x), s(y)) -> min(x, y),
                len(nil()) -> 0(),
          len(cons(x, xs)) -> s(len(xs)),
               sum(x, 0()) -> x,
              sum(x, s(y)) -> s(sum(x, y)),
                le(0(), x) -> true(),
             le(s(x), 0()) -> false(),
            le(s(x), s(y)) -> le(x, y),
    take(0(), cons(y, ys)) -> y,
   take(s(x), cons(y, ys)) -> take(x, ys),
  if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
   if(false(), c, x, y, z) -> z,
             addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
 DP:
  Strict:
   {         min#(s(x), s(y)) -> min#(x, y),
            len#(cons(x, xs)) -> len#(xs),
                sum#(x, s(y)) -> sum#(x, y),
              le#(s(x), s(y)) -> le#(x, y),
     take#(s(x), cons(y, ys)) -> take#(x, ys),
    if#(true(), c, xs, ys, z) -> min#(len(xs), len(ys)),
    if#(true(), c, xs, ys, z) -> len#(xs),
    if#(true(), c, xs, ys, z) -> len#(ys),
    if#(true(), c, xs, ys, z) -> sum#(take(c, xs), take(c, ys)),
    if#(true(), c, xs, ys, z) -> le#(s(c), min(len(xs), len(ys))),
    if#(true(), c, xs, ys, z) -> take#(c, xs),
    if#(true(), c, xs, ys, z) -> take#(c, ys),
    if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
               addList#(x, y) -> min#(len(x), len(y)),
               addList#(x, y) -> len#(y),
               addList#(x, y) -> len#(x),
               addList#(x, y) -> le#(0(), min(len(x), len(y))),
               addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
  Weak:
  {             min(0(), y) -> 0(),
             min(s(x), 0()) -> 0(),
            min(s(x), s(y)) -> min(x, y),
                 len(nil()) -> 0(),
           len(cons(x, xs)) -> s(len(xs)),
                sum(x, 0()) -> x,
               sum(x, s(y)) -> s(sum(x, y)),
                 le(0(), x) -> true(),
              le(s(x), 0()) -> false(),
             le(s(x), s(y)) -> le(x, y),
     take(0(), cons(y, ys)) -> y,
    take(s(x), cons(y, ys)) -> take(x, ys),
   if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
    if(false(), c, x, y, z) -> z,
              addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
  EDG:
   {(if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> take#(c, ys))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> take#(c, xs))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> le#(s(c), min(len(xs), len(ys))))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> sum#(take(c, xs), take(c, ys)))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> len#(ys))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> len#(xs))
    (if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)), if#(true(), c, xs, ys, z) -> min#(len(xs), len(ys)))
    (len#(cons(x, xs)) -> len#(xs), len#(cons(x, xs)) -> len#(xs))
    (if#(true(), c, xs, ys, z) -> min#(len(xs), len(ys)), min#(s(x), s(y)) -> min#(x, y))
    (addList#(x, y) -> len#(x), len#(cons(x, xs)) -> len#(xs))
    (take#(s(x), cons(y, ys)) -> take#(x, ys), take#(s(x), cons(y, ys)) -> take#(x, ys))
    (if#(true(), c, xs, ys, z) -> take#(c, xs), take#(s(x), cons(y, ys)) -> take#(x, ys))
    (sum#(x, s(y)) -> sum#(x, y), sum#(x, s(y)) -> sum#(x, y))
    (addList#(x, y) -> len#(y), len#(cons(x, xs)) -> len#(xs))
    (if#(true(), c, xs, ys, z) -> le#(s(c), min(len(xs), len(ys))), le#(s(x), s(y)) -> le#(x, y))
    (le#(s(x), s(y)) -> le#(x, y), le#(s(x), s(y)) -> le#(x, y))
    (min#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y))
    (if#(true(), c, xs, ys, z) -> take#(c, ys), take#(s(x), cons(y, ys)) -> take#(x, ys))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> min#(len(xs), len(ys)))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> len#(xs))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> len#(ys))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> sum#(take(c, xs), take(c, ys)))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> le#(s(c), min(len(xs), len(ys))))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> take#(c, xs))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> take#(c, ys))
    (addList#(x, y) -> if#(le(0(), min(len(x), len(y))), 0(), x, y, nil()), if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)))
    (addList#(x, y) -> min#(len(x), len(y)), min#(s(x), s(y)) -> min#(x, y))
    (if#(true(), c, xs, ys, z) -> len#(xs), len#(cons(x, xs)) -> len#(xs))
    (if#(true(), c, xs, ys, z) -> sum#(take(c, xs), take(c, ys)), sum#(x, s(y)) -> sum#(x, y))
    (if#(true(), c, xs, ys, z) -> len#(ys), len#(cons(x, xs)) -> len#(xs))}
   SCCS:
    Scc:
     {if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))}
    Scc:
     {take#(s(x), cons(y, ys)) -> take#(x, ys)}
    Scc:
     {le#(s(x), s(y)) -> le#(x, y)}
    Scc:
     {sum#(x, s(y)) -> sum#(x, y)}
    Scc:
     {len#(cons(x, xs)) -> len#(xs)}
    Scc:
     {min#(s(x), s(y)) -> min#(x, y)}
    SCC:
     Strict:
      {if#(true(), c, xs, ys, z) -> if#(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     Fail
    SCC:
     Strict:
      {take#(s(x), cons(y, ys)) -> take#(x, ys)}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     SPSC:
      Simple Projection:
       pi(take#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {le#(s(x), s(y)) -> le#(x, y)}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {sum#(x, s(y)) -> sum#(x, y)}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     SPSC:
      Simple Projection:
       pi(sum#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {len#(cons(x, xs)) -> len#(xs)}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     SPSC:
      Simple Projection:
       pi(len#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {min#(s(x), s(y)) -> min#(x, y)}
     Weak:
     {             min(0(), y) -> 0(),
                min(s(x), 0()) -> 0(),
               min(s(x), s(y)) -> min(x, y),
                    len(nil()) -> 0(),
              len(cons(x, xs)) -> s(len(xs)),
                   sum(x, 0()) -> x,
                  sum(x, s(y)) -> s(sum(x, y)),
                    le(0(), x) -> true(),
                 le(s(x), 0()) -> false(),
                le(s(x), s(y)) -> le(x, y),
        take(0(), cons(y, ys)) -> y,
       take(s(x), cons(y, ys)) -> take(x, ys),
      if(true(), c, xs, ys, z) -> if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z)),
       if(false(), c, x, y, z) -> z,
                 addList(x, y) -> if(le(0(), min(len(x), len(y))), 0(), x, y, nil())}
     SPSC:
      Simple Projection:
       pi(min#) = 0
      Strict:
       {}
      Qed