(VAR N V1 V2 X X1 X2 XS Y YS ZS )
(RULES 
        U101(tt, V2) -> U102(isLNat(activate(V2)))
        U102(tt) -> tt
        U11(tt, N, XS) -> U12(isLNat(activate(XS)), activate(N), activate(XS))
        U111(tt) -> tt
        U12(tt, N, XS) -> snd(splitAt(activate(N), activate(XS)))
        U121(tt) -> tt
        U131(tt, V2) -> U132(isLNat(activate(V2)))
        U132(tt) -> tt
        U141(tt, V2) -> U142(isLNat(activate(V2)))
        U142(tt) -> tt
        U151(tt, V2) -> U152(isLNat(activate(V2)))
        U152(tt) -> tt
        U161(tt, N) -> cons(activate(N), n__natsFrom(s(activate(N))))
        U171(tt, N, XS) -> U172(isLNat(activate(XS)), activate(N), activate(XS))
        U172(tt, N, XS) -> head(afterNth(activate(N), activate(XS)))
        U181(tt, Y) -> U182(isLNat(activate(Y)), activate(Y))
        U182(tt, Y) -> activate(Y)
        U191(tt, XS) -> pair(nil, activate(XS))
        U201(tt, N, X, XS) -> U202(isNatural(activate(X)), activate(N), activate(X), activate(XS))
        U202(tt, N, X, XS) -> U203(isLNat(activate(XS)), activate(N), activate(X), activate(XS))
        U203(tt, N, X, XS) -> U204(splitAt(activate(N), activate(XS)), activate(X))
        U204(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
        U21(tt, X, Y) -> U22(isLNat(activate(Y)), activate(X))
        U211(tt, XS) -> U212(isLNat(activate(XS)), activate(XS))
        U212(tt, XS) -> activate(XS)
        U22(tt, X) -> activate(X)
        U221(tt, N, XS) -> U222(isLNat(activate(XS)), activate(N), activate(XS))
        U222(tt, N, XS) -> fst(splitAt(activate(N), activate(XS)))
        U31(tt, N, XS) -> U32(isLNat(activate(XS)), activate(N))
        U32(tt, N) -> activate(N)
        U41(tt, V2) -> U42(isLNat(activate(V2)))
        U42(tt) -> tt
        U51(tt, V2) -> U52(isLNat(activate(V2)))
        U52(tt) -> tt
        U61(tt) -> tt
        U71(tt) -> tt
        U81(tt) -> tt
        U91(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, activate(XS))
        isLNat(n__nil) -> tt
        isLNat(n__afterNth(V1, V2)) -> U41(isNatural(activate(V1)), activate(V2))
        isLNat(n__cons(V1, V2)) -> U51(isNatural(activate(V1)), activate(V2))
        isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1)))
        isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
        isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1)))
        isLNat(n__tail(V1)) -> U91(isLNat(activate(V1)))
        isLNat(n__take(V1, V2)) -> U101(isNatural(activate(V1)), activate(V2))
        isNatural(n__0) -> tt
        isNatural(n__head(V1)) -> U111(isLNat(activate(V1)))
        isNatural(n__s(V1)) -> U121(isNatural(activate(V1)))
        isNatural(n__sel(V1, V2)) -> U131(isNatural(activate(V1)), activate(V2))
        isPLNat(n__pair(V1, V2)) -> U141(isLNat(activate(V1)), activate(V2))
        isPLNat(n__splitAt(V1, V2)) -> U151(isNatural(activate(V1)), activate(V2))
        natsFrom(N) -> U161(isNatural(N), N)
        sel(N, XS) -> U171(isNatural(N), N, XS)
        snd(pair(X, Y)) -> U181(isLNat(X), Y)
        splitAt(0, XS) -> U191(isLNat(XS), XS)
        splitAt(s(N), cons(X, XS)) -> U201(isNatural(N), N, X, activate(XS))
        tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
        take(N, XS) -> U221(isNatural(N), N, XS)
        natsFrom(X) -> n__natsFrom(X)
        nil -> n__nil
        afterNth(X1, X2) -> n__afterNth(X1, X2)
        cons(X1, X2) -> n__cons(X1, X2)
        fst(X) -> n__fst(X)
        snd(X) -> n__snd(X)
        tail(X) -> n__tail(X)
        take(X1, X2) -> n__take(X1, X2)
        0 -> n__0
        head(X) -> n__head(X)
        s(X) -> n__s(X)
        sel(X1, X2) -> n__sel(X1, X2)
        pair(X1, X2) -> n__pair(X1, X2)
        splitAt(X1, X2) -> n__splitAt(X1, X2)
        activate(n__natsFrom(X)) -> natsFrom(X)
        activate(n__nil) -> nil
        activate(n__afterNth(X1, X2)) -> afterNth(X1, X2)
        activate(n__cons(X1, X2)) -> cons(X1, X2)
        activate(n__fst(X)) -> fst(X)
        activate(n__snd(X)) -> snd(X)
        activate(n__tail(X)) -> tail(X)
        activate(n__take(X1, X2)) -> take(X1, X2)
        activate(n__0) -> 0
        activate(n__head(X)) -> head(X)
        activate(n__s(X)) -> s(X)
        activate(n__sel(X1, X2)) -> sel(X1, X2)
        activate(n__pair(X1, X2)) -> pair(X1, X2)
        activate(n__splitAt(X1, X2)) -> splitAt(X1, X2)
        activate(X) -> X
        
)