YES

Problem:
 U11(tt(),N,X,XS) -> U12(splitAt(activate(N),activate(XS)),activate(X))
 U12(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 afterNth(N,XS) -> snd(splitAt(N,XS))
 and(tt(),X) -> activate(X)
 fst(pair(X,Y)) -> X
 head(cons(N,XS)) -> N
 natsFrom(N) -> cons(N,n__natsFrom(s(N)))
 sel(N,XS) -> head(afterNth(N,XS))
 snd(pair(X,Y)) -> Y
 splitAt(0(),XS) -> pair(nil(),XS)
 splitAt(s(N),cons(X,XS)) -> U11(tt(),N,X,activate(XS))
 tail(cons(N,XS)) -> activate(XS)
 take(N,XS) -> fst(splitAt(N,XS))
 natsFrom(X) -> n__natsFrom(X)
 activate(n__natsFrom(X)) -> natsFrom(X)
 activate(X) -> X

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