(VAR N X XS Y YS ZS )
(RULES 
        U12(tt) -> snd(splitAt(N, XS))
        U161(tt) -> cons(N)
        U172(tt) -> head(afterNth(N, XS))
        U182(tt) -> Y
        U191(tt) -> pair(nil, XS)
        U203(tt) -> U204(splitAt(N, XS))
        U204(pair(YS, ZS)) -> pair(cons(X), ZS)
        U212(tt) -> XS
        U22(tt) -> X
        U222(tt) -> fst(splitAt(N, XS))
        U32(tt) -> N
        U101(tt) -> U102(isLNat)
        U102(tt) -> tt
        U11(tt) -> U12(isLNat)
        U111(tt) -> tt
        U121(tt) -> tt
        U131(tt) -> U132(isLNat)
        U132(tt) -> tt
        U141(tt) -> U142(isLNat)
        U142(tt) -> tt
        U151(tt) -> U152(isLNat)
        U152(tt) -> tt
        U171(tt) -> U172(isLNat)
        U181(tt) -> U182(isLNat)
        U201(tt) -> U202(isNatural)
        U202(tt) -> U203(isLNat)
        U21(tt) -> U22(isLNat)
        U211(tt) -> U212(isLNat)
        U221(tt) -> U222(isLNat)
        U31(tt) -> U32(isLNat)
        U41(tt) -> U42(isLNat)
        U42(tt) -> tt
        U51(tt) -> U52(isLNat)
        U52(tt) -> tt
        U61(tt) -> tt
        U71(tt) -> tt
        U81(tt) -> tt
        U91(tt) -> tt
        afterNth(N, XS) -> U11(isNatural)
        fst(pair(X, Y)) -> U21(isLNat)
        head(cons(N)) -> U31(isNatural)
        isLNat -> tt
        isLNat -> U41(isNatural)
        isLNat -> U51(isNatural)
        isLNat -> U61(isPLNat)
        isLNat -> U71(isNatural)
        isLNat -> U81(isPLNat)
        isLNat -> U91(isLNat)
        isLNat -> U101(isNatural)
        isNatural -> tt
        isNatural -> U111(isLNat)
        isNatural -> U121(isNatural)
        isNatural -> U131(isNatural)
        isPLNat -> U141(isLNat)
        isPLNat -> U151(isNatural)
        natsFrom(N) -> U161(isNatural)
        sel(N, XS) -> U171(isNatural)
        snd(pair(X, Y)) -> U181(isLNat)
        splitAt(0, XS) -> U191(isLNat)
        splitAt(s(N), cons(X)) -> U201(isNatural)
        tail(cons(N)) -> U211(isNatural)
        take(N, XS) -> U221(isNatural)
        
)