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 v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U103 1) 0.008/0.008 (U104 1) 0.008/0.008 (U105 1) 0.008/0.008 (U106 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U112 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U122 1) 0.008/0.008 (U13 1) 0.008/0.008 (U131 1) 0.008/0.008 (U14 1) 0.008/0.008 (U141 1) 0.008/0.008 (U151 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U183 1) 0.008/0.008 (U191 1) 0.008/0.008 (U192 1) 0.008/0.008 (U193 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U205 1) 0.008/0.008 (U206 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U23 1) 0.008/0.008 (U231 1) 0.008/0.008 (U232 1) 0.008/0.008 (U24 1) 0.008/0.008 (U241 1) 0.008/0.008 (U242 1) 0.008/0.008 (U243 1) 0.008/0.008 (U244 1) 0.008/0.008 (U245 1) 0.008/0.008 (U246 1) 0.008/0.008 (U251 1) 0.008/0.008 (U252 1) 0.008/0.008 (U253 1) 0.008/0.008 (U254 1) 0.008/0.008 (U255 1) 0.008/0.008 (U256 1) 0.008/0.008 (U261 1) 0.008/0.008 (U262 1) 0.008/0.008 (U271 1) 0.008/0.008 (U272 1) 0.008/0.008 (U281 1) 0.008/0.008 (U282 1) 0.008/0.008 (U291 1) 0.008/0.008 (U292 1) 0.008/0.008 (U293 1) 0.008/0.008 (U294 1) 0.008/0.008 (U301 1) 0.008/0.008 (U302 1) 0.008/0.008 (U303 1) 0.008/0.008 (U304 1) 0.008/0.008 (U31 1) 0.008/0.008 (U311 1) 0.008/0.008 (U312 1) 0.008/0.008 (U32 1) 0.008/0.008 (U321 1) 0.008/0.008 (U322 1) 0.008/0.008 (U323 1) 0.008/0.008 (U324 1) 0.008/0.008 (U325 1) 0.008/0.008 (U326 1) 0.008/0.008 (U327 1) 0.008/0.008 (U33 1) 0.008/0.008 (U331 1) 0.008/0.008 (U332 1) 0.008/0.008 (U333 1) 0.008/0.008 (U334 1) 0.008/0.008 (U34 1) 0.008/0.008 (U341 1) 0.008/0.008 (U342 1) 0.008/0.008 (U343 1) 0.008/0.008 (U344 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U43 1) 0.008/0.008 (U44 1) 0.008/0.008 (U45 1) 0.008/0.008 (U46 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U53 1) 0.008/0.008 (U54 1) 0.008/0.008 (U55 1) 0.008/0.008 (U56 1) 0.008/0.008 (U61 1) 0.008/0.008 (U62 1) 0.008/0.008 (U63 1) 0.008/0.008 (U71 1) 0.008/0.008 (U72 1) 0.008/0.008 (U73 1) 0.008/0.008 (U81 1) 0.008/0.008 (U82 1) 0.008/0.008 (U83 1) 0.008/0.008 (U91 1) 0.008/0.008 (U92 1) 0.008/0.008 (U93 1) 0.008/0.008 (afterNth) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat 1) 0.008/0.008 (isLNatKind 1) 0.008/0.008 (isNatural 1) 0.008/0.008 (isNaturalKind 1) 0.008/0.008 (isPLNat 1) 0.008/0.008 (isPLNatKind 1) 0.008/0.008 (natsFrom) 0.008/0.008 (sel) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take) 0.008/0.008 (cons) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (num0) 0.008/0.008 (pair) 0.008/0.008 (s) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V1:S:S,V2:S:S) -> U102(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U102(tt,V1:S:S,V2:S:S) -> U103(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U103(tt,V1:S:S,V2:S:S) -> U104(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U104(tt,V1:S:S,V2:S:S) -> U105(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U105(tt,V2:S:S) -> U106(isLNat(V2:S:S)) 0.008/0.008 U106(tt) -> tt 0.008/0.008 U11(tt,N:S:S,XS:S:S) -> U12(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U111(tt,V2:S:S) -> U112(isLNatKind(V2:S:S)) 0.008/0.008 U112(tt) -> tt 0.008/0.008 U12(tt,N:S:S,XS:S:S) -> U13(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U121(tt,V2:S:S) -> U122(isLNatKind(V2:S:S)) 0.008/0.008 U122(tt) -> tt 0.008/0.008 U13(tt,N:S:S,XS:S:S) -> U14(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U131(tt) -> tt 0.008/0.008 U14(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U141(tt) -> tt 0.008/0.008 U151(tt) -> tt 0.008/0.008 U161(tt) -> tt 0.008/0.008 U171(tt,V2:S:S) -> U172(isLNatKind(V2:S:S)) 0.008/0.008 U172(tt) -> tt 0.008/0.008 U181(tt,V1:S:S) -> U182(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U182(tt,V1:S:S) -> U183(isLNat(V1:S:S)) 0.008/0.008 U183(tt) -> tt 0.008/0.008 U191(tt,V1:S:S) -> U192(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U192(tt,V1:S:S) -> U193(isNatural(V1:S:S)) 0.008/0.008 U193(tt) -> tt 0.008/0.008 U201(tt,V1:S:S,V2:S:S) -> U202(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U202(tt,V1:S:S,V2:S:S) -> U203(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U203(tt,V1:S:S,V2:S:S) -> U204(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U204(tt,V1:S:S,V2:S:S) -> U205(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U205(tt,V2:S:S) -> U206(isLNat(V2:S:S)) 0.008/0.008 U206(tt) -> tt 0.008/0.008 U21(tt,X:S:S,Y:S:S) -> U22(isLNatKind(X:S:S),X:S:S,Y:S:S) 0.008/0.008 U211(tt) -> tt 0.008/0.008 U22(tt,X:S:S,Y:S:S) -> U23(isLNat(Y:S:S),X:S:S,Y:S:S) 0.008/0.008 U221(tt) -> tt 0.008/0.008 U23(tt,X:S:S,Y:S:S) -> U24(isLNatKind(Y:S:S),X:S:S) 0.008/0.008 U231(tt,V2:S:S) -> U232(isLNatKind(V2:S:S)) 0.008/0.008 U232(tt) -> tt 0.008/0.008 U24(tt,X:S:S) -> X:S:S 0.008/0.008 U241(tt,V1:S:S,V2:S:S) -> U242(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U242(tt,V1:S:S,V2:S:S) -> U243(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U243(tt,V1:S:S,V2:S:S) -> U244(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U244(tt,V1:S:S,V2:S:S) -> U245(isLNat(V1:S:S),V2:S:S) 0.008/0.008 U245(tt,V2:S:S) -> U246(isLNat(V2:S:S)) 0.008/0.008 U246(tt) -> tt 0.008/0.008 U251(tt,V1:S:S,V2:S:S) -> U252(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U252(tt,V1:S:S,V2:S:S) -> U253(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U253(tt,V1:S:S,V2:S:S) -> U254(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U254(tt,V1:S:S,V2:S:S) -> U255(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U255(tt,V2:S:S) -> U256(isLNat(V2:S:S)) 0.008/0.008 U256(tt) -> tt 0.008/0.008 U261(tt,V2:S:S) -> U262(isLNatKind(V2:S:S)) 0.008/0.008 U262(tt) -> tt 0.008/0.008 U271(tt,V2:S:S) -> U272(isLNatKind(V2:S:S)) 0.008/0.008 U272(tt) -> tt 0.008/0.008 U281(tt,N:S:S) -> U282(isNaturalKind(N:S:S),N:S:S) 0.008/0.008 U282(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.008/0.008 U291(tt,N:S:S,XS:S:S) -> U292(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U292(tt,N:S:S,XS:S:S) -> U293(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U293(tt,N:S:S,XS:S:S) -> U294(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U294(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.008/0.008 U301(tt,X:S:S,Y:S:S) -> U302(isLNatKind(X:S:S),Y:S:S) 0.008/0.008 U302(tt,Y:S:S) -> U303(isLNat(Y:S:S),Y:S:S) 0.008/0.008 U303(tt,Y:S:S) -> U304(isLNatKind(Y:S:S),Y:S:S) 0.008/0.008 U304(tt,Y:S:S) -> Y:S:S 0.008/0.008 U31(tt,N:S:S,XS:S:S) -> U32(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U311(tt,XS:S:S) -> U312(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U312(tt,XS:S:S) -> pair(nil,XS:S:S) 0.008/0.008 U32(tt,N:S:S,XS:S:S) -> U33(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U321(tt,N:S:S,X:S:S,XS:S:S) -> U322(isNaturalKind(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U322(tt,N:S:S,X:S:S,XS:S:S) -> U323(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U323(tt,N:S:S,X:S:S,XS:S:S) -> U324(isNaturalKind(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U324(tt,N:S:S,X:S:S,XS:S:S) -> U325(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U325(tt,N:S:S,X:S:S,XS:S:S) -> U326(isLNatKind(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U326(tt,N:S:S,X:S:S,XS:S:S) -> U327(splitAt(N:S:S,XS:S:S),X:S:S) 0.008/0.008 U327(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.008/0.008 U33(tt,N:S:S,XS:S:S) -> U34(isLNatKind(XS:S:S),N:S:S) 0.008/0.008 U331(tt,N:S:S,XS:S:S) -> U332(isNaturalKind(N:S:S),XS:S:S) 0.008/0.008 U332(tt,XS:S:S) -> U333(isLNat(XS:S:S),XS:S:S) 0.008/0.008 U333(tt,XS:S:S) -> U334(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U334(tt,XS:S:S) -> XS:S:S 0.008/0.008 U34(tt,N:S:S) -> N:S:S 0.008/0.008 U341(tt,N:S:S,XS:S:S) -> U342(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U342(tt,N:S:S,XS:S:S) -> U343(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U343(tt,N:S:S,XS:S:S) -> U344(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U344(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U41(tt,V1:S:S,V2:S:S) -> U42(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U42(tt,V1:S:S,V2:S:S) -> U43(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U43(tt,V1:S:S,V2:S:S) -> U44(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U44(tt,V1:S:S,V2:S:S) -> U45(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U45(tt,V2:S:S) -> U46(isLNat(V2:S:S)) 0.008/0.008 U46(tt) -> tt 0.008/0.008 U51(tt,V1:S:S,V2:S:S) -> U52(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U52(tt,V1:S:S,V2:S:S) -> U53(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U53(tt,V1:S:S,V2:S:S) -> U54(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U54(tt,V1:S:S,V2:S:S) -> U55(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U55(tt,V2:S:S) -> U56(isLNat(V2:S:S)) 0.008/0.008 U56(tt) -> tt 0.008/0.008 U61(tt,V1:S:S) -> U62(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U62(tt,V1:S:S) -> U63(isPLNat(V1:S:S)) 0.008/0.008 U63(tt) -> tt 0.008/0.008 U71(tt,V1:S:S) -> U72(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U72(tt,V1:S:S) -> U73(isNatural(V1:S:S)) 0.008/0.008 U73(tt) -> tt 0.008/0.008 U81(tt,V1:S:S) -> U82(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U82(tt,V1:S:S) -> U83(isPLNat(V1:S:S)) 0.008/0.008 U83(tt) -> tt 0.008/0.008 U91(tt,V1:S:S) -> U92(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U92(tt,V1:S:S) -> U93(isLNat(V1:S:S)) 0.008/0.008 U93(tt) -> tt 0.008/0.008 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> U111(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(fst(V1:S:S)) -> U131(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(natsFrom(V1:S:S)) -> U141(isNaturalKind(V1:S:S)) 0.008/0.008 isLNatKind(snd(V1:S:S)) -> U151(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(tail(V1:S:S)) -> U161(isLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(take(V1:S:S,V2:S:S)) -> U171(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(cons(V1:S:S,V2:S:S)) -> U121(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(nil) -> tt 0.008/0.008 isNatural(head(V1:S:S)) -> U181(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isNatural(sel(V1:S:S,V2:S:S)) -> U201(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isNatural(num0) -> tt 0.008/0.008 isNatural(s(V1:S:S)) -> U191(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isNaturalKind(head(V1:S:S)) -> U211(isLNatKind(V1:S:S)) 0.008/0.008 isNaturalKind(sel(V1:S:S,V2:S:S)) -> U231(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isNaturalKind(num0) -> tt 0.008/0.008 isNaturalKind(s(V1:S:S)) -> U221(isNaturalKind(V1:S:S)) 0.008/0.008 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U251(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNat(pair(V1:S:S,V2:S:S)) -> U241(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> U271(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isPLNatKind(pair(V1:S:S,V2:S:S)) -> U261(isLNatKind(V1:S:S),V2:S:S) 0.008/0.008 natsFrom(N:S:S) -> U281(isNatural(N:S:S),N:S:S) 0.008/0.008 sel(N:S:S,XS:S:S) -> U291(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 snd(pair(X:S:S,Y:S:S)) -> U301(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 splitAt(num0,XS:S:S) -> U311(isLNat(XS:S:S),XS:S:S) 0.008/0.008 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 tail(cons(N:S:S,XS:S:S)) -> U331(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 take(N:S:S,XS:S:S) -> U341(isNatural(N:S:S),N:S:S,XS:S: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 v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U103 1) 0.008/0.008 (U104 1) 0.008/0.008 (U105 1) 0.008/0.008 (U106 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U112 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U122 1) 0.008/0.008 (U13 1) 0.008/0.008 (U131 1) 0.008/0.008 (U14 1) 0.008/0.008 (U141 1) 0.008/0.008 (U151 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U183 1) 0.008/0.008 (U191 1) 0.008/0.008 (U192 1) 0.008/0.008 (U193 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U205 1) 0.008/0.008 (U206 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U23 1) 0.008/0.008 (U231 1) 0.008/0.008 (U232 1) 0.008/0.008 (U24 1) 0.008/0.008 (U241 1) 0.008/0.008 (U242 1) 0.008/0.008 (U243 1) 0.008/0.008 (U244 1) 0.008/0.008 (U245 1) 0.008/0.008 (U246 1) 0.008/0.008 (U251 1) 0.008/0.008 (U252 1) 0.008/0.008 (U253 1) 0.008/0.008 (U254 1) 0.008/0.008 (U255 1) 0.008/0.008 (U256 1) 0.008/0.008 (U261 1) 0.008/0.008 (U262 1) 0.008/0.008 (U271 1) 0.008/0.008 (U272 1) 0.008/0.008 (U281 1) 0.008/0.008 (U282 1) 0.008/0.008 (U291 1) 0.008/0.008 (U292 1) 0.008/0.008 (U293 1) 0.008/0.008 (U294 1) 0.008/0.008 (U301 1) 0.008/0.008 (U302 1) 0.008/0.008 (U303 1) 0.008/0.008 (U304 1) 0.008/0.008 (U31 1) 0.008/0.008 (U311 1) 0.008/0.008 (U312 1) 0.008/0.008 (U32 1) 0.008/0.008 (U321 1) 0.008/0.008 (U322 1) 0.008/0.008 (U323 1) 0.008/0.008 (U324 1) 0.008/0.008 (U325 1) 0.008/0.008 (U326 1) 0.008/0.008 (U327 1) 0.008/0.008 (U33 1) 0.008/0.008 (U331 1) 0.008/0.008 (U332 1) 0.008/0.008 (U333 1) 0.008/0.008 (U334 1) 0.008/0.008 (U34 1) 0.008/0.008 (U341 1) 0.008/0.008 (U342 1) 0.008/0.008 (U343 1) 0.008/0.008 (U344 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U43 1) 0.008/0.008 (U44 1) 0.008/0.008 (U45 1) 0.008/0.008 (U46 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U53 1) 0.008/0.008 (U54 1) 0.008/0.008 (U55 1) 0.008/0.008 (U56 1) 0.008/0.008 (U61 1) 0.008/0.008 (U62 1) 0.008/0.008 (U63 1) 0.008/0.008 (U71 1) 0.008/0.008 (U72 1) 0.008/0.008 (U73 1) 0.008/0.008 (U81 1) 0.008/0.008 (U82 1) 0.008/0.008 (U83 1) 0.008/0.008 (U91 1) 0.008/0.008 (U92 1) 0.008/0.008 (U93 1) 0.008/0.008 (afterNth) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat 1) 0.008/0.008 (isLNatKind 1) 0.008/0.008 (isNatural 1) 0.008/0.008 (isNaturalKind 1) 0.008/0.008 (isPLNat 1) 0.008/0.008 (isPLNatKind 1) 0.008/0.008 (natsFrom) 0.008/0.008 (sel) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take) 0.008/0.008 (cons) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (num0) 0.008/0.008 (pair) 0.008/0.008 (s) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V1:S:S,V2:S:S) -> U102(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U102(tt,V1:S:S,V2:S:S) -> U103(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U103(tt,V1:S:S,V2:S:S) -> U104(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U104(tt,V1:S:S,V2:S:S) -> U105(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U105(tt,V2:S:S) -> U106(isLNat(V2:S:S)) 0.008/0.008 U106(tt) -> tt 0.008/0.008 U11(tt,N:S:S,XS:S:S) -> U12(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U111(tt,V2:S:S) -> U112(isLNatKind(V2:S:S)) 0.008/0.008 U112(tt) -> tt 0.008/0.008 U12(tt,N:S:S,XS:S:S) -> U13(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U121(tt,V2:S:S) -> U122(isLNatKind(V2:S:S)) 0.008/0.008 U122(tt) -> tt 0.008/0.008 U13(tt,N:S:S,XS:S:S) -> U14(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U131(tt) -> tt 0.008/0.008 U14(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U141(tt) -> tt 0.008/0.008 U151(tt) -> tt 0.008/0.008 U161(tt) -> tt 0.008/0.008 U171(tt,V2:S:S) -> U172(isLNatKind(V2:S:S)) 0.008/0.008 U172(tt) -> tt 0.008/0.008 U181(tt,V1:S:S) -> U182(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U182(tt,V1:S:S) -> U183(isLNat(V1:S:S)) 0.008/0.008 U183(tt) -> tt 0.008/0.008 U191(tt,V1:S:S) -> U192(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U192(tt,V1:S:S) -> U193(isNatural(V1:S:S)) 0.008/0.008 U193(tt) -> tt 0.008/0.008 U201(tt,V1:S:S,V2:S:S) -> U202(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U202(tt,V1:S:S,V2:S:S) -> U203(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U203(tt,V1:S:S,V2:S:S) -> U204(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U204(tt,V1:S:S,V2:S:S) -> U205(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U205(tt,V2:S:S) -> U206(isLNat(V2:S:S)) 0.008/0.008 U206(tt) -> tt 0.008/0.008 U21(tt,X:S:S,Y:S:S) -> U22(isLNatKind(X:S:S),X:S:S,Y:S:S) 0.008/0.008 U211(tt) -> tt 0.008/0.008 U22(tt,X:S:S,Y:S:S) -> U23(isLNat(Y:S:S),X:S:S,Y:S:S) 0.008/0.008 U221(tt) -> tt 0.008/0.008 U23(tt,X:S:S,Y:S:S) -> U24(isLNatKind(Y:S:S),X:S:S) 0.008/0.008 U231(tt,V2:S:S) -> U232(isLNatKind(V2:S:S)) 0.008/0.008 U232(tt) -> tt 0.008/0.008 U24(tt,X:S:S) -> X:S:S 0.008/0.008 U241(tt,V1:S:S,V2:S:S) -> U242(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U242(tt,V1:S:S,V2:S:S) -> U243(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U243(tt,V1:S:S,V2:S:S) -> U244(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U244(tt,V1:S:S,V2:S:S) -> U245(isLNat(V1:S:S),V2:S:S) 0.008/0.008 U245(tt,V2:S:S) -> U246(isLNat(V2:S:S)) 0.008/0.008 U246(tt) -> tt 0.008/0.008 U251(tt,V1:S:S,V2:S:S) -> U252(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U252(tt,V1:S:S,V2:S:S) -> U253(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U253(tt,V1:S:S,V2:S:S) -> U254(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U254(tt,V1:S:S,V2:S:S) -> U255(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U255(tt,V2:S:S) -> U256(isLNat(V2:S:S)) 0.008/0.008 U256(tt) -> tt 0.008/0.008 U261(tt,V2:S:S) -> U262(isLNatKind(V2:S:S)) 0.008/0.008 U262(tt) -> tt 0.008/0.008 U271(tt,V2:S:S) -> U272(isLNatKind(V2:S:S)) 0.008/0.008 U272(tt) -> tt 0.008/0.008 U281(tt,N:S:S) -> U282(isNaturalKind(N:S:S),N:S:S) 0.008/0.008 U282(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.008/0.008 U291(tt,N:S:S,XS:S:S) -> U292(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U292(tt,N:S:S,XS:S:S) -> U293(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U293(tt,N:S:S,XS:S:S) -> U294(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U294(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.008/0.008 U301(tt,X:S:S,Y:S:S) -> U302(isLNatKind(X:S:S),Y:S:S) 0.008/0.008 U302(tt,Y:S:S) -> U303(isLNat(Y:S:S),Y:S:S) 0.008/0.008 U303(tt,Y:S:S) -> U304(isLNatKind(Y:S:S),Y:S:S) 0.008/0.008 U304(tt,Y:S:S) -> Y:S:S 0.008/0.008 U31(tt,N:S:S,XS:S:S) -> U32(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U311(tt,XS:S:S) -> U312(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U312(tt,XS:S:S) -> pair(nil,XS:S:S) 0.008/0.008 U32(tt,N:S:S,XS:S:S) -> U33(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U321(tt,N:S:S,X:S:S,XS:S:S) -> U322(isNaturalKind(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U322(tt,N:S:S,X:S:S,XS:S:S) -> U323(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U323(tt,N:S:S,X:S:S,XS:S:S) -> U324(isNaturalKind(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U324(tt,N:S:S,X:S:S,XS:S:S) -> U325(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U325(tt,N:S:S,X:S:S,XS:S:S) -> U326(isLNatKind(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U326(tt,N:S:S,X:S:S,XS:S:S) -> U327(splitAt(N:S:S,XS:S:S),X:S:S) 0.008/0.008 U327(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.008/0.008 U33(tt,N:S:S,XS:S:S) -> U34(isLNatKind(XS:S:S),N:S:S) 0.008/0.008 U331(tt,N:S:S,XS:S:S) -> U332(isNaturalKind(N:S:S),XS:S:S) 0.008/0.008 U332(tt,XS:S:S) -> U333(isLNat(XS:S:S),XS:S:S) 0.008/0.008 U333(tt,XS:S:S) -> U334(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U334(tt,XS:S:S) -> XS:S:S 0.008/0.008 U34(tt,N:S:S) -> N:S:S 0.008/0.008 U341(tt,N:S:S,XS:S:S) -> U342(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U342(tt,N:S:S,XS:S:S) -> U343(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U343(tt,N:S:S,XS:S:S) -> U344(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U344(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U41(tt,V1:S:S,V2:S:S) -> U42(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U42(tt,V1:S:S,V2:S:S) -> U43(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U43(tt,V1:S:S,V2:S:S) -> U44(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U44(tt,V1:S:S,V2:S:S) -> U45(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U45(tt,V2:S:S) -> U46(isLNat(V2:S:S)) 0.008/0.008 U46(tt) -> tt 0.008/0.008 U51(tt,V1:S:S,V2:S:S) -> U52(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U52(tt,V1:S:S,V2:S:S) -> U53(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U53(tt,V1:S:S,V2:S:S) -> U54(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U54(tt,V1:S:S,V2:S:S) -> U55(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U55(tt,V2:S:S) -> U56(isLNat(V2:S:S)) 0.008/0.008 U56(tt) -> tt 0.008/0.008 U61(tt,V1:S:S) -> U62(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U62(tt,V1:S:S) -> U63(isPLNat(V1:S:S)) 0.008/0.008 U63(tt) -> tt 0.008/0.008 U71(tt,V1:S:S) -> U72(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U72(tt,V1:S:S) -> U73(isNatural(V1:S:S)) 0.008/0.008 U73(tt) -> tt 0.008/0.008 U81(tt,V1:S:S) -> U82(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U82(tt,V1:S:S) -> U83(isPLNat(V1:S:S)) 0.008/0.008 U83(tt) -> tt 0.008/0.008 U91(tt,V1:S:S) -> U92(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U92(tt,V1:S:S) -> U93(isLNat(V1:S:S)) 0.008/0.008 U93(tt) -> tt 0.008/0.008 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> U111(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(fst(V1:S:S)) -> U131(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(natsFrom(V1:S:S)) -> U141(isNaturalKind(V1:S:S)) 0.008/0.008 isLNatKind(snd(V1:S:S)) -> U151(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(tail(V1:S:S)) -> U161(isLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(take(V1:S:S,V2:S:S)) -> U171(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(cons(V1:S:S,V2:S:S)) -> U121(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(nil) -> tt 0.008/0.008 isNatural(head(V1:S:S)) -> U181(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isNatural(sel(V1:S:S,V2:S:S)) -> U201(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isNatural(num0) -> tt 0.008/0.008 isNatural(s(V1:S:S)) -> U191(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isNaturalKind(head(V1:S:S)) -> U211(isLNatKind(V1:S:S)) 0.008/0.008 isNaturalKind(sel(V1:S:S,V2:S:S)) -> U231(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isNaturalKind(num0) -> tt 0.008/0.008 isNaturalKind(s(V1:S:S)) -> U221(isNaturalKind(V1:S:S)) 0.008/0.008 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U251(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNat(pair(V1:S:S,V2:S:S)) -> U241(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> U271(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isPLNatKind(pair(V1:S:S,V2:S:S)) -> U261(isLNatKind(V1:S:S),V2:S:S) 0.008/0.008 natsFrom(N:S:S) -> U281(isNatural(N:S:S),N:S:S) 0.008/0.008 sel(N:S:S,XS:S:S) -> U291(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 snd(pair(X:S:S,Y:S:S)) -> U301(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 splitAt(num0,XS:S:S) -> U311(isLNat(XS:S:S),XS:S:S) 0.008/0.008 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 tail(cons(N:S:S,XS:S:S)) -> U331(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 take(N:S:S,XS:S:S) -> U341(isNatural(N:S:S),N:S:S,XS:S: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 v_NonEmpty:S:S N:S:S V1:S:S V2:S:S X:S:S XS:S:S Y:S:S YS:S:S ZS:S:S) 0.008/0.008 (STRATEGY CONTEXTSENSITIVE 0.008/0.008 (U101 1) 0.008/0.008 (U102 1) 0.008/0.008 (U103 1) 0.008/0.008 (U104 1) 0.008/0.008 (U105 1) 0.008/0.008 (U106 1) 0.008/0.008 (U11 1) 0.008/0.008 (U111 1) 0.008/0.008 (U112 1) 0.008/0.008 (U12 1) 0.008/0.008 (U121 1) 0.008/0.008 (U122 1) 0.008/0.008 (U13 1) 0.008/0.008 (U131 1) 0.008/0.008 (U14 1) 0.008/0.008 (U141 1) 0.008/0.008 (U151 1) 0.008/0.008 (U161 1) 0.008/0.008 (U171 1) 0.008/0.008 (U172 1) 0.008/0.008 (U181 1) 0.008/0.008 (U182 1) 0.008/0.008 (U183 1) 0.008/0.008 (U191 1) 0.008/0.008 (U192 1) 0.008/0.008 (U193 1) 0.008/0.008 (U201 1) 0.008/0.008 (U202 1) 0.008/0.008 (U203 1) 0.008/0.008 (U204 1) 0.008/0.008 (U205 1) 0.008/0.008 (U206 1) 0.008/0.008 (U21 1) 0.008/0.008 (U211 1) 0.008/0.008 (U22 1) 0.008/0.008 (U221 1) 0.008/0.008 (U23 1) 0.008/0.008 (U231 1) 0.008/0.008 (U232 1) 0.008/0.008 (U24 1) 0.008/0.008 (U241 1) 0.008/0.008 (U242 1) 0.008/0.008 (U243 1) 0.008/0.008 (U244 1) 0.008/0.008 (U245 1) 0.008/0.008 (U246 1) 0.008/0.008 (U251 1) 0.008/0.008 (U252 1) 0.008/0.008 (U253 1) 0.008/0.008 (U254 1) 0.008/0.008 (U255 1) 0.008/0.008 (U256 1) 0.008/0.008 (U261 1) 0.008/0.008 (U262 1) 0.008/0.008 (U271 1) 0.008/0.008 (U272 1) 0.008/0.008 (U281 1) 0.008/0.008 (U282 1) 0.008/0.008 (U291 1) 0.008/0.008 (U292 1) 0.008/0.008 (U293 1) 0.008/0.008 (U294 1) 0.008/0.008 (U301 1) 0.008/0.008 (U302 1) 0.008/0.008 (U303 1) 0.008/0.008 (U304 1) 0.008/0.008 (U31 1) 0.008/0.008 (U311 1) 0.008/0.008 (U312 1) 0.008/0.008 (U32 1) 0.008/0.008 (U321 1) 0.008/0.008 (U322 1) 0.008/0.008 (U323 1) 0.008/0.008 (U324 1) 0.008/0.008 (U325 1) 0.008/0.008 (U326 1) 0.008/0.008 (U327 1) 0.008/0.008 (U33 1) 0.008/0.008 (U331 1) 0.008/0.008 (U332 1) 0.008/0.008 (U333 1) 0.008/0.008 (U334 1) 0.008/0.008 (U34 1) 0.008/0.008 (U341 1) 0.008/0.008 (U342 1) 0.008/0.008 (U343 1) 0.008/0.008 (U344 1) 0.008/0.008 (U41 1) 0.008/0.008 (U42 1) 0.008/0.008 (U43 1) 0.008/0.008 (U44 1) 0.008/0.008 (U45 1) 0.008/0.008 (U46 1) 0.008/0.008 (U51 1) 0.008/0.008 (U52 1) 0.008/0.008 (U53 1) 0.008/0.008 (U54 1) 0.008/0.008 (U55 1) 0.008/0.008 (U56 1) 0.008/0.008 (U61 1) 0.008/0.008 (U62 1) 0.008/0.008 (U63 1) 0.008/0.008 (U71 1) 0.008/0.008 (U72 1) 0.008/0.008 (U73 1) 0.008/0.008 (U81 1) 0.008/0.008 (U82 1) 0.008/0.008 (U83 1) 0.008/0.008 (U91 1) 0.008/0.008 (U92 1) 0.008/0.008 (U93 1) 0.008/0.008 (afterNth) 0.008/0.008 (fst 1) 0.008/0.008 (head 1) 0.008/0.008 (isLNat 1) 0.008/0.008 (isLNatKind 1) 0.008/0.008 (isNatural 1) 0.008/0.008 (isNaturalKind 1) 0.008/0.008 (isPLNat 1) 0.008/0.008 (isPLNatKind 1) 0.008/0.008 (natsFrom) 0.008/0.008 (sel) 0.008/0.008 (snd 1) 0.008/0.008 (splitAt 1 2) 0.008/0.008 (tail 1) 0.008/0.008 (take) 0.008/0.008 (cons) 0.008/0.008 (fSNonEmpty) 0.008/0.008 (nil) 0.008/0.008 (num0) 0.008/0.008 (pair) 0.008/0.008 (s) 0.008/0.008 (tt) 0.008/0.008 ) 0.008/0.008 (RULES 0.008/0.008 U101(tt,V1:S:S,V2:S:S) -> U102(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U102(tt,V1:S:S,V2:S:S) -> U103(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U103(tt,V1:S:S,V2:S:S) -> U104(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U104(tt,V1:S:S,V2:S:S) -> U105(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U105(tt,V2:S:S) -> U106(isLNat(V2:S:S)) 0.008/0.008 U106(tt) -> tt 0.008/0.008 U11(tt,N:S:S,XS:S:S) -> U12(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U111(tt,V2:S:S) -> U112(isLNatKind(V2:S:S)) 0.008/0.008 U112(tt) -> tt 0.008/0.008 U12(tt,N:S:S,XS:S:S) -> U13(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U121(tt,V2:S:S) -> U122(isLNatKind(V2:S:S)) 0.008/0.008 U122(tt) -> tt 0.008/0.008 U13(tt,N:S:S,XS:S:S) -> U14(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U131(tt) -> tt 0.008/0.008 U14(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U141(tt) -> tt 0.008/0.008 U151(tt) -> tt 0.008/0.008 U161(tt) -> tt 0.008/0.008 U171(tt,V2:S:S) -> U172(isLNatKind(V2:S:S)) 0.008/0.008 U172(tt) -> tt 0.008/0.008 U181(tt,V1:S:S) -> U182(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U182(tt,V1:S:S) -> U183(isLNat(V1:S:S)) 0.008/0.008 U183(tt) -> tt 0.008/0.008 U191(tt,V1:S:S) -> U192(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U192(tt,V1:S:S) -> U193(isNatural(V1:S:S)) 0.008/0.008 U193(tt) -> tt 0.008/0.008 U201(tt,V1:S:S,V2:S:S) -> U202(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U202(tt,V1:S:S,V2:S:S) -> U203(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U203(tt,V1:S:S,V2:S:S) -> U204(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U204(tt,V1:S:S,V2:S:S) -> U205(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U205(tt,V2:S:S) -> U206(isLNat(V2:S:S)) 0.008/0.008 U206(tt) -> tt 0.008/0.008 U21(tt,X:S:S,Y:S:S) -> U22(isLNatKind(X:S:S),X:S:S,Y:S:S) 0.008/0.008 U211(tt) -> tt 0.008/0.008 U22(tt,X:S:S,Y:S:S) -> U23(isLNat(Y:S:S),X:S:S,Y:S:S) 0.008/0.008 U221(tt) -> tt 0.008/0.008 U23(tt,X:S:S,Y:S:S) -> U24(isLNatKind(Y:S:S),X:S:S) 0.008/0.008 U231(tt,V2:S:S) -> U232(isLNatKind(V2:S:S)) 0.008/0.008 U232(tt) -> tt 0.008/0.008 U24(tt,X:S:S) -> X:S:S 0.008/0.008 U241(tt,V1:S:S,V2:S:S) -> U242(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U242(tt,V1:S:S,V2:S:S) -> U243(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U243(tt,V1:S:S,V2:S:S) -> U244(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U244(tt,V1:S:S,V2:S:S) -> U245(isLNat(V1:S:S),V2:S:S) 0.008/0.008 U245(tt,V2:S:S) -> U246(isLNat(V2:S:S)) 0.008/0.008 U246(tt) -> tt 0.008/0.008 U251(tt,V1:S:S,V2:S:S) -> U252(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U252(tt,V1:S:S,V2:S:S) -> U253(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U253(tt,V1:S:S,V2:S:S) -> U254(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U254(tt,V1:S:S,V2:S:S) -> U255(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U255(tt,V2:S:S) -> U256(isLNat(V2:S:S)) 0.008/0.008 U256(tt) -> tt 0.008/0.008 U261(tt,V2:S:S) -> U262(isLNatKind(V2:S:S)) 0.008/0.008 U262(tt) -> tt 0.008/0.008 U271(tt,V2:S:S) -> U272(isLNatKind(V2:S:S)) 0.008/0.008 U272(tt) -> tt 0.008/0.008 U281(tt,N:S:S) -> U282(isNaturalKind(N:S:S),N:S:S) 0.008/0.008 U282(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.008/0.008 U291(tt,N:S:S,XS:S:S) -> U292(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U292(tt,N:S:S,XS:S:S) -> U293(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U293(tt,N:S:S,XS:S:S) -> U294(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U294(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.008/0.008 U301(tt,X:S:S,Y:S:S) -> U302(isLNatKind(X:S:S),Y:S:S) 0.008/0.008 U302(tt,Y:S:S) -> U303(isLNat(Y:S:S),Y:S:S) 0.008/0.008 U303(tt,Y:S:S) -> U304(isLNatKind(Y:S:S),Y:S:S) 0.008/0.008 U304(tt,Y:S:S) -> Y:S:S 0.008/0.008 U31(tt,N:S:S,XS:S:S) -> U32(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U311(tt,XS:S:S) -> U312(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U312(tt,XS:S:S) -> pair(nil,XS:S:S) 0.008/0.008 U32(tt,N:S:S,XS:S:S) -> U33(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U321(tt,N:S:S,X:S:S,XS:S:S) -> U322(isNaturalKind(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U322(tt,N:S:S,X:S:S,XS:S:S) -> U323(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U323(tt,N:S:S,X:S:S,XS:S:S) -> U324(isNaturalKind(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U324(tt,N:S:S,X:S:S,XS:S:S) -> U325(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U325(tt,N:S:S,X:S:S,XS:S:S) -> U326(isLNatKind(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U326(tt,N:S:S,X:S:S,XS:S:S) -> U327(splitAt(N:S:S,XS:S:S),X:S:S) 0.008/0.008 U327(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.008/0.008 U33(tt,N:S:S,XS:S:S) -> U34(isLNatKind(XS:S:S),N:S:S) 0.008/0.008 U331(tt,N:S:S,XS:S:S) -> U332(isNaturalKind(N:S:S),XS:S:S) 0.008/0.008 U332(tt,XS:S:S) -> U333(isLNat(XS:S:S),XS:S:S) 0.008/0.008 U333(tt,XS:S:S) -> U334(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U334(tt,XS:S:S) -> XS:S:S 0.008/0.008 U34(tt,N:S:S) -> N:S:S 0.008/0.008 U341(tt,N:S:S,XS:S:S) -> U342(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U342(tt,N:S:S,XS:S:S) -> U343(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U343(tt,N:S:S,XS:S:S) -> U344(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U344(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U41(tt,V1:S:S,V2:S:S) -> U42(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U42(tt,V1:S:S,V2:S:S) -> U43(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U43(tt,V1:S:S,V2:S:S) -> U44(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U44(tt,V1:S:S,V2:S:S) -> U45(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U45(tt,V2:S:S) -> U46(isLNat(V2:S:S)) 0.008/0.008 U46(tt) -> tt 0.008/0.008 U51(tt,V1:S:S,V2:S:S) -> U52(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U52(tt,V1:S:S,V2:S:S) -> U53(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U53(tt,V1:S:S,V2:S:S) -> U54(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U54(tt,V1:S:S,V2:S:S) -> U55(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U55(tt,V2:S:S) -> U56(isLNat(V2:S:S)) 0.008/0.008 U56(tt) -> tt 0.008/0.008 U61(tt,V1:S:S) -> U62(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U62(tt,V1:S:S) -> U63(isPLNat(V1:S:S)) 0.008/0.008 U63(tt) -> tt 0.008/0.008 U71(tt,V1:S:S) -> U72(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U72(tt,V1:S:S) -> U73(isNatural(V1:S:S)) 0.008/0.008 U73(tt) -> tt 0.008/0.008 U81(tt,V1:S:S) -> U82(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U82(tt,V1:S:S) -> U83(isPLNat(V1:S:S)) 0.008/0.008 U83(tt) -> tt 0.008/0.008 U91(tt,V1:S:S) -> U92(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U92(tt,V1:S:S) -> U93(isLNat(V1:S:S)) 0.008/0.008 U93(tt) -> tt 0.008/0.008 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> U111(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(fst(V1:S:S)) -> U131(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(natsFrom(V1:S:S)) -> U141(isNaturalKind(V1:S:S)) 0.008/0.008 isLNatKind(snd(V1:S:S)) -> U151(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(tail(V1:S:S)) -> U161(isLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(take(V1:S:S,V2:S:S)) -> U171(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(cons(V1:S:S,V2:S:S)) -> U121(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(nil) -> tt 0.008/0.008 isNatural(head(V1:S:S)) -> U181(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isNatural(sel(V1:S:S,V2:S:S)) -> U201(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isNatural(num0) -> tt 0.008/0.008 isNatural(s(V1:S:S)) -> U191(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isNaturalKind(head(V1:S:S)) -> U211(isLNatKind(V1:S:S)) 0.008/0.008 isNaturalKind(sel(V1:S:S,V2:S:S)) -> U231(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isNaturalKind(num0) -> tt 0.008/0.008 isNaturalKind(s(V1:S:S)) -> U221(isNaturalKind(V1:S:S)) 0.008/0.008 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U251(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNat(pair(V1:S:S,V2:S:S)) -> U241(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> U271(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isPLNatKind(pair(V1:S:S,V2:S:S)) -> U261(isLNatKind(V1:S:S),V2:S:S) 0.008/0.008 natsFrom(N:S:S) -> U281(isNatural(N:S:S),N:S:S) 0.008/0.008 sel(N:S:S,XS:S:S) -> U291(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 snd(pair(X:S:S,Y:S:S)) -> U301(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 splitAt(num0,XS:S:S) -> U311(isLNat(XS:S:S),XS:S:S) 0.008/0.008 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 tail(cons(N:S:S,XS:S:S)) -> U331(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 take(N:S:S,XS:S:S) -> U341(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 ) 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,V1:S:S,V2:S:S) -> U102(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U102(tt,V1:S:S,V2:S:S) -> U103(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U103(tt,V1:S:S,V2:S:S) -> U104(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U104(tt,V1:S:S,V2:S:S) -> U105(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U105(tt,V2:S:S) -> U106(isLNat(V2:S:S)) 0.008/0.008 U106(tt) -> tt 0.008/0.008 U11(tt,N:S:S,XS:S:S) -> U12(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U111(tt,V2:S:S) -> U112(isLNatKind(V2:S:S)) 0.008/0.008 U112(tt) -> tt 0.008/0.008 U12(tt,N:S:S,XS:S:S) -> U13(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U121(tt,V2:S:S) -> U122(isLNatKind(V2:S:S)) 0.008/0.008 U122(tt) -> tt 0.008/0.008 U13(tt,N:S:S,XS:S:S) -> U14(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U131(tt) -> tt 0.008/0.008 U14(tt,N:S:S,XS:S:S) -> snd(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U141(tt) -> tt 0.008/0.008 U151(tt) -> tt 0.008/0.008 U161(tt) -> tt 0.008/0.008 U171(tt,V2:S:S) -> U172(isLNatKind(V2:S:S)) 0.008/0.008 U172(tt) -> tt 0.008/0.008 U181(tt,V1:S:S) -> U182(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U182(tt,V1:S:S) -> U183(isLNat(V1:S:S)) 0.008/0.008 U183(tt) -> tt 0.008/0.008 U191(tt,V1:S:S) -> U192(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U192(tt,V1:S:S) -> U193(isNatural(V1:S:S)) 0.008/0.008 U193(tt) -> tt 0.008/0.008 U201(tt,V1:S:S,V2:S:S) -> U202(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U202(tt,V1:S:S,V2:S:S) -> U203(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U203(tt,V1:S:S,V2:S:S) -> U204(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U204(tt,V1:S:S,V2:S:S) -> U205(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U205(tt,V2:S:S) -> U206(isLNat(V2:S:S)) 0.008/0.008 U206(tt) -> tt 0.008/0.008 U21(tt,X:S:S,Y:S:S) -> U22(isLNatKind(X:S:S),X:S:S,Y:S:S) 0.008/0.008 U211(tt) -> tt 0.008/0.008 U22(tt,X:S:S,Y:S:S) -> U23(isLNat(Y:S:S),X:S:S,Y:S:S) 0.008/0.008 U221(tt) -> tt 0.008/0.008 U23(tt,X:S:S,Y:S:S) -> U24(isLNatKind(Y:S:S),X:S:S) 0.008/0.008 U231(tt,V2:S:S) -> U232(isLNatKind(V2:S:S)) 0.008/0.008 U232(tt) -> tt 0.008/0.008 U24(tt,X:S:S) -> X:S:S 0.008/0.008 U241(tt,V1:S:S,V2:S:S) -> U242(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U242(tt,V1:S:S,V2:S:S) -> U243(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U243(tt,V1:S:S,V2:S:S) -> U244(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U244(tt,V1:S:S,V2:S:S) -> U245(isLNat(V1:S:S),V2:S:S) 0.008/0.008 U245(tt,V2:S:S) -> U246(isLNat(V2:S:S)) 0.008/0.008 U246(tt) -> tt 0.008/0.008 U251(tt,V1:S:S,V2:S:S) -> U252(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U252(tt,V1:S:S,V2:S:S) -> U253(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U253(tt,V1:S:S,V2:S:S) -> U254(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U254(tt,V1:S:S,V2:S:S) -> U255(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U255(tt,V2:S:S) -> U256(isLNat(V2:S:S)) 0.008/0.008 U256(tt) -> tt 0.008/0.008 U261(tt,V2:S:S) -> U262(isLNatKind(V2:S:S)) 0.008/0.008 U262(tt) -> tt 0.008/0.008 U271(tt,V2:S:S) -> U272(isLNatKind(V2:S:S)) 0.008/0.008 U272(tt) -> tt 0.008/0.008 U281(tt,N:S:S) -> U282(isNaturalKind(N:S:S),N:S:S) 0.008/0.008 U282(tt,N:S:S) -> cons(N:S:S,natsFrom(s(N:S:S))) 0.008/0.008 U291(tt,N:S:S,XS:S:S) -> U292(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U292(tt,N:S:S,XS:S:S) -> U293(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U293(tt,N:S:S,XS:S:S) -> U294(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U294(tt,N:S:S,XS:S:S) -> head(afterNth(N:S:S,XS:S:S)) 0.008/0.008 U301(tt,X:S:S,Y:S:S) -> U302(isLNatKind(X:S:S),Y:S:S) 0.008/0.008 U302(tt,Y:S:S) -> U303(isLNat(Y:S:S),Y:S:S) 0.008/0.008 U303(tt,Y:S:S) -> U304(isLNatKind(Y:S:S),Y:S:S) 0.008/0.008 U304(tt,Y:S:S) -> Y:S:S 0.008/0.008 U31(tt,N:S:S,XS:S:S) -> U32(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U311(tt,XS:S:S) -> U312(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U312(tt,XS:S:S) -> pair(nil,XS:S:S) 0.008/0.008 U32(tt,N:S:S,XS:S:S) -> U33(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U321(tt,N:S:S,X:S:S,XS:S:S) -> U322(isNaturalKind(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U322(tt,N:S:S,X:S:S,XS:S:S) -> U323(isNatural(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U323(tt,N:S:S,X:S:S,XS:S:S) -> U324(isNaturalKind(X:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U324(tt,N:S:S,X:S:S,XS:S:S) -> U325(isLNat(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U325(tt,N:S:S,X:S:S,XS:S:S) -> U326(isLNatKind(XS:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 U326(tt,N:S:S,X:S:S,XS:S:S) -> U327(splitAt(N:S:S,XS:S:S),X:S:S) 0.008/0.008 U327(pair(YS:S:S,ZS:S:S),X:S:S) -> pair(cons(X:S:S,YS:S:S),ZS:S:S) 0.008/0.008 U33(tt,N:S:S,XS:S:S) -> U34(isLNatKind(XS:S:S),N:S:S) 0.008/0.008 U331(tt,N:S:S,XS:S:S) -> U332(isNaturalKind(N:S:S),XS:S:S) 0.008/0.008 U332(tt,XS:S:S) -> U333(isLNat(XS:S:S),XS:S:S) 0.008/0.008 U333(tt,XS:S:S) -> U334(isLNatKind(XS:S:S),XS:S:S) 0.008/0.008 U334(tt,XS:S:S) -> XS:S:S 0.008/0.008 U34(tt,N:S:S) -> N:S:S 0.008/0.008 U341(tt,N:S:S,XS:S:S) -> U342(isNaturalKind(N:S:S),N:S:S,XS:S:S) 0.008/0.008 U342(tt,N:S:S,XS:S:S) -> U343(isLNat(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U343(tt,N:S:S,XS:S:S) -> U344(isLNatKind(XS:S:S),N:S:S,XS:S:S) 0.008/0.008 U344(tt,N:S:S,XS:S:S) -> fst(splitAt(N:S:S,XS:S:S)) 0.008/0.008 U41(tt,V1:S:S,V2:S:S) -> U42(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U42(tt,V1:S:S,V2:S:S) -> U43(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U43(tt,V1:S:S,V2:S:S) -> U44(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U44(tt,V1:S:S,V2:S:S) -> U45(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U45(tt,V2:S:S) -> U46(isLNat(V2:S:S)) 0.008/0.008 U46(tt) -> tt 0.008/0.008 U51(tt,V1:S:S,V2:S:S) -> U52(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 U52(tt,V1:S:S,V2:S:S) -> U53(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U53(tt,V1:S:S,V2:S:S) -> U54(isLNatKind(V2:S:S),V1:S:S,V2:S:S) 0.008/0.008 U54(tt,V1:S:S,V2:S:S) -> U55(isNatural(V1:S:S),V2:S:S) 0.008/0.008 U55(tt,V2:S:S) -> U56(isLNat(V2:S:S)) 0.008/0.008 U56(tt) -> tt 0.008/0.008 U61(tt,V1:S:S) -> U62(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U62(tt,V1:S:S) -> U63(isPLNat(V1:S:S)) 0.008/0.008 U63(tt) -> tt 0.008/0.008 U71(tt,V1:S:S) -> U72(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 U72(tt,V1:S:S) -> U73(isNatural(V1:S:S)) 0.008/0.008 U73(tt) -> tt 0.008/0.008 U81(tt,V1:S:S) -> U82(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U82(tt,V1:S:S) -> U83(isPLNat(V1:S:S)) 0.008/0.008 U83(tt) -> tt 0.008/0.008 U91(tt,V1:S:S) -> U92(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 U92(tt,V1:S:S) -> U93(isLNat(V1:S:S)) 0.008/0.008 U93(tt) -> tt 0.008/0.008 afterNth(N:S:S,XS:S:S) -> U11(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 fst(pair(X:S:S,Y:S:S)) -> U21(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 head(cons(N:S:S,XS:S:S)) -> U31(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 isLNat(afterNth(V1:S:S,V2:S:S)) -> U41(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(fst(V1:S:S)) -> U61(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(natsFrom(V1:S:S)) -> U71(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(snd(V1:S:S)) -> U81(isPLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(tail(V1:S:S)) -> U91(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isLNat(take(V1:S:S,V2:S:S)) -> U101(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(cons(V1:S:S,V2:S:S)) -> U51(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isLNat(nil) -> tt 0.008/0.008 isLNatKind(afterNth(V1:S:S,V2:S:S)) -> U111(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(fst(V1:S:S)) -> U131(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(natsFrom(V1:S:S)) -> U141(isNaturalKind(V1:S:S)) 0.008/0.008 isLNatKind(snd(V1:S:S)) -> U151(isPLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(tail(V1:S:S)) -> U161(isLNatKind(V1:S:S)) 0.008/0.008 isLNatKind(take(V1:S:S,V2:S:S)) -> U171(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(cons(V1:S:S,V2:S:S)) -> U121(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isLNatKind(nil) -> tt 0.008/0.008 isNatural(head(V1:S:S)) -> U181(isLNatKind(V1:S:S),V1:S:S) 0.008/0.008 isNatural(sel(V1:S:S,V2:S:S)) -> U201(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isNatural(num0) -> tt 0.008/0.008 isNatural(s(V1:S:S)) -> U191(isNaturalKind(V1:S:S),V1:S:S) 0.008/0.008 isNaturalKind(head(V1:S:S)) -> U211(isLNatKind(V1:S:S)) 0.008/0.008 isNaturalKind(sel(V1:S:S,V2:S:S)) -> U231(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isNaturalKind(num0) -> tt 0.008/0.008 isNaturalKind(s(V1:S:S)) -> U221(isNaturalKind(V1:S:S)) 0.008/0.008 isPLNat(splitAt(V1:S:S,V2:S:S)) -> U251(isNaturalKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNat(pair(V1:S:S,V2:S:S)) -> U241(isLNatKind(V1:S:S),V1:S:S,V2:S:S) 0.008/0.008 isPLNatKind(splitAt(V1:S:S,V2:S:S)) -> U271(isNaturalKind(V1:S:S),V2:S:S) 0.008/0.008 isPLNatKind(pair(V1:S:S,V2:S:S)) -> U261(isLNatKind(V1:S:S),V2:S:S) 0.008/0.008 natsFrom(N:S:S) -> U281(isNatural(N:S:S),N:S:S) 0.008/0.008 sel(N:S:S,XS:S:S) -> U291(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 snd(pair(X:S:S,Y:S:S)) -> U301(isLNat(X:S:S),X:S:S,Y:S:S) 0.008/0.008 splitAt(num0,XS:S:S) -> U311(isLNat(XS:S:S),XS:S:S) 0.008/0.008 splitAt(s(N:S:S),cons(X:S:S,XS:S:S)) -> U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S) 0.008/0.008 tail(cons(N:S:S,XS:S:S)) -> U331(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 take(N:S:S,XS:S:S) -> U341(isNatural(N:S:S),N:S:S,XS:S:S) 0.008/0.008 -> Vars: 0.008/0.008 V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, N:S, XS:S, V2:S, N:S, XS:S, V2:S, N:S, XS:S, N:S, XS:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, X:S, Y:S, X:S, Y:S, X:S, Y:S, V2:S, X:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V2:S, V2:S, N:S, N:S, N:S, XS:S, N:S, XS:S, N:S, XS:S, N:S, XS:S, X:S, Y:S, Y:S, Y:S, Y:S, N:S, XS:S, XS:S, XS:S, N:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, N:S, X:S, XS:S, X:S, YS:S, ZS:S, N:S, XS:S, N:S, XS:S, XS:S, XS:S, XS:S, N:S, N:S, XS:S, N:S, XS:S, N:S, XS:S, N:S, XS:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V1:S, V1:S, V1:S, N:S, XS:S, X:S, Y:S, N:S, XS:S, V1:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V1:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V1:S, V1:S, V2:S, V1:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, V1:S, V2:S, N:S, N:S, XS:S, X:S, Y:S, XS:S, N:S, X:S, XS:S, N:S, XS:S, N:S, XS:S 0.008/0.008 -> UVars: 0.008/0.008 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 4, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 5, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 6, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 7, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 8, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 9, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 10, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 11, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 12, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 13, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 14, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 15, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 16, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 17, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 18, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 19, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 20, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 21, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 22, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 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: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 25, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 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: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 28, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 29, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 30, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 31, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 32, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 33, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.008/0.008 (UV-RuleId: 34, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 35, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.008/0.008 (UV-RuleId: 36, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 37, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S]) 0.008/0.008 (UV-RuleId: 38, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 39, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 40, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 41, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 42, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 43, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 44, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 45, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 46, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 47, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 48, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 49, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 50, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 51, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 52, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 53, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 54, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 55, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 56, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 57, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.008/0.008 (UV-RuleId: 58, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.008/0.008 (UV-RuleId: 59, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 60, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 61, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 62, UV-LActive: [], UV-RActive: [], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 63, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [Y:S]) 0.008/0.008 (UV-RuleId: 64, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: [Y:S]) 0.008/0.008 (UV-RuleId: 65, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: [Y:S]) 0.008/0.008 (UV-RuleId: 66, UV-LActive: [], UV-RActive: [Y:S], UV-LFrozen: [Y:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 67, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 68, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 69, UV-LActive: [], UV-RActive: [], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 70, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 71, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 72, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 73, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 74, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 75, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 76, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [X:S]) 0.008/0.008 (UV-RuleId: 77, UV-LActive: [], UV-RActive: [], UV-LFrozen: [X:S, YS:S, ZS:S], UV-RFrozen: [X:S, YS:S, ZS:S]) 0.008/0.008 (UV-RuleId: 78, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S]) 0.008/0.008 (UV-RuleId: 79, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 80, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 81, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 82, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [XS:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 83, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 84, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 85, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 86, UV-LActive: [], UV-RActive: [XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 87, UV-LActive: [], UV-RActive: [N:S, XS:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 88, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 89, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 90, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 91, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 92, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 93, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 94, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 95, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 96, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 97, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 98, UV-LActive: [], UV-RActive: [V2:S], UV-LFrozen: [V2:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 99, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 100, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 101, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 102, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 103, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 104, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 105, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 106, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 107, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 108, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 109, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 110, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 111, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 112, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 113, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.008/0.008 (UV-RuleId: 114, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 115, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 116, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 117, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 118, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 119, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 120, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 121, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 122, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 123, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 124, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 125, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 126, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 127, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 128, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 129, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 130, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 131, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 132, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 133, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 134, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: [V1:S]) 0.008/0.008 (UV-RuleId: 135, UV-LActive: [V1:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 136, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 137, UV-LActive: [], UV-RActive: [], UV-LFrozen: [], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 138, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S], UV-RFrozen: []) 0.008/0.008 (UV-RuleId: 139, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 140, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V1:S, V2:S]) 0.008/0.008 (UV-RuleId: 141, UV-LActive: [V1:S, V2:S], UV-RActive: [V1:S], UV-LFrozen: [], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 142, UV-LActive: [], UV-RActive: [V1:S], UV-LFrozen: [V1:S, V2:S], UV-RFrozen: [V2:S]) 0.008/0.008 (UV-RuleId: 143, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S], UV-RFrozen: [N:S]) 0.008/0.008 (UV-RuleId: 144, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 145, UV-LActive: [], UV-RActive: [X:S], UV-LFrozen: [X:S, Y:S], UV-RFrozen: [X:S, Y:S]) 0.008/0.008 (UV-RuleId: 146, UV-LActive: [XS:S], UV-RActive: [XS:S], UV-LFrozen: [], UV-RFrozen: [XS:S]) 0.008/0.008 (UV-RuleId: 147, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, X:S, XS:S], UV-RFrozen: [N:S, X:S, XS:S]) 0.008/0.008 (UV-RuleId: 148, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 (UV-RuleId: 149, UV-LActive: [], UV-RActive: [N:S], UV-LFrozen: [N:S, XS:S], UV-RFrozen: [N:S, XS:S]) 0.008/0.008 -> FVars: 0.008/0.008 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, x65, x66, x67, x68, x69, x70, x71, x72, x73, x74, x75, x76, x77, x78, x79, x80, x81, x82, x83, x84, x85, x86, x87, x88, x89, x90, x91, x92, x93, x94, x95, x96, x97, x98, x99, x100, x101, x102, x103, x104, x105, x106, x107, x108, x109, x110, x111, x112, x113, x114, x115, x116, x117, x118, x119, x120, x121, x122, x123, x124, x125, x126, x127, x128, x129, x130, x131, x132, x133, x134, x135, x136, x137, x138, x139, x140, x141, x142, x143, x144, x145, x146, x147, x148, x149, x150, x151, x152, x153, x154, x155, x156, x157, x158, x159, x160, x161, x162, x163, x164, x165, x166, x167, x168, x169, x170, x171, x172, x173, x174, x175, x176, x177, x178, x179, x180, x181, x182, x183, x184, x185, x186, x187, x188, x189, x190, x191, x192, x193, x194, x195, x196, x197, x198, x199, x200, x201, x202, x203, x204, x205, x206, x207, x208, x209 0.008/0.008 -> PVars: 0.008/0.008 V1:S: [x10, x12, x14, x16, x30, x31, x32, x33, x34, x36, x38, x40, x51, x53, x55, x57, x60, x62, x64, x66, x129, x131, x133, x135, x138, x140, x142, x144, x147, x148, x149, x150, x151, x152, x153, x154, x161, x163, x164, x165, x166, x167, x169, x171, x173, x174, x175, x176, x177, x179, x181, x182, x184, x185, x186, x188, x189, x191, x193, x195], V2:S: [x11, x13, x15, x17, x18, x21, x24, x29, x35, x37, x39, x41, x42, x49, x52, x54, x56, x58, x59, x61, x63, x65, x67, x68, x69, x70, x130, x132, x134, x136, x137, x139, x141, x143, x145, x146, x162, x168, x170, x172, x178, x180, x183, x187, x190, x192, x194, x196], N:S: [x19, x22, x25, x27, x71, x72, x73, x75, x77, x79, x86, x90, x92, x95, x98, x101, x104, x107, x113, x115, x120, x121, x123, x125, x127, x155, x159, x197, x198, x203, x206, x208], XS:S: [x20, x23, x26, x28, x74, x76, x78, x80, x87, x88, x89, x91, x94, x97, x100, x103, x106, x109, x114, x116, x117, x118, x119, x122, x124, x126, x128, x156, x160, x199, x202, x205, x207, x209], X:S: [x43, x45, x47, x50, x81, x93, x96, x99, x102, x105, x108, x110, x157, x200, x204], Y:S: [x44, x46, x48, x82, x83, x84, x85, x158, x201], YS:S: [x111], ZS:S: [x112] 0.008/0.008 0.008/0.008 -> Rlps: 0.008/0.008 (rule: U101(tt,x10:S,x11:S) -> U102(isNaturalKind(x10:S),x10:S,x11:S), id: 1, possubterms: U101(tt,x10:S,x11:S)->[], tt->[1]) 0.008/0.008 (rule: U102(tt,x12:S,x13:S) -> U103(isLNatKind(x13:S),x12:S,x13:S), id: 2, possubterms: U102(tt,x12:S,x13:S)->[], tt->[1]) 0.008/0.008 (rule: U103(tt,x14:S,x15:S) -> U104(isLNatKind(x15:S),x14:S,x15:S), id: 3, possubterms: U103(tt,x14:S,x15:S)->[], tt->[1]) 0.008/0.008 (rule: U104(tt,x16:S,x17:S) -> U105(isNatural(x16:S),x17:S), id: 4, possubterms: U104(tt,x16:S,x17:S)->[], tt->[1]) 0.008/0.008 (rule: U105(tt,x18:S) -> U106(isLNat(x18:S)), id: 5, possubterms: U105(tt,x18:S)->[], tt->[1]) 0.008/0.008 (rule: U106(tt) -> tt, id: 6, possubterms: U106(tt)->[], tt->[1]) 0.008/0.008 (rule: U11(tt,x19:S,x20:S) -> U12(isNaturalKind(x19:S),x19:S,x20:S), id: 7, possubterms: U11(tt,x19:S,x20:S)->[], tt->[1]) 0.008/0.008 (rule: U111(tt,x21:S) -> U112(isLNatKind(x21:S)), id: 8, possubterms: U111(tt,x21:S)->[], tt->[1]) 0.008/0.008 (rule: U112(tt) -> tt, id: 9, possubterms: U112(tt)->[], tt->[1]) 0.008/0.008 (rule: U12(tt,x22:S,x23:S) -> U13(isLNat(x23:S),x22:S,x23:S), id: 10, possubterms: U12(tt,x22:S,x23:S)->[], tt->[1]) 0.008/0.008 (rule: U121(tt,x24:S) -> U122(isLNatKind(x24:S)), id: 11, possubterms: U121(tt,x24:S)->[], tt->[1]) 0.008/0.008 (rule: U122(tt) -> tt, id: 12, possubterms: U122(tt)->[], tt->[1]) 0.008/0.008 (rule: U13(tt,x25:S,x26:S) -> U14(isLNatKind(x26:S),x25:S,x26:S), id: 13, possubterms: U13(tt,x25:S,x26:S)->[], tt->[1]) 0.008/0.008 (rule: U131(tt) -> tt, id: 14, possubterms: U131(tt)->[], tt->[1]) 0.008/0.008 (rule: U14(tt,x27:S,x28:S) -> snd(splitAt(x27:S,x28:S)), id: 15, possubterms: U14(tt,x27:S,x28:S)->[], tt->[1]) 0.008/0.008 (rule: U141(tt) -> tt, id: 16, possubterms: U141(tt)->[], tt->[1]) 0.008/0.008 (rule: U151(tt) -> tt, id: 17, possubterms: U151(tt)->[], tt->[1]) 0.008/0.008 (rule: U161(tt) -> tt, id: 18, possubterms: U161(tt)->[], tt->[1]) 0.008/0.008 (rule: U171(tt,x29:S) -> U172(isLNatKind(x29:S)), id: 19, possubterms: U171(tt,x29:S)->[], tt->[1]) 0.008/0.008 (rule: U172(tt) -> tt, id: 20, possubterms: U172(tt)->[], tt->[1]) 0.008/0.008 (rule: U181(tt,x30:S) -> U182(isLNatKind(x30:S),x30:S), id: 21, possubterms: U181(tt,x30:S)->[], tt->[1]) 0.008/0.008 (rule: U182(tt,x31:S) -> U183(isLNat(x31:S)), id: 22, possubterms: U182(tt,x31:S)->[], tt->[1]) 0.008/0.008 (rule: U183(tt) -> tt, id: 23, possubterms: U183(tt)->[], tt->[1]) 0.008/0.008 (rule: U191(tt,x32:S) -> U192(isNaturalKind(x32:S),x32:S), id: 24, possubterms: U191(tt,x32:S)->[], tt->[1]) 0.008/0.008 (rule: U192(tt,x33:S) -> U193(isNatural(x33:S)), id: 25, possubterms: U192(tt,x33:S)->[], tt->[1]) 0.008/0.008 (rule: U193(tt) -> tt, id: 26, possubterms: U193(tt)->[], tt->[1]) 0.008/0.008 (rule: U201(tt,x34:S,x35:S) -> U202(isNaturalKind(x34:S),x34:S,x35:S), id: 27, possubterms: U201(tt,x34:S,x35:S)->[], tt->[1]) 0.008/0.008 (rule: U202(tt,x36:S,x37:S) -> U203(isLNatKind(x37:S),x36:S,x37:S), id: 28, possubterms: U202(tt,x36:S,x37:S)->[], tt->[1]) 0.008/0.008 (rule: U203(tt,x38:S,x39:S) -> U204(isLNatKind(x39:S),x38:S,x39:S), id: 29, possubterms: U203(tt,x38:S,x39:S)->[], tt->[1]) 0.008/0.008 (rule: U204(tt,x40:S,x41:S) -> U205(isNatural(x40:S),x41:S), id: 30, possubterms: U204(tt,x40:S,x41:S)->[], tt->[1]) 0.008/0.008 (rule: U205(tt,x42:S) -> U206(isLNat(x42:S)), id: 31, possubterms: U205(tt,x42:S)->[], tt->[1]) 0.008/0.008 (rule: U206(tt) -> tt, id: 32, possubterms: U206(tt)->[], tt->[1]) 0.008/0.008 (rule: U21(tt,x43:S,x44:S) -> U22(isLNatKind(x43:S),x43:S,x44:S), id: 33, possubterms: U21(tt,x43:S,x44:S)->[], tt->[1]) 0.008/0.008 (rule: U211(tt) -> tt, id: 34, possubterms: U211(tt)->[], tt->[1]) 0.008/0.008 (rule: U22(tt,x45:S,x46:S) -> U23(isLNat(x46:S),x45:S,x46:S), id: 35, possubterms: U22(tt,x45:S,x46:S)->[], tt->[1]) 0.008/0.008 (rule: U221(tt) -> tt, id: 36, possubterms: U221(tt)->[], tt->[1]) 0.008/0.008 (rule: U23(tt,x47:S,x48:S) -> U24(isLNatKind(x48:S),x47:S), id: 37, possubterms: U23(tt,x47:S,x48:S)->[], tt->[1]) 0.008/0.008 (rule: U231(tt,x49:S) -> U232(isLNatKind(x49:S)), id: 38, possubterms: U231(tt,x49:S)->[], tt->[1]) 0.008/0.008 (rule: U232(tt) -> tt, id: 39, possubterms: U232(tt)->[], tt->[1]) 0.008/0.008 (rule: U24(tt,x50:S) -> x50:S, id: 40, possubterms: U24(tt,x50:S)->[], tt->[1]) 0.008/0.008 (rule: U241(tt,x51:S,x52:S) -> U242(isLNatKind(x51:S),x51:S,x52:S), id: 41, possubterms: U241(tt,x51:S,x52:S)->[], tt->[1]) 0.008/0.008 (rule: U242(tt,x53:S,x54:S) -> U243(isLNatKind(x54:S),x53:S,x54:S), id: 42, possubterms: U242(tt,x53:S,x54:S)->[], tt->[1]) 0.008/0.008 (rule: U243(tt,x55:S,x56:S) -> U244(isLNatKind(x56:S),x55:S,x56:S), id: 43, possubterms: U243(tt,x55:S,x56:S)->[], tt->[1]) 0.008/0.008 (rule: U244(tt,x57:S,x58:S) -> U245(isLNat(x57:S),x58:S), id: 44, possubterms: U244(tt,x57:S,x58:S)->[], tt->[1]) 0.008/0.008 (rule: U245(tt,x59:S) -> U246(isLNat(x59:S)), id: 45, possubterms: U245(tt,x59:S)->[], tt->[1]) 0.008/0.008 (rule: U246(tt) -> tt, id: 46, possubterms: U246(tt)->[], tt->[1]) 0.008/0.008 (rule: U251(tt,x60:S,x61:S) -> U252(isNaturalKind(x60:S),x60:S,x61:S), id: 47, possubterms: U251(tt,x60:S,x61:S)->[], tt->[1]) 0.008/0.008 (rule: U252(tt,x62:S,x63:S) -> U253(isLNatKind(x63:S),x62:S,x63:S), id: 48, possubterms: U252(tt,x62:S,x63:S)->[], tt->[1]) 0.008/0.008 (rule: U253(tt,x64:S,x65:S) -> U254(isLNatKind(x65:S),x64:S,x65:S), id: 49, possubterms: U253(tt,x64:S,x65:S)->[], tt->[1]) 0.008/0.008 (rule: U254(tt,x66:S,x67:S) -> U255(isNatural(x66:S),x67:S), id: 50, possubterms: U254(tt,x66:S,x67:S)->[], tt->[1]) 0.008/0.008 (rule: U255(tt,x68:S) -> U256(isLNat(x68:S)), id: 51, possubterms: U255(tt,x68:S)->[], tt->[1]) 0.008/0.008 (rule: U256(tt) -> tt, id: 52, possubterms: U256(tt)->[], tt->[1]) 0.008/0.008 (rule: U261(tt,x69:S) -> U262(isLNatKind(x69:S)), id: 53, possubterms: U261(tt,x69:S)->[], tt->[1]) 0.008/0.008 (rule: U262(tt) -> tt, id: 54, possubterms: U262(tt)->[], tt->[1]) 0.008/0.008 (rule: U271(tt,x70:S) -> U272(isLNatKind(x70:S)), id: 55, possubterms: U271(tt,x70:S)->[], tt->[1]) 0.008/0.008 (rule: U272(tt) -> tt, id: 56, possubterms: U272(tt)->[], tt->[1]) 0.008/0.008 (rule: U281(tt,x71:S) -> U282(isNaturalKind(x71:S),x71:S), id: 57, possubterms: U281(tt,x71:S)->[], tt->[1]) 0.008/0.008 (rule: U282(tt,x72:S) -> cons(x72:S,natsFrom(s(x72:S))), id: 58, possubterms: U282(tt,x72:S)->[], tt->[1]) 0.008/0.008 (rule: U291(tt,x73:S,x74:S) -> U292(isNaturalKind(x73:S),x73:S,x74:S), id: 59, possubterms: U291(tt,x73:S,x74:S)->[], tt->[1]) 0.008/0.008 (rule: U292(tt,x75:S,x76:S) -> U293(isLNat(x76:S),x75:S,x76:S), id: 60, possubterms: U292(tt,x75:S,x76:S)->[], tt->[1]) 0.008/0.008 (rule: U293(tt,x77:S,x78:S) -> U294(isLNatKind(x78:S),x77:S,x78:S), id: 61, possubterms: U293(tt,x77:S,x78:S)->[], tt->[1]) 0.008/0.008 (rule: U294(tt,x79:S,x80:S) -> head(afterNth(x79:S,x80:S)), id: 62, possubterms: U294(tt,x79:S,x80:S)->[], tt->[1]) 0.008/0.008 (rule: U301(tt,x81:S,x82:S) -> U302(isLNatKind(x81:S),x82:S), id: 63, possubterms: U301(tt,x81:S,x82:S)->[], tt->[1]) 0.008/0.008 (rule: U302(tt,x83:S) -> U303(isLNat(x83:S),x83:S), id: 64, possubterms: U302(tt,x83:S)->[], tt->[1]) 0.008/0.008 (rule: U303(tt,x84:S) -> U304(isLNatKind(x84:S),x84:S), id: 65, possubterms: U303(tt,x84:S)->[], tt->[1]) 0.008/0.008 (rule: U304(tt,x85:S) -> x85:S, id: 66, possubterms: U304(tt,x85:S)->[], tt->[1]) 0.008/0.008 (rule: U31(tt,x86:S,x87:S) -> U32(isNaturalKind(x86:S),x86:S,x87:S), id: 67, possubterms: U31(tt,x86:S,x87:S)->[], tt->[1]) 0.008/0.008 (rule: U311(tt,x88:S) -> U312(isLNatKind(x88:S),x88:S), id: 68, possubterms: U311(tt,x88:S)->[], tt->[1]) 0.008/0.008 (rule: U312(tt,x89:S) -> pair(nil,x89:S), id: 69, possubterms: U312(tt,x89:S)->[], tt->[1]) 0.008/0.008 (rule: U32(tt,x90:S,x91:S) -> U33(isLNat(x91:S),x90:S,x91:S), id: 70, possubterms: U32(tt,x90:S,x91:S)->[], tt->[1]) 0.008/0.008 (rule: U321(tt,x92:S,x93:S,x94:S) -> U322(isNaturalKind(x92:S),x92:S,x93:S,x94:S), id: 71, possubterms: U321(tt,x92:S,x93:S,x94:S)->[], tt->[1]) 0.008/0.008 (rule: U322(tt,x95:S,x96:S,x97:S) -> U323(isNatural(x96:S),x95:S,x96:S,x97:S), id: 72, possubterms: U322(tt,x95:S,x96:S,x97:S)->[], tt->[1]) 0.008/0.008 (rule: U323(tt,x98:S,x99:S,x100:S) -> U324(isNaturalKind(x99:S),x98:S,x99:S,x100:S), id: 73, possubterms: U323(tt,x98:S,x99:S,x100:S)->[], tt->[1]) 0.008/0.008 (rule: U324(tt,x101:S,x102:S,x103:S) -> U325(isLNat(x103:S),x101:S,x102:S,x103:S), id: 74, possubterms: U324(tt,x101:S,x102:S,x103:S)->[], tt->[1]) 0.008/0.008 (rule: U325(tt,x104:S,x105:S,x106:S) -> U326(isLNatKind(x106:S),x104:S,x105:S,x106:S), id: 75, possubterms: U325(tt,x104:S,x105:S,x106:S)->[], tt->[1]) 0.008/0.008 (rule: U326(tt,x107:S,x108:S,x109:S) -> U327(splitAt(x107:S,x109:S),x108:S), id: 76, possubterms: U326(tt,x107:S,x108:S,x109:S)->[], tt->[1]) 0.008/0.008 (rule: U327(pair(x111:S,x112:S),x110:S) -> pair(cons(x110:S,x111:S),x112:S), id: 77, possubterms: U327(pair(x111:S,x112:S),x110:S)->[], pair(x111:S,x112:S)->[1]) 0.008/0.008 (rule: U33(tt,x113:S,x114:S) -> U34(isLNatKind(x114:S),x113:S), id: 78, possubterms: U33(tt,x113:S,x114:S)->[], tt->[1]) 0.008/0.008 (rule: U331(tt,x115:S,x116:S) -> U332(isNaturalKind(x115:S),x116:S), id: 79, possubterms: U331(tt,x115:S,x116:S)->[], tt->[1]) 0.008/0.008 (rule: U332(tt,x117:S) -> U333(isLNat(x117:S),x117:S), id: 80, possubterms: U332(tt,x117:S)->[], tt->[1]) 0.008/0.008 (rule: U333(tt,x118:S) -> U334(isLNatKind(x118:S),x118:S), id: 81, possubterms: U333(tt,x118:S)->[], tt->[1]) 0.008/0.008 (rule: U334(tt,x119:S) -> x119:S, id: 82, possubterms: U334(tt,x119:S)->[], tt->[1]) 0.008/0.008 (rule: U34(tt,x120:S) -> x120:S, id: 83, possubterms: U34(tt,x120:S)->[], tt->[1]) 0.008/0.008 (rule: U341(tt,x121:S,x122:S) -> U342(isNaturalKind(x121:S),x121:S,x122:S), id: 84, possubterms: U341(tt,x121:S,x122:S)->[], tt->[1]) 0.008/0.008 (rule: U342(tt,x123:S,x124:S) -> U343(isLNat(x124:S),x123:S,x124:S), id: 85, possubterms: U342(tt,x123:S,x124:S)->[], tt->[1]) 0.008/0.008 (rule: U343(tt,x125:S,x126:S) -> U344(isLNatKind(x126:S),x125:S,x126:S), id: 86, possubterms: U343(tt,x125:S,x126:S)->[], tt->[1]) 0.008/0.008 (rule: U344(tt,x127:S,x128:S) -> fst(splitAt(x127:S,x128:S)), id: 87, possubterms: U344(tt,x127:S,x128:S)->[], tt->[1]) 0.008/0.008 (rule: U41(tt,x129:S,x130:S) -> U42(isNaturalKind(x129:S),x129:S,x130:S), id: 88, possubterms: U41(tt,x129:S,x130:S)->[], tt->[1]) 0.008/0.008 (rule: U42(tt,x131:S,x132:S) -> U43(isLNatKind(x132:S),x131:S,x132:S), id: 89, possubterms: U42(tt,x131:S,x132:S)->[], tt->[1]) 0.008/0.008 (rule: U43(tt,x133:S,x134:S) -> U44(isLNatKind(x134:S),x133:S,x134:S), id: 90, possubterms: U43(tt,x133:S,x134:S)->[], tt->[1]) 0.008/0.008 (rule: U44(tt,x135:S,x136:S) -> U45(isNatural(x135:S),x136:S), id: 91, possubterms: U44(tt,x135:S,x136:S)->[], tt->[1]) 0.008/0.008 (rule: U45(tt,x137:S) -> U46(isLNat(x137:S)), id: 92, possubterms: U45(tt,x137:S)->[], tt->[1]) 0.008/0.008 (rule: U46(tt) -> tt, id: 93, possubterms: U46(tt)->[], tt->[1]) 0.008/0.008 (rule: U51(tt,x138:S,x139:S) -> U52(isNaturalKind(x138:S),x138:S,x139:S), id: 94, possubterms: U51(tt,x138:S,x139:S)->[], tt->[1]) 0.008/0.008 (rule: U52(tt,x140:S,x141:S) -> U53(isLNatKind(x141:S),x140:S,x141:S), id: 95, possubterms: U52(tt,x140:S,x141:S)->[], tt->[1]) 0.008/0.008 (rule: U53(tt,x142:S,x143:S) -> U54(isLNatKind(x143:S),x142:S,x143:S), id: 96, possubterms: U53(tt,x142:S,x143:S)->[], tt->[1]) 0.008/0.008 (rule: U54(tt,x144:S,x145:S) -> U55(isNatural(x144:S),x145:S), id: 97, possubterms: U54(tt,x144:S,x145:S)->[], tt->[1]) 0.008/0.008 (rule: U55(tt,x146:S) -> U56(isLNat(x146:S)), id: 98, possubterms: U55(tt,x146:S)->[], tt->[1]) 0.008/0.008 (rule: U56(tt) -> tt, id: 99, possubterms: U56(tt)->[], tt->[1]) 0.008/0.008 (rule: U61(tt,x147:S) -> U62(isPLNatKind(x147:S),x147:S), id: 100, possubterms: U61(tt,x147:S)->[], tt->[1]) 0.008/0.008 (rule: U62(tt,x148:S) -> U63(isPLNat(x148:S)), id: 101, possubterms: U62(tt,x148:S)->[], tt->[1]) 0.008/0.008 (rule: U63(tt) -> tt, id: 102, possubterms: U63(tt)->[], tt->[1]) 0.008/0.008 (rule: U71(tt,x149:S) -> U72(isNaturalKind(x149:S),x149:S), id: 103, possubterms: U71(tt,x149:S)->[], tt->[1]) 0.008/0.008 (rule: U72(tt,x150:S) -> U73(isNatural(x150:S)), id: 104, possubterms: U72(tt,x150:S)->[], tt->[1]) 0.008/0.008 (rule: U73(tt) -> tt, id: 105, possubterms: U73(tt)->[], tt->[1]) 0.008/0.008 (rule: U81(tt,x151:S) -> U82(isPLNatKind(x151:S),x151:S), id: 106, possubterms: U81(tt,x151:S)->[], tt->[1]) 0.008/0.008 (rule: U82(tt,x152:S) -> U83(isPLNat(x152:S)), id: 107, possubterms: U82(tt,x152:S)->[], tt->[1]) 0.008/0.008 (rule: U83(tt) -> tt, id: 108, possubterms: U83(tt)->[], tt->[1]) 0.008/0.008 (rule: U91(tt,x153:S) -> U92(isLNatKind(x153:S),x153:S), id: 109, possubterms: U91(tt,x153:S)->[], tt->[1]) 0.008/0.008 (rule: U92(tt,x154:S) -> U93(isLNat(x154:S)), id: 110, possubterms: U92(tt,x154:S)->[], tt->[1]) 0.008/0.008 (rule: U93(tt) -> tt, id: 111, possubterms: U93(tt)->[], tt->[1]) 0.008/0.008 (rule: afterNth(x155:S,x156:S) -> U11(isNatural(x155:S),x155:S,x156:S), id: 112, possubterms: afterNth(x155:S,x156:S)->[]) 0.008/0.008 (rule: fst(pair(x157:S,x158:S)) -> U21(isLNat(x157:S),x157:S,x158:S), id: 113, possubterms: fst(pair(x157:S,x158:S))->[], pair(x157:S,x158:S)->[1]) 0.008/0.008 (rule: head(cons(x159:S,x160:S)) -> U31(isNatural(x159:S),x159:S,x160:S), id: 114, possubterms: head(cons(x159:S,x160:S))->[], cons(x159:S,x160:S)->[1]) 0.008/0.008 (rule: isLNat(afterNth(x161:S,x162:S)) -> U41(isNaturalKind(x161:S),x161:S,x162:S), id: 115, possubterms: isLNat(afterNth(x161:S,x162:S))->[], afterNth(x161:S,x162:S)->[1]) 0.008/0.008 (rule: isLNat(fst(x163:S)) -> U61(isPLNatKind(x163:S),x163:S), id: 116, possubterms: isLNat(fst(x163:S))->[], fst(x163:S)->[1]) 0.008/0.008 (rule: isLNat(natsFrom(x164:S)) -> U71(isNaturalKind(x164:S),x164:S), id: 117, possubterms: isLNat(natsFrom(x164:S))->[], natsFrom(x164:S)->[1]) 0.008/0.008 (rule: isLNat(snd(x165:S)) -> U81(isPLNatKind(x165:S),x165:S), id: 118, possubterms: isLNat(snd(x165:S))->[], snd(x165:S)->[1]) 0.008/0.008 (rule: isLNat(tail(x166:S)) -> U91(isLNatKind(x166:S),x166:S), id: 119, possubterms: isLNat(tail(x166:S))->[], tail(x166:S)->[1]) 0.008/0.008 (rule: isLNat(take(x167:S,x168:S)) -> U101(isNaturalKind(x167:S),x167:S,x168:S), id: 120, possubterms: isLNat(take(x167:S,x168:S))->[], take(x167:S,x168:S)->[1]) 0.008/0.008 (rule: isLNat(cons(x169:S,x170:S)) -> U51(isNaturalKind(x169:S),x169:S,x170:S), id: 121, possubterms: isLNat(cons(x169:S,x170:S))->[], cons(x169:S,x170:S)->[1]) 0.008/0.008 (rule: isLNat(nil) -> tt, id: 122, possubterms: isLNat(nil)->[], nil->[1]) 0.008/0.008 (rule: isLNatKind(afterNth(x171:S,x172:S)) -> U111(isNaturalKind(x171:S),x172:S), id: 123, possubterms: isLNatKind(afterNth(x171:S,x172:S))->[], afterNth(x171:S,x172:S)->[1]) 0.008/0.008 (rule: isLNatKind(fst(x173:S)) -> U131(isPLNatKind(x173:S)), id: 124, possubterms: isLNatKind(fst(x173:S))->[], fst(x173:S)->[1]) 0.008/0.008 (rule: isLNatKind(natsFrom(x174:S)) -> U141(isNaturalKind(x174:S)), id: 125, possubterms: isLNatKind(natsFrom(x174:S))->[], natsFrom(x174:S)->[1]) 0.008/0.008 (rule: isLNatKind(snd(x175:S)) -> U151(isPLNatKind(x175:S)), id: 126, possubterms: isLNatKind(snd(x175:S))->[], snd(x175:S)->[1]) 0.008/0.008 (rule: isLNatKind(tail(x176:S)) -> U161(isLNatKind(x176:S)), id: 127, possubterms: isLNatKind(tail(x176:S))->[], tail(x176:S)->[1]) 0.008/0.008 (rule: isLNatKind(take(x177:S,x178:S)) -> U171(isNaturalKind(x177:S),x178:S), id: 128, possubterms: isLNatKind(take(x177:S,x178:S))->[], take(x177:S,x178:S)->[1]) 0.008/0.008 (rule: isLNatKind(cons(x179:S,x180:S)) -> U121(isNaturalKind(x179:S),x180:S), id: 129, possubterms: isLNatKind(cons(x179:S,x180:S))->[], cons(x179:S,x180:S)->[1]) 0.008/0.008 (rule: isLNatKind(nil) -> tt, id: 130, possubterms: isLNatKind(nil)->[], nil->[1]) 0.008/0.008 (rule: isNatural(head(x181:S)) -> U181(isLNatKind(x181:S),x181:S), id: 131, possubterms: isNatural(head(x181:S))->[], head(x181:S)->[1]) 0.008/0.008 (rule: isNatural(sel(x182:S,x183:S)) -> U201(isNaturalKind(x182:S),x182:S,x183:S), id: 132, possubterms: isNatural(sel(x182:S,x183:S))->[], sel(x182:S,x183:S)->[1]) 0.008/0.008 (rule: isNatural(num0) -> tt, id: 133, possubterms: isNatural(num0)->[], num0->[1]) 0.008/0.008 (rule: isNatural(s(x184:S)) -> U191(isNaturalKind(x184:S),x184:S), id: 134, possubterms: isNatural(s(x184:S))->[], s(x184:S)->[1]) 0.008/0.008 (rule: isNaturalKind(head(x185:S)) -> U211(isLNatKind(x185:S)), id: 135, possubterms: isNaturalKind(head(x185:S))->[], head(x185:S)->[1]) 0.008/0.008 (rule: isNaturalKind(sel(x186:S,x187:S)) -> U231(isNaturalKind(x186:S),x187:S), id: 136, possubterms: isNaturalKind(sel(x186:S,x187:S))->[], sel(x186:S,x187:S)->[1]) 0.008/0.008 (rule: isNaturalKind(num0) -> tt, id: 137, possubterms: isNaturalKind(num0)->[], num0->[1]) 0.008/0.008 (rule: isNaturalKind(s(x188:S)) -> U221(isNaturalKind(x188:S)), id: 138, possubterms: isNaturalKind(s(x188:S))->[], s(x188:S)->[1]) 0.008/0.008 (rule: isPLNat(splitAt(x189:S,x190:S)) -> U251(isNaturalKind(x189:S),x189:S,x190:S), id: 139, possubterms: isPLNat(splitAt(x189:S,x190:S))->[], splitAt(x189:S,x190:S)->[1]) 0.008/0.008 (rule: isPLNat(pair(x191:S,x192:S)) -> U241(isLNatKind(x191:S),x191:S,x192:S), id: 140, possubterms: isPLNat(pair(x191:S,x192:S))->[], pair(x191:S,x192:S)->[1]) 0.008/0.008 (rule: isPLNatKind(splitAt(x193:S,x194:S)) -> U271(isNaturalKind(x193:S),x194:S), id: 141, possubterms: isPLNatKind(splitAt(x193:S,x194:S))->[], splitAt(x193:S,x194:S)->[1]) 0.008/0.008 (rule: isPLNatKind(pair(x195:S,x196:S)) -> U261(isLNatKind(x195:S),x196:S), id: 142, possubterms: isPLNatKind(pair(x195:S,x196:S))->[], pair(x195:S,x196:S)->[1]) 0.008/0.008 (rule: natsFrom(x197:S) -> U281(isNatural(x197:S),x197:S), id: 143, possubterms: natsFrom(x197:S)->[]) 0.008/0.008 (rule: sel(x198:S,x199:S) -> U291(isNatural(x198:S),x198:S,x199:S), id: 144, possubterms: sel(x198:S,x199:S)->[]) 0.008/0.008 (rule: snd(pair(x200:S,x201:S)) -> U301(isLNat(x200:S),x200:S,x201:S), id: 145, possubterms: snd(pair(x200:S,x201:S))->[], pair(x200:S,x201:S)->[1]) 0.008/0.008 (rule: splitAt(num0,x202:S) -> U311(isLNat(x202:S),x202:S), id: 146, possubterms: splitAt(num0,x202:S)->[], num0->[1]) 0.008/0.008 (rule: splitAt(s(x203:S),cons(x204:S,x205:S)) -> U321(isNatural(x203:S),x203:S,x204:S,x205:S), id: 147, possubterms: splitAt(s(x203:S),cons(x204:S,x205:S))->[], s(x203:S)->[1], cons(x204:S,x205:S)->[2]) 0.008/0.008 (rule: tail(cons(x206:S,x207:S)) -> U331(isNatural(x206:S),x206:S,x207:S), id: 148, possubterms: tail(cons(x206:S,x207:S))->[], cons(x206:S,x207:S)->[1]) 0.008/0.008 (rule: take(x208:S,x209:S) -> U341(isNatural(x208:S),x208:S,x209:S), id: 149, possubterms: take(x208:S,x209:S)->[]) 0.008/0.008 0.008/0.008 -> Unifications: 0.008/0.008 (R115 unifies with R112 at p: [1], l: isLNat(afterNth(x161:S,x162:S)), lp: afterNth(x161:S,x162:S), sig: {x161:S -> N:S:S,x162:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: U41(isNaturalKind(x161:S),x161:S,x162:S), r': U11(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R116 unifies with R113 at p: [1], l: isLNat(fst(x163:S)), lp: fst(x163:S), sig: {x163:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: U61(isPLNatKind(x163:S),x163:S), r': U21(isLNat(X:S:S),X:S:S,Y:S:S)) 0.008/0.008 (R117 unifies with R143 at p: [1], l: isLNat(natsFrom(x164:S)), lp: natsFrom(x164:S), sig: {x164:S -> N:S:S}, l': natsFrom(N:S:S), r: U71(isNaturalKind(x164:S),x164:S), r': U281(isNatural(N:S:S),N:S:S)) 0.008/0.008 (R118 unifies with R145 at p: [1], l: isLNat(snd(x165:S)), lp: snd(x165:S), sig: {x165:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: U81(isPLNatKind(x165:S),x165:S), r': U301(isLNat(X:S:S),X:S:S,Y:S:S)) 0.008/0.008 (R119 unifies with R148 at p: [1], l: isLNat(tail(x166:S)), lp: tail(x166:S), sig: {x166:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: U91(isLNatKind(x166:S),x166:S), r': U331(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R120 unifies with R149 at p: [1], l: isLNat(take(x167:S,x168:S)), lp: take(x167:S,x168:S), sig: {x167:S -> N:S:S,x168:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: U101(isNaturalKind(x167:S),x167:S,x168:S), r': U341(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R123 unifies with R112 at p: [1], l: isLNatKind(afterNth(x171:S,x172:S)), lp: afterNth(x171:S,x172:S), sig: {x171:S -> N:S:S,x172:S -> XS:S:S}, l': afterNth(N:S:S,XS:S:S), r: U111(isNaturalKind(x171:S),x172:S), r': U11(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R124 unifies with R113 at p: [1], l: isLNatKind(fst(x173:S)), lp: fst(x173:S), sig: {x173:S -> pair(X:S:S,Y:S:S)}, l': fst(pair(X:S:S,Y:S:S)), r: U131(isPLNatKind(x173:S)), r': U21(isLNat(X:S:S),X:S:S,Y:S:S)) 0.008/0.008 (R125 unifies with R143 at p: [1], l: isLNatKind(natsFrom(x174:S)), lp: natsFrom(x174:S), sig: {x174:S -> N:S:S}, l': natsFrom(N:S:S), r: U141(isNaturalKind(x174:S)), r': U281(isNatural(N:S:S),N:S:S)) 0.008/0.008 (R126 unifies with R145 at p: [1], l: isLNatKind(snd(x175:S)), lp: snd(x175:S), sig: {x175:S -> pair(X:S:S,Y:S:S)}, l': snd(pair(X:S:S,Y:S:S)), r: U151(isPLNatKind(x175:S)), r': U301(isLNat(X:S:S),X:S:S,Y:S:S)) 0.008/0.008 (R127 unifies with R148 at p: [1], l: isLNatKind(tail(x176:S)), lp: tail(x176:S), sig: {x176:S -> cons(N:S:S,XS:S:S)}, l': tail(cons(N:S:S,XS:S:S)), r: U161(isLNatKind(x176:S)), r': U331(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R128 unifies with R149 at p: [1], l: isLNatKind(take(x177:S,x178:S)), lp: take(x177:S,x178:S), sig: {x177:S -> N:S:S,x178:S -> XS:S:S}, l': take(N:S:S,XS:S:S), r: U171(isNaturalKind(x177:S),x178:S), r': U341(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R131 unifies with R114 at p: [1], l: isNatural(head(x181:S)), lp: head(x181:S), sig: {x181:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: U181(isLNatKind(x181:S),x181:S), r': U31(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R132 unifies with R144 at p: [1], l: isNatural(sel(x182:S,x183:S)), lp: sel(x182:S,x183:S), sig: {x182:S -> N:S:S,x183:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: U201(isNaturalKind(x182:S),x182:S,x183:S), r': U291(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R135 unifies with R114 at p: [1], l: isNaturalKind(head(x185:S)), lp: head(x185:S), sig: {x185:S -> cons(N:S:S,XS:S:S)}, l': head(cons(N:S:S,XS:S:S)), r: U211(isLNatKind(x185:S)), r': U31(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R136 unifies with R144 at p: [1], l: isNaturalKind(sel(x186:S,x187:S)), lp: sel(x186:S,x187:S), sig: {x186:S -> N:S:S,x187:S -> XS:S:S}, l': sel(N:S:S,XS:S:S), r: U231(isNaturalKind(x186:S),x187:S), r': U291(isNatural(N:S:S),N:S:S,XS:S:S)) 0.008/0.008 (R139 unifies with R146 at p: [1], l: isPLNat(splitAt(x189:S,x190:S)), lp: splitAt(x189:S,x190:S), sig: {x189:S -> num0,x190:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: U251(isNaturalKind(x189:S),x189:S,x190:S), r': U311(isLNat(XS:S:S),XS:S:S)) 0.008/0.008 (R139 unifies with R147 at p: [1], l: isPLNat(splitAt(x189:S,x190:S)), lp: splitAt(x189:S,x190:S), sig: {x189:S -> s(N:S:S),x190:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: U251(isNaturalKind(x189:S),x189:S,x190:S), r': U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S)) 0.008/0.008 (R141 unifies with R146 at p: [1], l: isPLNatKind(splitAt(x193:S,x194:S)), lp: splitAt(x193:S,x194:S), sig: {x193:S -> num0,x194:S -> XS:S:S}, l': splitAt(num0,XS:S:S), r: U271(isNaturalKind(x193:S),x194:S), r': U311(isLNat(XS:S:S),XS:S:S)) 0.008/0.008 (R141 unifies with R147 at p: [1], l: isPLNatKind(splitAt(x193:S,x194:S)), lp: splitAt(x193:S,x194:S), sig: {x193:S -> s(N:S:S),x194:S -> cons(X:S:S,XS:S:S)}, l': splitAt(s(N:S:S),cons(X:S:S,XS:S:S)), r: U271(isNaturalKind(x193:S),x194:S), r': U321(isNatural(N:S:S),N:S:S,X:S:S,XS:S:S)) 0.008/0.008 0.008/0.008 -> Critical pairs info: 0.008/0.008 => Not trivial, Not overlay, NW0, N1 0.008/0.008 => Not trivial, Not overlay, NW0, N2 0.008/0.008 => Not trivial, Not overlay, NW0, N3 0.008/0.008 => Not trivial, Not overlay, NW0, N4 0.008/0.008 => Not trivial, Not overlay, NW0, N5 0.008/0.008 => Not trivial, Not overlay, NW0, N6 0.008/0.008 => Not trivial, Not overlay, NW0, N7 0.008/0.008 => Not trivial, Not overlay, NW0, N8 0.008/0.008 => Not trivial, Not overlay, NW0, N9 0.008/0.008 => Not trivial, Not overlay, NW0, N10 0.008/0.008 => Not trivial, Not overlay, NW0, N11 0.008/0.008 => Not trivial, Not overlay, NW0, N12 0.008/0.008 => Not trivial, Not overlay, NW0, N13 0.008/0.008 => Not trivial, Not overlay, NW0, N14 0.008/0.008 => Not trivial, Not overlay, NW0, N15 0.008/0.008 => Not trivial, Not overlay, NW0, N16 0.008/0.008 => Not trivial, Not overlay, NW0, N17 0.008/0.008 => Not trivial, Not overlay, NW0, N18 0.008/0.008 => Not trivial, Not overlay, NW0, N19 0.008/0.008 => Not trivial, Not overlay, NW0, N20 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 Different Normal CP Terms Processor: 0.008/0.008 => Not trivial, Not overlay, NW0, N1, Normal and not trivial cp 0.008/0.008 0.008/0.008 The problem is not joinable. 0.008/0.008 0.07user 0.00system 0:00.08elapsed 98%CPU (0avgtext+0avgdata 15764maxresident)k 0.008/0.008 16inputs+0outputs (0major+2123minor)pagefaults 0swaps