MAYBE
Time: 0.003656
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:
  DP:
   {           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())}
  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())}
  UR:
   {           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),
                   a(w, v) -> w,
                   a(w, v) -> v}
   EDG:
    {(if#(true(), c, xs, ys, z) -> len# xs, len# cons(x, xs) -> len# xs)
     (addList#(x, y) -> len# x, 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# y, 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))
     (if#(true(), c, xs, ys, z) -> le#(s c, min(len xs, len ys)), le#(s x, s y) -> le#(x, y))
     (if#(true(), c, xs, ys, z) -> len# ys, len# cons(x, xs) -> len# xs)
     (addList#(x, y) -> le#(0(), min(len x, len y)), 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) -> sum#(take(c, xs), take(c, ys)), sum#(x, s y) -> sum#(x, y))
     (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))
     (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) -> 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) -> 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) -> 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) -> 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) -> if#(le(s c, min(len xs, len ys)), s c, xs, ys, cons(sum(take(c, xs), take(c, ys)), z)))
     (len# cons(x, xs) -> len# xs, len# cons(x, xs) -> len# xs)}
    STATUS:
     arrows: 0.901235
     SCCS (6):
      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:
       {min#(s x, s y) -> min#(x, y)}
      Scc:
       {len# cons(x, xs) -> len# xs}
      
      
      
      
      
      
      SCC (1):
       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())}
       Open
      
      
      SCC (1):
       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())}
       Open
      
      SCC (1):
       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())}
       Open
      
      SCC (1):
       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())}
       Open
      
      
      SCC (1):
       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())}
       Open
      
      SCC (1):
       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())}
       Open