MAYBE

Problem:
 zeros() -> cons(0(),n__zeros())
 and(tt(),X) -> activate(X)
 length(nil()) -> 0()
 length(cons(N,L)) -> s(length(activate(L)))
 take(0(),IL) -> nil()
 take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
 zeros() -> n__zeros()
 take(X1,X2) -> n__take(X1,X2)
 activate(n__zeros()) -> zeros()
 activate(n__take(X1,X2)) -> take(X1,X2)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   and#(tt(),X) -> activate#(X)
   length#(cons(N,L)) -> activate#(L)
   length#(cons(N,L)) -> length#(activate(L))
   take#(s(M),cons(N,IL)) -> activate#(IL)
   activate#(n__zeros()) -> zeros#()
   activate#(n__take(X1,X2)) -> take#(X1,X2)
  TRS:
   zeros() -> cons(0(),n__zeros())
   and(tt(),X) -> activate(X)
   length(nil()) -> 0()
   length(cons(N,L)) -> s(length(activate(L)))
   take(0(),IL) -> nil()
   take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
   zeros() -> n__zeros()
   take(X1,X2) -> n__take(X1,X2)
   activate(n__zeros()) -> zeros()
   activate(n__take(X1,X2)) -> take(X1,X2)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    and#(tt(),X) -> activate#(X)
    length#(cons(N,L)) -> activate#(L)
    length#(cons(N,L)) -> length#(activate(L))
    take#(s(M),cons(N,IL)) -> activate#(IL)
    activate#(n__zeros()) -> zeros#()
    activate#(n__take(X1,X2)) -> take#(X1,X2)
   TRS:
    activate(n__zeros()) -> zeros()
    activate(n__take(X1,X2)) -> take(X1,X2)
    activate(X) -> X
    zeros() -> cons(0(),n__zeros())
    zeros() -> n__zeros()
    take(0(),IL) -> nil()
    take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
    take(X1,X2) -> n__take(X1,X2)
   ADG Processor:
    DPs:
     and#(tt(),X) -> activate#(X)
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> length#(activate(L))
     take#(s(M),cons(N,IL)) -> activate#(IL)
     activate#(n__zeros()) -> zeros#()
     activate#(n__take(X1,X2)) -> take#(X1,X2)
    TRS:
     activate(n__zeros()) -> zeros()
     activate(n__take(X1,X2)) -> take(X1,X2)
     activate(X) -> X
     zeros() -> cons(0(),n__zeros())
     zeros() -> n__zeros()
     take(0(),IL) -> nil()
     take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
     take(X1,X2) -> n__take(X1,X2)
    graph:
     take#(s(M),cons(N,IL)) -> activate#(IL) ->
     activate#(n__zeros()) -> zeros#()
     take#(s(M),cons(N,IL)) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> take#(X1,X2)
     length#(cons(N,L)) -> length#(activate(L)) ->
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> length#(activate(L)) ->
     length#(cons(N,L)) -> length#(activate(L))
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> take#(X1,X2)
     activate#(n__take(X1,X2)) -> take#(X1,X2) ->
     take#(s(M),cons(N,IL)) -> activate#(IL)
     and#(tt(),X) -> activate#(X) -> activate#(n__zeros()) -> zeros#()
     and#(tt(),X) -> activate#(X) -> activate#(n__take(X1,X2)) -> take#(X1,X2)
    Restore Modifier:
     DPs:
      and#(tt(),X) -> activate#(X)
      length#(cons(N,L)) -> activate#(L)
      length#(cons(N,L)) -> length#(activate(L))
      take#(s(M),cons(N,IL)) -> activate#(IL)
      activate#(n__zeros()) -> zeros#()
      activate#(n__take(X1,X2)) -> take#(X1,X2)
     TRS:
      zeros() -> cons(0(),n__zeros())
      and(tt(),X) -> activate(X)
      length(nil()) -> 0()
      length(cons(N,L)) -> s(length(activate(L)))
      take(0(),IL) -> nil()
      take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
      zeros() -> n__zeros()
      take(X1,X2) -> n__take(X1,X2)
      activate(n__zeros()) -> zeros()
      activate(n__take(X1,X2)) -> take(X1,X2)
      activate(X) -> X
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 9/36
      DPs:
       length#(cons(N,L)) -> length#(activate(L))
      TRS:
       zeros() -> cons(0(),n__zeros())
       and(tt(),X) -> activate(X)
       length(nil()) -> 0()
       length(cons(N,L)) -> s(length(activate(L)))
       take(0(),IL) -> nil()
       take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
       zeros() -> n__zeros()
       take(X1,X2) -> n__take(X1,X2)
       activate(n__zeros()) -> zeros()
       activate(n__take(X1,X2)) -> take(X1,X2)
       activate(X) -> X
      Open
      
      DPs:
       take#(s(M),cons(N,IL)) -> activate#(IL)
       activate#(n__take(X1,X2)) -> take#(X1,X2)
      TRS:
       zeros() -> cons(0(),n__zeros())
       and(tt(),X) -> activate(X)
       length(nil()) -> 0()
       length(cons(N,L)) -> s(length(activate(L)))
       take(0(),IL) -> nil()
       take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL)))
       zeros() -> n__zeros()
       take(X1,X2) -> n__take(X1,X2)
       activate(n__zeros()) -> zeros()
       activate(n__take(X1,X2)) -> take(X1,X2)
       activate(X) -> X
      Open