YES
(VAR N X XS YS ZS Y)
(RULES 
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
)

Proving termination of rewriting for LISTUTILITIES_nosorts_FR:

-> Dependency pairs:
nF_U11(tt,N,X,XS) -> nF_U12(splitAt(activate(N),activate(XS)),activate(X))
nF_U11(tt,N,X,XS) -> nF_splitAt(activate(N),activate(XS))
nF_U11(tt,N,X,XS) -> nF_activate(N)
nF_U11(tt,N,X,XS) -> nF_activate(XS)
nF_U11(tt,N,X,XS) -> nF_activate(X)
nF_U12(pair(YS,ZS),X) -> nF_activate(X)
nF_afterNth(N,XS) -> nF_snd(splitAt(N,XS))
nF_afterNth(N,XS) -> nF_splitAt(N,XS)
nF_and(tt,X) -> nF_activate(X)
nF_sel(N,XS) -> nF_head(afterNth(N,XS))
nF_sel(N,XS) -> nF_afterNth(N,XS)
nF_splitAt(s(N),cons(X,XS)) -> nF_U11(tt,N,X,activate(XS))
nF_splitAt(s(N),cons(X,XS)) -> nF_activate(XS)
nF_tail(cons(N,XS)) -> nF_activate(XS)
nF_take(N,XS) -> nF_fst(splitAt(N,XS))
nF_take(N,XS) -> nF_splitAt(N,XS)
nF_activate(n__natsFrom(X)) -> nF_natsFrom(activate(X))
nF_activate(n__natsFrom(X)) -> nF_activate(X)
nF_activate(n__s(X)) -> nF_s(activate(X))
nF_activate(n__s(X)) -> nF_activate(X)

-> Proof of termination for LISTUTILITIES_nosorts_FR_1_1:
-> -> Dependency pairs in cycle:
nF_U11(tt,N,X,XS) -> nF_splitAt(activate(N),activate(XS))
nF_splitAt(s(N),cons(X,XS)) -> nF_U11(tt,N,X,activate(XS))

UsableRules:
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
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

Polynomial Interpretation:

[U11](X1,X2,X3,X4) = 0
[tt] = 1
[U12](X1,X2) = 0
[splitAt](X1,X2) = 0
[activate](X) = X
[pair](X1,X2) = 0
[cons](X1,X2) = 0
[afterNth](X1,X2) = 0
[snd](X) = 0
[and](X1,X2) = 0
[fst](X) = 0
[head](X) = 0
[natsFrom](X) = 0
[n__natsFrom](X) = 0
[n__s](X) = X + 1
[sel](X1,X2) = 0
[0] = 0
[nil] = 0
[s](X) = X + 1
[tail](X) = 0
[take](X1,X2) = 0
[nF_U11](X1,X2,X3,X4) = X1 + X2
[nF_splitAt](X1,X2) = X1 + 1

TIME: 5.5902e-2


-> Proof of termination for LISTUTILITIES_nosorts_FR_1_2:
-> -> Dependency pairs in cycle:
nF_activate(n__s(X)) -> nF_activate(X)
nF_activate(n__natsFrom(X)) -> nF_activate(X)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.