MAYBE
Time: 0.005619
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:
  DP:
   {          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)}
  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)}
  UR:
   {     plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, y),
         length nil() -> 0(),
    length cons(x, y) -> s length y,
           ge(x, 0()) -> true(),
         ge(0(), s x) -> false(),
         ge(s x, s y) -> ge(x, y),
              a(z, w) -> z,
              a(z, w) -> w}
   EDG:
    {(length# cons(x, y) -> length# y, length# cons(x, y) -> length# y)
     (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(x, y))
     (helpa#(c, l, ys, zs) -> ge#(c, l), ge#(s x, s y) -> ge#(x, y))
     (app#(x, y) -> length# x, length# cons(x, y) -> length# y)
     (helpb#(c, l, ys, zs) -> helpa#(s c, l, ys, zs), helpa#(c, l, ys, zs) -> ge#(c, l))
     (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) -> take#(c, ys, zs), take#(s c, cons(x, xs()), ys) -> take#(c, xs(), ys))
     (helpb#(c, l, ys, zs) -> take#(c, ys, zs), take#(s c, nil(), cons(y, ys)) -> take#(c, nil(), ys))
     (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))
     (app#(x, y) -> helpa#(0(), plus(length x, length y), x, y), helpa#(c, l, ys, zs) -> ge#(c, l))
     (if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs), helpb#(c, l, ys, zs) -> helpa#(s c, l, ys, zs))
     (if#(false(), c, l, ys, zs) -> helpb#(c, l, ys, zs), helpb#(c, l, ys, zs) -> take#(c, ys, zs))
     (app#(x, y) -> plus#(length x, length y), plus#(x, s y) -> plus#(x, y))
     (take#(s c, nil(), cons(y, ys)) -> take#(c, nil(), ys), take#(s c, nil(), cons(y, ys)) -> take#(c, nil(), ys))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (app#(x, y) -> length# y, length# cons(x, y) -> length# 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))}
    STATUS:
     arrows: 0.913265
     SCCS (5):
      Scc:
       {plus#(x, s y) -> plus#(x, y)}
      Scc:
       {length# cons(x, y) -> length# 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:
       {take#(s c, nil(), cons(y, ys)) -> take#(c, nil(), ys)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      
      
      
      
      SCC (1):
       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)}
       Open
      
      SCC (1):
       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)}
       Open
      SCC (3):
       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)}
       Open
      
      
      SCC (1):
       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)}
       Open
      
      SCC (1):
       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)}
       Open