MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { U11(tt(), N, XS) -> U12(tt(), N, XS) , U12(tt(), N, XS) -> snd(splitAt(N, XS)) , snd(pair(X, Y)) -> U51(tt(), Y) , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS) , splitAt(0(), XS) -> pair(nil(), XS) , U21(tt(), X) -> U22(tt(), X) , U22(tt(), X) -> X , U31(tt(), N) -> U32(tt(), N) , U32(tt(), N) -> N , U41(tt(), N, XS) -> U42(tt(), N, XS) , U42(tt(), N, XS) -> head(afterNth(N, XS)) , head(cons(N, XS)) -> U31(tt(), N) , afterNth(N, XS) -> U11(tt(), N, XS) , U51(tt(), Y) -> U52(tt(), Y) , U52(tt(), Y) -> Y , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS) , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS) , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X) , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS) , U71(tt(), XS) -> U72(tt(), XS) , U72(tt(), XS) -> XS , U81(tt(), N, XS) -> U82(tt(), N, XS) , U82(tt(), N, XS) -> fst(splitAt(N, XS)) , fst(pair(X, Y)) -> U21(tt(), X) , natsFrom(N) -> cons(N, natsFrom(s(N))) , sel(N, XS) -> U41(tt(), N, XS) , tail(cons(N, XS)) -> U71(tt(), XS) , take(N, XS) -> U81(tt(), N, XS) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..