(VAR L N V V1 V2 )
(STRATEGY CONTEXTSENSITIVE
        (zeros ) 
        (cons 1) 
        (0 ) 
        (U11 1) 
        (tt ) 
        (U12 1) 
        (isNatIListKind ) 
        (U13 1) 
        (isNatList ) 
        (U21 1) 
        (U22 1) 
        (isNatKind ) 
        (U23 1) 
        (isNat ) 
        (U31 1) 
        (U32 1) 
        (U33 1) 
        (U41 1) 
        (U42 1) 
        (U43 1) 
        (U44 1) 
        (U45 1) 
        (U46 1) 
        (isNatIList ) 
        (U51 1) 
        (U52 1) 
        (U61 1) 
        (U71 1) 
        (U81 1) 
        (U82 1) 
        (U83 1) 
        (U84 1) 
        (U85 1) 
        (U86 1) 
        (U91 1) 
        (U92 1) 
        (U93 1) 
        (U94 1) 
        (s 1) 
        (length 1) 
        (nil ) 
)
(RULES 
        zeros -> cons(0, zeros)
        U11(tt, V1) -> U12(isNatIListKind(V1), V1)
        U12(tt, V1) -> U13(isNatList(V1))
        U13(tt) -> tt
        U21(tt, V1) -> U22(isNatKind(V1), V1)
        U22(tt, V1) -> U23(isNat(V1))
        U23(tt) -> tt
        U31(tt, V) -> U32(isNatIListKind(V), V)
        U32(tt, V) -> U33(isNatList(V))
        U33(tt) -> tt
        U41(tt, V1, V2) -> U42(isNatKind(V1), V1, V2)
        U42(tt, V1, V2) -> U43(isNatIListKind(V2), V1, V2)
        U43(tt, V1, V2) -> U44(isNatIListKind(V2), V1, V2)
        U44(tt, V1, V2) -> U45(isNat(V1), V2)
        U45(tt, V2) -> U46(isNatIList(V2))
        U46(tt) -> tt
        U51(tt, V2) -> U52(isNatIListKind(V2))
        U52(tt) -> tt
        U61(tt) -> tt
        U71(tt) -> tt
        U81(tt, V1, V2) -> U82(isNatKind(V1), V1, V2)
        U82(tt, V1, V2) -> U83(isNatIListKind(V2), V1, V2)
        U83(tt, V1, V2) -> U84(isNatIListKind(V2), V1, V2)
        U84(tt, V1, V2) -> U85(isNat(V1), V2)
        U85(tt, V2) -> U86(isNatList(V2))
        U86(tt) -> tt
        U91(tt, L, N) -> U92(isNatIListKind(L), L, N)
        U92(tt, L, N) -> U93(isNat(N), L, N)
        U93(tt, L, N) -> U94(isNatKind(N), L)
        U94(tt, L) -> s(length(L))
        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(isNatKind(V1), V1, V2)
        isNatIListKind(nil) -> tt
        isNatIListKind(zeros) -> tt
        isNatIListKind(cons(V1, V2)) -> U51(isNatKind(V1), V2)
        isNatKind(0) -> tt
        isNatKind(length(V1)) -> U61(isNatIListKind(V1))
        isNatKind(s(V1)) -> U71(isNatKind(V1))
        isNatList(nil) -> tt
        isNatList(cons(V1, V2)) -> U81(isNatKind(V1), V1, V2)
        length(nil) -> 0
        length(cons(N, L)) -> U91(isNatList(L), L, N)
        
)