(VAR IL L M N V V1 V2 X )
(STRATEGY CONTEXTSENSITIVE
        (zeros ) 
        (cons 1) 
        (0 ) 
        (U11 1) 
        (tt ) 
        (U12 1) 
        (isNatList ) 
        (U21 1) 
        (U22 1) 
        (isNat ) 
        (U31 1) 
        (U32 1) 
        (U41 1) 
        (U42 1) 
        (U43 1) 
        (isNatIList ) 
        (U51 1) 
        (U52 1) 
        (U53 1) 
        (U61 1) 
        (U62 1) 
        (U63 1) 
        (U71 1) 
        (s 1) 
        (length 1) 
        (U81 1) 
        (nil ) 
        (U91 1) 
        (take 1 2) 
        (and 1) 
        (isNatIListKind ) 
        (isNatKind ) 
)
(RULES 
        zeros -> cons(0, zeros)
        U11(tt, V1) -> U12(isNatList(V1))
        U12(tt) -> tt
        U21(tt, V1) -> U22(isNat(V1))
        U22(tt) -> tt
        U31(tt, V) -> U32(isNatList(V))
        U32(tt) -> tt
        U41(tt, V1, V2) -> U42(isNat(V1), V2)
        U42(tt, V2) -> U43(isNatIList(V2))
        U43(tt) -> tt
        U51(tt, V1, V2) -> U52(isNat(V1), V2)
        U52(tt, V2) -> U53(isNatList(V2))
        U53(tt) -> tt
        U61(tt, V1, V2) -> U62(isNat(V1), V2)
        U62(tt, V2) -> U63(isNatIList(V2))
        U63(tt) -> tt
        U71(tt, L) -> s(length(L))
        U81(tt) -> nil
        U91(tt, IL, M, N) -> cons(N, take(M, IL))
        and(tt, X) -> X
        isNat(0) -> tt
        isNat(length(V1)) -> U11(isNatIListKind(V1), V1)
        isNat(s(V1)) -> U21(isNatKind(V1), V1)
        isNatIList(V) -> U31(isNatIListKind(V), V)
        isNatIList(zeros) -> tt
        isNatIList(cons(V1, V2)) -> U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
        isNatIListKind(nil) -> tt
        isNatIListKind(zeros) -> tt
        isNatIListKind(cons(V1, V2)) -> and(isNatKind(V1), isNatIListKind(V2))
        isNatIListKind(take(V1, V2)) -> and(isNatKind(V1), isNatIListKind(V2))
        isNatKind(0) -> tt
        isNatKind(length(V1)) -> isNatIListKind(V1)
        isNatKind(s(V1)) -> isNatKind(V1)
        isNatList(nil) -> tt
        isNatList(cons(V1, V2)) -> U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
        isNatList(take(V1, V2)) -> U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
        length(nil) -> 0
        length(cons(N, L)) -> U71(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
        take(0, IL) -> U81(and(isNatIList(IL), isNatIListKind(IL)))
        take(s(M), cons(N, IL)) -> U91(and(and(isNatIList(IL), isNatIListKind(IL)), and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), IL, M, N)
        
)