MAYBE
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:
  Strict:
   {           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)}
  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))}
  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))
    (help#(c, l, cons(x, y), z) -> append#(y, cons(x, nil())), append#(cons(x, y), z) -> append#(y, 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))
    (rev#(x) -> length#(x), length#(cons(x, y)) -> length#(y))
    (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))
    (length#(cons(x, y)) -> length#(y), length#(cons(x, y)) -> length#(y))}
   SCCS:
    Scc:
     {append#(cons(x, y), z) -> append#(y, z)}
    Scc:
     {length#(cons(x, y)) -> length#(y)}
    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:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(append#) = 0
      Strict:
       {}
      Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(length#) = 0
      Strict:
       {}
      Qed
    SCC:
     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))}
     Fail
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed