YES(?,POLY)

'Pop* with parameter subtitution (timeout of 60.0 seconds)'
-----------------------------------------------------------
Answer:           YES(?,POLY)
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  natsFrom(N) -> cons(N, n__natsFrom(s(N)))
     , 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))
     , u(pair(YS, ZS), N, X, XS) -> pair(cons(activate(X), YS), ZS)
     , head(cons(N, XS)) -> N
     , tail(cons(N, XS)) -> activate(XS)
     , sel(N, XS) -> head(afterNth(N, XS))
     , take(N, XS) -> fst(splitAt(N, XS))
     , afterNth(N, XS) -> snd(splitAt(N, XS))
     , natsFrom(X) -> n__natsFrom(X)
     , activate(n__natsFrom(X)) -> natsFrom(X)
     , activate(X) -> X}

Proof Output:    
  The input was oriented with the instance of POP* as induced by the precedence
  
   fst > natsFrom, fst > u, fst > activate, fst > head,
   snd > natsFrom, snd > fst, snd > splitAt, snd > u, snd > activate,
   snd > head, splitAt > natsFrom, splitAt > u, splitAt > activate,
   splitAt > head, u > natsFrom, u > head, activate > natsFrom,
   activate > head, tail > natsFrom, tail > fst, tail > snd,
   tail > splitAt, tail > u, tail > activate, tail > head, tail > sel,
   tail > afterNth, tail > take, sel > natsFrom, sel > fst, sel > snd,
   sel > splitAt, sel > u, sel > activate, sel > head, sel > afterNth,
   afterNth > natsFrom, afterNth > fst, afterNth > splitAt,
   afterNth > u, afterNth > activate, afterNth > head,
   take > natsFrom, take > fst, take > snd, take > splitAt, take > u,
   take > activate, take > head, take > sel, take > afterNth,
   natsFrom ~ head, fst ~ splitAt, snd ~ afterNth, u ~ activate
  
  and 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, 3, 4}, safe(activate) = {1}, safe(head) = {1},
   safe(tail) = {1}, safe(sel) = {2}, safe(afterNth) = {2},
   safe(take) = {2} .
  
  For your convenience, here is the input in predicative notation:
  
   Rules:
    {  natsFrom(; N) -> cons(; N, n__natsFrom(; s(; N)))
     , fst(; pair(; XS, YS)) -> XS
     , snd(; pair(; XS, YS)) -> YS
     , splitAt(0(); XS) -> pair(; nil(), XS)
     , splitAt(s(; N); cons(; X, XS)) ->
       u(N; splitAt(N; activate(; XS)), X, activate(; XS))
     , u(N; pair(; YS, ZS), X, XS) ->
       pair(; cons(; activate(; X), YS), ZS)
     , head(; cons(; N, XS)) -> N
     , tail(; cons(; N, XS)) -> activate(; XS)
     , sel(N; XS) -> head(; afterNth(N; XS))
     , take(N; XS) -> fst(; splitAt(N; XS))
     , afterNth(N; XS) -> snd(; splitAt(N; XS))
     , natsFrom(; X) -> n__natsFrom(; X)
     , activate(; n__natsFrom(; X)) -> natsFrom(; X)
     , activate(; X) -> X}