MAYBE

Problem:
 eq(n__0(),n__0()) -> true()
 eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y))
 eq(X,Y) -> false()
 inf(X) -> cons(X,n__inf(s(X)))
 take(0(),X) -> nil()
 take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
 length(nil()) -> 0()
 length(cons(X,L)) -> s(n__length(activate(L)))
 0() -> n__0()
 s(X) -> n__s(X)
 inf(X) -> n__inf(X)
 take(X1,X2) -> n__take(X1,X2)
 length(X) -> n__length(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)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   eq#(n__s(X),n__s(Y)) -> activate#(Y)
   eq#(n__s(X),n__s(Y)) -> activate#(X)
   eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y))
   inf#(X) -> s#(X)
   take#(s(X),cons(Y,L)) -> activate#(L)
   take#(s(X),cons(Y,L)) -> activate#(X)
   take#(s(X),cons(Y,L)) -> activate#(Y)
   length#(nil()) -> 0#()
   length#(cons(X,L)) -> activate#(L)
   length#(cons(X,L)) -> s#(n__length(activate(L)))
   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)
  TRS:
   eq(n__0(),n__0()) -> true()
   eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y))
   eq(X,Y) -> false()
   inf(X) -> cons(X,n__inf(s(X)))
   take(0(),X) -> nil()
   take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
   length(nil()) -> 0()
   length(cons(X,L)) -> s(n__length(activate(L)))
   0() -> n__0()
   s(X) -> n__s(X)
   inf(X) -> n__inf(X)
   take(X1,X2) -> n__take(X1,X2)
   length(X) -> n__length(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)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    eq#(n__s(X),n__s(Y)) -> activate#(Y)
    eq#(n__s(X),n__s(Y)) -> activate#(X)
    eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y))
    inf#(X) -> s#(X)
    take#(s(X),cons(Y,L)) -> activate#(L)
    take#(s(X),cons(Y,L)) -> activate#(X)
    take#(s(X),cons(Y,L)) -> activate#(Y)
    length#(nil()) -> 0#()
    length#(cons(X,L)) -> activate#(L)
    length#(cons(X,L)) -> s#(n__length(activate(L)))
    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)
   TRS:
    f23(x,y) -> x
    f23(x,y) -> 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)
    activate(X) -> X
    0() -> n__0()
    s(X) -> n__s(X)
    inf(X) -> cons(X,n__inf(s(X)))
    inf(X) -> n__inf(X)
    take(0(),X) -> nil()
    take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
    take(X1,X2) -> n__take(X1,X2)
    length(nil()) -> 0()
    length(cons(X,L)) -> s(n__length(activate(L)))
    length(X) -> n__length(X)
   EDG Processor:
    DPs:
     eq#(n__s(X),n__s(Y)) -> activate#(Y)
     eq#(n__s(X),n__s(Y)) -> activate#(X)
     eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y))
     inf#(X) -> s#(X)
     take#(s(X),cons(Y,L)) -> activate#(L)
     take#(s(X),cons(Y,L)) -> activate#(X)
     take#(s(X),cons(Y,L)) -> activate#(Y)
     length#(nil()) -> 0#()
     length#(cons(X,L)) -> activate#(L)
     length#(cons(X,L)) -> s#(n__length(activate(L)))
     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)
    TRS:
     f23(x,y) -> x
     f23(x,y) -> 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)
     activate(X) -> X
     0() -> n__0()
     s(X) -> n__s(X)
     inf(X) -> cons(X,n__inf(s(X)))
     inf(X) -> n__inf(X)
     take(0(),X) -> nil()
     take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
     take(X1,X2) -> n__take(X1,X2)
     length(nil()) -> 0()
     length(cons(X,L)) -> s(n__length(activate(L)))
     length(X) -> n__length(X)
    graph:
     length#(cons(X,L)) -> activate#(L) ->
     activate#(n__0()) -> 0#()
     length#(cons(X,L)) -> activate#(L) ->
     activate#(n__s(X)) -> s#(X)
     length#(cons(X,L)) -> activate#(L) ->
     activate#(n__inf(X)) -> inf#(X)
     length#(cons(X,L)) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> take#(X1,X2)
     length#(cons(X,L)) -> activate#(L) ->
     activate#(n__length(X)) -> length#(X)
     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)
     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)
     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#(nil()) -> 0#()
     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__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#(X)
     activate#(n__take(X1,X2)) -> take#(X1,X2) ->
     take#(s(X),cons(Y,L)) -> activate#(Y)
     activate#(n__inf(X)) -> inf#(X) -> inf#(X) -> s#(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)) -> 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)
     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)) -> 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)) -> eq#(activate(X),activate(Y))
    Restore Modifier:
     DPs:
      eq#(n__s(X),n__s(Y)) -> activate#(Y)
      eq#(n__s(X),n__s(Y)) -> activate#(X)
      eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y))
      inf#(X) -> s#(X)
      take#(s(X),cons(Y,L)) -> activate#(L)
      take#(s(X),cons(Y,L)) -> activate#(X)
      take#(s(X),cons(Y,L)) -> activate#(Y)
      length#(nil()) -> 0#()
      length#(cons(X,L)) -> activate#(L)
      length#(cons(X,L)) -> s#(n__length(activate(L)))
      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)
     TRS:
      eq(n__0(),n__0()) -> true()
      eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y))
      eq(X,Y) -> false()
      inf(X) -> cons(X,n__inf(s(X)))
      take(0(),X) -> nil()
      take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
      length(nil()) -> 0()
      length(cons(X,L)) -> s(n__length(activate(L)))
      0() -> n__0()
      s(X) -> n__s(X)
      inf(X) -> n__inf(X)
      take(X1,X2) -> n__take(X1,X2)
      length(X) -> n__length(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)
      activate(X) -> X
     SCC Processor:
      #sccs: 2
      #rules: 7
      #arcs: 40/225
      DPs:
       eq#(n__s(X),n__s(Y)) -> eq#(activate(X),activate(Y))
      TRS:
       eq(n__0(),n__0()) -> true()
       eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y))
       eq(X,Y) -> false()
       inf(X) -> cons(X,n__inf(s(X)))
       take(0(),X) -> nil()
       take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
       length(nil()) -> 0()
       length(cons(X,L)) -> s(n__length(activate(L)))
       0() -> n__0()
       s(X) -> n__s(X)
       inf(X) -> n__inf(X)
       take(X1,X2) -> n__take(X1,X2)
       length(X) -> n__length(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)
       activate(X) -> X
      Open
      
      DPs:
       length#(cons(X,L)) -> activate#(L)
       activate#(n__length(X)) -> length#(X)
       activate#(n__take(X1,X2)) -> take#(X1,X2)
       take#(s(X),cons(Y,L)) -> activate#(Y)
       take#(s(X),cons(Y,L)) -> activate#(X)
       take#(s(X),cons(Y,L)) -> activate#(L)
      TRS:
       eq(n__0(),n__0()) -> true()
       eq(n__s(X),n__s(Y)) -> eq(activate(X),activate(Y))
       eq(X,Y) -> false()
       inf(X) -> cons(X,n__inf(s(X)))
       take(0(),X) -> nil()
       take(s(X),cons(Y,L)) -> cons(activate(Y),n__take(activate(X),activate(L)))
       length(nil()) -> 0()
       length(cons(X,L)) -> s(n__length(activate(L)))
       0() -> n__0()
       s(X) -> n__s(X)
       inf(X) -> n__inf(X)
       take(X1,X2) -> n__take(X1,X2)
       length(X) -> n__length(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)
       activate(X) -> X
      Open