MAYBE
* Step 1: InnermostRuleRemoval MAYBE
    + Considered Problem:
        - Strict TRS:
            0() -> n__0()
            U11(tt(),L) -> s(length(activate(L)))
            U21(tt()) -> nil()
            U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            length(cons(N,L)) -> U11(and(isNatList(activate(L)),n__isNat(N)),activate(L))
            length(nil()) -> 0()
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            take(0(),IL) -> U21(isNatIList(IL))
            take(s(M),cons(N,IL)) -> U31(and(isNatIList(activate(IL)),n__and(isNat(M),n__isNat(N))),activate(IL),M,N)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1
            ,n__take/2,n__zeros/0,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,activate,and,cons,isNat,isNatIList
            ,isNatList,length,nil,s,take,zeros} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        InnermostRuleRemoval
    + Details:
        Arguments of following rules are not normal-forms.
          length(cons(N,L)) -> U11(and(isNatList(activate(L)),n__isNat(N)),activate(L))
          length(nil()) -> 0()
          take(0(),IL) -> U21(isNatIList(IL))
          take(s(M),cons(N,IL)) -> U31(and(isNatIList(activate(IL)),n__and(isNat(M),n__isNat(N))),activate(IL),M,N)
        All above mentioned rules can be savely removed.
* Step 2: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            0() -> n__0()
            U11(tt(),L) -> s(length(activate(L)))
            U21(tt()) -> nil()
            U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1,n__length/1,n__nil/0,n__s/1
            ,n__take/2,n__zeros/0,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0,U11,U21,U31,activate,and,cons,isNat,isNatIList
            ,isNatList,length,nil,s,take,zeros} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          0#() -> c_1()
          U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
          U21#(tt()) -> c_3(nil#())
          U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                  ,activate#(N)
                                  ,activate#(M)
                                  ,activate#(IL))
          activate#(X) -> c_5()
          activate#(n__0()) -> c_6(0#())
          activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          activate#(n__isNat(X)) -> c_9(isNat#(X))
          activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          activate#(n__length(X)) -> c_12(length#(X))
          activate#(n__nil()) -> c_13(nil#())
          activate#(n__s(X)) -> c_14(s#(X))
          activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          activate#(n__zeros()) -> c_16(zeros#())
          and#(X1,X2) -> c_17()
          and#(tt(),X) -> c_18(activate#(X))
          cons#(X1,X2) -> c_19()
          isNat#(X) -> c_20()
          isNat#(n__0()) -> c_21()
          isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          isNatIList#(X) -> c_25()
          isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                             ,isNat#(activate(V1))
                                             ,activate#(V1)
                                             ,activate#(V2))
          isNatIList#(n__zeros()) -> c_27()
          isNatList#(X) -> c_28()
          isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
          isNatList#(n__nil()) -> c_30()
          isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
          length#(X) -> c_32()
          nil#() -> c_33()
          s#(X) -> c_34()
          take#(X1,X2) -> c_35()
          zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          zeros#() -> c_37()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 3: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            0#() -> c_1()
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U21#(tt()) -> c_3(nil#())
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(X) -> c_5()
            activate#(n__0()) -> c_6(0#())
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            activate#(n__length(X)) -> c_12(length#(X))
            activate#(n__nil()) -> c_13(nil#())
            activate#(n__s(X)) -> c_14(s#(X))
            activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
            activate#(n__zeros()) -> c_16(zeros#())
            and#(X1,X2) -> c_17()
            and#(tt(),X) -> c_18(activate#(X))
            cons#(X1,X2) -> c_19()
            isNat#(X) -> c_20()
            isNat#(n__0()) -> c_21()
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(X) -> c_25()
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatIList#(n__zeros()) -> c_27()
            isNatList#(X) -> c_28()
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__nil()) -> c_30()
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            length#(X) -> c_32()
            nil#() -> c_33()
            s#(X) -> c_34()
            take#(X1,X2) -> c_35()
            zeros#() -> c_36(cons#(0(),n__zeros()),0#())
            zeros#() -> c_37()
        - Weak TRS:
            0() -> n__0()
            U11(tt(),L) -> s(length(activate(L)))
            U21(tt()) -> nil()
            U31(tt(),IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL)))
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          0() -> n__0()
          activate(X) -> X
          activate(n__0()) -> 0()
          activate(n__and(X1,X2)) -> and(X1,X2)
          activate(n__cons(X1,X2)) -> cons(X1,X2)
          activate(n__isNat(X)) -> isNat(X)
          activate(n__isNatIList(X)) -> isNatIList(X)
          activate(n__isNatList(X)) -> isNatList(X)
          activate(n__length(X)) -> length(X)
          activate(n__nil()) -> nil()
          activate(n__s(X)) -> s(X)
          activate(n__take(X1,X2)) -> take(X1,X2)
          activate(n__zeros()) -> zeros()
          and(X1,X2) -> n__and(X1,X2)
          and(tt(),X) -> activate(X)
          cons(X1,X2) -> n__cons(X1,X2)
          isNat(X) -> n__isNat(X)
          isNat(n__0()) -> tt()
          isNat(n__length(V1)) -> isNatList(activate(V1))
          isNat(n__s(V1)) -> isNat(activate(V1))
          isNatIList(V) -> isNatList(activate(V))
          isNatIList(X) -> n__isNatIList(X)
          isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
          isNatIList(n__zeros()) -> tt()
          isNatList(X) -> n__isNatList(X)
          isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
          isNatList(n__nil()) -> tt()
          isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
          length(X) -> n__length(X)
          nil() -> n__nil()
          s(X) -> n__s(X)
          take(X1,X2) -> n__take(X1,X2)
          zeros() -> cons(0(),n__zeros())
          zeros() -> n__zeros()
          0#() -> c_1()
          U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
          U21#(tt()) -> c_3(nil#())
          U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                  ,activate#(N)
                                  ,activate#(M)
                                  ,activate#(IL))
          activate#(X) -> c_5()
          activate#(n__0()) -> c_6(0#())
          activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          activate#(n__isNat(X)) -> c_9(isNat#(X))
          activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          activate#(n__length(X)) -> c_12(length#(X))
          activate#(n__nil()) -> c_13(nil#())
          activate#(n__s(X)) -> c_14(s#(X))
          activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          activate#(n__zeros()) -> c_16(zeros#())
          and#(X1,X2) -> c_17()
          and#(tt(),X) -> c_18(activate#(X))
          cons#(X1,X2) -> c_19()
          isNat#(X) -> c_20()
          isNat#(n__0()) -> c_21()
          isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          isNatIList#(X) -> c_25()
          isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                             ,isNat#(activate(V1))
                                             ,activate#(V1)
                                             ,activate#(V2))
          isNatIList#(n__zeros()) -> c_27()
          isNatList#(X) -> c_28()
          isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
          isNatList#(n__nil()) -> c_30()
          isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
          length#(X) -> c_32()
          nil#() -> c_33()
          s#(X) -> c_34()
          take#(X1,X2) -> c_35()
          zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          zeros#() -> c_37()
