MAYBE
TRS:
 {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                    plus(x, 0()) -> x,
                   plus(x, s(y)) -> s(plus(x, y)),
                   length(nil()) -> 0(),
              length(cons(x, y)) -> s(length(y)),
                       app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
        if(true(), c, l, ys, zs) -> nil(),
       if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                      ge(x, 0()) -> true(),
                   ge(0(), s(x)) -> false(),
                  ge(s(x), s(y)) -> ge(x, y),
             helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
   take(0(), nil(), cons(y, ys)) -> y,
    take(0(), cons(x, xs()), ys) -> x,
  take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
   take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
 DP:
  Strict:
   {           helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs),
               helpa#(c, l, ys, zs) -> ge#(c, l),
                     plus#(x, s(y)) -> plus#(x, y),
                length#(cons(x, y)) -> length#(y),
                         app#(x, y) -> helpa#(0(), plus(length(x), length(y)), x, y),
                         app#(x, y) -> plus#(length(x), length(y)),
                         app#(x, y) -> length#(x),
                         app#(x, y) -> length#(y),
         if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs),
                    ge#(s(x), s(y)) -> ge#(x, y),
               helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs),
               helpb#(c, l, ys, zs) -> take#(c, ys, zs),
    take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys),
     take#(s(c), cons(x, xs()), ys) -> take#(c, xs(), ys)}
  Weak:
  {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                     plus(x, 0()) -> x,
                    plus(x, s(y)) -> s(plus(x, y)),
                    length(nil()) -> 0(),
               length(cons(x, y)) -> s(length(y)),
                        app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
         if(true(), c, l, ys, zs) -> nil(),
        if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                       ge(x, 0()) -> true(),
                    ge(0(), s(x)) -> false(),
                   ge(s(x), s(y)) -> ge(x, y),
              helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
    take(0(), nil(), cons(y, ys)) -> y,
     take(0(), cons(x, xs()), ys) -> x,
   take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
    take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
  EDG:
   {(ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys), take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys))
    (app#(x, y) -> length#(x), length#(cons(x, y)) -> length#(y))
    (app#(x, y) -> plus#(length(x), length(y)), plus#(x, s(y)) -> plus#(x, y))
    (length#(cons(x, y)) -> length#(y), length#(cons(x, y)) -> length#(y))
    (if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs), helpb#(c, l, ys, zs) -> take#(c, ys, zs))
    (if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs), helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs))
    (app#(x, y) -> helpa#(0(), plus(length(x), length(y)), x, y), helpa#(c, l, ys, zs) -> ge#(c, l))
    (app#(x, y) -> helpa#(0(), plus(length(x), length(y)), x, y), helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs))
    (helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs), helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs))
    (helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs), helpa#(c, l, ys, zs) -> ge#(c, l))
    (app#(x, y) -> length#(y), length#(cons(x, y)) -> length#(y))
    (helpb#(c, l, ys, zs) -> take#(c, ys, zs), take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys))
    (helpb#(c, l, ys, zs) -> take#(c, ys, zs), take#(s(c), cons(x, xs()), ys) -> take#(c, xs(), ys))
    (helpa#(c, l, ys, zs) -> ge#(c, l), ge#(s(x), s(y)) -> ge#(x, y))
    (helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs), if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs))
    (plus#(x, s(y)) -> plus#(x, y), plus#(x, s(y)) -> plus#(x, y))}
   SCCS:
    Scc:
     {take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys)}
    Scc:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    Scc:
     {length#(cons(x, y)) -> length#(y)}
    Scc:
     {plus#(x, s(y)) -> plus#(x, y)}
    Scc:
     {      helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs),
      if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs),
            helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs)}
    SCC:
     Strict:
      {take#(s(c), nil(), cons(y, ys)) -> take#(c, nil(), ys)}
     Weak:
     {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                        plus(x, 0()) -> x,
                       plus(x, s(y)) -> s(plus(x, y)),
                       length(nil()) -> 0(),
                  length(cons(x, y)) -> s(length(y)),
                           app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
            if(true(), c, l, ys, zs) -> nil(),
           if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                          ge(x, 0()) -> true(),
                       ge(0(), s(x)) -> false(),
                      ge(s(x), s(y)) -> ge(x, y),
                 helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
       take(0(), nil(), cons(y, ys)) -> y,
        take(0(), cons(x, xs()), ys) -> x,
      take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
       take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
     SPSC:
      Simple Projection:
       pi(take#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {ge#(s(x), s(y)) -> ge#(x, y)}
     Weak:
     {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                        plus(x, 0()) -> x,
                       plus(x, s(y)) -> s(plus(x, y)),
                       length(nil()) -> 0(),
                  length(cons(x, y)) -> s(length(y)),
                           app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
            if(true(), c, l, ys, zs) -> nil(),
           if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                          ge(x, 0()) -> true(),
                       ge(0(), s(x)) -> false(),
                      ge(s(x), s(y)) -> ge(x, y),
                 helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
       take(0(), nil(), cons(y, ys)) -> y,
        take(0(), cons(x, xs()), ys) -> x,
      take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
       take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {length#(cons(x, y)) -> length#(y)}
     Weak:
     {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                        plus(x, 0()) -> x,
                       plus(x, s(y)) -> s(plus(x, y)),
                       length(nil()) -> 0(),
                  length(cons(x, y)) -> s(length(y)),
                           app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
            if(true(), c, l, ys, zs) -> nil(),
           if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                          ge(x, 0()) -> true(),
                       ge(0(), s(x)) -> false(),
                      ge(s(x), s(y)) -> ge(x, y),
                 helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
       take(0(), nil(), cons(y, ys)) -> y,
        take(0(), cons(x, xs()), ys) -> x,
      take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
       take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
     SPSC:
      Simple Projection:
       pi(length#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {plus#(x, s(y)) -> plus#(x, y)}
     Weak:
     {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                        plus(x, 0()) -> x,
                       plus(x, s(y)) -> s(plus(x, y)),
                       length(nil()) -> 0(),
                  length(cons(x, y)) -> s(length(y)),
                           app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
            if(true(), c, l, ys, zs) -> nil(),
           if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                          ge(x, 0()) -> true(),
                       ge(0(), s(x)) -> false(),
                      ge(s(x), s(y)) -> ge(x, y),
                 helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
       take(0(), nil(), cons(y, ys)) -> y,
        take(0(), cons(x, xs()), ys) -> x,
      take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
       take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
     SPSC:
      Simple Projection:
       pi(plus#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {      helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs),
       if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs),
             helpb#(c, l, ys, zs) -> helpa#(s(c), l, ys, zs)}
     Weak:
     {           helpa(c, l, ys, zs) -> if(ge(c, l), c, l, ys, zs),
                        plus(x, 0()) -> x,
                       plus(x, s(y)) -> s(plus(x, y)),
                       length(nil()) -> 0(),
                  length(cons(x, y)) -> s(length(y)),
                           app(x, y) -> helpa(0(), plus(length(x), length(y)), x, y),
            if(true(), c, l, ys, zs) -> nil(),
           if(false(), c, l, ys, zs) -> helpb(c, l, ys, zs),
                          ge(x, 0()) -> true(),
                       ge(0(), s(x)) -> false(),
                      ge(s(x), s(y)) -> ge(x, y),
                 helpb(c, l, ys, zs) -> cons(take(c, ys, zs), helpa(s(c), l, ys, zs)),
       take(0(), nil(), cons(y, ys)) -> y,
        take(0(), cons(x, xs()), ys) -> x,
      take(s(c), nil(), cons(y, ys)) -> take(c, nil(), ys),
       take(s(c), cons(x, xs()), ys) -> take(c, xs(), ys)}
     Fail