NO
0.18/0.20	NO
0.18/0.20	
0.18/0.20	Problem:
0.18/0.20	 U12(tt()) -> snd(splitAt(N,XS))
0.18/0.20	 U161(tt()) -> cons(N)
0.18/0.20	 U172(tt()) -> head(afterNth(N,XS))
0.18/0.20	 U182(tt()) -> Y
0.18/0.20	 U191(tt()) -> pair(nil(),XS)
0.18/0.20	 U203(tt()) -> U204(splitAt(N,XS))
0.18/0.20	 U204(pair(YS,ZS)) -> pair(cons(X),ZS)
0.18/0.20	 U212(tt()) -> XS
0.18/0.20	 U22(tt()) -> X
0.18/0.20	 U222(tt()) -> fst(splitAt(N,XS))
0.18/0.20	 U32(tt()) -> N
0.18/0.20	 U101(tt()) -> U102(isLNat())
0.18/0.20	 U102(tt()) -> tt()
0.18/0.20	 U11(tt()) -> U12(isLNat())
0.18/0.20	 U111(tt()) -> tt()
0.18/0.20	 U121(tt()) -> tt()
0.18/0.20	 U131(tt()) -> U132(isLNat())
0.18/0.20	 U132(tt()) -> tt()
0.18/0.20	 U141(tt()) -> U142(isLNat())
0.18/0.20	 U142(tt()) -> tt()
0.18/0.20	 U151(tt()) -> U152(isLNat())
0.18/0.20	 U152(tt()) -> tt()
0.18/0.20	 U171(tt()) -> U172(isLNat())
0.18/0.20	 U181(tt()) -> U182(isLNat())
0.18/0.20	 U201(tt()) -> U202(isNatural())
0.18/0.20	 U202(tt()) -> U203(isLNat())
0.18/0.20	 U21(tt()) -> U22(isLNat())
0.18/0.20	 U211(tt()) -> U212(isLNat())
0.18/0.20	 U221(tt()) -> U222(isLNat())
0.18/0.20	 U31(tt()) -> U32(isLNat())
0.18/0.20	 U41(tt()) -> U42(isLNat())
0.18/0.20	 U42(tt()) -> tt()
0.18/0.20	 U51(tt()) -> U52(isLNat())
0.18/0.20	 U52(tt()) -> tt()
0.18/0.20	 U61(tt()) -> tt()
0.18/0.20	 U71(tt()) -> tt()
0.18/0.20	 U81(tt()) -> tt()
0.18/0.20	 U91(tt()) -> tt()
0.18/0.20	 afterNth(N,XS) -> U11(isNatural())
0.18/0.20	 fst(pair(X,Y)) -> U21(isLNat())
0.18/0.20	 head(cons(N)) -> U31(isNatural())
0.18/0.20	 isLNat() -> tt()
0.18/0.20	 isLNat() -> U41(isNatural())
0.18/0.20	 isLNat() -> U51(isNatural())
0.18/0.20	 isLNat() -> U61(isPLNat())
0.18/0.20	 isLNat() -> U71(isNatural())
0.18/0.20	 isLNat() -> U81(isPLNat())
0.18/0.20	 isLNat() -> U91(isLNat())
0.18/0.20	 isLNat() -> U101(isNatural())
0.18/0.20	 isNatural() -> tt()
0.18/0.20	 isNatural() -> U111(isLNat())
0.18/0.20	 isNatural() -> U121(isNatural())
0.18/0.20	 isNatural() -> U131(isNatural())
0.18/0.20	 isPLNat() -> U141(isLNat())
0.18/0.20	 isPLNat() -> U151(isNatural())
0.18/0.20	 natsFrom(N) -> U161(isNatural())
0.18/0.20	 sel(N,XS) -> U171(isNatural())
0.18/0.20	 snd(pair(X,Y)) -> U181(isLNat())
0.18/0.20	 splitAt(0(),XS) -> U191(isLNat())
0.18/0.20	 splitAt(s(N),cons(X)) -> U201(isNatural())
0.18/0.20	 tail(cons(N)) -> U211(isNatural())
0.18/0.20	 take(N,XS) -> U221(isNatural())
0.18/0.20	
0.18/0.20	Proof:
0.18/0.20	 Fresh Variable Processor:
0.18/0.20	  loop length: 1
0.18/0.20	  terms:
0.18/0.20	   U12(tt())
0.18/0.20	  context: snd(splitAt([],XS))
0.18/0.20	  substitution:
0.18/0.20	   N -> U12(tt())
0.18/0.20	  Qed
0.18/0.21	EOF