MAYBE
Time: 0.009504
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:
  DP:
   {         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}
  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()}
  UR:
   {}
   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))}
    STATUS:
     arrows: 0.750000
     SCCS (4):
      Scc:
       {inf# X -> inf# s X}
      Scc:
       {eq#(s X, s Y) -> eq#(X, Y)}
      Scc:
       {length# cons(X, L) -> length# L}
      Scc:
       {take#(s X, cons(Y, L)) -> take#(X, L)}
      
      SCC (1):
       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()}
       Open
      SCC (1):
       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()}
       Open
      SCC (1):
       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()}
       Open
      SCC (1):
       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()}
       Open