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
  TDG 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
   graph:
    take#(N,XS) -> splitAt#(N,XS) ->
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
    take#(N,XS) -> splitAt#(N,XS) ->
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    tail#(cons(N,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    sel#(N,XS) -> afterNth#(N,XS) ->
    afterNth#(N,XS) -> snd#(splitAt(N,XS))
    sel#(N,XS) -> afterNth#(N,XS) -> afterNth#(N,XS) -> splitAt#(N,XS)
    and#(tt(),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    afterNth#(N,XS) -> splitAt#(N,XS) ->
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
    afterNth#(N,XS) -> splitAt#(N,XS) ->
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    U12#(pair(YS,ZS),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    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))
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS)) ->
    U11#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS)) ->
    U11#(tt(),N,X,XS) -> activate#(N)
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS)) ->
    U11#(tt(),N,X,XS) -> activate#(XS)
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS)) ->
    U11#(tt(),N,X,XS) -> activate#(X)
    U11#(tt(),N,X,XS) -> U12#(splitAt(activate(N),activate(XS)),activate(X)) ->
    U12#(pair(YS,ZS),X) -> activate#(X)
    U11#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) ->
    splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
    U11#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS)) ->
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    U11#(tt(),N,X,XS) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    U11#(tt(),N,X,XS) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(X)
    U11#(tt(),N,X,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> natsFrom#(X)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 21/289
    DPs:
     splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
     U11#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    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:
      splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
      U11#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
     TRS:
      activate(n__natsFrom(X)) -> natsFrom(X)
      activate(X) -> X
      natsFrom(N) -> cons(N,n__natsFrom(s(N)))
      natsFrom(X) -> n__natsFrom(X)
     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)
      interpretation:
       [splitAt#](x0, x1) = 4x0,
       
       [U11#](x0, x1, x2, x3) = -8x0 + 6x1 + -16,
       
       [n__natsFrom](x0) = 4x0 + -7,
       
       [s](x0) = 2x0 + -12,
       
       [natsFrom](x0) = 5x0 + -6,
       
       [cons](x0, x1) = 5x0 + -6,
       
       [activate](x0) = 1x0,
       
       [tt] = 0
      orientation:
       splitAt#(s(N),cons(X,XS)) = 6N + -8 >= 6N + -8 = U11#(tt(),N,X,activate(XS))
       
       U11#(tt(),N,X,XS) = 6N + -8 >= 5N = splitAt#(activate(N),activate(XS))
       
       activate(n__natsFrom(X)) = 5X + -6 >= 5X + -6 = natsFrom(X)
       
       activate(X) = 1X >= X = X
       
       natsFrom(N) = 5N + -6 >= 5N + -6 = cons(N,n__natsFrom(s(N)))
       
       natsFrom(X) = 5X + -6 >= 4X + -7 = n__natsFrom(X)
      problem:
       DPs:
        splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
       TRS:
        activate(n__natsFrom(X)) -> natsFrom(X)
        activate(X) -> X
        natsFrom(N) -> cons(N,n__natsFrom(s(N)))
        natsFrom(X) -> n__natsFrom(X)
      Restore Modifier:
       DPs:
        splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
       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
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 2/1