(VAR N XS YS ZS X Y)
(RULES 
U11(tt) -> U12(splitAt(N,XS))
U12(pair(YS,ZS)) -> pair(cons(X),ZS)
afterNth(N,XS) -> snd(splitAt(N,XS))
and(tt) -> X
fst(pair(X,Y)) -> X
head(cons(N)) -> N
natsFrom(N) -> cons(N)
sel(N,XS) -> head(afterNth(N,XS))
snd(pair(X,Y)) -> Y
splitAt(0,XS) -> pair(nil,XS)
splitAt(s(N),cons(X)) -> U11(tt)
tail(cons(N)) -> XS
take(N,XS) -> fst(splitAt(N,XS))
)