MAYBE
Time: 0.007899
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:
  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, 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)}
  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}
  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),
           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,
                   a(z, w) -> z,
                   a(z, w) -> w}
   EDG:
    {(if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> helpc#(ge(length ys, length zs), zs, ys))
     (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) -> length# zs)
     (if#(false(), c, l, ys, zs) -> smaller#(ys, zs), smaller#(ys, zs) -> length# ys)
     (greater#(ys, zs) -> length# zs, length# cons(x, y) -> length# y)
     (greater#(ys, zs) -> length# ys, length# cons(x, y) -> length# y)
     (app#(x, y) -> plus#(length x, length y), plus#(x, s y) -> plus#(x, y))
     (greater#(ys, zs) -> ge#(length ys, length zs), ge#(s x, s y) -> ge#(x, y))
     (length# cons(x, y) -> length# y, length# cons(x, y) -> length# y)
     (app#(x, y) -> length# x, length# cons(x, y) -> length# y)
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (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, cons(y, ys), zs) -> helpa#(s c, l, ys, zs), helpa#(c, l, ys, zs) -> if#(ge(c, l), c, l, ys, zs))
     (helpb#(c, l, cons(y, ys), zs) -> helpa#(s c, l, ys, zs), helpa#(c, l, ys, zs) -> ge#(c, l))
     (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(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, greater(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) -> smaller#(ys, zs))
     (smaller#(ys, zs) -> ge#(length ys, length zs), 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))
     (smaller#(ys, zs) -> length# ys, length# cons(x, y) -> length# y)
     (smaller#(ys, zs) -> length# zs, length# cons(x, y) -> length# y)
     (helpa#(c, l, ys, zs) -> ge#(c, l), ge#(s x, s y) -> ge#(x, y))
     (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> length# ys)
     (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) -> ge#(length ys, length zs))
     (if#(false(), c, l, ys, zs) -> greater#(ys, zs), greater#(ys, zs) -> helpc#(ge(length ys, length zs), ys, zs))}
    STATUS:
     arrows: 0.934240
     SCCS (4):
      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:
       {plus#(x, s y) -> plus#(x, y)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      Scc:
       {length# cons(x, y) -> length# y}
      
      
      
      
      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, 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}
       Open
      
      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, 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}
       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, 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}
       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, 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}
       Open