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
  CDG 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
   graph:
    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))
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/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