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