MAYBE
Time: 0.007692
TRS:
 {                eq(X, Y) -> false(),
        eq(n__0(), n__0()) -> true(),
        eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                activate X -> X,
           activate n__0() -> 0(),
           activate n__s X -> s X,
         activate n__inf X -> inf X,
  activate n__take(X1, X2) -> take(X1, X2),
      activate n__length X -> length X,
                       s X -> n__s X,
                     inf X -> cons(X, n__inf s X),
                     inf X -> n__inf X,
              take(X1, X2) -> n__take(X1, X2),
     take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
              take(0(), X) -> nil(),
                       0() -> n__0(),
                  length X -> n__length X,
         length cons(X, L) -> s n__length activate L,
              length nil() -> 0()}
 DP:
  DP:
   {      eq#(n__s X, n__s Y) -> eq#(activate X, activate Y),
          eq#(n__s X, n__s Y) -> activate# X,
          eq#(n__s X, n__s Y) -> activate# Y,
             activate# n__0() -> 0#(),
             activate# n__s X -> s# X,
           activate# n__inf X -> inf# X,
    activate# n__take(X1, X2) -> take#(X1, X2),
        activate# n__length X -> length# X,
                       inf# X -> s# X,
       take#(s X, cons(Y, L)) -> activate# X,
       take#(s X, cons(Y, L)) -> activate# Y,
       take#(s X, cons(Y, L)) -> activate# L,
           length# cons(X, L) -> activate# L,
           length# cons(X, L) -> s# n__length activate L,
                length# nil() -> 0#()}
  TRS:
  {                eq(X, Y) -> false(),
         eq(n__0(), n__0()) -> true(),
         eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                 activate X -> X,
            activate n__0() -> 0(),
            activate n__s X -> s X,
          activate n__inf X -> inf X,
   activate n__take(X1, X2) -> take(X1, X2),
       activate n__length X -> length X,
                        s X -> n__s X,
                      inf X -> cons(X, n__inf s X),
                      inf X -> n__inf X,
               take(X1, X2) -> n__take(X1, X2),
      take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
               take(0(), X) -> nil(),
                        0() -> n__0(),
                   length X -> n__length X,
          length cons(X, L) -> s n__length activate L,
               length nil() -> 0()}
  UR:
   {              activate X -> X,
             activate n__0() -> 0(),
             activate n__s X -> s X,
           activate n__inf X -> inf X,
    activate n__take(X1, X2) -> take(X1, X2),
        activate n__length X -> length X,
                         s X -> n__s X,
                       inf X -> cons(X, n__inf s X),
                       inf X -> n__inf X,
                take(X1, X2) -> n__take(X1, X2),
       take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
                take(0(), X) -> nil(),
                         0() -> n__0(),
                    length X -> n__length X,
           length cons(X, L) -> s n__length activate L,
                length nil() -> 0(),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# X)
     (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
     (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# X)
     (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X)
     (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#())
     (length# cons(X, L) -> activate# L, activate# n__length X -> length# X)
     (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
     (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# X)
     (length# cons(X, L) -> activate# L, activate# n__s X -> s# X)
     (length# cons(X, L) -> activate# L, activate# n__0() -> 0#())
     (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# L)
     (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# Y)
     (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# X)
     (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# X)
     (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
     (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# X)
     (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X)
     (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
     (activate# n__inf X -> inf# X, inf# X -> s# X)
     (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#())
     (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X)
     (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# X)
     (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
     (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# X)
     (activate# n__length X -> length# X, length# cons(X, L) -> activate# L)
     (activate# n__length X -> length# X, length# cons(X, L) -> s# n__length activate L)
     (activate# n__length X -> length# X, length# nil() -> 0#())
     (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#())
     (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X)
     (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# X)
     (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
     (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# X)
     (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y))
     (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X)
     (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y)
     (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
     (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X)
     (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# X)
     (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
     (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# X)}
    EDG:
     {(take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# X)
      (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
      (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# X)
      (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X)
      (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#())
      (length# cons(X, L) -> activate# L, activate# n__length X -> length# X)
      (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
      (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# X)
      (length# cons(X, L) -> activate# L, activate# n__s X -> s# X)
      (length# cons(X, L) -> activate# L, activate# n__0() -> 0#())
      (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# L)
      (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# Y)
      (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# X)
      (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# X)
      (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
      (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# X)
      (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X)
      (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
      (activate# n__inf X -> inf# X, inf# X -> s# X)
      (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#())
      (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X)
      (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# X)
      (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
      (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# X)
      (activate# n__length X -> length# X, length# cons(X, L) -> activate# L)
      (activate# n__length X -> length# X, length# cons(X, L) -> s# n__length activate L)
      (activate# n__length X -> length# X, length# nil() -> 0#())
      (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#())
      (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X)
      (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# X)
      (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
      (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# X)
      (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y))
      (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X)
      (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y)
      (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
      (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X)
      (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# X)
      (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
      (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# X)}
     EDG:
      {(take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# X)
       (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
       (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# X)
       (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X)
       (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#())
       (length# cons(X, L) -> activate# L, activate# n__length X -> length# X)
       (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
       (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# X)
       (length# cons(X, L) -> activate# L, activate# n__s X -> s# X)
       (length# cons(X, L) -> activate# L, activate# n__0() -> 0#())
       (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# L)
       (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# Y)
       (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# X)
       (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# X)
       (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
       (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# X)
       (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X)
       (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
       (activate# n__inf X -> inf# X, inf# X -> s# X)
       (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#())
       (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X)
       (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# X)
       (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
       (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# X)
       (activate# n__length X -> length# X, length# cons(X, L) -> activate# L)
       (activate# n__length X -> length# X, length# cons(X, L) -> s# n__length activate L)
       (activate# n__length X -> length# X, length# nil() -> 0#())
       (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#())
       (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X)
       (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# X)
       (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
       (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# X)
       (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y))
       (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X)
       (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y)
       (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
       (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X)
       (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# X)
       (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
       (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# X)}
      EDG:
       {(take#(s X, cons(Y, L)) -> activate# Y, activate# n__length X -> length# X)
        (take#(s X, cons(Y, L)) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
        (take#(s X, cons(Y, L)) -> activate# Y, activate# n__inf X -> inf# X)
        (take#(s X, cons(Y, L)) -> activate# Y, activate# n__s X -> s# X)
        (take#(s X, cons(Y, L)) -> activate# Y, activate# n__0() -> 0#())
        (length# cons(X, L) -> activate# L, activate# n__length X -> length# X)
        (length# cons(X, L) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
        (length# cons(X, L) -> activate# L, activate# n__inf X -> inf# X)
        (length# cons(X, L) -> activate# L, activate# n__s X -> s# X)
        (length# cons(X, L) -> activate# L, activate# n__0() -> 0#())
        (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# L)
        (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# Y)
        (activate# n__take(X1, X2) -> take#(X1, X2), take#(s X, cons(Y, L)) -> activate# X)
        (eq#(n__s X, n__s Y) -> activate# X, activate# n__length X -> length# X)
        (eq#(n__s X, n__s Y) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
        (eq#(n__s X, n__s Y) -> activate# X, activate# n__inf X -> inf# X)
        (eq#(n__s X, n__s Y) -> activate# X, activate# n__s X -> s# X)
        (eq#(n__s X, n__s Y) -> activate# X, activate# n__0() -> 0#())
        (activate# n__inf X -> inf# X, inf# X -> s# X)
        (take#(s X, cons(Y, L)) -> activate# X, activate# n__0() -> 0#())
        (take#(s X, cons(Y, L)) -> activate# X, activate# n__s X -> s# X)
        (take#(s X, cons(Y, L)) -> activate# X, activate# n__inf X -> inf# X)
        (take#(s X, cons(Y, L)) -> activate# X, activate# n__take(X1, X2) -> take#(X1, X2))
        (take#(s X, cons(Y, L)) -> activate# X, activate# n__length X -> length# X)
        (activate# n__length X -> length# X, length# cons(X, L) -> activate# L)
        (activate# n__length X -> length# X, length# cons(X, L) -> s# n__length activate L)
        (activate# n__length X -> length# X, length# nil() -> 0#())
        (take#(s X, cons(Y, L)) -> activate# L, activate# n__0() -> 0#())
        (take#(s X, cons(Y, L)) -> activate# L, activate# n__s X -> s# X)
        (take#(s X, cons(Y, L)) -> activate# L, activate# n__inf X -> inf# X)
        (take#(s X, cons(Y, L)) -> activate# L, activate# n__take(X1, X2) -> take#(X1, X2))
        (take#(s X, cons(Y, L)) -> activate# L, activate# n__length X -> length# X)
        (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> eq#(activate X, activate Y))
        (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# X)
        (eq#(n__s X, n__s Y) -> eq#(activate X, activate Y), eq#(n__s X, n__s Y) -> activate# Y)
        (eq#(n__s X, n__s Y) -> activate# Y, activate# n__0() -> 0#())
        (eq#(n__s X, n__s Y) -> activate# Y, activate# n__s X -> s# X)
        (eq#(n__s X, n__s Y) -> activate# Y, activate# n__inf X -> inf# X)
        (eq#(n__s X, n__s Y) -> activate# Y, activate# n__take(X1, X2) -> take#(X1, X2))
        (eq#(n__s X, n__s Y) -> activate# Y, activate# n__length X -> length# X)}
       STATUS:
        arrows: 0.822222
        SCCS (2):
         Scc:
          {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)}
         Scc:
          {activate# n__take(X1, X2) -> take#(X1, X2),
               activate# n__length X -> length# X,
              take#(s X, cons(Y, L)) -> activate# X,
              take#(s X, cons(Y, L)) -> activate# Y,
              take#(s X, cons(Y, L)) -> activate# L,
                  length# cons(X, L) -> activate# L}
         
         SCC (1):
          Strict:
           {eq#(n__s X, n__s Y) -> eq#(activate X, activate Y)}
          Weak:
          {                eq(X, Y) -> false(),
                 eq(n__0(), n__0()) -> true(),
                 eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                         activate X -> X,
                    activate n__0() -> 0(),
                    activate n__s X -> s X,
                  activate n__inf X -> inf X,
           activate n__take(X1, X2) -> take(X1, X2),
               activate n__length X -> length X,
                                s X -> n__s X,
                              inf X -> cons(X, n__inf s X),
                              inf X -> n__inf X,
                       take(X1, X2) -> n__take(X1, X2),
              take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
                       take(0(), X) -> nil(),
                                0() -> n__0(),
                           length X -> n__length X,
                  length cons(X, L) -> s n__length activate L,
                       length nil() -> 0()}
          Open
         
         
         SCC (6):
          Strict:
           {activate# n__take(X1, X2) -> take#(X1, X2),
                activate# n__length X -> length# X,
               take#(s X, cons(Y, L)) -> activate# X,
               take#(s X, cons(Y, L)) -> activate# Y,
               take#(s X, cons(Y, L)) -> activate# L,
                   length# cons(X, L) -> activate# L}
          Weak:
          {                eq(X, Y) -> false(),
                 eq(n__0(), n__0()) -> true(),
                 eq(n__s X, n__s Y) -> eq(activate X, activate Y),
                         activate X -> X,
                    activate n__0() -> 0(),
                    activate n__s X -> s X,
                  activate n__inf X -> inf X,
           activate n__take(X1, X2) -> take(X1, X2),
               activate n__length X -> length X,
                                s X -> n__s X,
                              inf X -> cons(X, n__inf s X),
                              inf X -> n__inf X,
                       take(X1, X2) -> n__take(X1, X2),
              take(s X, cons(Y, L)) -> cons(activate Y, n__take(activate X, activate L)),
                       take(0(), X) -> nil(),
                                0() -> n__0(),
                           length X -> n__length X,
                  length cons(X, L) -> s n__length activate L,
                       length nil() -> 0()}
          Open