MAYBE

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

Proof:
 DP Processor:
  DPs:
   U11#(tt(),L) -> activate#(L)
   U11#(tt(),L) -> U12#(tt(),activate(L))
   U12#(tt(),L) -> activate#(L)
   U12#(tt(),L) -> length#(activate(L))
   U21#(tt(),IL,M,N) -> activate#(N)
   U21#(tt(),IL,M,N) -> activate#(M)
   U21#(tt(),IL,M,N) -> activate#(IL)
   U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
   U22#(tt(),IL,M,N) -> activate#(N)
   U22#(tt(),IL,M,N) -> activate#(M)
   U22#(tt(),IL,M,N) -> activate#(IL)
   U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
   U23#(tt(),IL,M,N) -> activate#(IL)
   U23#(tt(),IL,M,N) -> activate#(M)
   U23#(tt(),IL,M,N) -> activate#(N)
   length#(cons(N,L)) -> activate#(L)
   length#(cons(N,L)) -> U11#(tt(),activate(L))
   take#(s(M),cons(N,IL)) -> activate#(IL)
   take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
   activate#(n__zeros()) -> zeros#()
   activate#(n__take(X1,X2)) -> activate#(X2)
   activate#(n__take(X1,X2)) -> activate#(X1)
   activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
  TRS:
   zeros() -> cons(0(),n__zeros())
   U11(tt(),L) -> U12(tt(),activate(L))
   U12(tt(),L) -> s(length(activate(L)))
   U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
   U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
   U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
   length(nil()) -> 0()
   length(cons(N,L)) -> U11(tt(),activate(L))
   take(0(),IL) -> nil()
   take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
   zeros() -> n__zeros()
   take(X1,X2) -> n__take(X1,X2)
   activate(n__zeros()) -> zeros()
   activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    U11#(tt(),L) -> activate#(L)
    U11#(tt(),L) -> U12#(tt(),activate(L))
    U12#(tt(),L) -> activate#(L)
    U12#(tt(),L) -> length#(activate(L))
    U21#(tt(),IL,M,N) -> activate#(N)
    U21#(tt(),IL,M,N) -> activate#(M)
    U21#(tt(),IL,M,N) -> activate#(IL)
    U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
    U22#(tt(),IL,M,N) -> activate#(N)
    U22#(tt(),IL,M,N) -> activate#(M)
    U22#(tt(),IL,M,N) -> activate#(IL)
    U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
    U23#(tt(),IL,M,N) -> activate#(IL)
    U23#(tt(),IL,M,N) -> activate#(M)
    U23#(tt(),IL,M,N) -> activate#(N)
    length#(cons(N,L)) -> activate#(L)
    length#(cons(N,L)) -> U11#(tt(),activate(L))
    take#(s(M),cons(N,IL)) -> activate#(IL)
    take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
    activate#(n__zeros()) -> zeros#()
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
   TRS:
    activate(n__zeros()) -> zeros()
    activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
    activate(X) -> X
    zeros() -> cons(0(),n__zeros())
    zeros() -> n__zeros()
    take(0(),IL) -> nil()
    take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
    take(X1,X2) -> n__take(X1,X2)
    U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
    U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
    U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
   EDG Processor:
    DPs:
     U11#(tt(),L) -> activate#(L)
     U11#(tt(),L) -> U12#(tt(),activate(L))
     U12#(tt(),L) -> activate#(L)
     U12#(tt(),L) -> length#(activate(L))
     U21#(tt(),IL,M,N) -> activate#(N)
     U21#(tt(),IL,M,N) -> activate#(M)
     U21#(tt(),IL,M,N) -> activate#(IL)
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
     U22#(tt(),IL,M,N) -> activate#(N)
     U22#(tt(),IL,M,N) -> activate#(M)
     U22#(tt(),IL,M,N) -> activate#(IL)
     U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
     U23#(tt(),IL,M,N) -> activate#(IL)
     U23#(tt(),IL,M,N) -> activate#(M)
     U23#(tt(),IL,M,N) -> activate#(N)
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> U11#(tt(),activate(L))
     take#(s(M),cons(N,IL)) -> activate#(IL)
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
     activate#(n__zeros()) -> zeros#()
     activate#(n__take(X1,X2)) -> activate#(X2)
     activate#(n__take(X1,X2)) -> activate#(X1)
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    TRS:
     activate(n__zeros()) -> zeros()
     activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
     activate(X) -> X
     zeros() -> cons(0(),n__zeros())
     zeros() -> n__zeros()
     take(0(),IL) -> nil()
     take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
     take(X1,X2) -> n__take(X1,X2)
     U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
     U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
     U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
    graph:
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N) ->
     U21#(tt(),IL,M,N) -> activate#(N)
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N) ->
     U21#(tt(),IL,M,N) -> activate#(M)
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N) ->
     U21#(tt(),IL,M,N) -> activate#(IL)
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N) ->
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
     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)) -> activate#(X2)
     take#(s(M),cons(N,IL)) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     take#(s(M),cons(N,IL)) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U23#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__zeros()) -> zeros#()
     U23#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U23#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U23#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U23#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__zeros()) -> zeros#()
     U23#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U23#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U23#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U23#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__zeros()) -> zeros#()
     U23#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U23#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U23#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N)) ->
     U23#(tt(),IL,M,N) -> activate#(IL)
     U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N)) ->
     U23#(tt(),IL,M,N) -> activate#(M)
     U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N)) ->
     U23#(tt(),IL,M,N) -> activate#(N)
     U22#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__zeros()) -> zeros#()
     U22#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U22#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U22#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U22#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__zeros()) -> zeros#()
     U22#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U22#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U22#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U22#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__zeros()) -> zeros#()
     U22#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U22#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U22#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N)) ->
     U22#(tt(),IL,M,N) -> activate#(N)
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N)) ->
     U22#(tt(),IL,M,N) -> activate#(M)
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N)) ->
     U22#(tt(),IL,M,N) -> activate#(IL)
     U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N)) ->
     U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
     U21#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__zeros()) -> zeros#()
     U21#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U21#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U21#(tt(),IL,M,N) -> activate#(N) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U21#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__zeros()) -> zeros#()
     U21#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U21#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U21#(tt(),IL,M,N) -> activate#(M) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U21#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__zeros()) -> zeros#()
     U21#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U21#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U21#(tt(),IL,M,N) -> activate#(IL) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     length#(cons(N,L)) -> U11#(tt(),activate(L)) ->
     U11#(tt(),L) -> activate#(L)
     length#(cons(N,L)) -> U11#(tt(),activate(L)) ->
     U11#(tt(),L) -> U12#(tt(),activate(L))
     U12#(tt(),L) -> length#(activate(L)) ->
     length#(cons(N,L)) -> activate#(L)
     U12#(tt(),L) -> length#(activate(L)) ->
     length#(cons(N,L)) -> U11#(tt(),activate(L))
     U12#(tt(),L) -> activate#(L) -> activate#(n__zeros()) -> zeros#()
     U12#(tt(),L) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U12#(tt(),L) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U12#(tt(),L) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) ->
     take#(s(M),cons(N,IL)) -> activate#(IL)
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) ->
     take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
     activate#(n__take(X1,X2)) -> activate#(X2) ->
     activate#(n__zeros()) -> zeros#()
     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)) -> activate#(X1)
     activate#(n__take(X1,X2)) -> activate#(X2) ->
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     activate#(n__take(X1,X2)) -> activate#(X1) ->
     activate#(n__zeros()) -> zeros#()
     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__take(X1,X2)) -> take#(activate(X1),activate(X2))
     U11#(tt(),L) -> U12#(tt(),activate(L)) ->
     U12#(tt(),L) -> activate#(L)
     U11#(tt(),L) -> U12#(tt(),activate(L)) ->
     U12#(tt(),L) -> length#(activate(L))
     U11#(tt(),L) -> activate#(L) -> activate#(n__zeros()) -> zeros#()
     U11#(tt(),L) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X2)
     U11#(tt(),L) -> activate#(L) ->
     activate#(n__take(X1,X2)) -> activate#(X1)
     U11#(tt(),L) -> activate#(L) -> activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    Restore Modifier:
     DPs:
      U11#(tt(),L) -> activate#(L)
      U11#(tt(),L) -> U12#(tt(),activate(L))
      U12#(tt(),L) -> activate#(L)
      U12#(tt(),L) -> length#(activate(L))
      U21#(tt(),IL,M,N) -> activate#(N)
      U21#(tt(),IL,M,N) -> activate#(M)
      U21#(tt(),IL,M,N) -> activate#(IL)
      U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
      U22#(tt(),IL,M,N) -> activate#(N)
      U22#(tt(),IL,M,N) -> activate#(M)
      U22#(tt(),IL,M,N) -> activate#(IL)
      U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
      U23#(tt(),IL,M,N) -> activate#(IL)
      U23#(tt(),IL,M,N) -> activate#(M)
      U23#(tt(),IL,M,N) -> activate#(N)
      length#(cons(N,L)) -> activate#(L)
      length#(cons(N,L)) -> U11#(tt(),activate(L))
      take#(s(M),cons(N,IL)) -> activate#(IL)
      take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
      activate#(n__zeros()) -> zeros#()
      activate#(n__take(X1,X2)) -> activate#(X2)
      activate#(n__take(X1,X2)) -> activate#(X1)
      activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     TRS:
      zeros() -> cons(0(),n__zeros())
      U11(tt(),L) -> U12(tt(),activate(L))
      U12(tt(),L) -> s(length(activate(L)))
      U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
      U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
      U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
      length(nil()) -> 0()
      length(cons(N,L)) -> U11(tt(),activate(L))
      take(0(),IL) -> nil()
      take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
      zeros() -> n__zeros()
      take(X1,X2) -> n__take(X1,X2)
      activate(n__zeros()) -> zeros()
      activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
      activate(X) -> X
     SCC Processor:
      #sccs: 2
      #rules: 19
      #arcs: 79/529
      DPs:
       length#(cons(N,L)) -> U11#(tt(),activate(L))
       U11#(tt(),L) -> U12#(tt(),activate(L))
       U12#(tt(),L) -> length#(activate(L))
      TRS:
       zeros() -> cons(0(),n__zeros())
       U11(tt(),L) -> U12(tt(),activate(L))
       U12(tt(),L) -> s(length(activate(L)))
       U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
       U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
       U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
       length(nil()) -> 0()
       length(cons(N,L)) -> U11(tt(),activate(L))
       take(0(),IL) -> nil()
       take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
       zeros() -> n__zeros()
       take(X1,X2) -> n__take(X1,X2)
       activate(n__zeros()) -> zeros()
       activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
       activate(X) -> X
      Open
      
      DPs:
       take#(s(M),cons(N,IL)) -> U21#(tt(),activate(IL),M,N)
       U21#(tt(),IL,M,N) -> U22#(tt(),activate(IL),activate(M),activate(N))
       U22#(tt(),IL,M,N) -> U23#(tt(),activate(IL),activate(M),activate(N))
       U23#(tt(),IL,M,N) -> activate#(N)
       activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
       take#(s(M),cons(N,IL)) -> activate#(IL)
       activate#(n__take(X1,X2)) -> activate#(X1)
       activate#(n__take(X1,X2)) -> activate#(X2)
       U23#(tt(),IL,M,N) -> activate#(M)
       U23#(tt(),IL,M,N) -> activate#(IL)
       U22#(tt(),IL,M,N) -> activate#(IL)
       U22#(tt(),IL,M,N) -> activate#(M)
       U22#(tt(),IL,M,N) -> activate#(N)
       U21#(tt(),IL,M,N) -> activate#(IL)
       U21#(tt(),IL,M,N) -> activate#(M)
       U21#(tt(),IL,M,N) -> activate#(N)
      TRS:
       zeros() -> cons(0(),n__zeros())
       U11(tt(),L) -> U12(tt(),activate(L))
       U12(tt(),L) -> s(length(activate(L)))
       U21(tt(),IL,M,N) -> U22(tt(),activate(IL),activate(M),activate(N))
       U22(tt(),IL,M,N) -> U23(tt(),activate(IL),activate(M),activate(N))
       U23(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
       length(nil()) -> 0()
       length(cons(N,L)) -> U11(tt(),activate(L))
       take(0(),IL) -> nil()
       take(s(M),cons(N,IL)) -> U21(tt(),activate(IL),M,N)
       zeros() -> n__zeros()
       take(X1,X2) -> n__take(X1,X2)
       activate(n__zeros()) -> zeros()
       activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
       activate(X) -> X
      Open