* Step 4: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            0#() -> c_1()
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U21#(tt()) -> c_3(nil#())
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(X) -> c_5()
            activate#(n__0()) -> c_6(0#())
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            activate#(n__length(X)) -> c_12(length#(X))
            activate#(n__nil()) -> c_13(nil#())
            activate#(n__s(X)) -> c_14(s#(X))
            activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
            activate#(n__zeros()) -> c_16(zeros#())
            and#(X1,X2) -> c_17()
            and#(tt(),X) -> c_18(activate#(X))
            cons#(X1,X2) -> c_19()
            isNat#(X) -> c_20()
            isNat#(n__0()) -> c_21()
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(X) -> c_25()
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatIList#(n__zeros()) -> c_27()
            isNatList#(X) -> c_28()
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__nil()) -> c_30()
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            length#(X) -> c_32()
            nil#() -> c_33()
            s#(X) -> c_34()
            take#(X1,X2) -> c_35()
            zeros#() -> c_36(cons#(0(),n__zeros()),0#())
            zeros#() -> c_37()
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,5,17,19,20,21,25,27,28,30,32,33,34,35,37}
        by application of
          Pre({1,5,17,19,20,21,25,27,28,30,32,33,34,35,37}) = {2,3,4,6,7,8,9,10,11,12,13,14,15,16,18,22,23,24,26,29
          ,31,36}.
        Here rules are labelled as follows:
          1: 0#() -> c_1()
          2: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
          3: U21#(tt()) -> c_3(nil#())
          4: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                     ,activate#(N)
                                     ,activate#(M)
                                     ,activate#(IL))
          5: activate#(X) -> c_5()
          6: activate#(n__0()) -> c_6(0#())
          7: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          8: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          9: activate#(n__isNat(X)) -> c_9(isNat#(X))
          10: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          11: activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          12: activate#(n__length(X)) -> c_12(length#(X))
          13: activate#(n__nil()) -> c_13(nil#())
          14: activate#(n__s(X)) -> c_14(s#(X))
          15: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          16: activate#(n__zeros()) -> c_16(zeros#())
          17: and#(X1,X2) -> c_17()
          18: and#(tt(),X) -> c_18(activate#(X))
          19: cons#(X1,X2) -> c_19()
          20: isNat#(X) -> c_20()
          21: isNat#(n__0()) -> c_21()
          22: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          23: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          24: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          25: isNatIList#(X) -> c_25()
          26: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
          27: isNatIList#(n__zeros()) -> c_27()
          28: isNatList#(X) -> c_28()
          29: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          30: isNatList#(n__nil()) -> c_30()
          31: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          32: length#(X) -> c_32()
          33: nil#() -> c_33()
          34: s#(X) -> c_34()
          35: take#(X1,X2) -> c_35()
          36: zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          37: zeros#() -> c_37()
