MAYBE
TRS:
 {              eq(X, Y) -> false(),
            eq(0(), 0()) -> true(),
          eq(s(X), s(Y)) -> eq(X, Y),
                  inf(X) -> cons(X, inf(s(X))),
            take(0(), X) -> nil(),
  take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
      length(cons(X, L)) -> s(length(L)),
           length(nil()) -> 0()}
 DP:
  Strict:
   {        eq#(s(X), s(Y)) -> eq#(X, Y),
                    inf#(X) -> inf#(s(X)),
    take#(s(X), cons(Y, L)) -> take#(X, L),
        length#(cons(X, L)) -> length#(L)}
  Weak:
  {              eq(X, Y) -> false(),
             eq(0(), 0()) -> true(),
           eq(s(X), s(Y)) -> eq(X, Y),
                   inf(X) -> cons(X, inf(s(X))),
             take(0(), X) -> nil(),
   take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
       length(cons(X, L)) -> s(length(L)),
            length(nil()) -> 0()}
  EDG:
   {(length#(cons(X, L)) -> length#(L), length#(cons(X, L)) -> length#(L))
    (inf#(X) -> inf#(s(X)), inf#(X) -> inf#(s(X)))
    (eq#(s(X), s(Y)) -> eq#(X, Y), eq#(s(X), s(Y)) -> eq#(X, Y))
    (take#(s(X), cons(Y, L)) -> take#(X, L), take#(s(X), cons(Y, L)) -> take#(X, L))}
   SCCS:
    Scc:
     {length#(cons(X, L)) -> length#(L)}
    Scc:
     {take#(s(X), cons(Y, L)) -> take#(X, L)}
    Scc:
     {inf#(X) -> inf#(s(X))}
    Scc:
     {eq#(s(X), s(Y)) -> eq#(X, Y)}
    SCC:
     Strict:
      {length#(cons(X, L)) -> length#(L)}
     Weak:
     {              eq(X, Y) -> false(),
                eq(0(), 0()) -> true(),
              eq(s(X), s(Y)) -> eq(X, Y),
                      inf(X) -> cons(X, inf(s(X))),
                take(0(), X) -> nil(),
      take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
          length(cons(X, L)) -> s(length(L)),
               length(nil()) -> 0()}
     SPSC:
      Simple Projection:
       pi(length#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {take#(s(X), cons(Y, L)) -> take#(X, L)}
     Weak:
     {              eq(X, Y) -> false(),
                eq(0(), 0()) -> true(),
              eq(s(X), s(Y)) -> eq(X, Y),
                      inf(X) -> cons(X, inf(s(X))),
                take(0(), X) -> nil(),
      take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
          length(cons(X, L)) -> s(length(L)),
               length(nil()) -> 0()}
     SPSC:
      Simple Projection:
       pi(take#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {inf#(X) -> inf#(s(X))}
     Weak:
     {              eq(X, Y) -> false(),
                eq(0(), 0()) -> true(),
              eq(s(X), s(Y)) -> eq(X, Y),
                      inf(X) -> cons(X, inf(s(X))),
                take(0(), X) -> nil(),
      take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
          length(cons(X, L)) -> s(length(L)),
               length(nil()) -> 0()}
     Fail
    SCC:
     Strict:
      {eq#(s(X), s(Y)) -> eq#(X, Y)}
     Weak:
     {              eq(X, Y) -> false(),
                eq(0(), 0()) -> true(),
              eq(s(X), s(Y)) -> eq(X, Y),
                      inf(X) -> cons(X, inf(s(X))),
                take(0(), X) -> nil(),
      take(s(X), cons(Y, L)) -> cons(Y, take(X, L)),
          length(cons(X, L)) -> s(length(L)),
               length(nil()) -> 0()}
     SPSC:
      Simple Projection:
       pi(eq#) = 1
      Strict:
       {}
      Qed