YES

Problem:
 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:
 DP Processor:
  DPs:
   splitAt#(s(N),cons(X,XS)) -> activate#(XS)
   splitAt#(s(N),cons(X,XS)) -> splitAt#(N,activate(XS))
   splitAt#(s(N),cons(X,XS)) -> u#(splitAt(N,activate(XS)),N,X,activate(XS))
   u#(pair(YS,ZS),N,X,XS) -> activate#(X)
   tail#(cons(N,XS)) -> activate#(XS)
   sel#(N,XS) -> afterNth#(N,XS)
   sel#(N,XS) -> head#(afterNth(N,XS))
   take#(N,XS) -> splitAt#(N,XS)
   take#(N,XS) -> fst#(splitAt(N,XS))
   afterNth#(N,XS) -> splitAt#(N,XS)
   afterNth#(N,XS) -> snd#(splitAt(N,XS))
   activate#(n__natsFrom(X)) -> natsFrom#(X)
  TRS:
   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
  Usable Rule Processor:
   DPs:
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    splitAt#(s(N),cons(X,XS)) -> splitAt#(N,activate(XS))
    splitAt#(s(N),cons(X,XS)) -> u#(splitAt(N,activate(XS)),N,X,activate(XS))
    u#(pair(YS,ZS),N,X,XS) -> activate#(X)
    tail#(cons(N,XS)) -> activate#(XS)
    sel#(N,XS) -> afterNth#(N,XS)
    sel#(N,XS) -> head#(afterNth(N,XS))
    take#(N,XS) -> splitAt#(N,XS)
    take#(N,XS) -> fst#(splitAt(N,XS))
    afterNth#(N,XS) -> splitAt#(N,XS)
    afterNth#(N,XS) -> snd#(splitAt(N,XS))
    activate#(n__natsFrom(X)) -> natsFrom#(X)
   TRS:
    activate(n__natsFrom(X)) -> natsFrom(X)
    activate(X) -> X
    natsFrom(N) -> cons(N,n__natsFrom(s(N)))
    natsFrom(X) -> n__natsFrom(X)
    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)
    afterNth(N,XS) -> snd(splitAt(N,XS))
    snd(pair(XS,YS)) -> YS
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [take#](x0, x1) = 8x0 + x1 + 9,
     
     [afterNth#](x0, x1) = 2x0 + 8,
     
     [sel#](x0, x1) = 7x0 + x1 + 12,
     
     [tail#](x0) = 3x0 + 0,
     
     [head#](x0) = 9,
     
     [u#](x0, x1, x2, x3) = 2,
     
     [activate#](x0) = 1,
     
     [splitAt#](x0, x1) = x0 + 0,
     
     [snd#](x0) = 0,
     
     [fst#](x0) = 0,
     
     [natsFrom#](x0) = 0,
     
     [afterNth](x0, x1) = x0 + 5x1 + 4,
     
     [u](x0, x1, x2, x3) = x2 + 2x3 + 1,
     
     [activate](x0) = x0 + 0,
     
     [nil] = 2,
     
     [splitAt](x0, x1) = 1x0 + 2,
     
     [0] = 1,
     
     [snd](x0) = 5x0 + 8,
     
     [pair](x0, x1) = 2x1,
     
     [cons](x0, x1) = 7x0 + x1 + 1,
     
     [n__natsFrom](x0) = 2x0 + 0,
     
     [s](x0) = 4x0 + 4,
     
     [natsFrom](x0) = x0 + 1
    orientation:
     splitAt#(s(N),cons(X,XS)) = 4N + 4 >= 1 = activate#(XS)
     
     splitAt#(s(N),cons(X,XS)) = 4N + 4 >= N + 0 = splitAt#(N,activate(XS))
     
     splitAt#(s(N),cons(X,XS)) = 4N + 4 >= 2 = u#(splitAt(N,activate(XS)),N,X,activate(XS))
     
     u#(pair(YS,ZS),N,X,XS) = 2 >= 1 = activate#(X)
     
     tail#(cons(N,XS)) = 10N + 3XS + 4 >= 1 = activate#(XS)
     
     sel#(N,XS) = 7N + XS + 12 >= 2N + 8 = afterNth#(N,XS)
     
     sel#(N,XS) = 7N + XS + 12 >= 9 = head#(afterNth(N,XS))
     
     take#(N,XS) = 8N + XS + 9 >= N + 0 = splitAt#(N,XS)
     
     take#(N,XS) = 8N + XS + 9 >= 0 = fst#(splitAt(N,XS))
     
     afterNth#(N,XS) = 2N + 8 >= N + 0 = splitAt#(N,XS)
     
     afterNth#(N,XS) = 2N + 8 >= 0 = snd#(splitAt(N,XS))
     
     activate#(n__natsFrom(X)) = 1 >= 0 = natsFrom#(X)
     
     activate(n__natsFrom(X)) = 2X + 0 >= X + 1 = natsFrom(X)
     
     activate(X) = X + 0 >= X = X
     
     natsFrom(N) = N + 1 >= 7N + 6 = cons(N,n__natsFrom(s(N)))
     
     natsFrom(X) = X + 1 >= 2X + 0 = n__natsFrom(X)
     
     splitAt(0(),XS) = 2 >= 2XS = pair(nil(),XS)
     
     splitAt(s(N),cons(X,XS)) = 5N + 5 >= X + 2XS + 2 = u(splitAt(N,activate(XS)),N,X,activate(XS))
     
     u(pair(YS,ZS),N,X,XS) = X + 2XS + 1 >= 2ZS = pair(cons(activate(X),YS),ZS)
     
     afterNth(N,XS) = N + 5XS + 4 >= 6N + 8 = snd(splitAt(N,XS))
     
     snd(pair(XS,YS)) = 7YS + 8 >= YS = YS
    problem:
     DPs:
      
     TRS:
      activate(n__natsFrom(X)) -> natsFrom(X)
      activate(X) -> X
      natsFrom(N) -> cons(N,n__natsFrom(s(N)))
      natsFrom(X) -> n__natsFrom(X)
      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)
      afterNth(N,XS) -> snd(splitAt(N,XS))
      snd(pair(XS,YS)) -> YS
    Qed