* Step 5: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U21#(tt()) -> c_3(nil#())
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(n__0()) -> c_6(0#())
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            activate#(n__length(X)) -> c_12(length#(X))
            activate#(n__nil()) -> c_13(nil#())
            activate#(n__s(X)) -> c_14(s#(X))
            activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
            activate#(n__zeros()) -> c_16(zeros#())
            and#(tt(),X) -> c_18(activate#(X))
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            zeros#() -> c_36(cons#(0(),n__zeros()),0#())
        - Weak DPs:
            0#() -> c_1()
            activate#(X) -> c_5()
            and#(X1,X2) -> c_17()
            cons#(X1,X2) -> c_19()
            isNat#(X) -> c_20()
            isNat#(n__0()) -> c_21()
            isNatIList#(X) -> c_25()
            isNatIList#(n__zeros()) -> c_27()
            isNatList#(X) -> c_28()
            isNatList#(n__nil()) -> c_30()
            length#(X) -> c_32()
            nil#() -> c_33()
            s#(X) -> c_34()
            take#(X1,X2) -> c_35()
            zeros#() -> c_37()
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,6,10,11,12,13,22}
        by application of
          Pre({2,4,6,10,11,12,13,22}) = {1,3,14,15,16,17,18,19,20,21}.
        Here rules are labelled as follows:
          1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
          2: U21#(tt()) -> c_3(nil#())
          3: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                     ,activate#(N)
                                     ,activate#(M)
                                     ,activate#(IL))
          4: activate#(n__0()) -> c_6(0#())
          5: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          6: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          7: activate#(n__isNat(X)) -> c_9(isNat#(X))
          8: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          9: activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          10: activate#(n__length(X)) -> c_12(length#(X))
          11: activate#(n__nil()) -> c_13(nil#())
          12: activate#(n__s(X)) -> c_14(s#(X))
          13: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          14: activate#(n__zeros()) -> c_16(zeros#())
          15: and#(tt(),X) -> c_18(activate#(X))
          16: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          17: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          18: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          19: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
          20: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          21: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          22: zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          23: 0#() -> c_1()
          24: activate#(X) -> c_5()
          25: and#(X1,X2) -> c_17()
          26: cons#(X1,X2) -> c_19()
          27: isNat#(X) -> c_20()
          28: isNat#(n__0()) -> c_21()
          29: isNatIList#(X) -> c_25()
          30: isNatIList#(n__zeros()) -> c_27()
          31: isNatList#(X) -> c_28()
          32: isNatList#(n__nil()) -> c_30()
          33: length#(X) -> c_32()
          34: nil#() -> c_33()
          35: s#(X) -> c_34()
          36: take#(X1,X2) -> c_35()
          37: zeros#() -> c_37()
