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, greater(ys, zs), smaller(ys, zs)),
                    ge(x, 0()) -> true(),
                 ge(0(), s(x)) -> false(),
                ge(s(x), s(y)) -> ge(x, y),
  helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
               greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
               smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
         helpc(true(), ys, zs) -> ys,
        helpc(false(), ys, zs) -> zs}
 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, greater(ys, zs), smaller(ys, zs)),
       if#(false(), c, l, ys, zs) -> greater#(ys, zs),
       if#(false(), c, l, ys, zs) -> smaller#(ys, zs),
                  ge#(s(x), s(y)) -> ge#(x, y),
    helpb#(c, l, cons(y, ys), zs) -> helpa#(s(c), l, ys, zs),
                 greater#(ys, zs) -> length#(ys),
                 greater#(ys, zs) -> length#(zs),
                 greater#(ys, zs) -> ge#(length(ys), length(zs)),
                 greater#(ys, zs) -> helpc#(ge(length(ys), length(zs)), ys, zs),
                 smaller#(ys, zs) -> length#(ys),
                 smaller#(ys, zs) -> length#(zs),
                 smaller#(ys, zs) -> ge#(length(ys), length(zs)),
                 smaller#(ys, zs) -> helpc#(ge(length(ys), length(zs)), zs, 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, greater(ys, zs), smaller(ys, zs)),
                     ge(x, 0()) -> true(),
                  ge(0(), s(x)) -> false(),
                 ge(s(x), s(y)) -> ge(x, y),
   helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
                greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
                smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
          helpc(true(), ys, zs) -> ys,
         helpc(false(), ys, zs) -> zs}
  EDG:
   {(ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (if#(false(), c, l, ys, zs) -> helpb#(c, l, greater(ys, zs), smaller(ys, zs)), helpb#(c, l, cons(y, ys), zs) -> helpa#(s(c), l, ys, zs))
    (greater#(ys, zs) -> ge#(length(ys), length(zs)), ge#(s(x), s(y)) -> ge#(x, y))
    (smaller#(ys, zs) -> length#(zs), 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) -> smaller#(ys, zs))
    (helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs), if#(false(), c, l, ys, zs) -> greater#(ys, zs))
    (helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs), if#(false(), c, l, ys, zs) -> helpb#(c, l, greater(ys, zs), smaller(ys, zs)))
    (smaller#(ys, zs) -> length#(ys), length#(cons(x, y)) -> length#(y))
    (app#(x, y) -> length#(y), length#(cons(x, y)) -> length#(y))
    (helpb#(c, l, cons(y, ys), zs) -> helpa#(s(c), l, ys, zs), helpa#(c, l, ys, zs) -> ge#(c, l))
    (helpb#(c, l, cons(y, ys), zs) -> helpa#(s(c), l, ys, zs), helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs))
    (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> helpc#(ge(length(ys), length(zs)), ys, zs))
    (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> ge#(length(ys), length(zs)))
    (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> length#(zs))
    (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> length#(ys))
    (helpa#(c, l, ys, zs) -> ge#(c, l), ge#(s(x), s(y)) -> ge#(x, y))
    (if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> length#(ys))
    (if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> length#(zs))
    (if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> ge#(length(ys), length(zs)))
    (if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> helpc#(ge(length(ys), length(zs)), zs, 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))
    (app#(x, y) -> length#(x), length#(cons(x, y)) -> length#(y))
    (length#(cons(x, y)) -> length#(y), length#(cons(x, y)) -> length#(y))
    (greater#(ys, zs) -> length#(ys), length#(cons(x, y)) -> length#(y))
    (smaller#(ys, zs) -> ge#(length(ys), length(zs)), ge#(s(x), s(y)) -> ge#(x, y))
    (greater#(ys, zs) -> length#(zs), length#(cons(x, y)) -> length#(y))
    (app#(x, y) -> plus#(length(x), length(y)), plus#(x, s(y)) -> plus#(x, y))
    (plus#(x, s(y)) -> plus#(x, y), plus#(x, s(y)) -> plus#(x, y))}
   SCCS:
    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, greater(ys, zs), smaller(ys, zs)),
      helpb#(c, l, cons(y, ys), zs) -> helpa#(s(c), l, ys, zs)}
    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, greater(ys, zs), smaller(ys, zs)),
                        ge(x, 0()) -> true(),
                     ge(0(), s(x)) -> false(),
                    ge(s(x), s(y)) -> ge(x, y),
      helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
                   greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
                   smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
             helpc(true(), ys, zs) -> ys,
            helpc(false(), ys, zs) -> zs}
     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, greater(ys, zs), smaller(ys, zs)),
                        ge(x, 0()) -> true(),
                     ge(0(), s(x)) -> false(),
                    ge(s(x), s(y)) -> ge(x, y),
      helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
                   greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
                   smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
             helpc(true(), ys, zs) -> ys,
            helpc(false(), ys, zs) -> zs}
     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, greater(ys, zs), smaller(ys, zs)),
                        ge(x, 0()) -> true(),
                     ge(0(), s(x)) -> false(),
                    ge(s(x), s(y)) -> ge(x, y),
      helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
                   greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
                   smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
             helpc(true(), ys, zs) -> ys,
            helpc(false(), ys, zs) -> zs}
     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, greater(ys, zs), smaller(ys, zs)),
       helpb#(c, l, cons(y, 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, greater(ys, zs), smaller(ys, zs)),
                        ge(x, 0()) -> true(),
                     ge(0(), s(x)) -> false(),
                    ge(s(x), s(y)) -> ge(x, y),
      helpb(c, l, cons(y, ys), zs) -> cons(y, helpa(s(c), l, ys, zs)),
                   greater(ys, zs) -> helpc(ge(length(ys), length(zs)), ys, zs),
                   smaller(ys, zs) -> helpc(ge(length(ys), length(zs)), zs, ys),
             helpc(true(), ys, zs) -> ys,
            helpc(false(), ys, zs) -> zs}
     Fail