(VAR N V1 V2 X XS Y YS ZS )
(STRATEGY CONTEXTSENSITIVE
        (U101 1) 
        (tt ) 
        (U102 1) 
        (isNaturalKind ) 
        (U103 1) 
        (isLNatKind ) 
        (U104 1) 
        (U105 1) 
        (isNatural ) 
        (U106 1) 
        (isLNat ) 
        (U11 1) 
        (U12 1) 
        (U111 1) 
        (U112 1) 
        (U13 1) 
        (U121 1) 
        (U122 1) 
        (U14 1) 
        (U131 1) 
        (snd 1) 
        (splitAt 1 2) 
        (U141 1) 
        (U151 1) 
        (U161 1) 
        (U171 1) 
        (U172 1) 
        (U181 1) 
        (U182 1) 
        (U183 1) 
        (U191 1) 
        (U192 1) 
        (U193 1) 
        (U201 1) 
        (U202 1) 
        (U203 1) 
        (U204 1) 
        (U205 1) 
        (U206 1) 
        (U21 1) 
        (U22 1) 
        (U211 1) 
        (U23 1) 
        (U221 1) 
        (U24 1) 
        (U231 1) 
        (U232 1) 
        (U241 1) 
        (U242 1) 
        (U243 1) 
        (U244 1) 
        (U245 1) 
        (U246 1) 
        (U251 1) 
        (U252 1) 
        (U253 1) 
        (U254 1) 
        (U255 1) 
        (U256 1) 
        (U261 1) 
        (U262 1) 
        (U271 1) 
        (U272 1) 
        (U281 1) 
        (U282 1) 
        (cons 1) 
        (natsFrom 1) 
        (s 1) 
        (U291 1) 
        (U292 1) 
        (U293 1) 
        (U294 1) 
        (head 1) 
        (afterNth 1 2) 
        (U301 1) 
        (U302 1) 
        (U303 1) 
        (U304 1) 
        (U31 1) 
        (U32 1) 
        (U311 1) 
        (U312 1) 
        (pair 1 2) 
        (nil ) 
        (U33 1) 
        (U321 1) 
        (U322 1) 
        (U323 1) 
        (U324 1) 
        (U325 1) 
        (U326 1) 
        (U327 1) 
        (U34 1) 
        (U331 1) 
        (U332 1) 
        (U333 1) 
        (U334 1) 
        (U341 1) 
        (U342 1) 
        (U343 1) 
        (U344 1) 
        (fst 1) 
        (U41 1) 
        (U42 1) 
        (U43 1) 
        (U44 1) 
        (U45 1) 
        (U46 1) 
        (U51 1) 
        (U52 1) 
        (U53 1) 
        (U54 1) 
        (U55 1) 
        (U56 1) 
        (U61 1) 
        (U62 1) 
        (isPLNatKind ) 
        (U63 1) 
        (isPLNat ) 
        (U71 1) 
        (U72 1) 
        (U73 1) 
        (U81 1) 
        (U82 1) 
        (U83 1) 
        (U91 1) 
        (U92 1) 
        (U93 1) 
        (tail 1) 
        (take 1 2) 
        (0 ) 
        (sel 1 2) 
)
(RULES 
        U101(tt, V1, V2) -> U102(isNaturalKind(V1), V1, V2)
        U102(tt, V1, V2) -> U103(isLNatKind(V2), V1, V2)
        U103(tt, V1, V2) -> U104(isLNatKind(V2), V1, V2)
        U104(tt, V1, V2) -> U105(isNatural(V1), V2)
        U105(tt, V2) -> U106(isLNat(V2))
        U106(tt) -> tt
        U11(tt, N, XS) -> U12(isNaturalKind(N), N, XS)
        U111(tt, V2) -> U112(isLNatKind(V2))
        U112(tt) -> tt
        U12(tt, N, XS) -> U13(isLNat(XS), N, XS)
        U121(tt, V2) -> U122(isLNatKind(V2))
        U122(tt) -> tt
        U13(tt, N, XS) -> U14(isLNatKind(XS), N, XS)
        U131(tt) -> tt
        U14(tt, N, XS) -> snd(splitAt(N, XS))
        U141(tt) -> tt
        U151(tt) -> tt
        U161(tt) -> tt
        U171(tt, V2) -> U172(isLNatKind(V2))
        U172(tt) -> tt
        U181(tt, V1) -> U182(isLNatKind(V1), V1)
        U182(tt, V1) -> U183(isLNat(V1))
        U183(tt) -> tt
        U191(tt, V1) -> U192(isNaturalKind(V1), V1)
        U192(tt, V1) -> U193(isNatural(V1))
        U193(tt) -> tt
        U201(tt, V1, V2) -> U202(isNaturalKind(V1), V1, V2)
        U202(tt, V1, V2) -> U203(isLNatKind(V2), V1, V2)
        U203(tt, V1, V2) -> U204(isLNatKind(V2), V1, V2)
        U204(tt, V1, V2) -> U205(isNatural(V1), V2)
        U205(tt, V2) -> U206(isLNat(V2))
        U206(tt) -> tt
        U21(tt, X, Y) -> U22(isLNatKind(X), X, Y)
        U211(tt) -> tt
        U22(tt, X, Y) -> U23(isLNat(Y), X, Y)
        U221(tt) -> tt
        U23(tt, X, Y) -> U24(isLNatKind(Y), X)
        U231(tt, V2) -> U232(isLNatKind(V2))
        U232(tt) -> tt
        U24(tt, X) -> X
        U241(tt, V1, V2) -> U242(isLNatKind(V1), V1, V2)
        U242(tt, V1, V2) -> U243(isLNatKind(V2), V1, V2)
        U243(tt, V1, V2) -> U244(isLNatKind(V2), V1, V2)
        U244(tt, V1, V2) -> U245(isLNat(V1), V2)
        U245(tt, V2) -> U246(isLNat(V2))
        U246(tt) -> tt
        U251(tt, V1, V2) -> U252(isNaturalKind(V1), V1, V2)
        U252(tt, V1, V2) -> U253(isLNatKind(V2), V1, V2)
        U253(tt, V1, V2) -> U254(isLNatKind(V2), V1, V2)
        U254(tt, V1, V2) -> U255(isNatural(V1), V2)
        U255(tt, V2) -> U256(isLNat(V2))
        U256(tt) -> tt
        U261(tt, V2) -> U262(isLNatKind(V2))
        U262(tt) -> tt
        U271(tt, V2) -> U272(isLNatKind(V2))
        U272(tt) -> tt
        U281(tt, N) -> U282(isNaturalKind(N), N)
        U282(tt, N) -> cons(N, natsFrom(s(N)))
        U291(tt, N, XS) -> U292(isNaturalKind(N), N, XS)
        U292(tt, N, XS) -> U293(isLNat(XS), N, XS)
        U293(tt, N, XS) -> U294(isLNatKind(XS), N, XS)
        U294(tt, N, XS) -> head(afterNth(N, XS))
        U301(tt, X, Y) -> U302(isLNatKind(X), Y)
        U302(tt, Y) -> U303(isLNat(Y), Y)
        U303(tt, Y) -> U304(isLNatKind(Y), Y)
        U304(tt, Y) -> Y
        U31(tt, N, XS) -> U32(isNaturalKind(N), N, XS)
        U311(tt, XS) -> U312(isLNatKind(XS), XS)
        U312(tt, XS) -> pair(nil, XS)
        U32(tt, N, XS) -> U33(isLNat(XS), N, XS)
        U321(tt, N, X, XS) -> U322(isNaturalKind(N), N, X, XS)
        U322(tt, N, X, XS) -> U323(isNatural(X), N, X, XS)
        U323(tt, N, X, XS) -> U324(isNaturalKind(X), N, X, XS)
        U324(tt, N, X, XS) -> U325(isLNat(XS), N, X, XS)
        U325(tt, N, X, XS) -> U326(isLNatKind(XS), N, X, XS)
        U326(tt, N, X, XS) -> U327(splitAt(N, XS), X)
        U327(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
        U33(tt, N, XS) -> U34(isLNatKind(XS), N)
        U331(tt, N, XS) -> U332(isNaturalKind(N), XS)
        U332(tt, XS) -> U333(isLNat(XS), XS)
        U333(tt, XS) -> U334(isLNatKind(XS), XS)
        U334(tt, XS) -> XS
        U34(tt, N) -> N
        U341(tt, N, XS) -> U342(isNaturalKind(N), N, XS)
        U342(tt, N, XS) -> U343(isLNat(XS), N, XS)
        U343(tt, N, XS) -> U344(isLNatKind(XS), N, XS)
        U344(tt, N, XS) -> fst(splitAt(N, XS))
        U41(tt, V1, V2) -> U42(isNaturalKind(V1), V1, V2)
        U42(tt, V1, V2) -> U43(isLNatKind(V2), V1, V2)
        U43(tt, V1, V2) -> U44(isLNatKind(V2), V1, V2)
        U44(tt, V1, V2) -> U45(isNatural(V1), V2)
        U45(tt, V2) -> U46(isLNat(V2))
        U46(tt) -> tt
        U51(tt, V1, V2) -> U52(isNaturalKind(V1), V1, V2)
        U52(tt, V1, V2) -> U53(isLNatKind(V2), V1, V2)
        U53(tt, V1, V2) -> U54(isLNatKind(V2), V1, V2)
        U54(tt, V1, V2) -> U55(isNatural(V1), V2)
        U55(tt, V2) -> U56(isLNat(V2))
        U56(tt) -> tt
        U61(tt, V1) -> U62(isPLNatKind(V1), V1)
        U62(tt, V1) -> U63(isPLNat(V1))
        U63(tt) -> tt
        U71(tt, V1) -> U72(isNaturalKind(V1), V1)
        U72(tt, V1) -> U73(isNatural(V1))
        U73(tt) -> tt
        U81(tt, V1) -> U82(isPLNatKind(V1), V1)
        U82(tt, V1) -> U83(isPLNat(V1))
        U83(tt) -> tt
        U91(tt, V1) -> U92(isLNatKind(V1), V1)
        U92(tt, V1) -> U93(isLNat(V1))
        U93(tt) -> tt
        afterNth(N, XS) -> U11(isNatural(N), N, XS)
        fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
        head(cons(N, XS)) -> U31(isNatural(N), N, XS)
        isLNat(nil) -> tt
        isLNat(afterNth(V1, V2)) -> U41(isNaturalKind(V1), V1, V2)
        isLNat(cons(V1, V2)) -> U51(isNaturalKind(V1), V1, V2)
        isLNat(fst(V1)) -> U61(isPLNatKind(V1), V1)
        isLNat(natsFrom(V1)) -> U71(isNaturalKind(V1), V1)
        isLNat(snd(V1)) -> U81(isPLNatKind(V1), V1)
        isLNat(tail(V1)) -> U91(isLNatKind(V1), V1)
        isLNat(take(V1, V2)) -> U101(isNaturalKind(V1), V1, V2)
        isLNatKind(nil) -> tt
        isLNatKind(afterNth(V1, V2)) -> U111(isNaturalKind(V1), V2)
        isLNatKind(cons(V1, V2)) -> U121(isNaturalKind(V1), V2)
        isLNatKind(fst(V1)) -> U131(isPLNatKind(V1))
        isLNatKind(natsFrom(V1)) -> U141(isNaturalKind(V1))
        isLNatKind(snd(V1)) -> U151(isPLNatKind(V1))
        isLNatKind(tail(V1)) -> U161(isLNatKind(V1))
        isLNatKind(take(V1, V2)) -> U171(isNaturalKind(V1), V2)
        isNatural(0) -> tt
        isNatural(head(V1)) -> U181(isLNatKind(V1), V1)
        isNatural(s(V1)) -> U191(isNaturalKind(V1), V1)
        isNatural(sel(V1, V2)) -> U201(isNaturalKind(V1), V1, V2)
        isNaturalKind(0) -> tt
        isNaturalKind(head(V1)) -> U211(isLNatKind(V1))
        isNaturalKind(s(V1)) -> U221(isNaturalKind(V1))
        isNaturalKind(sel(V1, V2)) -> U231(isNaturalKind(V1), V2)
        isPLNat(pair(V1, V2)) -> U241(isLNatKind(V1), V1, V2)
        isPLNat(splitAt(V1, V2)) -> U251(isNaturalKind(V1), V1, V2)
        isPLNatKind(pair(V1, V2)) -> U261(isLNatKind(V1), V2)
        isPLNatKind(splitAt(V1, V2)) -> U271(isNaturalKind(V1), V2)
        natsFrom(N) -> U281(isNatural(N), N)
        sel(N, XS) -> U291(isNatural(N), N, XS)
        snd(pair(X, Y)) -> U301(isLNat(X), X, Y)
        splitAt(0, XS) -> U311(isLNat(XS), XS)
        splitAt(s(N), cons(X, XS)) -> U321(isNatural(N), N, X, XS)
        tail(cons(N, XS)) -> U331(isNatural(N), N, XS)
        take(N, XS) -> U341(isNatural(N), N, XS)
        
)