MAYBE
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(activate(X)),
  activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
     activate(n__length(X)) -> length(activate(X)),
                     inf(X) -> cons(X, n__inf(n__s(X))),
                     inf(X) -> n__inf(X),
               take(X1, X2) -> n__take(X1, X2),
               take(0(), X) -> nil(),
     take(s(X), cons(Y, L)) -> cons(activate(Y), n__take(activate(X), activate(L))),
                        0() -> n__0(),
                       s(X) -> n__s(X),
                  length(X) -> n__length(X),
         length(cons(X, L)) -> s(n__length(activate(L))),
              length(nil()) -> 0()}
 DP:
  Strict:
   {     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)) -> activate#(X),
          activate#(n__inf(X)) -> inf#(activate(X)),
    activate#(n__take(X1, X2)) -> activate#(X1),
    activate#(n__take(X1, X2)) -> activate#(X2),
    activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)),
       activate#(n__length(X)) -> activate#(X),
       activate#(n__length(X)) -> length#(activate(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#()}
  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(activate(X)),
   activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
      activate(n__length(X)) -> length(activate(X)),
                      inf(X) -> cons(X, n__inf(n__s(X))),
                      inf(X) -> n__inf(X),
                take(X1, X2) -> n__take(X1, X2),
                take(0(), X) -> nil(),
      take(s(X), cons(Y, L)) -> cons(activate(Y), n__take(activate(X), activate(L))),
                         0() -> n__0(),
                        s(X) -> n__s(X),
                   length(X) -> n__length(X),
          length(cons(X, L)) -> s(n__length(activate(L))),
               length(nil()) -> 0()}
  EDG:
   {(activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> length#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__length(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__inf(X)) -> inf#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__inf(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__s(X)) -> s#(X))
    (activate#(n__take(X1, X2)) -> activate#(X1), activate#(n__0()) -> 0#())
    (activate#(n__length(X)) -> length#(activate(X)), length#(nil()) -> 0#())
    (activate#(n__length(X)) -> length#(activate(X)), length#(cons(X, L)) -> s#(n__length(activate(L))))
    (activate#(n__length(X)) -> length#(activate(X)), length#(cons(X, L)) -> activate#(L))
    (length#(cons(X, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X)))
    (length#(cons(X, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X))
    (length#(cons(X, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (length#(cons(X, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2))
    (length#(cons(X, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1))
    (length#(cons(X, L)) -> activate#(L), activate#(n__inf(X)) -> inf#(activate(X)))
    (length#(cons(X, L)) -> activate#(L), activate#(n__inf(X)) -> activate#(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#(activate(X1), activate(X2)), take#(s(X), cons(Y, L)) -> activate#(L))
    (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(X), cons(Y, L)) -> activate#(Y))
    (activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)), take#(s(X), cons(Y, L)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__length(X)) -> length#(activate(X)))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__length(X)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__take(X1, X2)) -> activate#(X2))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__take(X1, X2)) -> activate#(X1))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__inf(X)) -> inf#(activate(X)))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__inf(X)) -> activate#(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#())
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__length(X)) -> activate#(X))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__inf(X)) -> inf#(activate(X)))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__inf(X)) -> activate#(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)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__inf(X)) -> inf#(activate(X)))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__inf(X)) -> activate#(X))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (activate#(n__inf(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__length(X)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__inf(X)) -> inf#(activate(X)))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__inf(X)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__length(X)) -> activate#(X), activate#(n__0()) -> 0#())
    (activate#(n__length(X)) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (activate#(n__length(X)) -> activate#(X), activate#(n__inf(X)) -> activate#(X))
    (activate#(n__length(X)) -> activate#(X), activate#(n__inf(X)) -> inf#(activate(X)))
    (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__length(X)) -> activate#(X), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> activate#(X))
    (activate#(n__length(X)) -> activate#(X), activate#(n__length(X)) -> length#(activate(X)))
    (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)) -> activate#(X))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__inf(X)) -> inf#(activate(X)))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__take(X1, X2)) -> activate#(X1))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__take(X1, X2)) -> activate#(X2))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__length(X)) -> activate#(X))
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__length(X)) -> length#(activate(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))
    (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)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__inf(X)) -> inf#(activate(X)))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X1))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__take(X1, X2)) -> activate#(X2))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__length(X)) -> activate#(X))
    (take#(s(X), cons(Y, L)) -> activate#(L), activate#(n__length(X)) -> length#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__0()) -> 0#())
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__s(X)) -> s#(X))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__inf(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__inf(X)) -> inf#(activate(X)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X1))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> activate#(X2))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> activate#(X))
    (activate#(n__take(X1, X2)) -> activate#(X2), activate#(n__length(X)) -> length#(activate(X)))}
   SCCS:
    Scc:
     {      activate#(n__inf(X)) -> activate#(X),
      activate#(n__take(X1, X2)) -> activate#(X1),
      activate#(n__take(X1, X2)) -> activate#(X2),
      activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)),
         activate#(n__length(X)) -> activate#(X),
         activate#(n__length(X)) -> length#(activate(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:
     {eq#(n__s(X), n__s(Y)) -> eq#(activate(X), activate(Y))}
    SCC:
     Strict:
      {      activate#(n__inf(X)) -> activate#(X),
       activate#(n__take(X1, X2)) -> activate#(X1),
       activate#(n__take(X1, X2)) -> activate#(X2),
       activate#(n__take(X1, X2)) -> take#(activate(X1), activate(X2)),
          activate#(n__length(X)) -> activate#(X),
          activate#(n__length(X)) -> length#(activate(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(activate(X)),
      activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
         activate(n__length(X)) -> length(activate(X)),
                         inf(X) -> cons(X, n__inf(n__s(X))),
                         inf(X) -> n__inf(X),
                   take(X1, X2) -> n__take(X1, X2),
                   take(0(), X) -> nil(),
         take(s(X), cons(Y, L)) -> cons(activate(Y), n__take(activate(X), activate(L))),
                            0() -> n__0(),
                           s(X) -> n__s(X),
                      length(X) -> n__length(X),
             length(cons(X, L)) -> s(n__length(activate(L))),
                  length(nil()) -> 0()}
     Fail
    SCC:
     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(activate(X)),
      activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)),
         activate(n__length(X)) -> length(activate(X)),
                         inf(X) -> cons(X, n__inf(n__s(X))),
                         inf(X) -> n__inf(X),
                   take(X1, X2) -> n__take(X1, X2),
                   take(0(), X) -> nil(),
         take(s(X), cons(Y, L)) -> cons(activate(Y), n__take(activate(X), activate(L))),
                            0() -> n__0(),
                           s(X) -> n__s(X),
                      length(X) -> n__length(X),
             length(cons(X, L)) -> s(n__length(activate(L))),
                  length(nil()) -> 0()}
     Fail