* Step 6: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            activate#(n__zeros()) -> c_16(zeros#())
            and#(tt(),X) -> c_18(activate#(X))
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
        - Weak DPs:
            0#() -> c_1()
            U21#(tt()) -> c_3(nil#())
            activate#(X) -> c_5()
            activate#(n__0()) -> c_6(0#())
            activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
            activate#(n__length(X)) -> c_12(length#(X))
            activate#(n__nil()) -> c_13(nil#())
            activate#(n__s(X)) -> c_14(s#(X))
            activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
            and#(X1,X2) -> c_17()
            cons#(X1,X2) -> c_19()
            isNat#(X) -> c_20()
            isNat#(n__0()) -> c_21()
            isNatIList#(X) -> c_25()
            isNatIList#(n__zeros()) -> c_27()
            isNatList#(X) -> c_28()
            isNatList#(n__nil()) -> c_30()
            length#(X) -> c_32()
            nil#() -> c_33()
            s#(X) -> c_34()
            take#(X1,X2) -> c_35()
            zeros#() -> c_36(cons#(0(),n__zeros()),0#())
            zeros#() -> c_37()
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {7}
        by application of
          Pre({7}) = {1,2,8,9,10,11,12,13,14}.
        Here rules are labelled as follows:
          1: U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
          2: U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                     ,activate#(N)
                                     ,activate#(M)
                                     ,activate#(IL))
          3: activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          4: activate#(n__isNat(X)) -> c_9(isNat#(X))
          5: activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          6: activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          7: activate#(n__zeros()) -> c_16(zeros#())
          8: and#(tt(),X) -> c_18(activate#(X))
          9: isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          10: isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          11: isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          12: isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
          13: isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          14: isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
          15: 0#() -> c_1()
          16: U21#(tt()) -> c_3(nil#())
          17: activate#(X) -> c_5()
          18: activate#(n__0()) -> c_6(0#())
          19: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          20: activate#(n__length(X)) -> c_12(length#(X))
          21: activate#(n__nil()) -> c_13(nil#())
          22: activate#(n__s(X)) -> c_14(s#(X))
          23: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          24: and#(X1,X2) -> c_17()
          25: cons#(X1,X2) -> c_19()
          26: isNat#(X) -> c_20()
          27: isNat#(n__0()) -> c_21()
          28: isNatIList#(X) -> c_25()
          29: isNatIList#(n__zeros()) -> c_27()
          30: isNatList#(X) -> c_28()
          31: isNatList#(n__nil()) -> c_30()
          32: length#(X) -> c_32()
          33: nil#() -> c_33()
          34: s#(X) -> c_34()
          35: take#(X1,X2) -> c_35()
          36: zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          37: zeros#() -> c_37()
