(VAR N XS X Y YS ZS)
(STRATEGY CONTEXTSENSITIVE 
  (U11 1)
  (tt)
  (U12 1)
  (snd 1)
  (splitAt 1 2)
  (U21 1)
  (U22 1)
  (U31 1)
  (U32 1)
  (U41 1)
  (U42 1)
  (head 1)
  (afterNth 1 2)
  (U51 1)
  (U52 1)
  (U61 1)
  (U62 1)
  (U63 1)
  (U64 1)
  (pair 1 2)
  (cons 1)
  (U71 1)
  (U72 1)
  (U81 1)
  (U82 1)
  (fst 1)
  (natsFrom 1)
  (s 1)
  (sel 1 2)
  (0)
  (nil)
  (tail 1)
  (take 1 2)
)
(RULES 
U11(tt,N,XS) -> U12(tt,N,XS)
U12(tt,N,XS) -> snd(splitAt(N,XS))
U21(tt,X) -> U22(tt,X)
U22(tt,X) -> X
U31(tt,N) -> U32(tt,N)
U32(tt,N) -> N
U41(tt,N,XS) -> U42(tt,N,XS)
U42(tt,N,XS) -> head(afterNth(N,XS))
U51(tt,Y) -> U52(tt,Y)
U52(tt,Y) -> Y
U61(tt,N,X,XS) -> U62(tt,N,X,XS)
U62(tt,N,X,XS) -> U63(tt,N,X,XS)
U63(tt,N,X,XS) -> U64(splitAt(N,XS),X)
U64(pair(YS,ZS),X) -> pair(cons(X,YS),ZS)
U71(tt,XS) -> U72(tt,XS)
U72(tt,XS) -> XS
U81(tt,N,XS) -> U82(tt,N,XS)
U82(tt,N,XS) -> fst(splitAt(N,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,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,XS)
tail(cons(N,XS)) -> U71(tt,XS)
take(N,XS) -> U81(tt,N,XS)
)

The TRS is orthogonal, thus termination of innermost context-sensitive rewriting is equivalent to termination of context-sensitive rewriting.

Proving termination of context-sensitive rewriting for LISTUTILITIES_nosorts_noand:

-> Dependency pairs:
nF_U11(tt,N,XS) -> nF_U12(tt,N,XS)
nF_U12(tt,N,XS) -> nF_snd(splitAt(N,XS))
nF_U12(tt,N,XS) -> nF_splitAt(N,XS)
nF_U12(tt,N,XS) -> N
nF_U12(tt,N,XS) -> XS
nF_U21(tt,X) -> nF_U22(tt,X)
nF_U22(tt,X) -> X
nF_U31(tt,N) -> nF_U32(tt,N)
nF_U32(tt,N) -> N
nF_U41(tt,N,XS) -> nF_U42(tt,N,XS)
nF_U42(tt,N,XS) -> nF_head(afterNth(N,XS))
nF_U42(tt,N,XS) -> nF_afterNth(N,XS)
nF_U42(tt,N,XS) -> N
nF_U42(tt,N,XS) -> XS
nF_U51(tt,Y) -> nF_U52(tt,Y)
nF_U52(tt,Y) -> Y
nF_U61(tt,N,X,XS) -> nF_U62(tt,N,X,XS)
nF_U62(tt,N,X,XS) -> nF_U63(tt,N,X,XS)
nF_U63(tt,N,X,XS) -> nF_U64(splitAt(N,XS),X)
nF_U63(tt,N,X,XS) -> nF_splitAt(N,XS)
nF_U63(tt,N,X,XS) -> N
nF_U63(tt,N,X,XS) -> XS
nF_U64(pair(YS,ZS),X) -> X
nF_U71(tt,XS) -> nF_U72(tt,XS)
nF_U72(tt,XS) -> XS
nF_U81(tt,N,XS) -> nF_U82(tt,N,XS)
nF_U82(tt,N,XS) -> nF_fst(splitAt(N,XS))
nF_U82(tt,N,XS) -> nF_splitAt(N,XS)
nF_U82(tt,N,XS) -> N
nF_U82(tt,N,XS) -> XS
nF_afterNth(N,XS) -> nF_U11(tt,N,XS)
nF_fst(pair(X,Y)) -> nF_U21(tt,X)
nF_head(cons(N,XS)) -> nF_U31(tt,N)
nF_sel(N,XS) -> nF_U41(tt,N,XS)
nF_snd(pair(X,Y)) -> nF_U51(tt,Y)
nF_splitAt(s(N),cons(X,XS)) -> nF_U61(tt,N,X,XS)
nF_tail(cons(N,XS)) -> nF_U71(tt,XS)
nF_take(N,XS) -> nF_U81(tt,N,XS)

-> Proof of termination for LISTUTILITIES_nosorts_noand_1:
-> -> Dependency pairs in cycle:
nF_splitAt(s(N),cons(X,XS)) -> nF_U61(tt,N,X,XS)
nF_U63(tt,N,X,XS) -> nF_splitAt(N,XS)
nF_U62(tt,N,X,XS) -> nF_U63(tt,N,X,XS)
nF_U61(tt,N,X,XS) -> nF_U62(tt,N,X,XS)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in CSDG + 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.