MAYBE
Time: 0.003885
TRS:
 {               ge(x, 0()) -> true(),
               ge(0(), s y) -> false(),
               ge(s x, s y) -> ge(x, y),
     if(x, true(), z, c, l) -> z,
    if(x, false(), z, c, l) -> help(s c, l, x, z),
               length nil() -> 0(),
          length cons(x, y) -> s length y,
                      rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
  help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
           append(nil(), y) -> y,
      append(cons(x, y), z) -> cons(x, append(y, z))}
 DP:
  DP:
   {             ge#(s x, s y) -> ge#(x, y),
      if#(x, false(), z, c, l) -> help#(s c, l, x, z),
            length# cons(x, y) -> length# y,
                        rev# x -> if#(x, eq(0(), length x), nil(), 0(), length x),
                        rev# x -> length# x,
    help#(c, l, cons(x, y), z) -> ge#(c, l),
    help#(c, l, cons(x, y), z) -> if#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
    help#(c, l, cons(x, y), z) -> append#(y, cons(x, nil())),
        append#(cons(x, y), z) -> append#(y, z)}
  TRS:
  {               ge(x, 0()) -> true(),
                ge(0(), s y) -> false(),
                ge(s x, s y) -> ge(x, y),
      if(x, true(), z, c, l) -> z,
     if(x, false(), z, c, l) -> help(s c, l, x, z),
                length nil() -> 0(),
           length cons(x, y) -> s length y,
                       rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
   help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
            append(nil(), y) -> y,
       append(cons(x, y), z) -> cons(x, append(y, z))}
  UR:
   {           ge(x, 0()) -> true(),
             ge(0(), s y) -> false(),
             ge(s x, s y) -> ge(x, y),
             length nil() -> 0(),
        length cons(x, y) -> s length y,
         append(nil(), y) -> y,
    append(cons(x, y), z) -> cons(x, append(y, z)),
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(if#(x, false(), z, c, l) -> help#(s c, l, x, z), help#(c, l, cons(x, y), z) -> append#(y, cons(x, nil())))
     (if#(x, false(), z, c, l) -> help#(s c, l, x, z), help#(c, l, cons(x, y), z) -> if#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l))
     (if#(x, false(), z, c, l) -> help#(s c, l, x, z), help#(c, l, cons(x, y), z) -> ge#(c, l))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (length# cons(x, y) -> length# y, length# cons(x, y) -> length# y)
     (help#(c, l, cons(x, y), z) -> if#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l), if#(x, false(), z, c, l) -> help#(s c, l, x, z))
     (help#(c, l, cons(x, y), z) -> append#(y, cons(x, nil())), append#(cons(x, y), z) -> append#(y, z))
     (append#(cons(x, y), z) -> append#(y, z), append#(cons(x, y), z) -> append#(y, z))
     (help#(c, l, cons(x, y), z) -> ge#(c, l), ge#(s x, s y) -> ge#(x, y))
     (rev# x -> length# x, length# cons(x, y) -> length# y)}
    STATUS:
     arrows: 0.876543
     SCCS (4):
      Scc:
       {  if#(x, false(), z, c, l) -> help#(s c, l, x, z),
        help#(c, l, cons(x, y), z) -> if#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)}
      Scc:
       {append#(cons(x, y), z) -> append#(y, z)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      Scc:
       {length# cons(x, y) -> length# y}
      
      SCC (2):
       Strict:
        {  if#(x, false(), z, c, l) -> help#(s c, l, x, z),
         help#(c, l, cons(x, y), z) -> if#(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l)}
       Weak:
       {               ge(x, 0()) -> true(),
                     ge(0(), s y) -> false(),
                     ge(s x, s y) -> ge(x, y),
           if(x, true(), z, c, l) -> z,
          if(x, false(), z, c, l) -> help(s c, l, x, z),
                     length nil() -> 0(),
                length cons(x, y) -> s length y,
                            rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
        help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
                 append(nil(), y) -> y,
            append(cons(x, y), z) -> cons(x, append(y, z))}
       Open
      
      SCC (1):
       Strict:
        {append#(cons(x, y), z) -> append#(y, z)}
       Weak:
       {               ge(x, 0()) -> true(),
                     ge(0(), s y) -> false(),
                     ge(s x, s y) -> ge(x, y),
           if(x, true(), z, c, l) -> z,
          if(x, false(), z, c, l) -> help(s c, l, x, z),
                     length nil() -> 0(),
                length cons(x, y) -> s length y,
                            rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
        help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
                 append(nil(), y) -> y,
            append(cons(x, y), z) -> cons(x, append(y, z))}
       Open
      
      SCC (1):
       Strict:
        {ge#(s x, s y) -> ge#(x, y)}
       Weak:
       {               ge(x, 0()) -> true(),
                     ge(0(), s y) -> false(),
                     ge(s x, s y) -> ge(x, y),
           if(x, true(), z, c, l) -> z,
          if(x, false(), z, c, l) -> help(s c, l, x, z),
                     length nil() -> 0(),
                length cons(x, y) -> s length y,
                            rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
        help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
                 append(nil(), y) -> y,
            append(cons(x, y), z) -> cons(x, append(y, z))}
       Open
      
      
      SCC (1):
       Strict:
        {length# cons(x, y) -> length# y}
       Weak:
       {               ge(x, 0()) -> true(),
                     ge(0(), s y) -> false(),
                     ge(s x, s y) -> ge(x, y),
           if(x, true(), z, c, l) -> z,
          if(x, false(), z, c, l) -> help(s c, l, x, z),
                     length nil() -> 0(),
                length cons(x, y) -> s length y,
                            rev x -> if(x, eq(0(), length x), nil(), 0(), length x),
        help(c, l, cons(x, y), z) -> if(append(y, cons(x, nil())), ge(c, l), cons(x, z), c, l),
                 append(nil(), y) -> y,
            append(cons(x, y), z) -> cons(x, append(y, z))}
       Open