YES

Problem:
 U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
 U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
 U21(tt(),X) -> U22(tt(),activate(X))
 U22(tt(),X) -> activate(X)
 U31(tt(),N) -> U32(tt(),activate(N))
 U32(tt(),N) -> activate(N)
 U41(tt(),N,XS) -> U42(tt(),activate(N),activate(XS))
 U42(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
 U51(tt(),Y) -> U52(tt(),activate(Y))
 U52(tt(),Y) -> activate(Y)
 U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
 U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
 U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
 U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 U71(tt(),XS) -> U72(tt(),activate(XS))
 U72(tt(),XS) -> activate(XS)
 U81(tt(),N,XS) -> U82(tt(),activate(N),activate(XS))
 U82(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
 afterNth(N,XS) -> U11(tt(),N,XS)
 fst(pair(X,Y)) -> U21(tt(),X)
 head(cons(N,XS)) -> U31(tt(),N)
 natsFrom(N) -> cons(N,n__natsFrom(s(N)))
 sel(N,XS) -> U41(tt(),N,XS)
 snd(pair(X,Y)) -> U51(tt(),Y)
 splitAt(0(),XS) -> pair(nil(),XS)
 splitAt(s(N),cons(X,XS)) -> U61(tt(),N,X,activate(XS))
 tail(cons(N,XS)) -> U71(tt(),activate(XS))
 take(N,XS) -> U81(tt(),N,XS)
 natsFrom(X) -> n__natsFrom(X)
 activate(n__natsFrom(X)) -> natsFrom(X)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U11#(tt(),N,XS) -> activate#(XS)
   U11#(tt(),N,XS) -> activate#(N)
   U11#(tt(),N,XS) -> U12#(tt(),activate(N),activate(XS))
   U12#(tt(),N,XS) -> activate#(XS)
   U12#(tt(),N,XS) -> activate#(N)
   U12#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U12#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
   U21#(tt(),X) -> activate#(X)
   U21#(tt(),X) -> U22#(tt(),activate(X))
   U22#(tt(),X) -> activate#(X)
   U31#(tt(),N) -> activate#(N)
   U31#(tt(),N) -> U32#(tt(),activate(N))
   U32#(tt(),N) -> activate#(N)
   U41#(tt(),N,XS) -> activate#(XS)
   U41#(tt(),N,XS) -> activate#(N)
   U41#(tt(),N,XS) -> U42#(tt(),activate(N),activate(XS))
   U42#(tt(),N,XS) -> activate#(XS)
   U42#(tt(),N,XS) -> activate#(N)
   U42#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
   U42#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
   U51#(tt(),Y) -> activate#(Y)
   U51#(tt(),Y) -> U52#(tt(),activate(Y))
   U52#(tt(),Y) -> activate#(Y)
   U61#(tt(),N,X,XS) -> activate#(XS)
   U61#(tt(),N,X,XS) -> activate#(X)
   U61#(tt(),N,X,XS) -> activate#(N)
   U61#(tt(),N,X,XS) -> U62#(tt(),activate(N),activate(X),activate(XS))
   U62#(tt(),N,X,XS) -> activate#(XS)
   U62#(tt(),N,X,XS) -> activate#(X)
   U62#(tt(),N,X,XS) -> activate#(N)
   U62#(tt(),N,X,XS) -> U63#(tt(),activate(N),activate(X),activate(XS))
   U63#(tt(),N,X,XS) -> activate#(X)
   U63#(tt(),N,X,XS) -> activate#(XS)
   U63#(tt(),N,X,XS) -> activate#(N)
   U63#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
   U63#(tt(),N,X,XS) -> U64#(splitAt(activate(N),activate(XS)),activate(X))
   U64#(pair(YS,ZS),X) -> activate#(X)
   U71#(tt(),XS) -> activate#(XS)
   U71#(tt(),XS) -> U72#(tt(),activate(XS))
   U72#(tt(),XS) -> activate#(XS)
   U81#(tt(),N,XS) -> activate#(XS)
   U81#(tt(),N,XS) -> activate#(N)
   U81#(tt(),N,XS) -> U82#(tt(),activate(N),activate(XS))
   U82#(tt(),N,XS) -> activate#(XS)
   U82#(tt(),N,XS) -> activate#(N)
   U82#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U82#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
   afterNth#(N,XS) -> U11#(tt(),N,XS)
   fst#(pair(X,Y)) -> U21#(tt(),X)
   head#(cons(N,XS)) -> U31#(tt(),N)
   sel#(N,XS) -> U41#(tt(),N,XS)
   snd#(pair(X,Y)) -> U51#(tt(),Y)
   splitAt#(s(N),cons(X,XS)) -> activate#(XS)
   splitAt#(s(N),cons(X,XS)) -> U61#(tt(),N,X,activate(XS))
   tail#(cons(N,XS)) -> activate#(XS)
   tail#(cons(N,XS)) -> U71#(tt(),activate(XS))
   take#(N,XS) -> U81#(tt(),N,XS)
   activate#(n__natsFrom(X)) -> natsFrom#(X)
  TRS:
   U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
   U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
   U21(tt(),X) -> U22(tt(),activate(X))
   U22(tt(),X) -> activate(X)
   U31(tt(),N) -> U32(tt(),activate(N))
   U32(tt(),N) -> activate(N)
   U41(tt(),N,XS) -> U42(tt(),activate(N),activate(XS))
   U42(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
   U51(tt(),Y) -> U52(tt(),activate(Y))
   U52(tt(),Y) -> activate(Y)
   U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
   U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
   U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
   U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
   U71(tt(),XS) -> U72(tt(),activate(XS))
   U72(tt(),XS) -> activate(XS)
   U81(tt(),N,XS) -> U82(tt(),activate(N),activate(XS))
   U82(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
   afterNth(N,XS) -> U11(tt(),N,XS)
   fst(pair(X,Y)) -> U21(tt(),X)
   head(cons(N,XS)) -> U31(tt(),N)
   natsFrom(N) -> cons(N,n__natsFrom(s(N)))
   sel(N,XS) -> U41(tt(),N,XS)
   snd(pair(X,Y)) -> U51(tt(),Y)
   splitAt(0(),XS) -> pair(nil(),XS)
   splitAt(s(N),cons(X,XS)) -> U61(tt(),N,X,activate(XS))
   tail(cons(N,XS)) -> U71(tt(),activate(XS))
   take(N,XS) -> U81(tt(),N,XS)
   natsFrom(X) -> n__natsFrom(X)
   activate(n__natsFrom(X)) -> natsFrom(X)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    U11#(tt(),N,XS) -> activate#(XS)
    U11#(tt(),N,XS) -> activate#(N)
    U11#(tt(),N,XS) -> U12#(tt(),activate(N),activate(XS))
    U12#(tt(),N,XS) -> activate#(XS)
    U12#(tt(),N,XS) -> activate#(N)
    U12#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U12#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
    U21#(tt(),X) -> activate#(X)
    U21#(tt(),X) -> U22#(tt(),activate(X))
    U22#(tt(),X) -> activate#(X)
    U31#(tt(),N) -> activate#(N)
    U31#(tt(),N) -> U32#(tt(),activate(N))
    U32#(tt(),N) -> activate#(N)
    U41#(tt(),N,XS) -> activate#(XS)
    U41#(tt(),N,XS) -> activate#(N)
    U41#(tt(),N,XS) -> U42#(tt(),activate(N),activate(XS))
    U42#(tt(),N,XS) -> activate#(XS)
    U42#(tt(),N,XS) -> activate#(N)
    U42#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
    U42#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
    U51#(tt(),Y) -> activate#(Y)
    U51#(tt(),Y) -> U52#(tt(),activate(Y))
    U52#(tt(),Y) -> activate#(Y)
    U61#(tt(),N,X,XS) -> activate#(XS)
    U61#(tt(),N,X,XS) -> activate#(X)
    U61#(tt(),N,X,XS) -> activate#(N)
    U61#(tt(),N,X,XS) -> U62#(tt(),activate(N),activate(X),activate(XS))
    U62#(tt(),N,X,XS) -> activate#(XS)
    U62#(tt(),N,X,XS) -> activate#(X)
    U62#(tt(),N,X,XS) -> activate#(N)
    U62#(tt(),N,X,XS) -> U63#(tt(),activate(N),activate(X),activate(XS))
    U63#(tt(),N,X,XS) -> activate#(X)
    U63#(tt(),N,X,XS) -> activate#(XS)
    U63#(tt(),N,X,XS) -> activate#(N)
    U63#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    U63#(tt(),N,X,XS) -> U64#(splitAt(activate(N),activate(XS)),activate(X))
    U64#(pair(YS,ZS),X) -> activate#(X)
    U71#(tt(),XS) -> activate#(XS)
    U71#(tt(),XS) -> U72#(tt(),activate(XS))
    U72#(tt(),XS) -> activate#(XS)
    U81#(tt(),N,XS) -> activate#(XS)
    U81#(tt(),N,XS) -> activate#(N)
    U81#(tt(),N,XS) -> U82#(tt(),activate(N),activate(XS))
    U82#(tt(),N,XS) -> activate#(XS)
    U82#(tt(),N,XS) -> activate#(N)
    U82#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U82#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
    afterNth#(N,XS) -> U11#(tt(),N,XS)
    fst#(pair(X,Y)) -> U21#(tt(),X)
    head#(cons(N,XS)) -> U31#(tt(),N)
    sel#(N,XS) -> U41#(tt(),N,XS)
    snd#(pair(X,Y)) -> U51#(tt(),Y)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    splitAt#(s(N),cons(X,XS)) -> U61#(tt(),N,X,activate(XS))
    tail#(cons(N,XS)) -> activate#(XS)
    tail#(cons(N,XS)) -> U71#(tt(),activate(XS))
    take#(N,XS) -> U81#(tt(),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)) -> U61(tt(),N,X,activate(XS))
    U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
    U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
    U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
    U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    afterNth(N,XS) -> U11(tt(),N,XS)
    U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
    U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    snd(pair(X,Y)) -> U51(tt(),Y)
    U51(tt(),Y) -> U52(tt(),activate(Y))
    U52(tt(),Y) -> activate(Y)
   Matrix Interpretation Processor: dim=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)) -> U61(tt(),N,X,activate(XS))
     U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
     U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
     U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
     U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    interpretation:
     [take#](x0, x1) = 7x0 + 5x1 + 7,
     
     [tail#](x0) = 7,
     
     [sel#](x0, x1) = 4x0 + 4x1 + 7,
     
     [natsFrom#](x0) = 0,
     
     [fst#](x0) = 7x0 + 2,
     
     [U82#](x0, x1, x2) = 7x1 + 5x2 + 4,
     
     [U81#](x0, x1, x2) = 3x0 + 7x1 + 5x2 + 3,
     
     [U72#](x0, x1) = 2x0,
     
     [U71#](x0, x1) = 4x0,
     
     [U64#](x0, x1) = 2,
     
     [U63#](x0, x1, x2, x3) = 4x1 + 4,
     
     [U62#](x0, x1, x2, x3) = 4x1 + 5,
     
     [U61#](x0, x1, x2, x3) = x0 + 4x1 + 5,
     
     [U52#](x0, x1) = 2,
     
     [U51#](x0, x1) = 3,
     
     [head#](x0) = 4,
     
     [afterNth#](x0, x1) = 4x0 + 2x1 + 4,
     
     [U42#](x0, x1, x2) = 3x0 + 4x1 + 4x2 + 2,
     
     [U41#](x0, x1, x2) = 2x0 + 4x1 + 4x2 + 4,
     
     [U32#](x0, x1) = 2,
     
     [U31#](x0, x1) = 3,
     
     [U22#](x0, x1) = 2x0,
     
     [U21#](x0, x1) = 3x0,
     
     [snd#](x0) = 2x0,
     
     [splitAt#](x0, x1) = x0 + 1,
     
     [U12#](x0, x1, x2) = x0 + 2x1 + x2 + 1,
     
     [activate#](x0) = 1,
     
     [U11#](x0, x1, x2) = 3x1 + 2x2 + 3,
     
     [nil] = 0,
     
     [0] = 2,
     
     [n__natsFrom](x0) = 0,
     
     [s](x0) = 4x0 + 6,
     
     [natsFrom](x0) = 0,
     
     [cons](x0, x1) = 0,
     
     [pair](x0, x1) = 2,
     
     [U64](x0, x1) = x0 + 2,
     
     [U63](x0, x1, x2, x3) = x1 + 2,
     
     [U62](x0, x1, x2, x3) = x0 + 2x1 + 1,
     
     [U61](x0, x1, x2, x3) = x0 + 4x1 + 1,
     
     [U52](x0, x1) = 4x0 + 4,
     
     [U51](x0, x1) = 3x0,
     
     [afterNth](x0, x1) = 0,
     
     [snd](x0) = 2,
     
     [splitAt](x0, x1) = x0,
     
     [U12](x0, x1, x2) = 4x1 + 4x2 + 4,
     
     [activate](x0) = x0,
     
     [U11](x0, x1, x2) = 2x0 + 4,
     
     [tt] = 1
    orientation:
     U11#(tt(),N,XS) = 3N + 2XS + 3 >= 1 = activate#(XS)
     
     U11#(tt(),N,XS) = 3N + 2XS + 3 >= 1 = activate#(N)
     
     U11#(tt(),N,XS) = 3N + 2XS + 3 >= 2N + XS + 2 = U12#(tt(),activate(N),activate(XS))
     
     U12#(tt(),N,XS) = 2N + XS + 2 >= 1 = activate#(XS)
     
     U12#(tt(),N,XS) = 2N + XS + 2 >= 1 = activate#(N)
     
     U12#(tt(),N,XS) = 2N + XS + 2 >= N + 1 = splitAt#(activate(N),activate(XS))
     
     U12#(tt(),N,XS) = 2N + XS + 2 >= 2N = snd#(splitAt(activate(N),activate(XS)))
     
     U21#(tt(),X) = 3 >= 1 = activate#(X)
     
     U21#(tt(),X) = 3 >= 2 = U22#(tt(),activate(X))
     
     U22#(tt(),X) = 2 >= 1 = activate#(X)
     
     U31#(tt(),N) = 3 >= 1 = activate#(N)
     
     U31#(tt(),N) = 3 >= 2 = U32#(tt(),activate(N))
     
     U32#(tt(),N) = 2 >= 1 = activate#(N)
     
     U41#(tt(),N,XS) = 4N + 4XS + 6 >= 1 = activate#(XS)
     
     U41#(tt(),N,XS) = 4N + 4XS + 6 >= 1 = activate#(N)
     
     U41#(tt(),N,XS) = 4N + 4XS + 6 >= 4N + 4XS + 5 = U42#(tt(),activate(N),activate(XS))
     
     U42#(tt(),N,XS) = 4N + 4XS + 5 >= 1 = activate#(XS)
     
     U42#(tt(),N,XS) = 4N + 4XS + 5 >= 1 = activate#(N)
     
     U42#(tt(),N,XS) = 4N + 4XS + 5 >= 4N + 2XS + 4 = afterNth#(activate(N),activate(XS))
     
     U42#(tt(),N,XS) = 4N + 4XS + 5 >= 4 = head#(afterNth(activate(N),activate(XS)))
     
     U51#(tt(),Y) = 3 >= 1 = activate#(Y)
     
     U51#(tt(),Y) = 3 >= 2 = U52#(tt(),activate(Y))
     
     U52#(tt(),Y) = 2 >= 1 = activate#(Y)
     
     U61#(tt(),N,X,XS) = 4N + 6 >= 1 = activate#(XS)
     
     U61#(tt(),N,X,XS) = 4N + 6 >= 1 = activate#(X)
     
     U61#(tt(),N,X,XS) = 4N + 6 >= 1 = activate#(N)
     
     U61#(tt(),N,X,XS) = 4N + 6 >= 4N + 5 = U62#(tt(),activate(N),activate(X),activate(XS))
     
     U62#(tt(),N,X,XS) = 4N + 5 >= 1 = activate#(XS)
     
     U62#(tt(),N,X,XS) = 4N + 5 >= 1 = activate#(X)
     
     U62#(tt(),N,X,XS) = 4N + 5 >= 1 = activate#(N)
     
     U62#(tt(),N,X,XS) = 4N + 5 >= 4N + 4 = U63#(tt(),activate(N),activate(X),activate(XS))
     
     U63#(tt(),N,X,XS) = 4N + 4 >= 1 = activate#(X)
     
     U63#(tt(),N,X,XS) = 4N + 4 >= 1 = activate#(XS)
     
     U63#(tt(),N,X,XS) = 4N + 4 >= 1 = activate#(N)
     
     U63#(tt(),N,X,XS) = 4N + 4 >= N + 1 = splitAt#(activate(N),activate(XS))
     
     U63#(tt(),N,X,XS) = 4N + 4 >= 2 = U64#(splitAt(activate(N),activate(XS)),activate(X))
     
     U64#(pair(YS,ZS),X) = 2 >= 1 = activate#(X)
     
     U71#(tt(),XS) = 4 >= 1 = activate#(XS)
     
     U71#(tt(),XS) = 4 >= 2 = U72#(tt(),activate(XS))
     
     U72#(tt(),XS) = 2 >= 1 = activate#(XS)
     
     U81#(tt(),N,XS) = 7N + 5XS + 6 >= 1 = activate#(XS)
     
     U81#(tt(),N,XS) = 7N + 5XS + 6 >= 1 = activate#(N)
     
     U81#(tt(),N,XS) = 7N + 5XS + 6 >= 7N + 5XS + 4 = U82#(tt(),activate(N),activate(XS))
     
     U82#(tt(),N,XS) = 7N + 5XS + 4 >= 1 = activate#(XS)
     
     U82#(tt(),N,XS) = 7N + 5XS + 4 >= 1 = activate#(N)
     
     U82#(tt(),N,XS) = 7N + 5XS + 4 >= N + 1 = splitAt#(activate(N),activate(XS))
     
     U82#(tt(),N,XS) = 7N + 5XS + 4 >= 7N + 2 = fst#(splitAt(activate(N),activate(XS)))
     
     afterNth#(N,XS) = 4N + 2XS + 4 >= 3N + 2XS + 3 = U11#(tt(),N,XS)
     
     fst#(pair(X,Y)) = 16 >= 3 = U21#(tt(),X)
     
     head#(cons(N,XS)) = 4 >= 3 = U31#(tt(),N)
     
     sel#(N,XS) = 4N + 4XS + 7 >= 4N + 4XS + 6 = U41#(tt(),N,XS)
     
     snd#(pair(X,Y)) = 4 >= 3 = U51#(tt(),Y)
     
     splitAt#(s(N),cons(X,XS)) = 4N + 7 >= 1 = activate#(XS)
     
     splitAt#(s(N),cons(X,XS)) = 4N + 7 >= 4N + 6 = U61#(tt(),N,X,activate(XS))
     
     tail#(cons(N,XS)) = 7 >= 1 = activate#(XS)
     
     tail#(cons(N,XS)) = 7 >= 4 = U71#(tt(),activate(XS))
     
     take#(N,XS) = 7N + 5XS + 7 >= 7N + 5XS + 6 = U81#(tt(),N,XS)
     
     activate#(n__natsFrom(X)) = 1 >= 0 = natsFrom#(X)
     
     activate(n__natsFrom(X)) = 0 >= 0 = natsFrom(X)
     
     activate(X) = X >= X = X
     
     natsFrom(N) = 0 >= 0 = cons(N,n__natsFrom(s(N)))
     
     natsFrom(X) = 0 >= 0 = n__natsFrom(X)
     
     splitAt(0(),XS) = 2 >= 2 = pair(nil(),XS)
     
     splitAt(s(N),cons(X,XS)) = 4N + 6 >= 4N + 2 = U61(tt(),N,X,activate(XS))
     
     U61(tt(),N,X,XS) = 4N + 2 >= 2N + 2 = U62(tt(),activate(N),activate(X),activate(XS))
     
     U62(tt(),N,X,XS) = 2N + 2 >= N + 2 = U63(tt(),activate(N),activate(X),activate(XS))
     
     U63(tt(),N,X,XS) = N + 2 >= N + 2 = U64(splitAt(activate(N),activate(XS)),activate(X))
     
     U64(pair(YS,ZS),X) = 4 >= 2 = pair(cons(activate(X),YS),ZS)
     
     afterNth(N,XS) = 0 >= 6 = U11(tt(),N,XS)
     
     U11(tt(),N,XS) = 6 >= 4N + 4XS + 4 = U12(tt(),activate(N),activate(XS))
     
     U12(tt(),N,XS) = 4N + 4XS + 4 >= 2 = snd(splitAt(activate(N),activate(XS)))
     
     snd(pair(X,Y)) = 2 >= 3 = U51(tt(),Y)
     
     U51(tt(),Y) = 3 >= 8 = U52(tt(),activate(Y))
     
     U52(tt(),Y) = 8 >= Y = activate(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)) -> U61(tt(),N,X,activate(XS))
      U61(tt(),N,X,XS) -> U62(tt(),activate(N),activate(X),activate(XS))
      U62(tt(),N,X,XS) -> U63(tt(),activate(N),activate(X),activate(XS))
      U63(tt(),N,X,XS) -> U64(splitAt(activate(N),activate(XS)),activate(X))
      U64(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
      afterNth(N,XS) -> U11(tt(),N,XS)
      U11(tt(),N,XS) -> U12(tt(),activate(N),activate(XS))
      U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
      snd(pair(X,Y)) -> U51(tt(),Y)
      U51(tt(),Y) -> U52(tt(),activate(Y))
      U52(tt(),Y) -> activate(Y)
    Qed