* Step 7: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            and#(tt(),X) -> c_18(activate#(X))
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
        - Weak DPs:
            0#() -> c_1()
            U21#(tt()) -> c_3(nil#())
            activate#(X) -> c_5()
            activate#(n__0()) -> c_6(0#())
            activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
            activate#(n__length(X)) -> c_12(length#(X))
            activate#(n__nil()) -> c_13(nil#())
            activate#(n__s(X)) -> c_14(s#(X))
            activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
            activate#(n__zeros()) -> c_16(zeros#())
            and#(X1,X2) -> c_17()
            cons#(X1,X2) -> c_19()
            isNat#(X) -> c_20()
            isNat#(n__0()) -> c_21()
            isNatIList#(X) -> c_25()
            isNatIList#(n__zeros()) -> c_27()
            isNatList#(X) -> c_28()
            isNatList#(n__nil()) -> c_30()
            length#(X) -> c_32()
            nil#() -> c_33()
            s#(X) -> c_34()
            take#(X1,X2) -> c_35()
            zeros#() -> c_36(cons#(0(),n__zeros()),0#())
            zeros#() -> c_37()
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
             -->_3 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_3 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_3 activate#(n__nil()) -> c_13(nil#()):20
             -->_3 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_3 activate#(n__0()) -> c_6(0#()):17
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_1 s#(X) -> c_34():34
             -->_2 length#(X) -> c_32():32
             -->_3 activate#(X) -> c_5():16
          
          2:S:U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                      ,activate#(N)
                                      ,activate#(M)
                                      ,activate#(IL))
             -->_4 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_3 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_2 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_4 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_3 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_2 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_4 activate#(n__nil()) -> c_13(nil#()):20
             -->_3 activate#(n__nil()) -> c_13(nil#()):20
             -->_2 activate#(n__nil()) -> c_13(nil#()):20
             -->_4 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_3 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_2 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_4 activate#(n__0()) -> c_6(0#()):17
             -->_3 activate#(n__0()) -> c_6(0#()):17
             -->_2 activate#(n__0()) -> c_6(0#()):17
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_1 cons#(X1,X2) -> c_19():25
             -->_4 activate#(X) -> c_5():16
             -->_3 activate#(X) -> c_5():16
             -->_2 activate#(X) -> c_5():16
          
          3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_1 and#(X1,X2) -> c_17():24
          
          4:S:activate#(n__isNat(X)) -> c_9(isNat#(X))
             -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 isNat#(n__0()) -> c_21():27
             -->_1 isNat#(X) -> c_20():26
          
          5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
             -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                      ,isNat#(activate(V1))
                                                      ,activate#(V1)
                                                      ,activate#(V2)):11
             -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10
             -->_1 isNatIList#(n__zeros()) -> c_27():29
             -->_1 isNatIList#(X) -> c_25():28
          
          6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X))
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
             -->_1 isNatList#(n__nil()) -> c_30():31
             -->_1 isNatList#(X) -> c_28():30
          
          7:S:and#(tt(),X) -> c_18(activate#(X))
             -->_1 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_1 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_1 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_1 activate#(n__nil()) -> c_13(nil#()):20
             -->_1 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_1 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_1 activate#(n__0()) -> c_6(0#()):17
             -->_1 activate#(X) -> c_5():16
             -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
             -->_2 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_2 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_2 activate#(n__nil()) -> c_13(nil#()):20
             -->_2 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_2 activate#(n__0()) -> c_6(0#()):17
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
             -->_1 isNatList#(n__nil()) -> c_30():31
             -->_1 isNatList#(X) -> c_28():30
             -->_2 activate#(X) -> c_5():16
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
             -->_2 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_2 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_2 activate#(n__nil()) -> c_13(nil#()):20
             -->_2 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_2 activate#(n__0()) -> c_6(0#()):17
             -->_1 isNat#(n__0()) -> c_21():27
             -->_1 isNat#(X) -> c_20():26
             -->_2 activate#(X) -> c_5():16
             -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
             -->_2 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_2 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_2 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_2 activate#(n__nil()) -> c_13(nil#()):20
             -->_2 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_2 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_2 activate#(n__0()) -> c_6(0#()):17
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
             -->_1 isNatList#(n__nil()) -> c_30():31
             -->_1 isNatList#(X) -> c_28():30
             -->_2 activate#(X) -> c_5():16
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                  ,isNat#(activate(V1))
                                                  ,activate#(V1)
                                                  ,activate#(V2))
             -->_4 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_3 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_4 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_3 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_4 activate#(n__nil()) -> c_13(nil#()):20
             -->_3 activate#(n__nil()) -> c_13(nil#()):20
             -->_4 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_3 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_4 activate#(n__0()) -> c_6(0#()):17
             -->_3 activate#(n__0()) -> c_6(0#()):17
             -->_2 isNat#(n__0()) -> c_21():27
             -->_2 isNat#(X) -> c_20():26
             -->_1 and#(X1,X2) -> c_17():24
             -->_4 activate#(X) -> c_5():16
             -->_3 activate#(X) -> c_5():16
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
             -->_4 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_3 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_4 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_3 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_4 activate#(n__nil()) -> c_13(nil#()):20
             -->_3 activate#(n__nil()) -> c_13(nil#()):20
             -->_4 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_3 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_4 activate#(n__0()) -> c_6(0#()):17
             -->_3 activate#(n__0()) -> c_6(0#()):17
             -->_2 isNat#(n__0()) -> c_21():27
             -->_2 isNat#(X) -> c_20():26
             -->_1 and#(X1,X2) -> c_17():24
             -->_4 activate#(X) -> c_5():16
             -->_3 activate#(X) -> c_5():16
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
             -->_4 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_3 activate#(n__zeros()) -> c_16(zeros#()):23
             -->_4 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_3 activate#(n__take(X1,X2)) -> c_15(take#(X1,X2)):22
             -->_4 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_3 activate#(n__s(X)) -> c_14(s#(X)):21
             -->_4 activate#(n__nil()) -> c_13(nil#()):20
             -->_3 activate#(n__nil()) -> c_13(nil#()):20
             -->_4 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_3 activate#(n__length(X)) -> c_12(length#(X)):19
             -->_4 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_3 activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2)):18
             -->_4 activate#(n__0()) -> c_6(0#()):17
             -->_3 activate#(n__0()) -> c_6(0#()):17
             -->_2 isNat#(n__0()) -> c_21():27
             -->_2 isNat#(X) -> c_20():26
             -->_1 and#(X1,X2) -> c_17():24
             -->_4 activate#(X) -> c_5():16
             -->_3 activate#(X) -> c_5():16
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          14:W:0#() -> c_1()
             
          
          15:W:U21#(tt()) -> c_3(nil#())
             -->_1 nil#() -> c_33():33
          
          16:W:activate#(X) -> c_5()
             
          
          17:W:activate#(n__0()) -> c_6(0#())
             -->_1 0#() -> c_1():14
          
          18:W:activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
             -->_1 cons#(X1,X2) -> c_19():25
          
          19:W:activate#(n__length(X)) -> c_12(length#(X))
             -->_1 length#(X) -> c_32():32
          
          20:W:activate#(n__nil()) -> c_13(nil#())
             -->_1 nil#() -> c_33():33
          
          21:W:activate#(n__s(X)) -> c_14(s#(X))
             -->_1 s#(X) -> c_34():34
          
          22:W:activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
             -->_1 take#(X1,X2) -> c_35():35
          
          23:W:activate#(n__zeros()) -> c_16(zeros#())
             -->_1 zeros#() -> c_36(cons#(0(),n__zeros()),0#()):36
             -->_1 zeros#() -> c_37():37
          
          24:W:and#(X1,X2) -> c_17()
             
          
          25:W:cons#(X1,X2) -> c_19()
             
          
          26:W:isNat#(X) -> c_20()
             
          
          27:W:isNat#(n__0()) -> c_21()
             
          
          28:W:isNatIList#(X) -> c_25()
             
          
          29:W:isNatIList#(n__zeros()) -> c_27()
             
          
          30:W:isNatList#(X) -> c_28()
             
          
          31:W:isNatList#(n__nil()) -> c_30()
             
          
          32:W:length#(X) -> c_32()
             
          
          33:W:nil#() -> c_33()
             
          
          34:W:s#(X) -> c_34()
             
          
          35:W:take#(X1,X2) -> c_35()
             
          
          36:W:zeros#() -> c_36(cons#(0(),n__zeros()),0#())
             -->_1 cons#(X1,X2) -> c_19():25
             -->_2 0#() -> c_1():14
          
          37:W:zeros#() -> c_37()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          15: U21#(tt()) -> c_3(nil#())
          28: isNatIList#(X) -> c_25()
          29: isNatIList#(n__zeros()) -> c_27()
          30: isNatList#(X) -> c_28()
          31: isNatList#(n__nil()) -> c_30()
          16: activate#(X) -> c_5()
          24: and#(X1,X2) -> c_17()
          26: isNat#(X) -> c_20()
          27: isNat#(n__0()) -> c_21()
          17: activate#(n__0()) -> c_6(0#())
          18: activate#(n__cons(X1,X2)) -> c_8(cons#(X1,X2))
          19: activate#(n__length(X)) -> c_12(length#(X))
          32: length#(X) -> c_32()
          20: activate#(n__nil()) -> c_13(nil#())
          33: nil#() -> c_33()
          21: activate#(n__s(X)) -> c_14(s#(X))
          34: s#(X) -> c_34()
          22: activate#(n__take(X1,X2)) -> c_15(take#(X1,X2))
          35: take#(X1,X2) -> c_35()
          23: activate#(n__zeros()) -> c_16(zeros#())
          37: zeros#() -> c_37()
          36: zeros#() -> c_36(cons#(0(),n__zeros()),0#())
          14: 0#() -> c_1()
          25: cons#(X1,X2) -> c_19()
