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(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:
  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)) -> 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#()}
  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()}
  EDG:
   {(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__length(X)) -> length#(X), length#(nil()) -> 0#())
    (activate#(n__length(X)) -> length#(X), length#(cons(X, L)) -> s#(n__length(activate(L))))
    (activate#(n__length(X)) -> length#(X), length#(cons(X, L)) -> activate#(L))
    (take#(s(X), cons(Y, L)) -> activate#(X), activate#(n__length(X)) -> length#(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__inf(X)) -> inf#(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#())
    (eq#(n__s(X), n__s(Y)) -> activate#(Y), activate#(n__length(X)) -> length#(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__inf(X)) -> inf#(X))
    (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__0()) -> 0#())
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__0()) -> 0#())
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (take#(s(X), cons(Y, L)) -> activate#(Y), activate#(n__inf(X)) -> inf#(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__length(X)) -> length#(X))
    (activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(X), cons(Y, L)) -> activate#(X))
    (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#(L))
    (activate#(n__inf(X)) -> inf#(X), inf#(X) -> s#(X))
    (eq#(n__s(X), n__s(Y)) -> activate#(X), activate#(n__0()) -> 0#())
    (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__inf(X)) -> inf#(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__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))
    (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))}
   SCCS:
    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:
     {eq#(n__s(X), n__s(Y)) -> eq#(activate(X), activate(Y))}
    SCC:
     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()}
     POLY:
      Argument Filtering:
       pi(n__length) = [0], pi(length#) = [0], pi(length) = [], pi(n__take) = [0,1], pi(0) = [], pi(take#) = [0,1], pi(take) = [], pi(nil) = [], pi(inf) = [], pi(s) = 0, pi(n__inf) = [], pi(cons) = [0,1], pi(false) = [], pi(n__s) = [], pi(activate#) = [0], pi(activate) = [], pi(n__0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [take#](x0, x1) = x0 + x1,
       [length#](x0) = x0 + 1,
       [activate#](x0) = x0 + 1,
       [n__take](x0, x1) = x0 + x1 + 1,
       [cons](x0, x1) = x0 + x1 + 1,
       [n__length](x0) = x0 + 1
      Strict:
       {take#(s(X), cons(Y, L)) -> activate#(X),
        take#(s(X), cons(Y, L)) -> activate#(Y),
        take#(s(X), cons(Y, 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()}
      EDG:
       {}
       SCCS:
        
        Qed
    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(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()}
     Fail