0.008/0.008	NO
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	
0.008/0.008	
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	Confluence Problem:
0.008/0.008	(VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S)
0.008/0.008	(STRATEGY CONTEXTSENSITIVE
0.008/0.008	(U101 1)
0.008/0.008	(U11 1)
0.008/0.008	(U21 1)
0.008/0.008	(U31 1)
0.008/0.008	(U41 1)
0.008/0.008	(U51 1)
0.008/0.008	(U61 1)
0.008/0.008	(U71 1)
0.008/0.008	(U81 1)
0.008/0.008	(U82 1)
0.008/0.008	(U91 1)
0.008/0.008	(afterNth 1 2)
0.008/0.008	(and 1)
0.008/0.008	(fst 1)
0.008/0.008	(head 1)
0.008/0.008	(isLNat)
0.008/0.008	(isNatural)
0.008/0.008	(isPLNat)
0.008/0.008	(natsFrom 1)
0.008/0.008	(sel 1 2)
0.008/0.008	(snd 1)
0.008/0.008	(splitAt 1 2)
0.008/0.008	(tail 1)
0.008/0.008	(take 1 2)
0.008/0.008	(0)
0.008/0.008	(cons 1)
0.008/0.008	(fSNonEmpty)
0.008/0.008	(nil)
0.008/0.008	(pair 1 2)
0.008/0.008	(s 1)
0.008/0.008	(tt)
0.008/0.008	)
0.008/0.008	(RULES
0.008/0.008	U101(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S))
0.008/0.008	U11(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S))
0.008/0.008	U21(tt,X:S) -> X:S
0.008/0.008	U31(tt,N:S) -> N:S
0.008/0.008	U41(tt,N:S) -> cons(N:S,natsFrom(s(N:S)))
0.008/0.008	U51(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S))
0.008/0.008	U61(tt,Y:S) -> Y:S
0.008/0.008	U71(tt,XS:S) -> pair(nil,XS:S)
0.008/0.008	U81(tt,N:S,X:S,XS:S) -> U82(splitAt(N:S,XS:S),X:S)
0.008/0.008	U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	U91(tt,XS:S) -> XS:S
0.008/0.008	afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	and(tt,X:S) -> X:S
0.008/0.008	fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(nil) -> tt
0.008/0.008	isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isNatural(0) -> tt
0.008/0.008	isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	)
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	
0.008/0.008	CleanTRS Processor:
0.008/0.008	
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	Confluence Problem:
0.008/0.008	(VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S)
0.008/0.008	(STRATEGY CONTEXTSENSITIVE
0.008/0.008	(U101 1)
0.008/0.008	(U11 1)
0.008/0.008	(U21 1)
0.008/0.008	(U31 1)
0.008/0.008	(U41 1)
0.008/0.008	(U51 1)
0.008/0.008	(U61 1)
0.008/0.008	(U71 1)
0.008/0.008	(U81 1)
0.008/0.008	(U82 1)
0.008/0.008	(U91 1)
0.008/0.008	(afterNth 1 2)
0.008/0.008	(and 1)
0.008/0.008	(fst 1)
0.008/0.008	(head 1)
0.008/0.008	(isLNat)
0.008/0.008	(isNatural)
0.008/0.008	(isPLNat)
0.008/0.008	(natsFrom 1)
0.008/0.008	(sel 1 2)
0.008/0.008	(snd 1)
0.008/0.008	(splitAt 1 2)
0.008/0.008	(tail 1)
0.008/0.008	(take 1 2)
0.008/0.008	(0)
0.008/0.008	(cons 1)
0.008/0.008	(fSNonEmpty)
0.008/0.008	(nil)
0.008/0.008	(pair 1 2)
0.008/0.008	(s 1)
0.008/0.008	(tt)
0.008/0.008	)
0.008/0.008	(RULES
0.008/0.008	U101(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S))
0.008/0.008	U11(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S))
0.008/0.008	U21(tt,X:S) -> X:S
0.008/0.008	U31(tt,N:S) -> N:S
0.008/0.008	U41(tt,N:S) -> cons(N:S,natsFrom(s(N:S)))
0.008/0.008	U51(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S))
0.008/0.008	U61(tt,Y:S) -> Y:S
0.008/0.008	U71(tt,XS:S) -> pair(nil,XS:S)
0.008/0.008	U81(tt,N:S,X:S,XS:S) -> U82(splitAt(N:S,XS:S),X:S)
0.008/0.008	U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	U91(tt,XS:S) -> XS:S
0.008/0.008	afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	and(tt,X:S) -> X:S
0.008/0.008	fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(nil) -> tt
0.008/0.008	isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isNatural(0) -> tt
0.008/0.008	isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	)
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	
0.008/0.008	Modular Confluence Combinations Decomposition Processor:
0.008/0.008	It is a CTRS -> No modular confluence
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	CS-TRS Processor:
0.008/0.008	R is a CS-TRS
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	Confluence Problem:
0.008/0.008	(VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S)
0.008/0.008	(STRATEGY CONTEXTSENSITIVE
0.008/0.008	(U101 1)
0.008/0.008	(U11 1)
0.008/0.008	(U21 1)
0.008/0.008	(U31 1)
0.008/0.008	(U41 1)
0.008/0.008	(U51 1)
0.008/0.008	(U61 1)
0.008/0.008	(U71 1)
0.008/0.008	(U81 1)
0.008/0.008	(U82 1)
0.008/0.008	(U91 1)
0.008/0.008	(afterNth 1 2)
0.008/0.008	(and 1)
0.008/0.008	(fst 1)
0.008/0.008	(head 1)
0.008/0.008	(isLNat)
0.008/0.008	(isNatural)
0.008/0.008	(isPLNat)
0.008/0.008	(natsFrom 1)
0.008/0.008	(sel 1 2)
0.008/0.008	(snd 1)
0.008/0.008	(splitAt 1 2)
0.008/0.008	(tail 1)
0.008/0.008	(take 1 2)
0.008/0.008	(0)
0.008/0.008	(cons 1)
0.008/0.008	(fSNonEmpty)
0.008/0.008	(nil)
0.008/0.008	(pair 1 2)
0.008/0.008	(s 1)
0.008/0.008	(tt)
0.008/0.008	)
0.008/0.008	(RULES
0.008/0.008	U101(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S))
0.008/0.008	U11(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S))
0.008/0.008	U21(tt,X:S) -> X:S
0.008/0.008	U31(tt,N:S) -> N:S
0.008/0.008	U41(tt,N:S) -> cons(N:S,natsFrom(s(N:S)))
0.008/0.008	U51(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S))
0.008/0.008	U61(tt,Y:S) -> Y:S
0.008/0.008	U71(tt,XS:S) -> pair(nil,XS:S)
0.008/0.008	U81(tt,N:S,X:S,XS:S) -> U82(splitAt(N:S,XS:S),X:S)
0.008/0.008	U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	U91(tt,XS:S) -> XS:S
0.008/0.008	afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	and(tt,X:S) -> X:S
0.008/0.008	fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(nil) -> tt
0.008/0.008	isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isNatural(0) -> tt
0.008/0.008	isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	)
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	
0.008/0.008	Extended u-Critical Pairs NonLHRV Processor [JLAMP21]:
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 10 (l' :-> r') => U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> U82(pair(YS:S,ZS:S),X:S)}
0.008/0.008	 s => pair(cons(x23:S,U82(pair(YS:S,ZS:S),X:S)),x25:S)
0.008/0.008	 t => U82(pair(pair(cons(X:S,YS:S),ZS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 11 (l' :-> r') => U91(tt,XS:S) -> XS:S
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> U91(tt,XS:S)}
0.008/0.008	 s => pair(cons(x23:S,U91(tt,XS:S)),x25:S)
0.008/0.008	 t => U82(pair(XS:S,x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 12 (l' :-> r') => afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> afterNth(N:S,XS:S)}
0.008/0.008	 s => pair(cons(x23:S,afterNth(N:S,XS:S)),x25:S)
0.008/0.008	 t => U82(pair(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 13 (l' :-> r') => and(tt,X:S) -> X:S
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> and(tt,X:S)}
0.008/0.008	 s => pair(cons(x23:S,and(tt,X:S)),x25:S)
0.008/0.008	 t => U82(pair(X:S,x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 14 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> fst(pair(X:S,Y:S))}
0.008/0.008	 s => pair(cons(x23:S,fst(pair(X:S,Y:S))),x25:S)
0.008/0.008	 t => U82(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 15 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> head(cons(N:S,XS:S))}
0.008/0.008	 s => pair(cons(x23:S,head(cons(N:S,XS:S))),x25:S)
0.008/0.008	 t => U82(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 16 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(afterNth(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(afterNth(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 17 (l' :-> r') => isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(fst(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(fst(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isPLNat(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 18 (l' :-> r') => isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(natsFrom(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(natsFrom(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isNatural(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 19 (l' :-> r') => isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(snd(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(snd(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isPLNat(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 20 (l' :-> r') => isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(tail(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(tail(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isLNat(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 21 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(take(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(take(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 22 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(cons(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isLNat(cons(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 23 (l' :-> r') => isLNat(nil) -> tt
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isLNat(nil)}
0.008/0.008	 s => pair(cons(x23:S,isLNat(nil)),x25:S)
0.008/0.008	 t => U82(pair(tt,x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 24 (l' :-> r') => isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isNatural(head(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isNatural(head(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isLNat(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 25 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isNatural(sel(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isNatural(sel(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 26 (l' :-> r') => isNatural(0) -> tt
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isNatural(0)}
0.008/0.008	 s => pair(cons(x23:S,isNatural(0)),x25:S)
0.008/0.008	 t => U82(pair(tt,x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 27 (l' :-> r') => isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isNatural(s(V1:S))}
0.008/0.008	 s => pair(cons(x23:S,isNatural(s(V1:S))),x25:S)
0.008/0.008	 t => U82(pair(isNatural(V1:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 28 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isPLNat(splitAt(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isPLNat(splitAt(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 29 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> isPLNat(pair(V1:S,V2:S))}
0.008/0.008	 s => pair(cons(x23:S,isPLNat(pair(V1:S,V2:S))),x25:S)
0.008/0.008	 t => U82(pair(and(isLNat(V1:S),isLNat(V2:S)),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 30 (l' :-> r') => natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> natsFrom(N:S)}
0.008/0.008	 s => pair(cons(x23:S,natsFrom(N:S)),x25:S)
0.008/0.008	 t => U82(pair(U41(isNatural(N:S),N:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> sel(N:S,XS:S)}
0.008/0.008	 s => pair(cons(x23:S,sel(N:S,XS:S)),x25:S)
0.008/0.008	 t => U82(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => pair(cons(x23:S,snd(pair(X:S,Y:S))),x25:S)
0.008/0.008	 t => U82(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> splitAt(0,XS:S)}
0.008/0.008	 s => pair(cons(x23:S,splitAt(0,XS:S)),x25:S)
0.008/0.008	 t => U82(pair(U71(isLNat(XS:S),XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => pair(cons(x23:S,splitAt(s(N:S),cons(X:S,XS:S))),x25:S)
0.008/0.008	 t => U82(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => pair(cons(x23:S,tail(cons(N:S,XS:S))),x25:S)
0.008/0.008	 t => U82(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x24:S
0.008/0.008	 Pos x24:S in l => [1,1]
0.008/0.008	 Sigma => {x24:S -> take(N:S,XS:S)}
0.008/0.008	 s => pair(cons(x23:S,take(N:S,XS:S)),x25:S)
0.008/0.008	 t => U82(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 12 (l' :-> r') => afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> afterNth(N:S,XS:S)}
0.008/0.008	 s => U11(and(isNatural(afterNth(N:S,XS:S)),isLNat(x28:S)),afterNth(N:S,XS:S),x28:S)
0.008/0.008	 t => afterNth(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 13 (l' :-> r') => and(tt,X:S) -> X:S
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> and(tt,X:S)}
0.008/0.008	 s => U11(and(isNatural(and(tt,X:S)),isLNat(x28:S)),and(tt,X:S),x28:S)
0.008/0.008	 t => afterNth(X:S,x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 14 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> fst(pair(X:S,Y:S))}
0.008/0.008	 s => U11(and(isNatural(fst(pair(X:S,Y:S))),isLNat(x28:S)),fst(pair(X:S,Y:S)),x28:S)
0.008/0.008	 t => afterNth(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 15 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> head(cons(N:S,XS:S))}
0.008/0.008	 s => U11(and(isNatural(head(cons(N:S,XS:S))),isLNat(x28:S)),head(cons(N:S,XS:S)),x28:S)
0.008/0.008	 t => afterNth(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x28:S)
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 16 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(afterNth(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(x28:S)),isLNat(afterNth(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 17 (l' :-> r') => isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(fst(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(fst(V1:S))),isLNat(x28:S)),isLNat(fst(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isPLNat(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 18 (l' :-> r') => isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(natsFrom(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(x28:S)),isLNat(natsFrom(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isNatural(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 19 (l' :-> r') => isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(snd(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(snd(V1:S))),isLNat(x28:S)),isLNat(snd(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isPLNat(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 20 (l' :-> r') => isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(tail(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(tail(V1:S))),isLNat(x28:S)),isLNat(tail(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isLNat(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 21 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(take(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(x28:S)),isLNat(take(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 22 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(cons(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(x28:S)),isLNat(cons(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 23 (l' :-> r') => isLNat(nil) -> tt
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isLNat(nil)}
0.008/0.008	 s => U11(and(isNatural(isLNat(nil)),isLNat(x28:S)),isLNat(nil),x28:S)
0.008/0.008	 t => afterNth(tt,x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 24 (l' :-> r') => isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isNatural(head(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isNatural(head(V1:S))),isLNat(x28:S)),isNatural(head(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isLNat(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 25 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isNatural(sel(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(x28:S)),isNatural(sel(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 26 (l' :-> r') => isNatural(0) -> tt
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isNatural(0)}
0.008/0.008	 s => U11(and(isNatural(isNatural(0)),isLNat(x28:S)),isNatural(0),x28:S)
0.008/0.008	 t => afterNth(tt,x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 27 (l' :-> r') => isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isNatural(s(V1:S))}
0.008/0.008	 s => U11(and(isNatural(isNatural(s(V1:S))),isLNat(x28:S)),isNatural(s(V1:S)),x28:S)
0.008/0.008	 t => afterNth(isNatural(V1:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 28 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isPLNat(splitAt(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(x28:S)),isPLNat(splitAt(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 29 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> isPLNat(pair(V1:S,V2:S))}
0.008/0.008	 s => U11(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(x28:S)),isPLNat(pair(V1:S,V2:S)),x28:S)
0.008/0.008	 t => afterNth(and(isLNat(V1:S),isLNat(V2:S)),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 30 (l' :-> r') => natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> natsFrom(N:S)}
0.008/0.008	 s => U11(and(isNatural(natsFrom(N:S)),isLNat(x28:S)),natsFrom(N:S),x28:S)
0.008/0.008	 t => afterNth(U41(isNatural(N:S),N:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> sel(N:S,XS:S)}
0.008/0.008	 s => U11(and(isNatural(sel(N:S,XS:S)),isLNat(x28:S)),sel(N:S,XS:S),x28:S)
0.008/0.008	 t => afterNth(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U11(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x28:S)),snd(pair(X:S,Y:S)),x28:S)
0.008/0.008	 t => afterNth(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U11(and(isNatural(splitAt(0,XS:S)),isLNat(x28:S)),splitAt(0,XS:S),x28:S)
0.008/0.008	 t => afterNth(U71(isLNat(XS:S),XS:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U11(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x28:S)),splitAt(s(N:S),cons(X:S,XS:S)),x28:S)
0.008/0.008	 t => afterNth(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U11(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x28:S)),tail(cons(N:S,XS:S)),x28:S)
0.008/0.008	 t => afterNth(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x27:S
0.008/0.008	 Pos x27:S in l => [1]
0.008/0.008	 Sigma => {x27:S -> take(N:S,XS:S)}
0.008/0.008	 s => U11(and(isNatural(take(N:S,XS:S)),isLNat(x28:S)),take(N:S,XS:S),x28:S)
0.008/0.008	 t => afterNth(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 14 (l' :-> r') => fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> fst(pair(X:S,Y:S))}
0.008/0.008	 s => U21(and(isLNat(fst(pair(X:S,Y:S))),isLNat(x31:S)),fst(pair(X:S,Y:S)))
0.008/0.008	 t => fst(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x31:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 15 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> head(cons(N:S,XS:S))}
0.008/0.008	 s => U21(and(isLNat(head(cons(N:S,XS:S))),isLNat(x31:S)),head(cons(N:S,XS:S)))
0.008/0.008	 t => fst(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 16 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(afterNth(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(afterNth(V1:S,V2:S))),isLNat(x31:S)),isLNat(afterNth(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 17 (l' :-> r') => isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(fst(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(fst(V1:S))),isLNat(x31:S)),isLNat(fst(V1:S)))
0.008/0.008	 t => fst(pair(isPLNat(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 18 (l' :-> r') => isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(natsFrom(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(natsFrom(V1:S))),isLNat(x31:S)),isLNat(natsFrom(V1:S)))
0.008/0.008	 t => fst(pair(isNatural(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 19 (l' :-> r') => isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(snd(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(snd(V1:S))),isLNat(x31:S)),isLNat(snd(V1:S)))
0.008/0.008	 t => fst(pair(isPLNat(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 20 (l' :-> r') => isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(tail(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(tail(V1:S))),isLNat(x31:S)),isLNat(tail(V1:S)))
0.008/0.008	 t => fst(pair(isLNat(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 21 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(take(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(take(V1:S,V2:S))),isLNat(x31:S)),isLNat(take(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 22 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(cons(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isLNat(cons(V1:S,V2:S))),isLNat(x31:S)),isLNat(cons(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 23 (l' :-> r') => isLNat(nil) -> tt
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isLNat(nil)}
0.008/0.008	 s => U21(and(isLNat(isLNat(nil)),isLNat(x31:S)),isLNat(nil))
0.008/0.008	 t => fst(pair(tt,x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 24 (l' :-> r') => isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isNatural(head(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isNatural(head(V1:S))),isLNat(x31:S)),isNatural(head(V1:S)))
0.008/0.008	 t => fst(pair(isLNat(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 25 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isNatural(sel(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isNatural(sel(V1:S,V2:S))),isLNat(x31:S)),isNatural(sel(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 26 (l' :-> r') => isNatural(0) -> tt
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isNatural(0)}
0.008/0.008	 s => U21(and(isLNat(isNatural(0)),isLNat(x31:S)),isNatural(0))
0.008/0.008	 t => fst(pair(tt,x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 27 (l' :-> r') => isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isNatural(s(V1:S))}
0.008/0.008	 s => U21(and(isLNat(isNatural(s(V1:S))),isLNat(x31:S)),isNatural(s(V1:S)))
0.008/0.008	 t => fst(pair(isNatural(V1:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 28 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isPLNat(splitAt(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isPLNat(splitAt(V1:S,V2:S))),isLNat(x31:S)),isPLNat(splitAt(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 29 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> isPLNat(pair(V1:S,V2:S))}
0.008/0.008	 s => U21(and(isLNat(isPLNat(pair(V1:S,V2:S))),isLNat(x31:S)),isPLNat(pair(V1:S,V2:S)))
0.008/0.008	 t => fst(pair(and(isLNat(V1:S),isLNat(V2:S)),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 30 (l' :-> r') => natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> natsFrom(N:S)}
0.008/0.008	 s => U21(and(isLNat(natsFrom(N:S)),isLNat(x31:S)),natsFrom(N:S))
0.008/0.008	 t => fst(pair(U41(isNatural(N:S),N:S),x31:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> sel(N:S,XS:S)}
0.008/0.008	 s => U21(and(isLNat(sel(N:S,XS:S)),isLNat(x31:S)),sel(N:S,XS:S))
0.008/0.008	 t => fst(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U21(and(isLNat(snd(pair(X:S,Y:S))),isLNat(x31:S)),snd(pair(X:S,Y:S)))
0.008/0.008	 t => fst(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x31:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U21(and(isLNat(splitAt(0,XS:S)),isLNat(x31:S)),splitAt(0,XS:S))
0.008/0.008	 t => fst(pair(U71(isLNat(XS:S),XS:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U21(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x31:S)),splitAt(s(N:S),cons(X:S,XS:S)))
0.008/0.008	 t => fst(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x31:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U21(and(isLNat(tail(cons(N:S,XS:S))),isLNat(x31:S)),tail(cons(N:S,XS:S)))
0.008/0.008	 t => fst(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x31:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x30:S
0.008/0.008	 Pos x30:S in l => [1,1]
0.008/0.008	 Sigma => {x30:S -> take(N:S,XS:S)}
0.008/0.008	 s => U21(and(isLNat(take(N:S,XS:S)),isLNat(x31:S)),take(N:S,XS:S))
0.008/0.008	 t => fst(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x31:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 15 (l' :-> r') => head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> head(cons(N:S,XS:S))}
0.008/0.008	 s => U31(and(isNatural(head(cons(N:S,XS:S))),isLNat(x33:S)),head(cons(N:S,XS:S)))
0.008/0.008	 t => head(cons(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x33:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 16 (l' :-> r') => isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(afterNth(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(x33:S)),isLNat(afterNth(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 17 (l' :-> r') => isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(fst(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(fst(V1:S))),isLNat(x33:S)),isLNat(fst(V1:S)))
0.008/0.008	 t => head(cons(isPLNat(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 18 (l' :-> r') => isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(natsFrom(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(x33:S)),isLNat(natsFrom(V1:S)))
0.008/0.008	 t => head(cons(isNatural(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 19 (l' :-> r') => isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(snd(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(snd(V1:S))),isLNat(x33:S)),isLNat(snd(V1:S)))
0.008/0.008	 t => head(cons(isPLNat(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 20 (l' :-> r') => isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(tail(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(tail(V1:S))),isLNat(x33:S)),isLNat(tail(V1:S)))
0.008/0.008	 t => head(cons(isLNat(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 21 (l' :-> r') => isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(take(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(x33:S)),isLNat(take(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 22 (l' :-> r') => isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(cons(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(x33:S)),isLNat(cons(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 23 (l' :-> r') => isLNat(nil) -> tt
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isLNat(nil)}
0.008/0.008	 s => U31(and(isNatural(isLNat(nil)),isLNat(x33:S)),isLNat(nil))
0.008/0.008	 t => head(cons(tt,x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 24 (l' :-> r') => isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isNatural(head(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isNatural(head(V1:S))),isLNat(x33:S)),isNatural(head(V1:S)))
0.008/0.008	 t => head(cons(isLNat(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 25 (l' :-> r') => isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isNatural(sel(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(x33:S)),isNatural(sel(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 26 (l' :-> r') => isNatural(0) -> tt
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isNatural(0)}
0.008/0.008	 s => U31(and(isNatural(isNatural(0)),isLNat(x33:S)),isNatural(0))
0.008/0.008	 t => head(cons(tt,x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 27 (l' :-> r') => isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isNatural(s(V1:S))}
0.008/0.008	 s => U31(and(isNatural(isNatural(s(V1:S))),isLNat(x33:S)),isNatural(s(V1:S)))
0.008/0.008	 t => head(cons(isNatural(V1:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 28 (l' :-> r') => isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isPLNat(splitAt(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(x33:S)),isPLNat(splitAt(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 29 (l' :-> r') => isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> isPLNat(pair(V1:S,V2:S))}
0.008/0.008	 s => U31(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(x33:S)),isPLNat(pair(V1:S,V2:S)))
0.008/0.008	 t => head(cons(and(isLNat(V1:S),isLNat(V2:S)),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 30 (l' :-> r') => natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> natsFrom(N:S)}
0.008/0.008	 s => U31(and(isNatural(natsFrom(N:S)),isLNat(x33:S)),natsFrom(N:S))
0.008/0.008	 t => head(cons(U41(isNatural(N:S),N:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> sel(N:S,XS:S)}
0.008/0.008	 s => U31(and(isNatural(sel(N:S,XS:S)),isLNat(x33:S)),sel(N:S,XS:S))
0.008/0.008	 t => head(cons(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x33:S))
0.008/0.008	 NW => 0
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U31(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x33:S)),snd(pair(X:S,Y:S)))
0.008/0.008	 t => head(cons(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U31(and(isNatural(splitAt(0,XS:S)),isLNat(x33:S)),splitAt(0,XS:S))
0.008/0.008	 t => head(cons(U71(isLNat(XS:S),XS:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U31(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x33:S)),splitAt(s(N:S),cons(X:S,XS:S)))
0.008/0.008	 t => head(cons(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U31(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x33:S)),tail(cons(N:S,XS:S)))
0.008/0.008	 t => head(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x32:S
0.008/0.008	 Pos x32:S in l => [1,1]
0.008/0.008	 Sigma => {x32:S -> take(N:S,XS:S)}
0.008/0.008	 s => U31(and(isNatural(take(N:S,XS:S)),isLNat(x33:S)),take(N:S,XS:S))
0.008/0.008	 t => head(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x33:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 30 (l' :-> r') => natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> natsFrom(N:S)}
0.008/0.008	 s => U41(isNatural(natsFrom(N:S)),natsFrom(N:S))
0.008/0.008	 t => natsFrom(U41(isNatural(N:S),N:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> sel(N:S,XS:S)}
0.008/0.008	 s => U41(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S))
0.008/0.008	 t => natsFrom(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U41(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S)))
0.008/0.008	 t => natsFrom(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U41(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S))
0.008/0.008	 t => natsFrom(U71(isLNat(XS:S),XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U41(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)))
0.008/0.008	 t => natsFrom(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U41(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)))
0.008/0.008	 t => natsFrom(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x52:S
0.008/0.008	 Pos x52:S in l => [1]
0.008/0.008	 Sigma => {x52:S -> take(N:S,XS:S)}
0.008/0.008	 s => U41(isNatural(take(N:S,XS:S)),take(N:S,XS:S))
0.008/0.008	 t => natsFrom(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 31 (l' :-> r') => sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> sel(N:S,XS:S)}
0.008/0.008	 s => U51(and(isNatural(sel(N:S,XS:S)),isLNat(x54:S)),sel(N:S,XS:S),x54:S)
0.008/0.008	 t => sel(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U51(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x54:S)),snd(pair(X:S,Y:S)),x54:S)
0.008/0.008	 t => sel(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U51(and(isNatural(splitAt(0,XS:S)),isLNat(x54:S)),splitAt(0,XS:S),x54:S)
0.008/0.008	 t => sel(U71(isLNat(XS:S),XS:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U51(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x54:S)),splitAt(s(N:S),cons(X:S,XS:S)),x54:S)
0.008/0.008	 t => sel(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U51(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x54:S)),tail(cons(N:S,XS:S)),x54:S)
0.008/0.008	 t => sel(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x53:S
0.008/0.008	 Pos x53:S in l => [1]
0.008/0.008	 Sigma => {x53:S -> take(N:S,XS:S)}
0.008/0.008	 s => U51(and(isNatural(take(N:S,XS:S)),isLNat(x54:S)),take(N:S,XS:S),x54:S)
0.008/0.008	 t => sel(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x54:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S)
0.008/0.008	 Rule 32 (l' :-> r') => snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 Var => x55:S
0.008/0.008	 Pos x55:S in l => [1,1]
0.008/0.008	 Sigma => {x55:S -> snd(pair(X:S,Y:S))}
0.008/0.008	 s => U61(and(isLNat(snd(pair(X:S,Y:S))),isLNat(x56:S)),x56:S)
0.008/0.008	 t => snd(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x56:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x55:S
0.008/0.008	 Pos x55:S in l => [1,1]
0.008/0.008	 Sigma => {x55:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U61(and(isLNat(splitAt(0,XS:S)),isLNat(x56:S)),x56:S)
0.008/0.008	 t => snd(pair(U71(isLNat(XS:S),XS:S),x56:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x55:S
0.008/0.008	 Pos x55:S in l => [1,1]
0.008/0.008	 Sigma => {x55:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U61(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x56:S)),x56:S)
0.008/0.008	 t => snd(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x56:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x55:S
0.008/0.008	 Pos x55:S in l => [1,1]
0.008/0.008	 Sigma => {x55:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U61(and(isLNat(tail(cons(N:S,XS:S))),isLNat(x56:S)),x56:S)
0.008/0.008	 t => snd(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x56:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x55:S
0.008/0.008	 Pos x55:S in l => [1,1]
0.008/0.008	 Sigma => {x55:S -> take(N:S,XS:S)}
0.008/0.008	 s => U61(and(isLNat(take(N:S,XS:S)),isLNat(x56:S)),x56:S)
0.008/0.008	 t => snd(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x56:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(0,x57:S) -> U71(isLNat(x57:S),x57:S)
0.008/0.008	 Rule 33 (l' :-> r') => splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 Var => x57:S
0.008/0.008	 Pos x57:S in l => [2]
0.008/0.008	 Sigma => {x57:S -> splitAt(0,XS:S)}
0.008/0.008	 s => U71(isLNat(splitAt(0,XS:S)),splitAt(0,XS:S))
0.008/0.008	 t => splitAt(0,U71(isLNat(XS:S),XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(0,x57:S) -> U71(isLNat(x57:S),x57:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x57:S
0.008/0.008	 Pos x57:S in l => [2]
0.008/0.008	 Sigma => {x57:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U71(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S)))
0.008/0.008	 t => splitAt(0,U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(0,x57:S) -> U71(isLNat(x57:S),x57:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x57:S
0.008/0.008	 Pos x57:S in l => [2]
0.008/0.008	 Sigma => {x57:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U71(isLNat(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S)))
0.008/0.008	 t => splitAt(0,U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(0,x57:S) -> U71(isLNat(x57:S),x57:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x57:S
0.008/0.008	 Pos x57:S in l => [2]
0.008/0.008	 Sigma => {x57:S -> take(N:S,XS:S)}
0.008/0.008	 s => U71(isLNat(take(N:S,XS:S)),take(N:S,XS:S))
0.008/0.008	 t => splitAt(0,U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(s(x58:S),cons(x59:S,x60:S)) -> U81(and(isNatural(x58:S),and(isNatural(x59:S),isLNat(x60:S))),x58:S,x59:S,x60:S)
0.008/0.008	 Rule 34 (l' :-> r') => splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 Var => x58:S
0.008/0.008	 Pos x58:S in l => [1,1]
0.008/0.008	 Sigma => {x58:S -> splitAt(s(N:S),cons(X:S,XS:S))}
0.008/0.008	 s => U81(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),and(isNatural(x59:S),isLNat(x60:S))),splitAt(s(N:S),cons(X:S,XS:S)),x59:S,x60:S)
0.008/0.008	 t => splitAt(s(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)),cons(x59:S,x60:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(s(x58:S),cons(x59:S,x60:S)) -> U81(and(isNatural(x58:S),and(isNatural(x59:S),isLNat(x60:S))),x58:S,x59:S,x60:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x58:S
0.008/0.008	 Pos x58:S in l => [1,1]
0.008/0.008	 Sigma => {x58:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U81(and(isNatural(tail(cons(N:S,XS:S))),and(isNatural(x59:S),isLNat(x60:S))),tail(cons(N:S,XS:S)),x59:S,x60:S)
0.008/0.008	 t => splitAt(s(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)),cons(x59:S,x60:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => splitAt(s(x58:S),cons(x59:S,x60:S)) -> U81(and(isNatural(x58:S),and(isNatural(x59:S),isLNat(x60:S))),x58:S,x59:S,x60:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x58:S
0.008/0.008	 Pos x58:S in l => [1,1]
0.008/0.008	 Sigma => {x58:S -> take(N:S,XS:S)}
0.008/0.008	 s => U81(and(isNatural(take(N:S,XS:S)),and(isNatural(x59:S),isLNat(x60:S))),take(N:S,XS:S),x59:S,x60:S)
0.008/0.008	 t => splitAt(s(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)),cons(x59:S,x60:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => tail(cons(x61:S,x62:S)) -> U91(and(isNatural(x61:S),isLNat(x62:S)),x62:S)
0.008/0.008	 Rule 35 (l' :-> r') => tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 Var => x61:S
0.008/0.008	 Pos x61:S in l => [1,1]
0.008/0.008	 Sigma => {x61:S -> tail(cons(N:S,XS:S))}
0.008/0.008	 s => U91(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x62:S)),x62:S)
0.008/0.008	 t => tail(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x62:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => tail(cons(x61:S,x62:S)) -> U91(and(isNatural(x61:S),isLNat(x62:S)),x62:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x61:S
0.008/0.008	 Pos x61:S in l => [1,1]
0.008/0.008	 Sigma => {x61:S -> take(N:S,XS:S)}
0.008/0.008	 s => U91(and(isNatural(take(N:S,XS:S)),isLNat(x62:S)),x62:S)
0.008/0.008	 t => tail(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x62:S))
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	->Extended u-Critical Pair:
0.008/0.008	 Rule 1 (l :-> r) => take(x63:S,x64:S) -> U101(and(isNatural(x63:S),isLNat(x64:S)),x63:S,x64:S)
0.008/0.008	 Rule 36 (l' :-> r') => take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 Var => x63:S
0.008/0.008	 Pos x63:S in l => [1]
0.008/0.008	 Sigma => {x63:S -> take(N:S,XS:S)}
0.008/0.008	 s => U101(and(isNatural(take(N:S,XS:S)),isLNat(x64:S)),take(N:S,XS:S),x64:S)
0.008/0.008	 t => take(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x64:S)
0.008/0.008	 NW => 1
0.008/0.008	
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	Confluence Problem:
0.008/0.008	(VAR vNonEmpty:S N:S V1:S V2:S X:S XS:S Y:S YS:S ZS:S)
0.008/0.008	(STRATEGY CONTEXTSENSITIVE
0.008/0.008	(U101 1)
0.008/0.008	(U11 1)
0.008/0.008	(U21 1)
0.008/0.008	(U31 1)
0.008/0.008	(U41 1)
0.008/0.008	(U51 1)
0.008/0.008	(U61 1)
0.008/0.008	(U71 1)
0.008/0.008	(U81 1)
0.008/0.008	(U82 1)
0.008/0.008	(U91 1)
0.008/0.008	(afterNth 1 2)
0.008/0.008	(and 1)
0.008/0.008	(fst 1)
0.008/0.008	(head 1)
0.008/0.008	(isLNat)
0.008/0.008	(isNatural)
0.008/0.008	(isPLNat)
0.008/0.008	(natsFrom 1)
0.008/0.008	(sel 1 2)
0.008/0.008	(snd 1)
0.008/0.008	(splitAt 1 2)
0.008/0.008	(tail 1)
0.008/0.008	(take 1 2)
0.008/0.008	(0)
0.008/0.008	(cons 1)
0.008/0.008	(fSNonEmpty)
0.008/0.008	(nil)
0.008/0.008	(pair 1 2)
0.008/0.008	(s 1)
0.008/0.008	(tt)
0.008/0.008	)
0.008/0.008	(RULES
0.008/0.008	U101(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S))
0.008/0.008	U11(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S))
0.008/0.008	U21(tt,X:S) -> X:S
0.008/0.008	U31(tt,N:S) -> N:S
0.008/0.008	U41(tt,N:S) -> cons(N:S,natsFrom(s(N:S)))
0.008/0.008	U51(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S))
0.008/0.008	U61(tt,Y:S) -> Y:S
0.008/0.008	U71(tt,XS:S) -> pair(nil,XS:S)
0.008/0.008	U81(tt,N:S,X:S,XS:S) -> U82(splitAt(N:S,XS:S),X:S)
0.008/0.008	U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	U91(tt,XS:S) -> XS:S
0.008/0.008	afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	and(tt,X:S) -> X:S
0.008/0.008	fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isLNat(nil) -> tt
0.008/0.008	isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isNatural(0) -> tt
0.008/0.008	isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	)
0.008/0.008	Critical Pairs:
0.008/0.008	<pair(cons(x23:S,U82(pair(YS:S,ZS:S),X:S)),x25:S),U82(pair(pair(cons(X:S,YS:S),ZS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N1
0.008/0.008	<pair(cons(x23:S,U91(tt,XS:S)),x25:S),U82(pair(XS:S,x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N2
0.008/0.008	<pair(cons(x23:S,afterNth(N:S,XS:S)),x25:S),U82(pair(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N3
0.008/0.008	<pair(cons(x23:S,and(tt,X:S)),x25:S),U82(pair(X:S,x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N4
0.008/0.008	<pair(cons(x23:S,fst(pair(X:S,Y:S))),x25:S),U82(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N5
0.008/0.008	<pair(cons(x23:S,head(cons(N:S,XS:S))),x25:S),U82(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N6
0.008/0.008	<pair(cons(x23:S,isLNat(afterNth(V1:S,V2:S))),x25:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N7
0.008/0.008	<pair(cons(x23:S,isLNat(fst(V1:S))),x25:S),U82(pair(isPLNat(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N8
0.008/0.008	<pair(cons(x23:S,isLNat(natsFrom(V1:S))),x25:S),U82(pair(isNatural(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N9
0.008/0.008	<pair(cons(x23:S,isLNat(snd(V1:S))),x25:S),U82(pair(isPLNat(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N10
0.008/0.008	<pair(cons(x23:S,isLNat(tail(V1:S))),x25:S),U82(pair(isLNat(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N11
0.008/0.008	<pair(cons(x23:S,isLNat(take(V1:S,V2:S))),x25:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N12
0.008/0.008	<pair(cons(x23:S,isLNat(cons(V1:S,V2:S))),x25:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N13
0.008/0.008	<pair(cons(x23:S,isLNat(nil)),x25:S),U82(pair(tt,x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N14
0.008/0.008	<pair(cons(x23:S,isNatural(head(V1:S))),x25:S),U82(pair(isLNat(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N15
0.008/0.008	<pair(cons(x23:S,isNatural(sel(V1:S,V2:S))),x25:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N16
0.008/0.008	<pair(cons(x23:S,isNatural(0)),x25:S),U82(pair(tt,x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N17
0.008/0.008	<pair(cons(x23:S,isNatural(s(V1:S))),x25:S),U82(pair(isNatural(V1:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N18
0.008/0.008	<pair(cons(x23:S,isPLNat(splitAt(V1:S,V2:S))),x25:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N19
0.008/0.008	<pair(cons(x23:S,isPLNat(pair(V1:S,V2:S))),x25:S),U82(pair(and(isLNat(V1:S),isLNat(V2:S)),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N20
0.008/0.008	<pair(cons(x23:S,natsFrom(N:S)),x25:S),U82(pair(U41(isNatural(N:S),N:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N21
0.008/0.008	<pair(cons(x23:S,sel(N:S,XS:S)),x25:S),U82(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N22
0.008/0.008	<pair(cons(x23:S,snd(pair(X:S,Y:S))),x25:S),U82(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N23
0.008/0.008	<pair(cons(x23:S,splitAt(0,XS:S)),x25:S),U82(pair(U71(isLNat(XS:S),XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N24
0.008/0.008	<pair(cons(x23:S,splitAt(s(N:S),cons(X:S,XS:S))),x25:S),U82(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N25
0.008/0.008	<pair(cons(x23:S,tail(cons(N:S,XS:S))),x25:S),U82(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N26
0.008/0.008	<pair(cons(x23:S,take(N:S,XS:S)),x25:S),U82(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x25:S),x23:S)>   =>  Not trivial, Not overlay, NW1, N27
0.008/0.008	<U11(and(isNatural(afterNth(N:S,XS:S)),isLNat(x28:S)),afterNth(N:S,XS:S),x28:S),afterNth(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N28
0.008/0.008	<U11(and(isNatural(and(tt,X:S)),isLNat(x28:S)),and(tt,X:S),x28:S),afterNth(X:S,x28:S)>   =>  Not trivial, Not overlay, NW1, N29
0.008/0.008	<U11(and(isNatural(fst(pair(X:S,Y:S))),isLNat(x28:S)),fst(pair(X:S,Y:S)),x28:S),afterNth(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N30
0.008/0.008	<U11(and(isNatural(head(cons(N:S,XS:S))),isLNat(x28:S)),head(cons(N:S,XS:S)),x28:S),afterNth(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x28:S)>   =>  Not trivial, Not overlay, NW0, N31
0.008/0.008	<U11(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(x28:S)),isLNat(afterNth(V1:S,V2:S)),x28:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N32
0.008/0.008	<U11(and(isNatural(isLNat(fst(V1:S))),isLNat(x28:S)),isLNat(fst(V1:S)),x28:S),afterNth(isPLNat(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N33
0.008/0.008	<U11(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(x28:S)),isLNat(natsFrom(V1:S)),x28:S),afterNth(isNatural(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N34
0.008/0.008	<U11(and(isNatural(isLNat(snd(V1:S))),isLNat(x28:S)),isLNat(snd(V1:S)),x28:S),afterNth(isPLNat(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N35
0.008/0.008	<U11(and(isNatural(isLNat(tail(V1:S))),isLNat(x28:S)),isLNat(tail(V1:S)),x28:S),afterNth(isLNat(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N36
0.008/0.008	<U11(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(x28:S)),isLNat(take(V1:S,V2:S)),x28:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N37
0.008/0.008	<U11(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(x28:S)),isLNat(cons(V1:S,V2:S)),x28:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N38
0.008/0.008	<U11(and(isNatural(isLNat(nil)),isLNat(x28:S)),isLNat(nil),x28:S),afterNth(tt,x28:S)>   =>  Not trivial, Not overlay, NW1, N39
0.008/0.008	<U11(and(isNatural(isNatural(head(V1:S))),isLNat(x28:S)),isNatural(head(V1:S)),x28:S),afterNth(isLNat(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N40
0.008/0.008	<U11(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(x28:S)),isNatural(sel(V1:S,V2:S)),x28:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N41
0.008/0.008	<U11(and(isNatural(isNatural(0)),isLNat(x28:S)),isNatural(0),x28:S),afterNth(tt,x28:S)>   =>  Not trivial, Not overlay, NW1, N42
0.008/0.008	<U11(and(isNatural(isNatural(s(V1:S))),isLNat(x28:S)),isNatural(s(V1:S)),x28:S),afterNth(isNatural(V1:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N43
0.008/0.008	<U11(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(x28:S)),isPLNat(splitAt(V1:S,V2:S)),x28:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N44
0.008/0.008	<U11(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(x28:S)),isPLNat(pair(V1:S,V2:S)),x28:S),afterNth(and(isLNat(V1:S),isLNat(V2:S)),x28:S)>   =>  Not trivial, Not overlay, NW1, N45
0.008/0.008	<U11(and(isNatural(natsFrom(N:S)),isLNat(x28:S)),natsFrom(N:S),x28:S),afterNth(U41(isNatural(N:S),N:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N46
0.008/0.008	<U11(and(isNatural(sel(N:S,XS:S)),isLNat(x28:S)),sel(N:S,XS:S),x28:S),afterNth(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)>   =>  Not trivial, Not overlay, NW0, N47
0.008/0.008	<U11(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x28:S)),snd(pair(X:S,Y:S)),x28:S),afterNth(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N48
0.008/0.008	<U11(and(isNatural(splitAt(0,XS:S)),isLNat(x28:S)),splitAt(0,XS:S),x28:S),afterNth(U71(isLNat(XS:S),XS:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N49
0.008/0.008	<U11(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x28:S)),splitAt(s(N:S),cons(X:S,XS:S)),x28:S),afterNth(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N50
0.008/0.008	<U11(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x28:S)),tail(cons(N:S,XS:S)),x28:S),afterNth(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N51
0.008/0.008	<U11(and(isNatural(take(N:S,XS:S)),isLNat(x28:S)),take(N:S,XS:S),x28:S),afterNth(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x28:S)>   =>  Not trivial, Not overlay, NW1, N52
0.008/0.008	<U21(and(isLNat(fst(pair(X:S,Y:S))),isLNat(x31:S)),fst(pair(X:S,Y:S))),fst(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),x31:S))>   =>  Not trivial, Not overlay, NW0, N53
0.008/0.008	<U21(and(isLNat(head(cons(N:S,XS:S))),isLNat(x31:S)),head(cons(N:S,XS:S))),fst(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N54
0.008/0.008	<U21(and(isLNat(isLNat(afterNth(V1:S,V2:S))),isLNat(x31:S)),isLNat(afterNth(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N55
0.008/0.008	<U21(and(isLNat(isLNat(fst(V1:S))),isLNat(x31:S)),isLNat(fst(V1:S))),fst(pair(isPLNat(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N56
0.008/0.008	<U21(and(isLNat(isLNat(natsFrom(V1:S))),isLNat(x31:S)),isLNat(natsFrom(V1:S))),fst(pair(isNatural(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N57
0.008/0.008	<U21(and(isLNat(isLNat(snd(V1:S))),isLNat(x31:S)),isLNat(snd(V1:S))),fst(pair(isPLNat(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N58
0.008/0.008	<U21(and(isLNat(isLNat(tail(V1:S))),isLNat(x31:S)),isLNat(tail(V1:S))),fst(pair(isLNat(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N59
0.008/0.008	<U21(and(isLNat(isLNat(take(V1:S,V2:S))),isLNat(x31:S)),isLNat(take(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N60
0.008/0.008	<U21(and(isLNat(isLNat(cons(V1:S,V2:S))),isLNat(x31:S)),isLNat(cons(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N61
0.008/0.008	<U21(and(isLNat(isLNat(nil)),isLNat(x31:S)),isLNat(nil)),fst(pair(tt,x31:S))>   =>  Not trivial, Not overlay, NW1, N62
0.008/0.008	<U21(and(isLNat(isNatural(head(V1:S))),isLNat(x31:S)),isNatural(head(V1:S))),fst(pair(isLNat(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N63
0.008/0.008	<U21(and(isLNat(isNatural(sel(V1:S,V2:S))),isLNat(x31:S)),isNatural(sel(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N64
0.008/0.008	<U21(and(isLNat(isNatural(0)),isLNat(x31:S)),isNatural(0)),fst(pair(tt,x31:S))>   =>  Not trivial, Not overlay, NW1, N65
0.008/0.008	<U21(and(isLNat(isNatural(s(V1:S))),isLNat(x31:S)),isNatural(s(V1:S))),fst(pair(isNatural(V1:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N66
0.008/0.008	<U21(and(isLNat(isPLNat(splitAt(V1:S,V2:S))),isLNat(x31:S)),isPLNat(splitAt(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N67
0.008/0.008	<U21(and(isLNat(isPLNat(pair(V1:S,V2:S))),isLNat(x31:S)),isPLNat(pair(V1:S,V2:S))),fst(pair(and(isLNat(V1:S),isLNat(V2:S)),x31:S))>   =>  Not trivial, Not overlay, NW1, N68
0.008/0.008	<U21(and(isLNat(natsFrom(N:S)),isLNat(x31:S)),natsFrom(N:S)),fst(pair(U41(isNatural(N:S),N:S),x31:S))>   =>  Not trivial, Not overlay, NW0, N69
0.008/0.008	<U21(and(isLNat(sel(N:S,XS:S)),isLNat(x31:S)),sel(N:S,XS:S)),fst(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N70
0.008/0.008	<U21(and(isLNat(snd(pair(X:S,Y:S))),isLNat(x31:S)),snd(pair(X:S,Y:S))),fst(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x31:S))>   =>  Not trivial, Not overlay, NW0, N71
0.008/0.008	<U21(and(isLNat(splitAt(0,XS:S)),isLNat(x31:S)),splitAt(0,XS:S)),fst(pair(U71(isLNat(XS:S),XS:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N72
0.008/0.008	<U21(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x31:S)),splitAt(s(N:S),cons(X:S,XS:S))),fst(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x31:S))>   =>  Not trivial, Not overlay, NW1, N73
0.008/0.008	<U21(and(isLNat(tail(cons(N:S,XS:S))),isLNat(x31:S)),tail(cons(N:S,XS:S))),fst(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x31:S))>   =>  Not trivial, Not overlay, NW0, N74
0.008/0.008	<U21(and(isLNat(take(N:S,XS:S)),isLNat(x31:S)),take(N:S,XS:S)),fst(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x31:S))>   =>  Not trivial, Not overlay, NW0, N75
0.008/0.008	<U31(and(isNatural(head(cons(N:S,XS:S))),isLNat(x33:S)),head(cons(N:S,XS:S))),head(cons(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),x33:S))>   =>  Not trivial, Not overlay, NW0, N76
0.008/0.008	<U31(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(x33:S)),isLNat(afterNth(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N77
0.008/0.008	<U31(and(isNatural(isLNat(fst(V1:S))),isLNat(x33:S)),isLNat(fst(V1:S))),head(cons(isPLNat(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N78
0.008/0.008	<U31(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(x33:S)),isLNat(natsFrom(V1:S))),head(cons(isNatural(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N79
0.008/0.008	<U31(and(isNatural(isLNat(snd(V1:S))),isLNat(x33:S)),isLNat(snd(V1:S))),head(cons(isPLNat(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N80
0.008/0.008	<U31(and(isNatural(isLNat(tail(V1:S))),isLNat(x33:S)),isLNat(tail(V1:S))),head(cons(isLNat(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N81
0.008/0.008	<U31(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(x33:S)),isLNat(take(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N82
0.008/0.008	<U31(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(x33:S)),isLNat(cons(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N83
0.008/0.008	<U31(and(isNatural(isLNat(nil)),isLNat(x33:S)),isLNat(nil)),head(cons(tt,x33:S))>   =>  Not trivial, Not overlay, NW1, N84
0.008/0.008	<U31(and(isNatural(isNatural(head(V1:S))),isLNat(x33:S)),isNatural(head(V1:S))),head(cons(isLNat(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N85
0.008/0.008	<U31(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(x33:S)),isNatural(sel(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N86
0.008/0.008	<U31(and(isNatural(isNatural(0)),isLNat(x33:S)),isNatural(0)),head(cons(tt,x33:S))>   =>  Not trivial, Not overlay, NW1, N87
0.008/0.008	<U31(and(isNatural(isNatural(s(V1:S))),isLNat(x33:S)),isNatural(s(V1:S))),head(cons(isNatural(V1:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N88
0.008/0.008	<U31(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(x33:S)),isPLNat(splitAt(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N89
0.008/0.008	<U31(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(x33:S)),isPLNat(pair(V1:S,V2:S))),head(cons(and(isLNat(V1:S),isLNat(V2:S)),x33:S))>   =>  Not trivial, Not overlay, NW1, N90
0.008/0.008	<U31(and(isNatural(natsFrom(N:S)),isLNat(x33:S)),natsFrom(N:S)),head(cons(U41(isNatural(N:S),N:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N91
0.008/0.008	<U31(and(isNatural(sel(N:S,XS:S)),isLNat(x33:S)),sel(N:S,XS:S)),head(cons(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x33:S))>   =>  Not trivial, Not overlay, NW0, N92
0.008/0.008	<U31(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x33:S)),snd(pair(X:S,Y:S))),head(cons(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N93
0.008/0.008	<U31(and(isNatural(splitAt(0,XS:S)),isLNat(x33:S)),splitAt(0,XS:S)),head(cons(U71(isLNat(XS:S),XS:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N94
0.008/0.008	<U31(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x33:S)),splitAt(s(N:S),cons(X:S,XS:S))),head(cons(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N95
0.008/0.008	<U31(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x33:S)),tail(cons(N:S,XS:S))),head(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N96
0.008/0.008	<U31(and(isNatural(take(N:S,XS:S)),isLNat(x33:S)),take(N:S,XS:S)),head(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x33:S))>   =>  Not trivial, Not overlay, NW1, N97
0.008/0.008	<U41(isNatural(natsFrom(N:S)),natsFrom(N:S)),natsFrom(U41(isNatural(N:S),N:S))>   =>  Not trivial, Not overlay, NW1, N98
0.008/0.008	<U41(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S)),natsFrom(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N99
0.008/0.008	<U41(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S))),natsFrom(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N100
0.008/0.008	<U41(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S)),natsFrom(U71(isLNat(XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N101
0.008/0.008	<U41(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))),natsFrom(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N102
0.008/0.008	<U41(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))),natsFrom(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N103
0.008/0.008	<U41(isNatural(take(N:S,XS:S)),take(N:S,XS:S)),natsFrom(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N104
0.008/0.008	<U51(and(isNatural(sel(N:S,XS:S)),isLNat(x54:S)),sel(N:S,XS:S),x54:S),sel(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N105
0.008/0.008	<U51(and(isNatural(snd(pair(X:S,Y:S))),isLNat(x54:S)),snd(pair(X:S,Y:S)),x54:S),sel(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N106
0.008/0.008	<U51(and(isNatural(splitAt(0,XS:S)),isLNat(x54:S)),splitAt(0,XS:S),x54:S),sel(U71(isLNat(XS:S),XS:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N107
0.008/0.008	<U51(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x54:S)),splitAt(s(N:S),cons(X:S,XS:S)),x54:S),sel(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N108
0.008/0.008	<U51(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x54:S)),tail(cons(N:S,XS:S)),x54:S),sel(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N109
0.008/0.008	<U51(and(isNatural(take(N:S,XS:S)),isLNat(x54:S)),take(N:S,XS:S),x54:S),sel(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x54:S)>   =>  Not trivial, Not overlay, NW1, N110
0.008/0.008	<U61(and(isLNat(snd(pair(X:S,Y:S))),isLNat(x56:S)),x56:S),snd(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),x56:S))>   =>  Not trivial, Not overlay, NW1, N111
0.008/0.008	<U61(and(isLNat(splitAt(0,XS:S)),isLNat(x56:S)),x56:S),snd(pair(U71(isLNat(XS:S),XS:S),x56:S))>   =>  Not trivial, Not overlay, NW1, N112
0.008/0.008	<U61(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(x56:S)),x56:S),snd(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),x56:S))>   =>  Not trivial, Not overlay, NW1, N113
0.008/0.008	<U61(and(isLNat(tail(cons(N:S,XS:S))),isLNat(x56:S)),x56:S),snd(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x56:S))>   =>  Not trivial, Not overlay, NW1, N114
0.008/0.008	<U61(and(isLNat(take(N:S,XS:S)),isLNat(x56:S)),x56:S),snd(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x56:S))>   =>  Not trivial, Not overlay, NW1, N115
0.008/0.008	<U71(isLNat(splitAt(0,XS:S)),splitAt(0,XS:S)),splitAt(0,U71(isLNat(XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N116
0.008/0.008	<U71(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))),splitAt(0,U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N117
0.008/0.008	<U71(isLNat(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))),splitAt(0,U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N118
0.008/0.008	<U71(isLNat(take(N:S,XS:S)),take(N:S,XS:S)),splitAt(0,U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N119
0.008/0.008	<U81(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),and(isNatural(x59:S),isLNat(x60:S))),splitAt(s(N:S),cons(X:S,XS:S)),x59:S,x60:S),splitAt(s(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)),cons(x59:S,x60:S))>   =>  Not trivial, Not overlay, NW1, N120
0.008/0.008	<U81(and(isNatural(tail(cons(N:S,XS:S))),and(isNatural(x59:S),isLNat(x60:S))),tail(cons(N:S,XS:S)),x59:S,x60:S),splitAt(s(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)),cons(x59:S,x60:S))>   =>  Not trivial, Not overlay, NW1, N121
0.008/0.008	<U81(and(isNatural(take(N:S,XS:S)),and(isNatural(x59:S),isLNat(x60:S))),take(N:S,XS:S),x59:S,x60:S),splitAt(s(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)),cons(x59:S,x60:S))>   =>  Not trivial, Not overlay, NW1, N122
0.008/0.008	<U91(and(isNatural(tail(cons(N:S,XS:S))),isLNat(x62:S)),x62:S),tail(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),x62:S))>   =>  Not trivial, Not overlay, NW1, N123
0.008/0.008	<U91(and(isNatural(take(N:S,XS:S)),isLNat(x62:S)),x62:S),tail(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x62:S))>   =>  Not trivial, Not overlay, NW1, N124
0.008/0.008	<U101(and(isNatural(take(N:S,XS:S)),isLNat(x64:S)),take(N:S,XS:S),x64:S),take(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),x64:S)>   =>  Not trivial, Not overlay, NW1, N125
0.008/0.008	:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
0.008/0.008	
0.008/0.008	Huet Levy Processor:
0.008/0.008	-> Rules:
0.008/0.008	 U101(tt,N:S,XS:S) -> fst(splitAt(N:S,XS:S))
0.008/0.008	 U11(tt,N:S,XS:S) -> snd(splitAt(N:S,XS:S))
0.008/0.008	 U21(tt,X:S) -> X:S
0.008/0.008	 U31(tt,N:S) -> N:S
0.008/0.008	 U41(tt,N:S) -> cons(N:S,natsFrom(s(N:S)))
0.008/0.008	 U51(tt,N:S,XS:S) -> head(afterNth(N:S,XS:S))
0.008/0.008	 U61(tt,Y:S) -> Y:S
0.008/0.008	 U71(tt,XS:S) -> pair(nil,XS:S)
0.008/0.008	 U81(tt,N:S,X:S,XS:S) -> U82(splitAt(N:S,XS:S),X:S)
0.008/0.008	 U82(pair(YS:S,ZS:S),X:S) -> pair(cons(X:S,YS:S),ZS:S)
0.008/0.008	 U91(tt,XS:S) -> XS:S
0.008/0.008	 afterNth(N:S,XS:S) -> U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 and(tt,X:S) -> X:S
0.008/0.008	 fst(pair(X:S,Y:S)) -> U21(and(isLNat(X:S),isLNat(Y:S)),X:S)
0.008/0.008	 head(cons(N:S,XS:S)) -> U31(and(isNatural(N:S),isLNat(XS:S)),N:S)
0.008/0.008	 isLNat(afterNth(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 isLNat(fst(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 isLNat(natsFrom(V1:S)) -> isNatural(V1:S)
0.008/0.008	 isLNat(snd(V1:S)) -> isPLNat(V1:S)
0.008/0.008	 isLNat(tail(V1:S)) -> isLNat(V1:S)
0.008/0.008	 isLNat(take(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 isLNat(cons(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 isLNat(nil) -> tt
0.008/0.008	 isNatural(head(V1:S)) -> isLNat(V1:S)
0.008/0.008	 isNatural(sel(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 isNatural(0) -> tt
0.008/0.008	 isNatural(s(V1:S)) -> isNatural(V1:S)
0.008/0.008	 isPLNat(splitAt(V1:S,V2:S)) -> and(isNatural(V1:S),isLNat(V2:S))
0.008/0.008	 isPLNat(pair(V1:S,V2:S)) -> and(isLNat(V1:S),isLNat(V2:S))
0.008/0.008	 natsFrom(N:S) -> U41(isNatural(N:S),N:S)
0.008/0.008	 sel(N:S,XS:S) -> U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	 snd(pair(X:S,Y:S)) -> U61(and(isLNat(X:S),isLNat(Y:S)),Y:S)
0.008/0.008	 splitAt(0,XS:S) -> U71(isLNat(XS:S),XS:S)
0.008/0.008	 splitAt(s(N:S),cons(X:S,XS:S)) -> U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)
0.008/0.008	 tail(cons(N:S,XS:S)) -> U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)
0.008/0.008	 take(N:S,XS:S) -> U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)
0.008/0.008	-> Vars:
0.008/0.008	 N, XS, N, XS, X, N, N, N, XS, Y, XS, N, X, XS, X, YS, ZS, XS, N, XS, X, X, Y, N, XS, V1, V2, V1, V1, V1, V1, V1, V2, V1, V2, V1, V1, V2, V1, V1, V2, V1, V2, N, N, XS, X, Y, XS, N, X, XS, N, XS, N, XS
0.008/0.008	-> UVars:
0.008/0.008	 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [N], UV-LFrozen: [N], UV-RFrozen: [N])
0.008/0.008	 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, XS], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [Y], UV-LFrozen: [Y], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [N, XS], UV-LFrozen: [N, X, XS], UV-RFrozen: [X])
0.008/0.008	 (UV-RuleId: 10, UV-LActive: [YS, ZS], UV-RActive: [X, ZS], UV-LFrozen: [X], UV-RFrozen: [YS])
0.008/0.008	 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [XS], UV-LFrozen: [XS], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 12, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS])
0.008/0.008	 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [X], UV-LFrozen: [X], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 14, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X, Y])
0.008/0.008	 (UV-RuleId: 15, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, XS])
0.008/0.008	 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 23, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 24, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 26, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [])
0.008/0.008	 (UV-RuleId: 27, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1], UV-RFrozen: [V1])
0.008/0.008	 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [], UV-LFrozen: [V1, V2], UV-RFrozen: [V1, V2])
0.008/0.008	 (UV-RuleId: 30, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N])
0.008/0.008	 (UV-RuleId: 31, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS])
0.008/0.008	 (UV-RuleId: 32, UV-LActive: [X, Y], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [X, Y])
0.008/0.008	 (UV-RuleId: 33, UV-LActive: [XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [XS])
0.008/0.008	 (UV-RuleId: 34, UV-LActive: [N, X], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, X, XS])
0.008/0.008	 (UV-RuleId: 35, UV-LActive: [N], UV-RActive: [], UV-LFrozen: [XS], UV-RFrozen: [N, XS])
0.008/0.008	 (UV-RuleId: 36, UV-LActive: [N, XS], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: [N, XS])
0.008/0.008	-> FVars:
0.008/0.008	 x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30, x31, x32, x33, x34, x35, x36, x37, x38, x39, x40, x41, x42, x43, x44, x45, x46, x47, x48, x49, x50, x51, x52, x53, x54, x55, x56, x57, x58, x59, x60, x61, x62, x63, x64
0.008/0.008	-> PVars:
0.008/0.008	 N: [x9, x11, x14, x15, x16, x20, x27, x32, x52, x53, x58, x61, x63], XS: [x10, x12, x17, x19, x22, x26, x28, x33, x54, x57, x60, x62, x64], X: [x13, x21, x23, x29, x30, x55, x59], Y: [x18, x31, x56], YS: [x24], ZS: [x25], V1: [x34, x36, x37, x38, x39, x40, x42, x44, x45, x47, x48, x50], V2: [x35, x41, x43, x46, x49, x51]
0.008/0.008	
0.008/0.008	-> Rlps:
0.008/0.008	 (rule: U101(tt,x9:S,x10:S) -> fst(splitAt(x9:S,x10:S)), id: 1, possubterms: U101(tt,x9:S,x10:S)->[], tt->[1])
0.008/0.008	 (rule: U11(tt,x11:S,x12:S) -> snd(splitAt(x11:S,x12:S)), id: 2, possubterms: U11(tt,x11:S,x12:S)->[], tt->[1])
0.008/0.008	 (rule: U21(tt,x13:S) -> x13:S, id: 3, possubterms: U21(tt,x13:S)->[], tt->[1])
0.008/0.008	 (rule: U31(tt,x14:S) -> x14:S, id: 4, possubterms: U31(tt,x14:S)->[], tt->[1])
0.008/0.008	 (rule: U41(tt,x15:S) -> cons(x15:S,natsFrom(s(x15:S))), id: 5, possubterms: U41(tt,x15:S)->[], tt->[1])
0.008/0.008	 (rule: U51(tt,x16:S,x17:S) -> head(afterNth(x16:S,x17:S)), id: 6, possubterms: U51(tt,x16:S,x17:S)->[], tt->[1])
0.008/0.008	 (rule: U61(tt,x18:S) -> x18:S, id: 7, possubterms: U61(tt,x18:S)->[], tt->[1])
0.008/0.008	 (rule: U71(tt,x19:S) -> pair(nil,x19:S), id: 8, possubterms: U71(tt,x19:S)->[], tt->[1])
0.008/0.008	 (rule: U81(tt,x20:S,x21:S,x22:S) -> U82(splitAt(x20:S,x22:S),x21:S), id: 9, possubterms: U81(tt,x20:S,x21:S,x22:S)->[], tt->[1])
0.008/0.008	 (rule: U82(pair(x24:S,x25:S),x23:S) -> pair(cons(x23:S,x24:S),x25:S), id: 10, possubterms: U82(pair(x24:S,x25:S),x23:S)->[], pair(x24:S,x25:S)->[1])
0.008/0.008	 (rule: U91(tt,x26:S) -> x26:S, id: 11, possubterms: U91(tt,x26:S)->[], tt->[1])
0.008/0.008	 (rule: afterNth(x27:S,x28:S) -> U11(and(isNatural(x27:S),isLNat(x28:S)),x27:S,x28:S), id: 12, possubterms: afterNth(x27:S,x28:S)->[])
0.008/0.008	 (rule: and(tt,x29:S) -> x29:S, id: 13, possubterms: and(tt,x29:S)->[], tt->[1])
0.008/0.008	 (rule: fst(pair(x30:S,x31:S)) -> U21(and(isLNat(x30:S),isLNat(x31:S)),x30:S), id: 14, possubterms: fst(pair(x30:S,x31:S))->[], pair(x30:S,x31:S)->[1])
0.008/0.008	 (rule: head(cons(x32:S,x33:S)) -> U31(and(isNatural(x32:S),isLNat(x33:S)),x32:S), id: 15, possubterms: head(cons(x32:S,x33:S))->[], cons(x32:S,x33:S)->[1])
0.008/0.008	 (rule: isLNat(afterNth(x34:S,x35:S)) -> and(isNatural(x34:S),isLNat(x35:S)), id: 16, possubterms: isLNat(afterNth(x34:S,x35:S))->[])
0.008/0.008	 (rule: isLNat(fst(x36:S)) -> isPLNat(x36:S), id: 17, possubterms: isLNat(fst(x36:S))->[])
0.008/0.008	 (rule: isLNat(natsFrom(x37:S)) -> isNatural(x37:S), id: 18, possubterms: isLNat(natsFrom(x37:S))->[])
0.008/0.008	 (rule: isLNat(snd(x38:S)) -> isPLNat(x38:S), id: 19, possubterms: isLNat(snd(x38:S))->[])
0.008/0.008	 (rule: isLNat(tail(x39:S)) -> isLNat(x39:S), id: 20, possubterms: isLNat(tail(x39:S))->[])
0.008/0.008	 (rule: isLNat(take(x40:S,x41:S)) -> and(isNatural(x40:S),isLNat(x41:S)), id: 21, possubterms: isLNat(take(x40:S,x41:S))->[])
0.008/0.008	 (rule: isLNat(cons(x42:S,x43:S)) -> and(isNatural(x42:S),isLNat(x43:S)), id: 22, possubterms: isLNat(cons(x42:S,x43:S))->[])
0.008/0.008	 (rule: isLNat(nil) -> tt, id: 23, possubterms: isLNat(nil)->[])
0.008/0.008	 (rule: isNatural(head(x44:S)) -> isLNat(x44:S), id: 24, possubterms: isNatural(head(x44:S))->[])
0.008/0.008	 (rule: isNatural(sel(x45:S,x46:S)) -> and(isNatural(x45:S),isLNat(x46:S)), id: 25, possubterms: isNatural(sel(x45:S,x46:S))->[])
0.008/0.008	 (rule: isNatural(0) -> tt, id: 26, possubterms: isNatural(0)->[])
0.008/0.008	 (rule: isNatural(s(x47:S)) -> isNatural(x47:S), id: 27, possubterms: isNatural(s(x47:S))->[])
0.008/0.008	 (rule: isPLNat(splitAt(x48:S,x49:S)) -> and(isNatural(x48:S),isLNat(x49:S)), id: 28, possubterms: isPLNat(splitAt(x48:S,x49:S))->[])
0.008/0.008	 (rule: isPLNat(pair(x50:S,x51:S)) -> and(isLNat(x50:S),isLNat(x51:S)), id: 29, possubterms: isPLNat(pair(x50:S,x51:S))->[])
0.008/0.008	 (rule: natsFrom(x52:S) -> U41(isNatural(x52:S),x52:S), id: 30, possubterms: natsFrom(x52:S)->[])
0.008/0.008	 (rule: sel(x53:S,x54:S) -> U51(and(isNatural(x53:S),isLNat(x54:S)),x53:S,x54:S), id: 31, possubterms: sel(x53:S,x54:S)->[])
0.008/0.008	 (rule: snd(pair(x55:S,x56:S)) -> U61(and(isLNat(x55:S),isLNat(x56:S)),x56:S), id: 32, possubterms: snd(pair(x55:S,x56:S))->[], pair(x55:S,x56:S)->[1])
0.008/0.008	 (rule: splitAt(0,x57:S) -> U71(isLNat(x57:S),x57:S), id: 33, possubterms: splitAt(0,x57:S)->[], 0->[1])
0.008/0.008	 (rule: splitAt(s(x58:S),cons(x59:S,x60:S)) -> U81(and(isNatural(x58:S),and(isNatural(x59:S),isLNat(x60:S))),x58:S,x59:S,x60:S), id: 34, possubterms: splitAt(s(x58:S),cons(x59:S,x60:S))->[], s(x58:S)->[1], cons(x59:S,x60:S)->[2])
0.008/0.008	 (rule: tail(cons(x61:S,x62:S)) -> U91(and(isNatural(x61:S),isLNat(x62:S)),x62:S), id: 35, possubterms: tail(cons(x61:S,x62:S))->[], cons(x61:S,x62:S)->[1])
0.008/0.008	 (rule: take(x63:S,x64:S) -> U101(and(isNatural(x63:S),isLNat(x64:S)),x63:S,x64:S), id: 36, possubterms: take(x63:S,x64:S)->[])
0.008/0.008	
0.008/0.008	-> Unifications:
0.008/0.008	
0.008/0.008	
0.008/0.008	-> Critical pairs info:
0.008/0.008	<U11(and(isNatural(isNatural(head(V1:S))),isLNat(XS:S)),isNatural(head(V1:S)),XS:S),afterNth(isLNat(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N1
0.008/0.008	<U61(and(isLNat(splitAt(0,XS:S)),isLNat(Y:S)),Y:S),snd(pair(U71(isLNat(XS:S),XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N2
0.008/0.008	<U51(and(isNatural(tail(cons(N:S,XS:S))),isLNat(XS:S)),tail(cons(N:S,XS:S)),XS:S),sel(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N3
0.008/0.008	<U41(isNatural(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))),natsFrom(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N4
0.008/0.008	<pair(cons(X:S,isLNat(nil)),ZS:S),U82(pair(tt,ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N5
0.008/0.008	<U11(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(XS:S)),splitAt(s(N:S),cons(X:S,XS:S)),XS:S),afterNth(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N6
0.008/0.008	<U31(and(isNatural(splitAt(0,XS:S)),isLNat(XS:S)),splitAt(0,XS:S)),head(cons(U71(isLNat(XS:S),XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N7
0.008/0.008	<pair(cons(X:S,snd(pair(X:S,Y:S))),ZS:S),U82(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N8
0.008/0.008	<U21(and(isLNat(isLNat(fst(V1:S))),isLNat(Y:S)),isLNat(fst(V1:S))),fst(pair(isPLNat(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N9
0.008/0.008	<U11(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(XS:S)),isNatural(sel(V1:S,V2:S)),XS:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N10
0.008/0.008	<pair(cons(X:S,isNatural(head(V1:S))),ZS:S),U82(pair(isLNat(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N11
0.008/0.008	<U31(and(isNatural(tail(cons(N:S,XS:S))),isLNat(XS:S)),tail(cons(N:S,XS:S))),head(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N12
0.008/0.008	<U11(and(isNatural(isLNat(tail(V1:S))),isLNat(XS:S)),isLNat(tail(V1:S)),XS:S),afterNth(isLNat(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N13
0.008/0.008	<U71(isLNat(splitAt(0,XS:S)),splitAt(0,XS:S)),splitAt(0,U71(isLNat(XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N14
0.008/0.008	<U41(isNatural(snd(pair(X:S,Y:S))),snd(pair(X:S,Y:S))),natsFrom(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N15
0.008/0.008	<U31(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(XS:S)),isLNat(cons(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N16
0.008/0.008	<pair(cons(X:S,natsFrom(N:S)),ZS:S),U82(pair(U41(isNatural(N:S),N:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N17
0.008/0.008	<U71(isLNat(take(N:S,XS:S)),take(N:S,XS:S)),splitAt(0,U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N18
0.008/0.008	<U31(and(isNatural(sel(N:S,XS:S)),isLNat(XS:S)),sel(N:S,XS:S)),head(cons(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S))>   =>  Not trivial, Not overlay, NW0, N19
0.008/0.008	<U11(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(XS:S)),isLNat(take(V1:S,V2:S)),XS:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N20
0.008/0.008	<pair(cons(X:S,isLNat(afterNth(V1:S,V2:S))),ZS:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N21
0.008/0.008	<U31(and(isNatural(head(cons(N:S,XS:S))),isLNat(XS:S)),head(cons(N:S,XS:S))),head(cons(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),XS:S))>   =>  Not trivial, Not overlay, NW0, N22
0.008/0.008	<U81(and(isNatural(take(N:S,XS:S)),and(isNatural(X:S),isLNat(XS:S))),take(N:S,XS:S),X:S,XS:S),splitAt(s(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S)),cons(X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N23
0.008/0.008	<U31(and(isNatural(isNatural(sel(V1:S,V2:S))),isLNat(XS:S)),isNatural(sel(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N24
0.008/0.008	<U21(and(isLNat(sel(N:S,XS:S)),isLNat(Y:S)),sel(N:S,XS:S)),fst(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N25
0.008/0.008	<U21(and(isLNat(natsFrom(N:S)),isLNat(Y:S)),natsFrom(N:S)),fst(pair(U41(isNatural(N:S),N:S),Y:S))>   =>  Not trivial, Not overlay, NW0, N26
0.008/0.008	<U31(and(isNatural(snd(pair(X:S,Y:S))),isLNat(XS:S)),snd(pair(X:S,Y:S))),head(cons(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N27
0.008/0.008	<U21(and(isLNat(isLNat(tail(V1:S))),isLNat(Y:S)),isLNat(tail(V1:S))),fst(pair(isLNat(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N28
0.008/0.008	<pair(cons(X:S,fst(pair(X:S,Y:S))),ZS:S),U82(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N29
0.008/0.008	<U31(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(XS:S)),isPLNat(pair(V1:S,V2:S))),head(cons(and(isLNat(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N30
0.008/0.008	<U91(and(isNatural(tail(cons(N:S,XS:S))),isLNat(XS:S)),XS:S),tail(cons(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N31
0.008/0.008	<U31(and(isNatural(isLNat(snd(V1:S))),isLNat(XS:S)),isLNat(snd(V1:S))),head(cons(isPLNat(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N32
0.008/0.008	<pair(cons(X:S,isNatural(0)),ZS:S),U82(pair(tt,ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N33
0.008/0.008	<pair(cons(X:S,isLNat(snd(V1:S))),ZS:S),U82(pair(isPLNat(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N34
0.008/0.008	<U21(and(isLNat(isPLNat(splitAt(V1:S,V2:S))),isLNat(Y:S)),isPLNat(splitAt(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N35
0.008/0.008	<U101(and(isNatural(take(N:S,XS:S)),isLNat(XS:S)),take(N:S,XS:S),XS:S),take(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N36
0.008/0.008	<pair(cons(X:S,U82(pair(YS:S,ZS:S),X:S)),ZS:S),U82(pair(pair(cons(X:S,YS:S),ZS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N37
0.008/0.008	<U11(and(isNatural(tail(cons(N:S,XS:S))),isLNat(XS:S)),tail(cons(N:S,XS:S)),XS:S),afterNth(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N38
0.008/0.008	<U31(and(isNatural(isNatural(0)),isLNat(XS:S)),isNatural(0)),head(cons(tt,XS:S))>   =>  Not trivial, Not overlay, NW1, N39
0.008/0.008	<pair(cons(X:S,isNatural(sel(V1:S,V2:S))),ZS:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N40
0.008/0.008	<U31(and(isNatural(isLNat(nil)),isLNat(XS:S)),isLNat(nil)),head(cons(tt,XS:S))>   =>  Not trivial, Not overlay, NW1, N41
0.008/0.008	<U61(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(Y:S)),Y:S),snd(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N42
0.008/0.008	<U81(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),and(isNatural(X:S),isLNat(XS:S))),splitAt(s(N:S),cons(X:S,XS:S)),X:S,XS:S),splitAt(s(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S)),cons(X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N43
0.008/0.008	<U61(and(isLNat(tail(cons(N:S,XS:S))),isLNat(Y:S)),Y:S),snd(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N44
0.008/0.008	<U31(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(XS:S)),isLNat(natsFrom(V1:S))),head(cons(isNatural(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N45
0.008/0.008	<U51(and(isNatural(take(N:S,XS:S)),isLNat(XS:S)),take(N:S,XS:S),XS:S),sel(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N46
0.008/0.008	<U11(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(XS:S)),isPLNat(splitAt(V1:S,V2:S)),XS:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N47
0.008/0.008	<U21(and(isLNat(isLNat(take(V1:S,V2:S))),isLNat(Y:S)),isLNat(take(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N48
0.008/0.008	<U21(and(isLNat(snd(pair(X:S,Y:S))),isLNat(Y:S)),snd(pair(X:S,Y:S))),fst(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),Y:S))>   =>  Not trivial, Not overlay, NW0, N49
0.008/0.008	<U81(and(isNatural(tail(cons(N:S,XS:S))),and(isNatural(X:S),isLNat(XS:S))),tail(cons(N:S,XS:S)),X:S,XS:S),splitAt(s(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S)),cons(X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N50
0.008/0.008	<pair(cons(X:S,isLNat(cons(V1:S,V2:S))),ZS:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N51
0.008/0.008	<U21(and(isLNat(head(cons(N:S,XS:S))),isLNat(Y:S)),head(cons(N:S,XS:S))),fst(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N52
0.008/0.008	<U11(and(isNatural(take(N:S,XS:S)),isLNat(XS:S)),take(N:S,XS:S),XS:S),afterNth(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N53
0.008/0.008	<U71(isLNat(tail(cons(N:S,XS:S))),tail(cons(N:S,XS:S))),splitAt(0,U91(and(isNatural(N:S),isLNat(XS:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N54
0.008/0.008	<U51(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(XS:S)),splitAt(s(N:S),cons(X:S,XS:S)),XS:S),sel(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N55
0.008/0.008	<U21(and(isLNat(isNatural(head(V1:S))),isLNat(Y:S)),isNatural(head(V1:S))),fst(pair(isLNat(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N56
0.008/0.008	<pair(cons(X:S,isPLNat(pair(V1:S,V2:S))),ZS:S),U82(pair(and(isLNat(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N57
0.008/0.008	<U21(and(isLNat(isNatural(0)),isLNat(Y:S)),isNatural(0)),fst(pair(tt,Y:S))>   =>  Not trivial, Not overlay, NW1, N58
0.008/0.008	<U51(and(isNatural(snd(pair(X:S,Y:S))),isLNat(XS:S)),snd(pair(X:S,Y:S)),XS:S),sel(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N59
0.008/0.008	<pair(cons(X:S,isLNat(natsFrom(V1:S))),ZS:S),U82(pair(isNatural(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N60
0.008/0.008	<U11(and(isNatural(snd(pair(X:S,Y:S))),isLNat(XS:S)),snd(pair(X:S,Y:S)),XS:S),afterNth(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N61
0.008/0.008	<U31(and(isNatural(isLNat(tail(V1:S))),isLNat(XS:S)),isLNat(tail(V1:S))),head(cons(isLNat(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N62
0.008/0.008	<U11(and(isNatural(isNatural(0)),isLNat(XS:S)),isNatural(0),XS:S),afterNth(tt,XS:S)>   =>  Not trivial, Not overlay, NW1, N63
0.008/0.008	<U61(and(isLNat(snd(pair(X:S,Y:S))),isLNat(Y:S)),Y:S),snd(pair(U61(and(isLNat(X:S),isLNat(Y:S)),Y:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N64
0.008/0.008	<U11(and(isNatural(isLNat(natsFrom(V1:S))),isLNat(XS:S)),isLNat(natsFrom(V1:S)),XS:S),afterNth(isNatural(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N65
0.008/0.008	<U21(and(isLNat(take(N:S,XS:S)),isLNat(Y:S)),take(N:S,XS:S)),fst(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),Y:S))>   =>  Not trivial, Not overlay, NW0, N66
0.008/0.008	<U21(and(isLNat(isNatural(sel(V1:S,V2:S))),isLNat(Y:S)),isNatural(sel(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N67
0.008/0.008	<U11(and(isNatural(isNatural(s(V1:S))),isLNat(XS:S)),isNatural(s(V1:S)),XS:S),afterNth(isNatural(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N68
0.008/0.008	<U11(and(isNatural(isPLNat(pair(V1:S,V2:S))),isLNat(XS:S)),isPLNat(pair(V1:S,V2:S)),XS:S),afterNth(and(isLNat(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N69
0.008/0.008	<U21(and(isLNat(isLNat(cons(V1:S,V2:S))),isLNat(Y:S)),isLNat(cons(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N70
0.008/0.008	<U21(and(isLNat(splitAt(0,XS:S)),isLNat(Y:S)),splitAt(0,XS:S)),fst(pair(U71(isLNat(XS:S),XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N71
0.008/0.008	<U11(and(isNatural(natsFrom(N:S)),isLNat(XS:S)),natsFrom(N:S),XS:S),afterNth(U41(isNatural(N:S),N:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N72
0.008/0.008	<pair(cons(X:S,afterNth(N:S,XS:S)),ZS:S),U82(pair(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N73
0.008/0.008	<U11(and(isNatural(and(tt,X:S)),isLNat(XS:S)),and(tt,X:S),XS:S),afterNth(X:S,XS:S)>   =>  Not trivial, Not overlay, NW1, N74
0.008/0.008	<U11(and(isNatural(isLNat(snd(V1:S))),isLNat(XS:S)),isLNat(snd(V1:S)),XS:S),afterNth(isPLNat(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N75
0.008/0.008	<U31(and(isNatural(isLNat(fst(V1:S))),isLNat(XS:S)),isLNat(fst(V1:S))),head(cons(isPLNat(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N76
0.008/0.008	<U21(and(isLNat(isLNat(natsFrom(V1:S))),isLNat(Y:S)),isLNat(natsFrom(V1:S))),fst(pair(isNatural(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N77
0.008/0.008	<pair(cons(X:S,take(N:S,XS:S)),ZS:S),U82(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N78
0.008/0.008	<U71(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))),splitAt(0,U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N79
0.008/0.008	<U31(and(isNatural(isPLNat(splitAt(V1:S,V2:S))),isLNat(XS:S)),isPLNat(splitAt(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N80
0.008/0.008	<U11(and(isNatural(splitAt(0,XS:S)),isLNat(XS:S)),splitAt(0,XS:S),XS:S),afterNth(U71(isLNat(XS:S),XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N81
0.008/0.008	<pair(cons(X:S,and(tt,X:S)),ZS:S),U82(pair(X:S,ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N82
0.008/0.008	<U31(and(isNatural(isNatural(s(V1:S))),isLNat(XS:S)),isNatural(s(V1:S))),head(cons(isNatural(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N83
0.008/0.008	<pair(cons(X:S,splitAt(s(N:S),cons(X:S,XS:S))),ZS:S),U82(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N84
0.008/0.008	<pair(cons(X:S,isLNat(take(V1:S,V2:S))),ZS:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N85
0.008/0.008	<pair(cons(X:S,U91(tt,XS:S)),ZS:S),U82(pair(XS:S,ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N86
0.008/0.008	<U21(and(isLNat(isLNat(afterNth(V1:S,V2:S))),isLNat(Y:S)),isLNat(afterNth(V1:S,V2:S))),fst(pair(and(isNatural(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N87
0.008/0.008	<pair(cons(X:S,tail(cons(N:S,XS:S))),ZS:S),U82(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N88
0.008/0.008	<pair(cons(X:S,isLNat(fst(V1:S))),ZS:S),U82(pair(isPLNat(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N89
0.008/0.008	<U11(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(XS:S)),isLNat(afterNth(V1:S,V2:S)),XS:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N90
0.008/0.008	<U11(and(isNatural(fst(pair(X:S,Y:S))),isLNat(XS:S)),fst(pair(X:S,Y:S)),XS:S),afterNth(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N91
0.008/0.008	<pair(cons(X:S,isPLNat(splitAt(V1:S,V2:S))),ZS:S),U82(pair(and(isNatural(V1:S),isLNat(V2:S)),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N92
0.008/0.008	<U21(and(isLNat(tail(cons(N:S,XS:S))),isLNat(Y:S)),tail(cons(N:S,XS:S))),fst(pair(U91(and(isNatural(N:S),isLNat(XS:S)),XS:S),Y:S))>   =>  Not trivial, Not overlay, NW0, N93
0.008/0.008	<U41(isNatural(sel(N:S,XS:S)),sel(N:S,XS:S)),natsFrom(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N94
0.008/0.008	<U11(and(isNatural(isLNat(fst(V1:S))),isLNat(XS:S)),isLNat(fst(V1:S)),XS:S),afterNth(isPLNat(V1:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N95
0.008/0.008	<U21(and(isLNat(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(Y:S)),splitAt(s(N:S),cons(X:S,XS:S))),fst(pair(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N96
0.008/0.008	<U11(and(isNatural(isLNat(nil)),isLNat(XS:S)),isLNat(nil),XS:S),afterNth(tt,XS:S)>   =>  Not trivial, Not overlay, NW1, N97
0.008/0.008	<U31(and(isNatural(natsFrom(N:S)),isLNat(XS:S)),natsFrom(N:S)),head(cons(U41(isNatural(N:S),N:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N98
0.008/0.008	<U51(and(isNatural(sel(N:S,XS:S)),isLNat(XS:S)),sel(N:S,XS:S),XS:S),sel(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N99
0.008/0.008	<U51(and(isNatural(splitAt(0,XS:S)),isLNat(XS:S)),splitAt(0,XS:S),XS:S),sel(U71(isLNat(XS:S),XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N100
0.008/0.008	<U41(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),splitAt(s(N:S),cons(X:S,XS:S))),natsFrom(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N101
0.008/0.008	<U31(and(isNatural(isLNat(take(V1:S,V2:S))),isLNat(XS:S)),isLNat(take(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N102
0.008/0.008	<pair(cons(X:S,head(cons(N:S,XS:S))),ZS:S),U82(pair(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N103
0.008/0.008	<U11(and(isNatural(afterNth(N:S,XS:S)),isLNat(XS:S)),afterNth(N:S,XS:S),XS:S),afterNth(U11(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW1, N104
0.008/0.008	<U21(and(isLNat(isPLNat(pair(V1:S,V2:S))),isLNat(Y:S)),isPLNat(pair(V1:S,V2:S))),fst(pair(and(isLNat(V1:S),isLNat(V2:S)),Y:S))>   =>  Not trivial, Not overlay, NW1, N105
0.008/0.008	<U31(and(isNatural(isNatural(head(V1:S))),isLNat(XS:S)),isNatural(head(V1:S))),head(cons(isLNat(V1:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N106
0.008/0.008	<U41(isNatural(take(N:S,XS:S)),take(N:S,XS:S)),natsFrom(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S))>   =>  Not trivial, Not overlay, NW1, N107
0.008/0.008	<U21(and(isLNat(isLNat(nil)),isLNat(Y:S)),isLNat(nil)),fst(pair(tt,Y:S))>   =>  Not trivial, Not overlay, NW1, N108
0.008/0.008	<U41(isNatural(natsFrom(N:S)),natsFrom(N:S)),natsFrom(U41(isNatural(N:S),N:S))>   =>  Not trivial, Not overlay, NW1, N109
0.008/0.008	<U91(and(isNatural(take(N:S,XS:S)),isLNat(XS:S)),XS:S),tail(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N110
0.008/0.008	<pair(cons(X:S,sel(N:S,XS:S)),ZS:S),U82(pair(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N111
0.008/0.008	<pair(cons(X:S,splitAt(0,XS:S)),ZS:S),U82(pair(U71(isLNat(XS:S),XS:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N112
0.008/0.008	<U21(and(isLNat(isLNat(snd(V1:S))),isLNat(Y:S)),isLNat(snd(V1:S))),fst(pair(isPLNat(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N113
0.008/0.008	<U11(and(isNatural(sel(N:S,XS:S)),isLNat(XS:S)),sel(N:S,XS:S),XS:S),afterNth(U51(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S)>   =>  Not trivial, Not overlay, NW0, N114
0.008/0.008	<pair(cons(X:S,isLNat(tail(V1:S))),ZS:S),U82(pair(isLNat(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N115
0.008/0.008	<U31(and(isNatural(splitAt(s(N:S),cons(X:S,XS:S))),isLNat(XS:S)),splitAt(s(N:S),cons(X:S,XS:S))),head(cons(U81(and(isNatural(N:S),and(isNatural(X:S),isLNat(XS:S))),N:S,X:S,XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N116
0.008/0.008	<U41(isNatural(splitAt(0,XS:S)),splitAt(0,XS:S)),natsFrom(U71(isLNat(XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N117
0.008/0.008	<pair(cons(X:S,isNatural(s(V1:S))),ZS:S),U82(pair(isNatural(V1:S),ZS:S),X:S)>   =>  Not trivial, Not overlay, NW1, N118
0.008/0.008	<U31(and(isNatural(take(N:S,XS:S)),isLNat(XS:S)),take(N:S,XS:S)),head(cons(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),XS:S))>   =>  Not trivial, Not overlay, NW1, N119
0.008/0.008	<U11(and(isNatural(head(cons(N:S,XS:S))),isLNat(XS:S)),head(cons(N:S,XS:S)),XS:S),afterNth(U31(and(isNatural(N:S),isLNat(XS:S)),N:S),XS:S)>   =>  Not trivial, Not overlay, NW0, N120
0.008/0.008	<U31(and(isNatural(isLNat(afterNth(V1:S,V2:S))),isLNat(XS:S)),isLNat(afterNth(V1:S,V2:S))),head(cons(and(isNatural(V1:S),isLNat(V2:S)),XS:S))>   =>  Not trivial, Not overlay, NW1, N121
0.008/0.008	<U11(and(isNatural(isLNat(cons(V1:S,V2:S))),isLNat(XS:S)),isLNat(cons(V1:S,V2:S)),XS:S),afterNth(and(isNatural(V1:S),isLNat(V2:S)),XS:S)>   =>  Not trivial, Not overlay, NW1, N122
0.008/0.008	<U21(and(isLNat(fst(pair(X:S,Y:S))),isLNat(Y:S)),fst(pair(X:S,Y:S))),fst(pair(U21(and(isLNat(X:S),isLNat(Y:S)),X:S),Y:S))>   =>  Not trivial, Not overlay, NW0, N123
0.008/0.008	<U61(and(isLNat(take(N:S,XS:S)),isLNat(Y:S)),Y:S),snd(pair(U101(and(isNatural(N:S),isLNat(XS:S)),N:S,XS:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N124
0.008/0.008	<U21(and(isLNat(isNatural(s(V1:S))),isLNat(Y:S)),isNatural(s(V1:S))),fst(pair(isNatural(V1:S),Y:S))>   =>  Not trivial, Not overlay, NW1, N125
0.008/0.008	
0.008/0.008	-> Problem conclusions:
0.008/0.008	 Left linear, Not right linear, Not linear
0.008/0.008	 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
0.008/0.008	 Not Huet-Levy confluent, Not Newman confluent
0.008/0.008	 R is a CS-TRS, Not left-homogeneous u-replacing variables
0.008/0.008	
0.008/0.008	
0.008/0.008	Problem 1:
0.008/0.008	No Convergence Brute Force Processor:
0.008/0.008	-> Rewritings:
0.008/0.008	s: U11(and(isNatural(isNatural(head(V1:S))),isLNat(XS:S)),isNatural(head(V1:S)),XS:S)
0.008/0.008	Nodes: [0]
0.008/0.008	Edges: []
0.008/0.008	ID: 0 => ('U11(and(isNatural(isNatural(head(V1:S))),isLNat(XS:S)),isNatural(head(V1:S)),XS:S)', D0)
0.008/0.008	t: afterNth(isLNat(V1:S),XS:S)
0.008/0.008	Nodes: [0,1]
0.008/0.008	Edges: [(0,1)]
0.008/0.008	ID: 0 => ('afterNth(isLNat(V1:S),XS:S)', D0)
0.008/0.008	ID: 1 => ('U11(and(isNatural(isLNat(V1:S)),isLNat(XS:S)),isLNat(V1:S),XS:S)', D1, R12, P[], S{x27:S -> isLNat(V1:S), x28:S -> XS:S}), NR: 'U11(and(isNatural(isLNat(V1:S)),isLNat(XS:S)),isLNat(V1:S),XS:S)'
0.008/0.008	U11(and(isNatural(isNatural(head(V1:S))),isLNat(XS:S)),isNatural(head(V1:S)),XS:S) ->* no union *<- afterNth(isLNat(V1:S),XS:S)
0.008/0.008	"Not joinable"
0.008/0.008	
0.008/0.008	The problem is not joinable.
0.008/0.008	0.07user 0.00system 0:00.08elapsed 90%CPU (0avgtext+0avgdata 22324maxresident)k
0.008/0.008	0inputs+0outputs (0major+3770minor)pagefaults 0swaps