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

Strict Trs:
  { natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(0(), XS) -> pair(nil(), XS)
  , splitAt(s(N), cons(X, XS)) ->
    u(splitAt(N, activate(XS)), N, X, activate(XS))
  , s(X) -> n__s(X)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(activate(X))
  , activate(n__s(X)) -> s(activate(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(1),O(n^1))

Arguments of following rules are not normal-forms:

{ splitAt(s(N), cons(X, XS)) ->
  u(splitAt(N, activate(XS)), N, X, activate(XS)) }

All above mentioned rules can be savely removed.

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

Strict Trs:
  { natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(0(), XS) -> pair(nil(), XS)
  , s(X) -> n__s(X)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(activate(X))
  , activate(n__s(X)) -> s(activate(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(1),O(n^1))

We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.

Trs:
  { natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(0(), XS) -> pair(nil(), XS)
  , s(X) -> n__s(X)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(activate(X))
  , activate(n__s(X)) -> s(activate(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)) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The input was oriented with the instance of 'Small Polynomial Path
  Order (PS,1-bounded)' as induced by the safe mapping
  
   safe(natsFrom) = {1}, safe(cons) = {1, 2}, safe(n__natsFrom) = {1},
   safe(n__s) = {1}, safe(fst) = {1}, safe(pair) = {1, 2},
   safe(snd) = {1}, safe(splitAt) = {1, 2}, safe(0) = {},
   safe(nil) = {}, safe(s) = {1}, safe(u) = {1}, safe(activate) = {},
   safe(head) = {1}, safe(tail) = {}, safe(sel) = {},
   safe(afterNth) = {1, 2}, safe(take) = {}
  
  and precedence
  
   u > activate, activate > natsFrom, activate > s, tail > activate,
   sel > head, sel > afterNth, afterNth > snd, afterNth > splitAt,
   take > fst, take > splitAt .
  
  Following symbols are considered recursive:
  
   {activate}
  
  The recursion depth is 1.
  
  For your convenience, here are the satisfied ordering constraints:
  
                     natsFrom(; N) > cons(; N,  n__natsFrom(; n__s(; N)))  
                                                                           
                     natsFrom(; X) > n__natsFrom(; X)                      
                                                                           
            fst(; pair(; XS,  YS)) > XS                                    
                                                                           
            snd(; pair(; XS,  YS)) > YS                                    
                                                                           
               splitAt(; 0(),  XS) > pair(; nil(),  XS)                    
                                                                           
                            s(; X) > n__s(; X)                             
                                                                           
    u(N,  X,  XS; pair(; YS,  ZS)) > pair(; cons(; activate(X;),  YS),  ZS)
                                                                           
                      activate(X;) > X                                     
                                                                           
       activate(n__natsFrom(; X);) > natsFrom(; activate(X;))              
                                                                           
              activate(n__s(; X);) > s(; activate(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))              
                                                                           

We return to the main proof.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { natsFrom(N) -> cons(N, n__natsFrom(n__s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , fst(pair(XS, YS)) -> XS
  , snd(pair(XS, YS)) -> YS
  , splitAt(0(), XS) -> pair(nil(), XS)
  , s(X) -> n__s(X)
  , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(activate(X))
  , activate(n__s(X)) -> s(activate(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(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))