(VAR N X XS Y YS ZS )
(RULES 
        U101(tt) -> fst(splitAt(N, XS))
        U11(tt) -> snd(splitAt(N, XS))
        U21(tt) -> X
        U31(tt) -> N
        U41(tt) -> cons(N)
        U51(tt) -> head(afterNth(N, XS))
        U61(tt) -> Y
        U71(tt) -> pair(nil, XS)
        U81(tt) -> U82(splitAt(N, XS))
        U82(pair(YS, ZS)) -> pair(cons(X), ZS)
        U91(tt) -> XS
        and(tt) -> X
        afterNth(N, XS) -> U11(and(isNatural))
        fst(pair(X, Y)) -> U21(and(isLNat))
        head(cons(N)) -> U31(and(isNatural))
        isLNat -> tt
        isLNat -> and(isNatural)
        isLNat -> isPLNat
        isLNat -> isNatural
        isLNat -> isLNat
        isNatural -> tt
        isNatural -> isLNat
        isNatural -> isNatural
        isNatural -> and(isNatural)
        isPLNat -> and(isLNat)
        isPLNat -> and(isNatural)
        natsFrom(N) -> U41(isNatural)
        sel(N, XS) -> U51(and(isNatural))
        snd(pair(X, Y)) -> U61(and(isLNat))
        splitAt(0, XS) -> U71(isLNat)
        splitAt(s(N), cons(X)) -> U81(and(isNatural))
        tail(cons(N)) -> U91(and(isNatural))
        take(N, XS) -> U101(and(isNatural))
        
)