(VAR N XS Y YS ZS X)
(RULES 
U101(tt) -> U102(isLNat)
U102(tt) -> tt
U11(tt) -> U12(isLNat)
U111(tt) -> tt
U12(tt) -> snd(splitAt(N,XS))
U121(tt) -> tt
U131(tt) -> U132(isLNat)
U132(tt) -> tt
U141(tt) -> U142(isLNat)
U142(tt) -> tt
U151(tt) -> U152(isLNat)
U152(tt) -> tt
U161(tt) -> cons(N)
U171(tt) -> U172(isLNat)
U172(tt) -> head(afterNth(N,XS))
U181(tt) -> U182(isLNat)
U182(tt) -> Y
U191(tt) -> pair(nil,XS)
U201(tt) -> U202(isNatural)
U202(tt) -> U203(isLNat)
U203(tt) -> U204(splitAt(N,XS))
U204(pair(YS,ZS)) -> pair(cons(X),ZS)
U21(tt) -> U22(isLNat)
U211(tt) -> U212(isLNat)
U212(tt) -> XS
U22(tt) -> X
U221(tt) -> U222(isLNat)
U222(tt) -> fst(splitAt(N,XS))
U31(tt) -> U32(isLNat)
U32(tt) -> N
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)
)