NO
0.18/0.21	NO
0.18/0.22	
0.18/0.22	Problem:
0.18/0.22	 U11(tt()) -> snd(splitAt(N,XS))
0.18/0.22	 U161(tt()) -> cons(N)
0.18/0.22	 U171(tt()) -> head(afterNth(N,XS))
0.18/0.22	 U181(tt()) -> Y
0.18/0.22	 U191(tt()) -> pair(nil(),XS)
0.18/0.22	 U201(tt()) -> U202(splitAt(N,XS))
0.18/0.22	 U202(pair(YS,ZS)) -> pair(cons(X),ZS)
0.18/0.22	 U21(tt()) -> X
0.18/0.22	 U211(tt()) -> XS
0.18/0.22	 U221(tt()) -> fst(splitAt(N,XS))
0.18/0.22	 U31(tt()) -> N
0.18/0.22	 and(tt()) -> X
0.18/0.22	 U101(tt()) -> U102(isNatural())
0.18/0.22	 U102(tt()) -> U103(isLNat())
0.18/0.22	 U103(tt()) -> tt()
0.18/0.22	 U111(tt()) -> U112(isLNat())
0.18/0.22	 U112(tt()) -> tt()
0.18/0.22	 U121(tt()) -> U122(isNatural())
0.18/0.22	 U122(tt()) -> tt()
0.18/0.22	 U131(tt()) -> U132(isNatural())
0.18/0.22	 U132(tt()) -> U133(isLNat())
0.18/0.22	 U133(tt()) -> tt()
0.18/0.22	 U141(tt()) -> U142(isLNat())
0.18/0.22	 U142(tt()) -> U143(isLNat())
0.18/0.22	 U143(tt()) -> tt()
0.18/0.22	 U151(tt()) -> U152(isNatural())
0.18/0.22	 U152(tt()) -> U153(isLNat())
0.18/0.22	 U153(tt()) -> tt()
0.18/0.22	 U41(tt()) -> U42(isNatural())
0.18/0.22	 U42(tt()) -> U43(isLNat())
0.18/0.22	 U43(tt()) -> tt()
0.18/0.22	 U51(tt()) -> U52(isNatural())
0.18/0.22	 U52(tt()) -> U53(isLNat())
0.18/0.22	 U53(tt()) -> tt()
0.18/0.22	 U61(tt()) -> U62(isPLNat())
0.18/0.22	 U62(tt()) -> tt()
0.18/0.22	 U71(tt()) -> U72(isNatural())
0.18/0.22	 U72(tt()) -> tt()
0.18/0.22	 U81(tt()) -> U82(isPLNat())
0.18/0.22	 U82(tt()) -> tt()
0.18/0.22	 U91(tt()) -> U92(isLNat())
0.18/0.22	 U92(tt()) -> tt()
0.18/0.22	 afterNth(N,XS) -> U11(and(and(isNatural())))
0.18/0.22	 fst(pair(X,Y)) -> U21(and(and(isLNat())))
0.18/0.22	 head(cons(N)) -> U31(and(and(isNatural())))
0.18/0.22	 isLNat() -> tt()
0.18/0.22	 isLNat() -> U41(and(isNaturalKind()))
0.18/0.22	 isLNat() -> U51(and(isNaturalKind()))
0.18/0.22	 isLNat() -> U61(isPLNatKind())
0.18/0.22	 isLNat() -> U71(isNaturalKind())
0.18/0.22	 isLNat() -> U81(isPLNatKind())
0.18/0.22	 isLNat() -> U91(isLNatKind())
0.18/0.22	 isLNat() -> U101(and(isNaturalKind()))
0.18/0.22	 isLNatKind() -> tt()
0.18/0.22	 isLNatKind() -> and(isNaturalKind())
0.18/0.22	 isLNatKind() -> isPLNatKind()
0.18/0.22	 isLNatKind() -> isNaturalKind()
0.18/0.22	 isLNatKind() -> isLNatKind()
0.18/0.22	 isNatural() -> tt()
0.18/0.22	 isNatural() -> U111(isLNatKind())
0.18/0.22	 isNatural() -> U121(isNaturalKind())
0.18/0.22	 isNatural() -> U131(and(isNaturalKind()))
0.18/0.22	 isNaturalKind() -> tt()
0.18/0.22	 isNaturalKind() -> isLNatKind()
0.18/0.22	 isNaturalKind() -> isNaturalKind()
0.18/0.22	 isNaturalKind() -> and(isNaturalKind())
0.18/0.22	 isPLNat() -> U141(and(isLNatKind()))
0.18/0.22	 isPLNat() -> U151(and(isNaturalKind()))
0.18/0.22	 isPLNatKind() -> and(isLNatKind())
0.18/0.22	 isPLNatKind() -> and(isNaturalKind())
0.18/0.22	 natsFrom(N) -> U161(and(isNatural()))
0.18/0.22	 sel(N,XS) -> U171(and(and(isNatural())))
0.18/0.22	 snd(pair(X,Y)) -> U181(and(and(isLNat())))
0.18/0.22	 splitAt(0(),XS) -> U191(and(isLNat()))
0.18/0.22	 splitAt(s(N),cons(X)) -> U201(and(and(isNatural())))
0.18/0.22	 tail(cons(N)) -> U211(and(and(isNatural())))
0.18/0.22	 take(N,XS) -> U221(and(and(isNatural())))
0.18/0.22	
0.18/0.22	Proof:
0.18/0.22	 Fresh Variable Processor:
0.18/0.22	  loop length: 1
0.18/0.22	  terms:
0.18/0.22	   U11(tt())
0.18/0.22	  context: snd(splitAt([],XS))
0.18/0.22	  substitution:
0.18/0.22	   N -> U11(tt())
0.18/0.22	  Qed
0.18/0.22	EOF