MAYBE
Time: 0.002612
TRS:
 {             a__eq(X, Y) -> false(),
             a__eq(X1, X2) -> eq(X1, X2),
           a__eq(0(), 0()) -> true(),
           a__eq(s X, s Y) -> a__eq(X, Y),
                  a__inf X -> cons(X, inf s X),
                  a__inf X -> inf X,
           a__take(X1, X2) -> take(X1, X2),
           a__take(0(), X) -> nil(),
  a__take(s X, cons(Y, L)) -> cons(Y, take(X, L)),
               a__length X -> length X,
      a__length cons(X, L) -> s length L,
           a__length nil() -> 0(),
               mark true() -> true(),
                  mark 0() -> 0(),
                  mark s X -> s X,
              mark false() -> false(),
         mark cons(X1, X2) -> cons(X1, X2),
                mark inf X -> a__inf mark X,
                mark nil() -> nil(),
         mark take(X1, X2) -> a__take(mark X1, mark X2),
             mark length X -> a__length mark X,
           mark eq(X1, X2) -> a__eq(X1, X2)}
 DP:
  DP:
   {  a__eq#(s X, s Y) -> a__eq#(X, Y),
           mark# inf X -> a__inf# mark X,
           mark# inf X -> mark# X,
    mark# take(X1, X2) -> a__take#(mark X1, mark X2),
    mark# take(X1, X2) -> mark# X1,
    mark# take(X1, X2) -> mark# X2,
        mark# length X -> a__length# mark X,
        mark# length X -> mark# X,
      mark# eq(X1, X2) -> a__eq#(X1, X2)}
  TRS:
  {             a__eq(X, Y) -> false(),
              a__eq(X1, X2) -> eq(X1, X2),
            a__eq(0(), 0()) -> true(),
            a__eq(s X, s Y) -> a__eq(X, Y),
                   a__inf X -> cons(X, inf s X),
                   a__inf X -> inf X,
            a__take(X1, X2) -> take(X1, X2),
            a__take(0(), X) -> nil(),
   a__take(s X, cons(Y, L)) -> cons(Y, take(X, L)),
                a__length X -> length X,
       a__length cons(X, L) -> s length L,
            a__length nil() -> 0(),
                mark true() -> true(),
                   mark 0() -> 0(),
                   mark s X -> s X,
               mark false() -> false(),
          mark cons(X1, X2) -> cons(X1, X2),
                 mark inf X -> a__inf mark X,
                 mark nil() -> nil(),
          mark take(X1, X2) -> a__take(mark X1, mark X2),
              mark length X -> a__length mark X,
            mark eq(X1, X2) -> a__eq(X1, X2)}
  EDG:
   {(mark# length X -> mark# X, mark# eq(X1, X2) -> a__eq#(X1, X2))
    (mark# length X -> mark# X, mark# length X -> mark# X)
    (mark# length X -> mark# X, mark# length X -> a__length# mark X)
    (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X2)
    (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
    (mark# length X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
    (mark# length X -> mark# X, mark# inf X -> mark# X)
    (mark# length X -> mark# X, mark# inf X -> a__inf# mark X)
    (a__eq#(s X, s Y) -> a__eq#(X, Y), a__eq#(s X, s Y) -> a__eq#(X, Y))
    (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> a__eq#(X1, X2))
    (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
    (mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
    (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
    (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
    (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
    (mark# take(X1, X2) -> mark# X1, mark# inf X -> mark# X)
    (mark# take(X1, X2) -> mark# X1, mark# inf X -> a__inf# mark X)
    (mark# take(X1, X2) -> mark# X2, mark# inf X -> a__inf# mark X)
    (mark# take(X1, X2) -> mark# X2, mark# inf X -> mark# X)
    (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
    (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
    (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
    (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X)
    (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
    (mark# take(X1, X2) -> mark# X2, mark# eq(X1, X2) -> a__eq#(X1, X2))
    (mark# eq(X1, X2) -> a__eq#(X1, X2), a__eq#(s X, s Y) -> a__eq#(X, Y))
    (mark# inf X -> mark# X, mark# inf X -> a__inf# mark X)
    (mark# inf X -> mark# X, mark# inf X -> mark# X)
    (mark# inf X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
    (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X1)
    (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X2)
    (mark# inf X -> mark# X, mark# length X -> a__length# mark X)
    (mark# inf X -> mark# X, mark# length X -> mark# X)
    (mark# inf X -> mark# X, mark# eq(X1, X2) -> a__eq#(X1, X2))}
   STATUS:
    arrows: 0.580247
    SCCS (2):
     Scc:
      {       mark# inf X -> mark# X,
       mark# take(X1, X2) -> mark# X1,
       mark# take(X1, X2) -> mark# X2,
           mark# length X -> mark# X}
     Scc:
      {a__eq#(s X, s Y) -> a__eq#(X, Y)}
     
     SCC (4):
      Strict:
       {       mark# inf X -> mark# X,
        mark# take(X1, X2) -> mark# X1,
        mark# take(X1, X2) -> mark# X2,
            mark# length X -> mark# X}
      Weak:
      {             a__eq(X, Y) -> false(),
                  a__eq(X1, X2) -> eq(X1, X2),
                a__eq(0(), 0()) -> true(),
                a__eq(s X, s Y) -> a__eq(X, Y),
                       a__inf X -> cons(X, inf s X),
                       a__inf X -> inf X,
                a__take(X1, X2) -> take(X1, X2),
                a__take(0(), X) -> nil(),
       a__take(s X, cons(Y, L)) -> cons(Y, take(X, L)),
                    a__length X -> length X,
           a__length cons(X, L) -> s length L,
                a__length nil() -> 0(),
                    mark true() -> true(),
                       mark 0() -> 0(),
                       mark s X -> s X,
                   mark false() -> false(),
              mark cons(X1, X2) -> cons(X1, X2),
                     mark inf X -> a__inf mark X,
                     mark nil() -> nil(),
              mark take(X1, X2) -> a__take(mark X1, mark X2),
                  mark length X -> a__length mark X,
                mark eq(X1, X2) -> a__eq(X1, X2)}
      Open
     
     SCC (1):
      Strict:
       {a__eq#(s X, s Y) -> a__eq#(X, Y)}
      Weak:
      {             a__eq(X, Y) -> false(),
                  a__eq(X1, X2) -> eq(X1, X2),
                a__eq(0(), 0()) -> true(),
                a__eq(s X, s Y) -> a__eq(X, Y),
                       a__inf X -> cons(X, inf s X),
                       a__inf X -> inf X,
                a__take(X1, X2) -> take(X1, X2),
                a__take(0(), X) -> nil(),
       a__take(s X, cons(Y, L)) -> cons(Y, take(X, L)),
                    a__length X -> length X,
           a__length cons(X, L) -> s length L,
                a__length nil() -> 0(),
                    mark true() -> true(),
                       mark 0() -> 0(),
                       mark s X -> s X,
                   mark false() -> false(),
              mark cons(X1, X2) -> cons(X1, X2),
                     mark inf X -> a__inf mark X,
                     mark nil() -> nil(),
              mark take(X1, X2) -> a__take(mark X1, mark X2),
                  mark length X -> a__length mark X,
                mark eq(X1, X2) -> a__eq(X1, X2)}
      Open