* Step 8: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
            U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                    ,activate#(N)
                                    ,activate#(M)
                                    ,activate#(IL))
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            and#(tt(),X) -> c_18(activate#(X))
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/3,c_3/1,c_4/4,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:U11#(tt(),L) -> c_2(s#(length(activate(L))),length#(activate(L)),activate#(L))
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          2:S:U31#(tt(),IL,M,N) -> c_4(cons#(activate(N),n__take(activate(M),activate(IL)))
                                      ,activate#(N)
                                      ,activate#(M)
                                      ,activate#(IL))
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
          
          4:S:activate#(n__isNat(X)) -> c_9(isNat#(X))
             -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
          
          5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
             -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                      ,isNat#(activate(V1))
                                                      ,activate#(V1)
                                                      ,activate#(V2)):11
             -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10
          
          6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X))
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
          
          7:S:and#(tt(),X) -> c_18(activate#(X))
             -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
             -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
             -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):13
             -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                     ,isNat#(activate(V1))
                                                     ,activate#(V1)
                                                     ,activate#(V2)):12
             -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                  ,isNat#(activate(V1))
                                                  ,activate#(V1)
                                                  ,activate#(V2))
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
          13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                 ,isNat#(activate(V1))
                                                 ,activate#(V1)
                                                 ,activate#(V2))
             -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
             -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
             -->_1 and#(tt(),X) -> c_18(activate#(X)):7
             -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
             -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
             -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
             -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
             -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          U11#(tt(),L) -> c_2(activate#(L))
          U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL))
