YES(?,ELEMENTARY)

'epo* (timeout of 60.0 seconds)'
--------------------------------
Answer:           YES(?,ELEMENTARY)
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:    
  Strict Rules in Predicative Notation:
   {  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}
  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) = {}
  Argument Permutation:
   mu(natsFrom) = [1], mu(fst) = [1], mu(snd) = [1],
   mu(splitAt) = [1, 2], mu(u) = [1, 3, 4, 2], mu(activate) = [1],
   mu(head) = [1], mu(tail) = [1], mu(sel) = [2, 1],
   mu(afterNth) = [1, 2], mu(take) = [2, 1]
  Precedence:
   take ~ take, take > tail, take ~ head, take > activate, take > u,
   take > splitAt, take > snd, take > fst, take > natsFrom,
   afterNth > take, afterNth ~ afterNth, afterNth > tail,
   afterNth > head, afterNth > activate, afterNth > u,
   afterNth > splitAt, afterNth > snd, afterNth > fst,
   afterNth > natsFrom, sel > take, sel > afterNth, sel ~ sel,
   sel > tail, sel > head, sel > activate, sel > u, sel > splitAt,
   sel > snd, sel > fst, sel > natsFrom, tail ~ tail, tail > activate,
   tail ~ u, tail > snd, tail ~ fst, tail > natsFrom, head ~ take,
   head > tail, head ~ head, head > activate, head > u,
   head > splitAt, head > snd, head > fst, head > natsFrom,
   activate ~ activate, activate > snd, activate > natsFrom, u ~ tail,
   u > activate, u ~ u, u > snd, u ~ fst, u > natsFrom,
   splitAt > tail, splitAt > activate, splitAt > u, splitAt ~ splitAt,
   splitAt > snd, splitAt > fst, splitAt > natsFrom, snd ~ snd,
   snd ~ natsFrom, fst ~ tail, fst > activate, fst ~ u, fst > snd,
   fst ~ fst, fst > natsFrom, natsFrom ~ snd, natsFrom ~ natsFrom