YES

Problem:
 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)
 addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
 if(false(),c,x,y,z) -> 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))

Proof:
 DP Processor:
  DPs:
   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)
   addList#(x,y) -> len#(y)
   addList#(x,y) -> len#(x)
   addList#(x,y) -> min#(len(x),len(y))
   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())
   if#(true(),c,xs,ys,z) -> take#(c,ys)
   if#(true(),c,xs,ys,z) -> take#(c,xs)
   if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys))
   if#(true(),c,xs,ys,z) -> len#(ys)
   if#(true(),c,xs,ys,z) -> len#(xs)
   if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys))
   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))
  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)
   addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
   if(false(),c,x,y,z) -> 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))
  EDG Processor:
   DPs:
    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)
    addList#(x,y) -> len#(y)
    addList#(x,y) -> len#(x)
    addList#(x,y) -> min#(len(x),len(y))
    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())
    if#(true(),c,xs,ys,z) -> take#(c,ys)
    if#(true(),c,xs,ys,z) -> take#(c,xs)
    if#(true(),c,xs,ys,z) -> sum#(take(c,xs),take(c,ys))
    if#(true(),c,xs,ys,z) -> len#(ys)
    if#(true(),c,xs,ys,z) -> len#(xs)
    if#(true(),c,xs,ys,z) -> min#(len(xs),len(ys))
    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))
   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)
    addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
    if(false(),c,x,y,z) -> 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))
   graph:
    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) -> 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))
    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) ->
    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) ->
    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)
    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) -> 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)
    if#(true(),c,xs,ys,z) -> 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) -> 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) -> take#(c,xs)
    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) -> 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) -> 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) -> 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) ->
    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) -> len#(x) -> len#(cons(x,xs)) -> len#(xs)
    addList#(x,y) -> len#(y) -> len#(cons(x,xs)) -> len#(xs)
    addList#(x,y) -> min#(len(x),len(y)) ->
    min#(s(x),s(y)) -> min#(x,y)
    take#(s(x),cons(y,ys)) -> take#(x,ys) ->
    take#(s(x),cons(y,ys)) -> take#(x,ys)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
    sum#(x,s(y)) -> sum#(x,y) -> sum#(x,s(y)) -> sum#(x,y)
    len#(cons(x,xs)) -> len#(xs) -> len#(cons(x,xs)) -> len#(xs)
    min#(s(x),s(y)) -> min#(x,y) -> min#(s(x),s(y)) -> min#(x,y)
   SCC Processor:
    #sccs: 6
    #rules: 6
    #arcs: 31/324
    DPs:
     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))
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Usable Rule Processor:
     DPs:
      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))
     TRS:
      f20(x,y) -> x
      f20(x,y) -> y
      take(0(),cons(y,ys)) -> y
      take(s(x),cons(y,ys)) -> take(x,ys)
      sum(x,0()) -> x
      sum(x,s(y)) -> s(sum(x,y))
      len(nil()) -> 0()
      len(cons(x,xs)) -> s(len(xs))
      min(0(),y) -> 0()
      min(s(x),0()) -> 0()
      min(s(x),s(y)) -> min(x,y)
      le(s(x),0()) -> false()
      le(s(x),s(y)) -> le(x,y)
      le(0(),x) -> true()
     Bounds Processor:
      bound: 0
      enrichment: top-dp
      automaton:
       final states: {4}
       transitions:
        len0(25) -> 21*
        len0(20) -> 21*
        len0(15) -> 21*
        len0(22) -> 21*
        len0(24) -> 21*
        len0(26) -> 21*
        len0(21) -> 21*
        len0(16) -> 21*
        len0(23) -> 21*
        cons0(22,16) -> 16*
        cons0(22,20) -> 16*
        cons0(22,22) -> 16*
        cons0(22,24) -> 16*
        cons0(22,26) -> 16*
        cons0(23,15) -> 16*
        cons0(23,21) -> 16*
        cons0(23,23) -> 16*
        cons0(23,25) -> 16*
        cons0(24,16) -> 26*
        cons0(24,20) -> 26*
        cons0(24,22) -> 26*
        cons0(24,24) -> 26*
        cons0(24,26) -> 26*
        cons0(25,15) -> 16*
        cons0(20,15) -> 16*
        cons0(15,15) -> 16*
        cons0(25,21) -> 16*
        cons0(20,21) -> 16*
        cons0(25,23) -> 16*
        cons0(15,21) -> 16*
        cons0(20,23) -> 16*
        cons0(25,25) -> 16*
        cons0(15,23) -> 16*
        cons0(20,25) -> 16*
        cons0(15,25) -> 16*
        cons0(26,16) -> 16*
        cons0(21,16) -> 16*
        cons0(16,16) -> 16*
        cons0(26,20) -> 16*
        cons0(21,20) -> 16*
        cons0(26,22) -> 16*
        cons0(16,20) -> 16*
        cons0(21,22) -> 16*
        cons0(26,24) -> 16*
        cons0(16,22) -> 16*
        cons0(21,24) -> 16*
        cons0(26,26) -> 16*
        cons0(16,24) -> 16*
        cons0(21,26) -> 16*
        cons0(16,26) -> 16*
        cons0(22,15) -> 16*
        cons0(22,21) -> 16*
        cons0(22,23) -> 16*
        cons0(22,25) -> 16*
        cons0(23,16) -> 16*
        cons0(23,20) -> 16*
        cons0(23,22) -> 16*
        cons0(23,24) -> 16*
        cons0(23,26) -> 16*
        cons0(24,15) -> 26*
        cons0(24,21) -> 26*
        cons0(24,23) -> 26*
        cons0(24,25) -> 26*
        cons0(25,16) -> 16*
        cons0(20,16) -> 16*
        cons0(15,16) -> 16*
        cons0(25,20) -> 16*
        cons0(20,20) -> 16*
        cons0(25,22) -> 16*
        cons0(15,20) -> 16*
        cons0(20,22) -> 16*
        cons0(25,24) -> 16*
        cons0(15,22) -> 16*
        cons0(20,24) -> 16*
        cons0(25,26) -> 16*
        cons0(15,24) -> 16*
        cons0(20,26) -> 16*
        cons0(15,26) -> 16*
        cons0(26,15) -> 16*
        cons0(21,15) -> 16*
        cons0(16,15) -> 16*
        cons0(26,21) -> 16*
        cons0(21,21) -> 16*
        cons0(26,23) -> 16*
        cons0(16,21) -> 16*
        cons0(21,23) -> 16*
        cons0(26,25) -> 16*
        cons0(16,23) -> 16*
        cons0(21,25) -> 16*
        cons0(16,25) -> 16*
        sum0(22,16) -> 16*
        sum0(22,20) -> 16*
        sum0(22,22) -> 24*
        sum0(22,24) -> 16*
        sum0(22,26) -> 16*
        sum0(23,15) -> 16*
        sum0(23,21) -> 16*
        sum0(23,23) -> 16*
        sum0(23,25) -> 16*
        sum0(24,16) -> 16*
        sum0(24,20) -> 16*
        sum0(24,22) -> 16*
        sum0(24,24) -> 16*
        sum0(24,26) -> 16*
        sum0(25,15) -> 16*
        sum0(20,15) -> 16*
        sum0(15,15) -> 16*
        sum0(25,21) -> 16*
        sum0(20,21) -> 16*
        sum0(25,23) -> 16*
        sum0(15,21) -> 16*
        sum0(20,23) -> 16*
        sum0(25,25) -> 16*
        sum0(15,23) -> 16*
        sum0(20,25) -> 16*
        sum0(15,25) -> 16*
        sum0(26,16) -> 16*
        sum0(21,16) -> 16*
        sum0(16,16) -> 16*
        sum0(26,20) -> 16*
        sum0(21,20) -> 16*
        sum0(26,22) -> 16*
        sum0(16,20) -> 16*
        sum0(21,22) -> 16*
        sum0(26,24) -> 16*
        sum0(16,22) -> 16*
        sum0(21,24) -> 16*
        sum0(26,26) -> 16*
        sum0(16,24) -> 16*
        sum0(21,26) -> 16*
        sum0(16,26) -> 16*
        sum0(22,15) -> 16*
        sum0(22,21) -> 16*
        sum0(22,23) -> 16*
        sum0(22,25) -> 16*
        sum0(23,16) -> 16*
        sum0(23,20) -> 16*
        sum0(23,22) -> 16*
        sum0(23,24) -> 16*
        sum0(23,26) -> 16*
        sum0(24,15) -> 16*
        sum0(24,21) -> 16*
        sum0(24,23) -> 16*
        sum0(24,25) -> 16*
        sum0(25,16) -> 16*
        sum0(20,16) -> 16*
        sum0(15,16) -> 16*
        sum0(25,20) -> 16*
        sum0(20,20) -> 16*
        sum0(25,22) -> 16*
        sum0(15,20) -> 16*
        sum0(20,22) -> 16*
        sum0(25,24) -> 16*
        sum0(15,22) -> 16*
        sum0(20,24) -> 16*
        sum0(25,26) -> 16*
        sum0(15,24) -> 16*
        sum0(20,26) -> 16*
        sum0(15,26) -> 16*
        sum0(26,15) -> 16*
        sum0(21,15) -> 16*
        sum0(16,15) -> 16*
        sum0(26,21) -> 16*
        sum0(21,21) -> 16*
        sum0(26,23) -> 16*
        sum0(16,21) -> 16*
        sum0(21,23) -> 16*
        sum0(26,25) -> 16*
        sum0(16,23) -> 16*
        sum0(21,25) -> 16*
        sum0(16,25) -> 16*
        take0(22,16) -> 22*
        take0(22,20) -> 22*
        take0(22,22) -> 22*
        take0(22,24) -> 22*
        take0(22,26) -> 22*
        take0(23,15) -> 22*
        take0(23,21) -> 22*
        take0(23,23) -> 22*
        take0(23,25) -> 22*
        take0(24,16) -> 22*
        take0(24,20) -> 22*
        take0(24,22) -> 22*
        take0(24,24) -> 22*
        take0(24,26) -> 22*
        take0(25,15) -> 22*
        take0(20,15) -> 22*
        take0(15,15) -> 22*
        take0(25,21) -> 22*
        take0(20,21) -> 22*
        take0(25,23) -> 22*
        take0(15,21) -> 22*
        take0(20,23) -> 22*
        take0(25,25) -> 22*
        take0(15,23) -> 22*
        take0(20,25) -> 22*
        take0(15,25) -> 22*
        take0(26,16) -> 22*
        take0(21,16) -> 22*
        take0(16,16) -> 22*
        take0(26,20) -> 22*
        take0(21,20) -> 22*
        take0(26,22) -> 22*
        take0(16,20) -> 22*
        take0(21,22) -> 22*
        take0(26,24) -> 22*
        take0(16,22) -> 22*
        take0(21,24) -> 22*
        take0(26,26) -> 22*
        take0(16,24) -> 22*
        take0(21,26) -> 22*
        take0(16,26) -> 22*
        take0(22,15) -> 22*
        take0(22,21) -> 22*
        take0(22,23) -> 22*
        take0(22,25) -> 22*
        take0(23,16) -> 22*
        take0(23,20) -> 22*
        take0(23,22) -> 22*
        take0(23,24) -> 22*
        take0(23,26) -> 22*
        take0(24,15) -> 22*
        take0(24,21) -> 22*
        take0(24,23) -> 22*
        take0(24,25) -> 22*
        take0(25,16) -> 22*
        take0(20,16) -> 22*
        take0(15,16) -> 22*
        take0(25,20) -> 22*
        take0(20,20) -> 22*
        take0(25,22) -> 22*
        take0(15,20) -> 22*
        take0(20,22) -> 22*
        take0(25,24) -> 22*
        take0(15,22) -> 22*
        take0(20,24) -> 22*
        take0(25,26) -> 22*
        take0(15,24) -> 22*
        take0(20,26) -> 22*
        take0(15,26) -> 22*
        take0(26,15) -> 22*
        take0(21,15) -> 22*
        take0(16,15) -> 22*
        take0(26,21) -> 22*
        take0(21,21) -> 22*
        take0(26,23) -> 22*
        take0(16,21) -> 22*
        take0(21,23) -> 22*
        take0(26,25) -> 22*
        take0(16,23) -> 22*
        take0(21,25) -> 22*
        take0(16,25) -> 22*
        f200(22,16) -> 16*
        f200(22,20) -> 16*
        f200(22,22) -> 16*
        f200(22,24) -> 16*
        f200(22,26) -> 16*
        f200(23,15) -> 16*
        f200(23,21) -> 16*
        f200(23,23) -> 16*
        f200(23,25) -> 16*
        f200(24,16) -> 16*
        f200(24,20) -> 16*
        f200(24,22) -> 16*
        f200(24,24) -> 16*
        f200(24,26) -> 16*
        f200(25,15) -> 16*
        f200(20,15) -> 16*
        f200(15,15) -> 16*
        f200(25,21) -> 16*
        f200(20,21) -> 16*
        f200(25,23) -> 16*
        f200(15,21) -> 16*
        f200(20,23) -> 16*
        f200(25,25) -> 16*
        f200(15,23) -> 16*
        f200(20,25) -> 16*
        f200(15,25) -> 16*
        f200(26,16) -> 16*
        f200(21,16) -> 16*
        f200(16,16) -> 16*
        f200(26,20) -> 16*
        f200(21,20) -> 16*
        f200(26,22) -> 16*
        f200(16,20) -> 16*
        f200(21,22) -> 16*
        f200(26,24) -> 16*
        f200(16,22) -> 16*
        f200(21,24) -> 16*
        f200(26,26) -> 16*
        f200(16,24) -> 16*
        f200(21,26) -> 16*
        f200(16,26) -> 16*
        f200(22,15) -> 16*
        f200(22,21) -> 16*
        f200(22,23) -> 16*
        f200(22,25) -> 16*
        f200(23,16) -> 16*
        f200(23,20) -> 16*
        f200(23,22) -> 16*
        f200(23,24) -> 16*
        f200(23,26) -> 16*
        f200(24,15) -> 16*
        f200(24,21) -> 16*
        f200(24,23) -> 16*
        f200(24,25) -> 16*
        f200(25,16) -> 16*
        f200(20,16) -> 16*
        f200(15,16) -> 16*
        f200(25,20) -> 16*
        f200(20,20) -> 16*
        f200(25,22) -> 16*
        f200(15,20) -> 16*
        f200(20,22) -> 16*
        f200(25,24) -> 16*
        f200(15,22) -> 16*
        f200(20,24) -> 16*
        f200(25,26) -> 16*
        f200(15,24) -> 16*
        f200(20,26) -> 16*
        f200(15,26) -> 16*
        f200(26,15) -> 16*
        f200(21,15) -> 16*
        f200(16,15) -> 16*
        f200(26,21) -> 16*
        f200(21,21) -> 16*
        f200(26,23) -> 16*
        f200(16,21) -> 16*
        f200(21,23) -> 16*
        f200(26,25) -> 16*
        f200(16,23) -> 16*
        f200(21,25) -> 16*
        f200(16,25) -> 16*
        00() -> 23,21,16
        nil0() -> 16*
        false0() -> 25,16
        if{#,0}(25,20,26,21,26) -> 4*
        if{#,0}(25,20,21,21,26) -> 4*
        if{#,0}(25,20,16,21,26) -> 4*
        if{#,0}(25,20,26,23,26) -> 4*
        if{#,0}(25,20,21,23,26) -> 4*
        if{#,0}(25,20,16,23,26) -> 4*
        if{#,0}(25,20,26,25,26) -> 4*
        if{#,0}(25,20,21,25,26) -> 4*
        if{#,0}(25,20,16,25,26) -> 4*
        if{#,0}(25,20,22,16,26) -> 4*
        if{#,0}(25,20,22,20,26) -> 4*
        if{#,0}(25,20,22,22,26) -> 4*
        if{#,0}(25,20,22,24,26) -> 4*
        if{#,0}(25,20,22,26,26) -> 4*
        if{#,0}(25,20,23,15,26) -> 4*
        if{#,0}(25,20,23,21,26) -> 4*
        if{#,0}(25,20,23,23,26) -> 4*
        if{#,0}(25,20,23,25,26) -> 4*
        if{#,0}(25,20,24,16,26) -> 4*
        if{#,0}(25,20,24,20,26) -> 4*
        if{#,0}(25,20,24,22,26) -> 4*
        if{#,0}(25,20,24,24,26) -> 4*
        if{#,0}(25,20,24,26,26) -> 4*
        if{#,0}(25,20,25,15,26) -> 4*
        if{#,0}(25,20,20,15,26) -> 4*
        if{#,0}(25,20,15,15,26) -> 4*
        if{#,0}(25,20,25,21,26) -> 4*
        if{#,0}(25,20,20,21,26) -> 4*
        if{#,0}(25,20,25,23,26) -> 4*
        if{#,0}(25,20,15,21,26) -> 4*
        if{#,0}(25,20,20,23,26) -> 4*
        if{#,0}(25,20,15,23,26) -> 4*
        if{#,0}(25,20,25,25,26) -> 4*
        if{#,0}(25,20,20,25,26) -> 4*
        if{#,0}(25,20,15,25,26) -> 4*
        if{#,0}(25,20,26,16,26) -> 4*
        if{#,0}(25,20,21,16,26) -> 4*
        if{#,0}(25,20,16,16,26) -> 4*
        if{#,0}(25,20,26,20,26) -> 4*
        if{#,0}(25,20,21,20,26) -> 4*
        if{#,0}(25,20,16,20,26) -> 4*
        if{#,0}(25,20,26,22,26) -> 4*
        if{#,0}(25,20,21,22,26) -> 4*
        if{#,0}(25,20,16,22,26) -> 4*
        if{#,0}(25,20,26,24,26) -> 4*
        if{#,0}(25,20,21,24,26) -> 4*
        if{#,0}(25,20,26,26,26) -> 4*
        if{#,0}(25,20,16,24,26) -> 4*
        if{#,0}(25,20,21,26,26) -> 4*
        if{#,0}(25,20,16,26,26) -> 4*
        if{#,0}(25,20,22,15,26) -> 4*
        if{#,0}(25,20,22,21,26) -> 4*
        if{#,0}(25,20,22,23,26) -> 4*
        if{#,0}(25,20,22,25,26) -> 4*
        if{#,0}(25,20,23,16,26) -> 4*
        if{#,0}(25,20,23,20,26) -> 4*
        if{#,0}(25,20,23,22,26) -> 4*
        if{#,0}(25,20,23,24,26) -> 4*
        if{#,0}(25,20,23,26,26) -> 4*
        if{#,0}(25,20,24,15,26) -> 4*
        if{#,0}(25,20,24,21,26) -> 4*
        if{#,0}(25,20,24,23,26) -> 4*
        if{#,0}(25,20,24,25,26) -> 4*
        if{#,0}(25,20,25,16,26) -> 4*
        if{#,0}(25,20,20,16,26) -> 4*
        if{#,0}(25,20,15,16,26) -> 4*
        if{#,0}(25,20,25,20,26) -> 4*
        if{#,0}(25,20,20,20,26) -> 4*
        if{#,0}(25,20,15,20,26) -> 4*
        if{#,0}(25,20,25,22,26) -> 4*
        if{#,0}(25,20,20,22,26) -> 4*
        if{#,0}(25,20,15,22,26) -> 4*
        if{#,0}(25,20,25,24,26) -> 4*
        if{#,0}(25,20,20,24,26) -> 4*
        if{#,0}(25,20,15,24,26) -> 4*
        if{#,0}(25,20,25,26,26) -> 4*
        if{#,0}(25,20,20,26,26) -> 4*
        if{#,0}(25,20,15,26,26) -> 4*
        if{#,0}(25,20,26,15,26) -> 4*
        if{#,0}(25,20,21,15,26) -> 4*
        if{#,0}(25,20,16,15,26) -> 4*
        true0() -> 15*
        le0(22,16) -> 16*
        le0(22,20) -> 16*
        le0(22,22) -> 16*
        le0(22,24) -> 16*
        le0(22,26) -> 16*
        le0(23,15) -> 16*
        le0(23,21) -> 16*
        le0(23,23) -> 16*
        le0(23,25) -> 16*
        le0(24,16) -> 16*
        le0(24,20) -> 16*
        le0(24,22) -> 16*
        le0(24,24) -> 16*
        le0(24,26) -> 16*
        le0(25,15) -> 16*
        le0(20,15) -> 16*
        le0(15,15) -> 16*
        le0(25,21) -> 16*
        le0(20,21) -> 16*
        le0(25,23) -> 16*
        le0(15,21) -> 16*
        le0(20,23) -> 25*
        le0(25,25) -> 16*
        le0(15,23) -> 16*
        le0(20,25) -> 16*
        le0(15,25) -> 16*
        le0(26,16) -> 16*
        le0(21,16) -> 16*
        le0(16,16) -> 16*
        le0(26,20) -> 16*
        le0(21,20) -> 16*
        le0(26,22) -> 16*
        le0(16,20) -> 16*
        le0(21,22) -> 16*
        le0(26,24) -> 16*
        le0(16,22) -> 16*
        le0(21,24) -> 16*
        le0(26,26) -> 16*
        le0(16,24) -> 16*
        le0(21,26) -> 16*
        le0(16,26) -> 16*
        le0(22,15) -> 16*
        le0(22,21) -> 16*
        le0(22,23) -> 16*
        le0(22,25) -> 16*
        le0(23,16) -> 16*
        le0(23,20) -> 16*
        le0(23,22) -> 16*
        le0(23,24) -> 16*
        le0(23,26) -> 16*
        le0(24,15) -> 16*
        le0(24,21) -> 16*
        le0(24,23) -> 16*
        le0(24,25) -> 16*
        le0(25,16) -> 16*
        le0(20,16) -> 16*
        le0(15,16) -> 16*
        le0(25,20) -> 16*
        le0(20,20) -> 16*
        le0(25,22) -> 16*
        le0(15,20) -> 16*
        le0(20,22) -> 16*
        le0(25,24) -> 16*
        le0(15,22) -> 16*
        le0(20,24) -> 16*
        le0(25,26) -> 16*
        le0(15,24) -> 16*
        le0(20,26) -> 16*
        le0(15,26) -> 16*
        le0(26,15) -> 16*
        le0(21,15) -> 16*
        le0(16,15) -> 16*
        le0(26,21) -> 16*
        le0(21,21) -> 16*
        le0(26,23) -> 16*
        le0(16,21) -> 16*
        le0(21,23) -> 16*
        le0(26,25) -> 16*
        le0(16,23) -> 16*
        le0(21,25) -> 16*
        le0(16,25) -> 16*
        s0(25) -> 20*
        s0(20) -> 20*
        s0(15) -> 20*
        s0(22) -> 20*
        s0(24) -> 20*
        s0(26) -> 20*
        s0(21) -> 21,20
        s0(16) -> 20*
        s0(23) -> 20*
        min0(22,16) -> 16*
        min0(22,20) -> 16*
        min0(22,22) -> 16*
        min0(22,24) -> 16*
        min0(22,26) -> 16*
        min0(23,15) -> 16*
        min0(23,21) -> 16*
        min0(23,23) -> 16*
        min0(23,25) -> 16*
        min0(24,16) -> 16*
        min0(24,20) -> 16*
        min0(24,22) -> 16*
        min0(24,24) -> 16*
        min0(24,26) -> 16*
        min0(25,15) -> 16*
        min0(20,15) -> 16*
        min0(15,15) -> 16*
        min0(25,21) -> 16*
        min0(20,21) -> 16*
        min0(25,23) -> 16*
        min0(15,21) -> 16*
        min0(20,23) -> 16*
        min0(25,25) -> 16*
        min0(15,23) -> 16*
        min0(20,25) -> 16*
        min0(15,25) -> 16*
        min0(26,16) -> 16*
        min0(21,16) -> 16*
        min0(16,16) -> 16*
        min0(26,20) -> 16*
        min0(21,20) -> 16*
        min0(26,22) -> 16*
        min0(16,20) -> 16*
        min0(21,22) -> 16*
        min0(26,24) -> 16*
        min0(16,22) -> 16*
        min0(21,24) -> 16*
        min0(26,26) -> 16*
        min0(16,24) -> 16*
        min0(21,26) -> 16*
        min0(16,26) -> 16*
        min0(22,15) -> 16*
        min0(22,21) -> 16*
        min0(22,23) -> 16*
        min0(22,25) -> 16*
        min0(23,16) -> 16*
        min0(23,20) -> 16*
        min0(23,22) -> 16*
        min0(23,24) -> 16*
        min0(23,26) -> 16*
        min0(24,15) -> 16*
        min0(24,21) -> 16*
        min0(24,23) -> 16*
        min0(24,25) -> 16*
        min0(25,16) -> 16*
        min0(20,16) -> 16*
        min0(15,16) -> 16*
        min0(25,20) -> 16*
        min0(20,20) -> 16*
        min0(25,22) -> 16*
        min0(15,20) -> 16*
        min0(20,22) -> 16*
        min0(25,24) -> 16*
        min0(15,22) -> 16*
        min0(20,24) -> 16*
        min0(25,26) -> 16*
        min0(15,24) -> 16*
        min0(20,26) -> 16*
        min0(15,26) -> 16*
        min0(26,15) -> 16*
        min0(21,15) -> 16*
        min0(16,15) -> 16*
        min0(26,21) -> 16*
        min0(21,21) -> 23*
        min0(26,23) -> 16*
        min0(16,21) -> 16*
        min0(21,23) -> 16*
        min0(26,25) -> 16*
        min0(16,23) -> 16*
        min0(21,25) -> 16*
        min0(16,25) -> 16*
        15 -> 16*
        16 -> 22*
        20 -> 16*
        21 -> 16*
        22 -> 24,16
        23 -> 16*
        24 -> 22,16
        25 -> 16*
        26 -> 16*
      problem:
       DPs:
        
       TRS:
        f20(x,y) -> x
        f20(x,y) -> y
        take(0(),cons(y,ys)) -> y
        take(s(x),cons(y,ys)) -> take(x,ys)
        sum(x,0()) -> x
        sum(x,s(y)) -> s(sum(x,y))
        len(nil()) -> 0()
        len(cons(x,xs)) -> s(len(xs))
        min(0(),y) -> 0()
        min(s(x),0()) -> 0()
        min(s(x),s(y)) -> min(x,y)
        le(s(x),0()) -> false()
        le(s(x),s(y)) -> le(x,y)
        le(0(),x) -> true()
      Qed
    
    DPs:
     take#(s(x),cons(y,ys)) -> take#(x,ys)
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Subterm Criterion Processor:
     simple projection:
      pi(take#) = 1
     problem:
      DPs:
       
      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)
       addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
       if(false(),c,x,y,z) -> 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))
     Qed
    
    DPs:
     sum#(x,s(y)) -> sum#(x,y)
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Subterm Criterion Processor:
     simple projection:
      pi(sum#) = 1
     problem:
      DPs:
       
      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)
       addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
       if(false(),c,x,y,z) -> 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))
     Qed
    
    DPs:
     len#(cons(x,xs)) -> len#(xs)
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Subterm Criterion Processor:
     simple projection:
      pi(len#) = 0
     problem:
      DPs:
       
      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)
       addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
       if(false(),c,x,y,z) -> 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))
     Qed
    
    DPs:
     min#(s(x),s(y)) -> min#(x,y)
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Subterm Criterion Processor:
     simple projection:
      pi(min#) = 1
     problem:
      DPs:
       
      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)
       addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
       if(false(),c,x,y,z) -> 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))
     Qed
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    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)
     addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
     if(false(),c,x,y,z) -> 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))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      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)
       addList(x,y) -> if(le(0(),min(len(x),len(y))),0(),x,y,nil())
       if(false(),c,x,y,z) -> 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))
     Qed