* Step 9: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            U11#(tt(),L) -> c_2(activate#(L))
            U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL))
            activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
            activate#(n__isNat(X)) -> c_9(isNat#(X))
            activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
            activate#(n__isNatList(X)) -> c_11(isNatList#(X))
            and#(tt(),X) -> c_18(activate#(X))
            isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
            isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
            isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
            isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
            isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
            isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                              ,isNat#(activate(V1))
                                              ,activate#(V1)
                                              ,activate#(V2))
        - Weak TRS:
            0() -> n__0()
            activate(X) -> X
            activate(n__0()) -> 0()
            activate(n__and(X1,X2)) -> and(X1,X2)
            activate(n__cons(X1,X2)) -> cons(X1,X2)
            activate(n__isNat(X)) -> isNat(X)
            activate(n__isNatIList(X)) -> isNatIList(X)
            activate(n__isNatList(X)) -> isNatList(X)
            activate(n__length(X)) -> length(X)
            activate(n__nil()) -> nil()
            activate(n__s(X)) -> s(X)
            activate(n__take(X1,X2)) -> take(X1,X2)
            activate(n__zeros()) -> zeros()
            and(X1,X2) -> n__and(X1,X2)
            and(tt(),X) -> activate(X)
            cons(X1,X2) -> n__cons(X1,X2)
            isNat(X) -> n__isNat(X)
            isNat(n__0()) -> tt()
            isNat(n__length(V1)) -> isNatList(activate(V1))
            isNat(n__s(V1)) -> isNat(activate(V1))
            isNatIList(V) -> isNatList(activate(V))
            isNatIList(X) -> n__isNatIList(X)
            isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            isNatIList(n__zeros()) -> tt()
            isNatList(X) -> n__isNatList(X)
            isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
            isNatList(n__nil()) -> tt()
            isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
            length(X) -> n__length(X)
            nil() -> n__nil()
            s(X) -> n__s(X)
            take(X1,X2) -> n__take(X1,X2)
            zeros() -> cons(0(),n__zeros())
            zeros() -> n__zeros()
        - Signature:
            {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
            ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
            ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
            ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/1,c_3/1,c_4/3,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
            ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
            ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
            ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
            ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:U11#(tt(),L) -> c_2(activate#(L))
           -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        2:S:U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL))
           -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
           -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
           -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        3:S:activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
           -->_1 and#(tt(),X) -> c_18(activate#(X)):7
        
        4:S:activate#(n__isNat(X)) -> c_9(isNat#(X))
           -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
           -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
        
        5:S:activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
           -->_1 isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                    ,isNat#(activate(V1))
                                                    ,activate#(V1)
                                                    ,activate#(V2)):11
           -->_1 isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V)):10
        
        6:S:activate#(n__isNatList(X)) -> c_11(isNatList#(X))
           -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):13
           -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):12
        
        7:S:and#(tt(),X) -> c_18(activate#(X))
           -->_1 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_1 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_1 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_1 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        8:S:isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
           -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):13
           -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):12
           -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        9:S:isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
           -->_1 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
           -->_1 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
           -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        10:S:isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
           -->_1 isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):13
           -->_1 isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                                   ,isNat#(activate(V1))
                                                   ,activate#(V1)
                                                   ,activate#(V2)):12
           -->_2 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_2 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_2 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_2 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        11:S:isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                                ,isNat#(activate(V1))
                                                ,activate#(V1)
                                                ,activate#(V2))
           -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
           -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
           -->_1 and#(tt(),X) -> c_18(activate#(X)):7
           -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
           -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        12:S:isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
           -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
           -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
           -->_1 and#(tt(),X) -> c_18(activate#(X)):7
           -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
           -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        13:S:isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                               ,isNat#(activate(V1))
                                               ,activate#(V1)
                                               ,activate#(V2))
           -->_2 isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1)):9
           -->_2 isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1)):8
           -->_1 and#(tt(),X) -> c_18(activate#(X)):7
           -->_4 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_3 activate#(n__isNatList(X)) -> c_11(isNatList#(X)):6
           -->_4 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_3 activate#(n__isNatIList(X)) -> c_10(isNatIList#(X)):5
           -->_4 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_3 activate#(n__isNat(X)) -> c_9(isNat#(X)):4
           -->_4 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
           -->_3 activate#(n__and(X1,X2)) -> c_7(and#(X1,X2)):3
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(1,U11#(tt(),L) -> c_2(activate#(L)))
        ,(2,U31#(tt(),IL,M,N) -> c_4(activate#(N),activate#(M),activate#(IL)))]
* Step 10: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          activate#(n__and(X1,X2)) -> c_7(and#(X1,X2))
          activate#(n__isNat(X)) -> c_9(isNat#(X))
          activate#(n__isNatIList(X)) -> c_10(isNatIList#(X))
          activate#(n__isNatList(X)) -> c_11(isNatList#(X))
          and#(tt(),X) -> c_18(activate#(X))
          isNat#(n__length(V1)) -> c_22(isNatList#(activate(V1)),activate#(V1))
          isNat#(n__s(V1)) -> c_23(isNat#(activate(V1)),activate#(V1))
          isNatIList#(V) -> c_24(isNatList#(activate(V)),activate#(V))
          isNatIList#(n__cons(V1,V2)) -> c_26(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                             ,isNat#(activate(V1))
                                             ,activate#(V1)
                                             ,activate#(V2))
          isNatList#(n__cons(V1,V2)) -> c_29(and#(isNat(activate(V1)),n__isNatList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
          isNatList#(n__take(V1,V2)) -> c_31(and#(isNat(activate(V1)),n__isNatIList(activate(V2)))
                                            ,isNat#(activate(V1))
                                            ,activate#(V1)
                                            ,activate#(V2))
      - Weak TRS:
          0() -> n__0()
          activate(X) -> X
          activate(n__0()) -> 0()
          activate(n__and(X1,X2)) -> and(X1,X2)
          activate(n__cons(X1,X2)) -> cons(X1,X2)
          activate(n__isNat(X)) -> isNat(X)
          activate(n__isNatIList(X)) -> isNatIList(X)
          activate(n__isNatList(X)) -> isNatList(X)
          activate(n__length(X)) -> length(X)
          activate(n__nil()) -> nil()
          activate(n__s(X)) -> s(X)
          activate(n__take(X1,X2)) -> take(X1,X2)
          activate(n__zeros()) -> zeros()
          and(X1,X2) -> n__and(X1,X2)
          and(tt(),X) -> activate(X)
          cons(X1,X2) -> n__cons(X1,X2)
          isNat(X) -> n__isNat(X)
          isNat(n__0()) -> tt()
          isNat(n__length(V1)) -> isNatList(activate(V1))
          isNat(n__s(V1)) -> isNat(activate(V1))
          isNatIList(V) -> isNatList(activate(V))
          isNatIList(X) -> n__isNatIList(X)
          isNatIList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
          isNatIList(n__zeros()) -> tt()
          isNatList(X) -> n__isNatList(X)
          isNatList(n__cons(V1,V2)) -> and(isNat(activate(V1)),n__isNatList(activate(V2)))
          isNatList(n__nil()) -> tt()
          isNatList(n__take(V1,V2)) -> and(isNat(activate(V1)),n__isNatIList(activate(V2)))
          length(X) -> n__length(X)
          nil() -> n__nil()
          s(X) -> n__s(X)
          take(X1,X2) -> n__take(X1,X2)
          zeros() -> cons(0(),n__zeros())
          zeros() -> n__zeros()
      - Signature:
          {0/0,U11/2,U21/1,U31/4,activate/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2
          ,zeros/0,0#/0,U11#/2,U21#/1,U31#/4,activate#/1,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1
          ,nil#/0,s#/1,take#/2,zeros#/0} / {n__0/0,n__and/2,n__cons/2,n__isNat/1,n__isNatIList/1,n__isNatList/1
          ,n__length/1,n__nil/0,n__s/1,n__take/2,n__zeros/0,tt/0,c_1/0,c_2/1,c_3/1,c_4/3,c_5/0,c_6/1,c_7/1,c_8/1,c_9/1
          ,c_10/1,c_11/1,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/1,c_19/0,c_20/0,c_21/0,c_22/2,c_23/2,c_24/2
          ,c_25/0,c_26/4,c_27/0,c_28/0,c_29/4,c_30/0,c_31/4,c_32/0,c_33/0,c_34/0,c_35/0,c_36/2,c_37/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {0#,U11#,U21#,U31#,activate#,and#,cons#,isNat#,isNatIList#
          ,isNatList#,length#,nil#,s#,take#,zeros#} and constructors {n__0,n__and,n__cons,n__isNat,n__isNatIList
          ,n__isNatList,n__length,n__nil,n__s,n__take,n__zeros,tt}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE