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(n__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)
 s(X) -> n__s(X)
 activate(n__natsFrom(X)) -> natsFrom(activate(X))
 activate(n__s(X)) -> s(activate(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)) -> activate#(X)
   activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
   activate#(n__s(X)) -> activate#(X)
   activate#(n__s(X)) -> s#(activate(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(n__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)
   s(X) -> n__s(X)
   activate(n__natsFrom(X)) -> natsFrom(activate(X))
   activate(n__s(X)) -> s(activate(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)) -> activate#(X)
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> s#(activate(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(n__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)
    s(X) -> n__s(X)
    activate(n__natsFrom(X)) -> natsFrom(activate(X))
    activate(n__s(X)) -> s(activate(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__s(X)) -> s#(activate(X))
    tail#(cons(N,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    tail#(cons(N,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    tail#(cons(N,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> activate#(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__s(X)) -> s#(activate(X))
    and#(tt(),X) -> activate#(X) -> activate#(n__s(X)) -> activate#(X)
    and#(tt(),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    and#(tt(),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> activate#(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__s(X)) -> s#(activate(X))
    U12#(pair(YS,ZS),X) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    U12#(pair(YS,ZS),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    U12#(pair(YS,ZS),X) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> activate#(X)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> s#(activate(X))
    splitAt#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    splitAt#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> activate#(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)
    activate#(n__natsFrom(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__natsFrom(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__natsFrom(X)) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    activate#(n__natsFrom(X)) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> 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__s(X)) -> s#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    U11#(tt(),N,X,XS) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(XS) ->
    activate#(n__natsFrom(X)) -> activate#(X)
    U11#(tt(),N,X,XS) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    U11#(tt(),N,X,XS) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(X) ->
    activate#(n__natsFrom(X)) -> activate#(X)
    U11#(tt(),N,X,XS) -> activate#(N) ->
    activate#(n__s(X)) -> s#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(N) ->
    activate#(n__s(X)) -> activate#(X)
    U11#(tt(),N,X,XS) -> activate#(N) ->
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    U11#(tt(),N,X,XS) -> activate#(N) -> activate#(n__natsFrom(X)) -> activate#(X)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 50/400
    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(n__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)
     s(X) -> n__s(X)
     activate(n__natsFrom(X)) -> natsFrom(activate(X))
     activate(n__s(X)) -> s(activate(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(activate(X))
      activate(n__s(X)) -> s(activate(X))
      activate(X) -> X
      natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
      natsFrom(X) -> n__natsFrom(X)
      s(X) -> n__s(X)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       activate(n__natsFrom(X)) -> natsFrom(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(X) -> X
       natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
       natsFrom(X) -> n__natsFrom(X)
       s(X) -> n__s(X)
      interpretation:
       [splitAt#](x0, x1) = x0 + 0,
       
       [U11#](x0, x1, x2, x3) = 1x1 + 1,
       
       [s](x0) = 1x0 + 1,
       
       [n__natsFrom](x0) = x0 + 0,
       
       [n__s](x0) = 1x0 + 1,
       
       [natsFrom](x0) = x0 + 0,
       
       [cons](x0, x1) = x0 + -8x1 + -6,
       
       [activate](x0) = x0 + 0,
       
       [tt] = 4
      orientation:
       splitAt#(s(N),cons(X,XS)) = 1N + 1 >= 1N + 1 = U11#(tt(),N,X,activate(XS))
       
       U11#(tt(),N,X,XS) = 1N + 1 >= N + 0 = splitAt#(activate(N),activate(XS))
       
       activate(n__natsFrom(X)) = X + 0 >= X + 0 = natsFrom(activate(X))
       
       activate(n__s(X)) = 1X + 1 >= 1X + 1 = s(activate(X))
       
       activate(X) = X + 0 >= X = X
       
       natsFrom(N) = N + 0 >= N + -6 = cons(N,n__natsFrom(n__s(N)))
       
       natsFrom(X) = X + 0 >= X + 0 = n__natsFrom(X)
       
       s(X) = 1X + 1 >= 1X + 1 = n__s(X)
      problem:
       DPs:
        splitAt#(s(N),cons(X,XS)) -> U11#(tt(),N,X,activate(XS))
       TRS:
        activate(n__natsFrom(X)) -> natsFrom(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(X) -> X
        natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
        natsFrom(X) -> n__natsFrom(X)
        s(X) -> n__s(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(n__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)
        s(X) -> n__s(X)
        activate(n__natsFrom(X)) -> natsFrom(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(X) -> X
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 2/1
        
    
    DPs:
     activate#(n__natsFrom(X)) -> activate#(X)
     activate#(n__s(X)) -> activate#(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(n__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)
     s(X) -> n__s(X)
     activate(n__natsFrom(X)) -> natsFrom(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(X) -> X
    Subterm Criterion Processor:
     simple projection:
      pi(activate#) = 0
     problem:
      DPs:
       
      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(n__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)
       s(X) -> n__s(X)
       activate(n__natsFrom(X)) -> natsFrom(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(X) -> X
     Qed