TRS:
 {          U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)),
            U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))),
                U21(tt(), X) -> U22(tt(), activate(X)),
                U22(tt(), X) -> activate(X),
                U31(tt(), N) -> U32(tt(), activate(N)),
                U32(tt(), N) -> activate(N),
            U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)),
            U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))),
                U51(tt(), Y) -> U52(tt(), activate(Y)),
                U52(tt(), Y) -> activate(Y),
         U61(tt(), N, X, XS) -> U62(tt(), activate(N), activate(X), activate(XS)),
         U62(tt(), N, X, XS) -> U63(tt(), activate(N), activate(X), activate(XS)),
         U63(tt(), N, X, XS) -> U64(splitAt(activate(N), activate(XS)), activate(X)),
        U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
               U71(tt(), XS) -> U72(tt(), activate(XS)),
               U72(tt(), XS) -> activate(XS),
            U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)),
            U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))),
             afterNth(N, XS) -> U11(tt(), N, XS),
             fst(pair(X, Y)) -> U21(tt(), X),
           head(cons(N, XS)) -> U31(tt(), N),
                 natsFrom(N) -> cons(N, n__natsFrom(s(N))),
                  sel(N, XS) -> U41(tt(), N, XS),
             snd(pair(X, Y)) -> U51(tt(), Y),
            splitAt(0(), XS) -> pair(nil(), XS),
  splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)),
           tail(cons(N, XS)) -> U71(tt(), activate(XS)),
                 take(N, XS) -> U81(tt(), N, XS),
                 natsFrom(X) -> n__natsFrom(X),
    activate(n__natsFrom(X)) -> natsFrom(X),
                 activate(X) -> X}
 Fail