YES(?,O(n^7))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^7)).

Strict Trs:
  { natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(s(N), cons(X, XS)) ->
    u(splitAt(N, activate(XS)), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , head(cons(N, XS)) -> N
  , tail(cons(N, XS)) -> activate(XS)
  , sel(N, XS) -> head(afterNth(N, XS))
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^7))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS)' as induced by the safe mapping

 safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1},
 safe(s) = {1}, safe(fst) = {1}, safe(pair) = {1, 2},
 safe(snd) = {1}, safe(splitAt) = {2}, safe(0) = {}, safe(nil) = {},
 safe(u) = {1, 2, 3, 4}, safe(activate) = {1}, safe(head) = {1},
 safe(tail) = {1}, safe(sel) = {2}, safe(afterNth) = {2},
 safe(take) = {2}

and precedence

 fst > natsFrom, fst > snd, fst > splitAt, fst > u, fst > activate,
 snd > natsFrom, snd > splitAt, snd > u, snd > activate,
 splitAt > natsFrom, splitAt > u, splitAt > activate, u > natsFrom,
 u > activate, activate > natsFrom, head > natsFrom, head > snd,
 head > splitAt, head > u, head > activate, tail > natsFrom,
 tail > fst, tail > snd, tail > splitAt, tail > u, tail > activate,
 tail > head, tail > afterNth, sel > natsFrom, sel > fst, sel > snd,
 sel > splitAt, sel > u, sel > activate, sel > head, sel > afterNth,
 afterNth > natsFrom, afterNth > snd, afterNth > splitAt,
 afterNth > u, afterNth > activate, take > natsFrom, take > fst,
 take > snd, take > splitAt, take > u, take > activate, take > head,
 take > afterNth, fst ~ head, fst ~ afterNth, head ~ afterNth,
 tail ~ sel, tail ~ take, sel ~ take .

Following symbols are considered recursive:

 {natsFrom, fst, snd, splitAt, u, activate, head, tail, sel,
  afterNth, take}

The recursion depth is 7.

For your convenience, here are the satisfied ordering constraints:

                      natsFrom(; N) > cons(; N,  n__natsFrom(; s(; N)))                       
                                                                                              
                      natsFrom(; X) > n__natsFrom(; X)                                        
                                                                                              
             fst(; pair(; XS,  YS)) > XS                                                      
                                                                                              
             snd(; pair(; XS,  YS)) > YS                                                      
                                                                                              
    splitAt(s(; N); cons(; X,  XS)) > u(; splitAt(N; activate(; XS)),  N,  X,  activate(; XS))
                                                                                              
                   splitAt(0(); XS) > pair(; nil(),  XS)                                      
                                                                                              
  u(; pair(; YS,  ZS),  N,  X,  XS) > pair(; cons(; activate(; X),  YS),  ZS)                 
                                                                                              
                      activate(; X) > X                                                       
                                                                                              
       activate(; n__natsFrom(; X)) > natsFrom(; X)                                           
                                                                                              
             head(; cons(; N,  XS)) > N                                                       
                                                                                              
             tail(; cons(; N,  XS)) > activate(; XS)                                          
                                                                                              
                         sel(N; XS) > head(; afterNth(N; XS))                                 
                                                                                              
                    afterNth(N; XS) > snd(; splitAt(N; XS))                                   
                                                                                              
                        take(N; XS) > fst(; splitAt(N; XS))                                   
                                                                                              

Hurray, we answered YES(?,O(n^7))