MAYBE 0.00/0.07 The problem does not contain well-formed TRSs: 0.00/0.07 Strict Trs: 0.00/0.07 { U14(tt()) -> snd(splitAt(N, XS)) 0.00/0.07 , snd(pair(X, Y)) -> U301(isLNat()) 0.00/0.07 , splitAt(0(), XS) -> U311(isLNat()) 0.00/0.07 , splitAt(s(N), cons(X)) -> U321(isNatural()) 0.00/0.07 , U24(tt()) -> X 0.00/0.07 , U282(tt()) -> cons(N) 0.00/0.07 , U294(tt()) -> head(afterNth(N, XS)) 0.00/0.07 , head(cons(N)) -> U31(isNatural()) 0.00/0.07 , afterNth(N, XS) -> U11(isNatural()) 0.00/0.07 , U304(tt()) -> Y 0.00/0.07 , U312(tt()) -> pair(nil(), XS) 0.00/0.07 , U326(tt()) -> U327(splitAt(N, XS)) 0.00/0.07 , U327(pair(YS, ZS)) -> pair(cons(X), ZS) 0.00/0.07 , U334(tt()) -> XS 0.00/0.07 , U34(tt()) -> N 0.00/0.07 , U344(tt()) -> fst(splitAt(N, XS)) 0.00/0.07 , fst(pair(X, Y)) -> U21(isLNat()) 0.00/0.07 , U101(tt()) -> U102(isNaturalKind()) 0.00/0.07 , U102(tt()) -> U103(isLNatKind()) 0.00/0.07 , isNaturalKind() -> tt() 0.00/0.07 , isNaturalKind() -> U211(isLNatKind()) 0.00/0.07 , isNaturalKind() -> U221(isNaturalKind()) 0.00/0.07 , isNaturalKind() -> U231(isNaturalKind()) 0.00/0.07 , U103(tt()) -> U104(isLNatKind()) 0.00/0.07 , isLNatKind() -> tt() 0.00/0.07 , isLNatKind() -> U111(isNaturalKind()) 0.00/0.07 , isLNatKind() -> U121(isNaturalKind()) 0.00/0.07 , isLNatKind() -> U131(isPLNatKind()) 0.00/0.07 , isLNatKind() -> U141(isNaturalKind()) 0.00/0.07 , isLNatKind() -> U151(isPLNatKind()) 0.00/0.07 , isLNatKind() -> U161(isLNatKind()) 0.00/0.07 , isLNatKind() -> U171(isNaturalKind()) 0.00/0.07 , U104(tt()) -> U105(isNatural()) 0.00/0.07 , U105(tt()) -> U106(isLNat()) 0.00/0.07 , isNatural() -> tt() 0.00/0.07 , isNatural() -> U181(isLNatKind()) 0.00/0.07 , isNatural() -> U191(isNaturalKind()) 0.00/0.07 , isNatural() -> U201(isNaturalKind()) 0.00/0.07 , U106(tt()) -> tt() 0.00/0.07 , isLNat() -> tt() 0.00/0.07 , isLNat() -> U101(isNaturalKind()) 0.00/0.07 , isLNat() -> U41(isNaturalKind()) 0.00/0.07 , isLNat() -> U51(isNaturalKind()) 0.00/0.07 , isLNat() -> U61(isPLNatKind()) 0.00/0.07 , isLNat() -> U71(isNaturalKind()) 0.00/0.07 , isLNat() -> U81(isPLNatKind()) 0.00/0.07 , isLNat() -> U91(isLNatKind()) 0.00/0.07 , U11(tt()) -> U12(isNaturalKind()) 0.00/0.07 , U12(tt()) -> U13(isLNat()) 0.00/0.07 , U111(tt()) -> U112(isLNatKind()) 0.00/0.07 , U112(tt()) -> tt() 0.00/0.07 , U13(tt()) -> U14(isLNatKind()) 0.00/0.07 , U121(tt()) -> U122(isLNatKind()) 0.00/0.07 , U122(tt()) -> tt() 0.00/0.07 , U131(tt()) -> tt() 0.00/0.07 , U141(tt()) -> tt() 0.00/0.07 , U151(tt()) -> tt() 0.00/0.07 , U161(tt()) -> tt() 0.00/0.07 , U171(tt()) -> U172(isLNatKind()) 0.00/0.07 , U172(tt()) -> tt() 0.00/0.07 , U181(tt()) -> U182(isLNatKind()) 0.00/0.07 , U182(tt()) -> U183(isLNat()) 0.00/0.07 , U183(tt()) -> tt() 0.00/0.07 , U191(tt()) -> U192(isNaturalKind()) 0.00/0.07 , U192(tt()) -> U193(isNatural()) 0.00/0.07 , U193(tt()) -> tt() 0.00/0.07 , U201(tt()) -> U202(isNaturalKind()) 0.00/0.07 , U202(tt()) -> U203(isLNatKind()) 0.00/0.07 , U203(tt()) -> U204(isLNatKind()) 0.00/0.07 , U204(tt()) -> U205(isNatural()) 0.00/0.07 , U205(tt()) -> U206(isLNat()) 0.00/0.07 , U206(tt()) -> tt() 0.00/0.07 , U21(tt()) -> U22(isLNatKind()) 0.00/0.07 , U22(tt()) -> U23(isLNat()) 0.00/0.07 , U211(tt()) -> tt() 0.00/0.08 , U23(tt()) -> U24(isLNatKind()) 0.00/0.08 , U221(tt()) -> tt() 0.00/0.08 , U231(tt()) -> U232(isLNatKind()) 0.00/0.08 , U232(tt()) -> tt() 0.00/0.08 , U241(tt()) -> U242(isLNatKind()) 0.00/0.08 , U242(tt()) -> U243(isLNatKind()) 0.00/0.08 , U243(tt()) -> U244(isLNatKind()) 0.00/0.08 , U244(tt()) -> U245(isLNat()) 0.00/0.08 , U245(tt()) -> U246(isLNat()) 0.00/0.08 , U246(tt()) -> tt() 0.00/0.08 , U251(tt()) -> U252(isNaturalKind()) 0.00/0.08 , U252(tt()) -> U253(isLNatKind()) 0.00/0.08 , U253(tt()) -> U254(isLNatKind()) 0.00/0.08 , U254(tt()) -> U255(isNatural()) 0.00/0.08 , U255(tt()) -> U256(isLNat()) 0.00/0.08 , U256(tt()) -> tt() 0.00/0.08 , U261(tt()) -> U262(isLNatKind()) 0.00/0.08 , U262(tt()) -> tt() 0.00/0.08 , U271(tt()) -> U272(isLNatKind()) 0.00/0.08 , U272(tt()) -> tt() 0.00/0.08 , U281(tt()) -> U282(isNaturalKind()) 0.00/0.08 , U291(tt()) -> U292(isNaturalKind()) 0.00/0.08 , U292(tt()) -> U293(isLNat()) 0.00/0.08 , U293(tt()) -> U294(isLNatKind()) 0.00/0.08 , U301(tt()) -> U302(isLNatKind()) 0.00/0.08 , U302(tt()) -> U303(isLNat()) 0.00/0.08 , U303(tt()) -> U304(isLNatKind()) 0.00/0.08 , U31(tt()) -> U32(isNaturalKind()) 0.00/0.08 , U32(tt()) -> U33(isLNat()) 0.00/0.08 , U311(tt()) -> U312(isLNatKind()) 0.00/0.08 , U33(tt()) -> U34(isLNatKind()) 0.00/0.08 , U321(tt()) -> U322(isNaturalKind()) 0.00/0.08 , U322(tt()) -> U323(isNatural()) 0.00/0.08 , U323(tt()) -> U324(isNaturalKind()) 0.00/0.08 , U324(tt()) -> U325(isLNat()) 0.00/0.08 , U325(tt()) -> U326(isLNatKind()) 0.00/0.08 , U331(tt()) -> U332(isNaturalKind()) 0.00/0.08 , U332(tt()) -> U333(isLNat()) 0.00/0.08 , U333(tt()) -> U334(isLNatKind()) 0.00/0.08 , U341(tt()) -> U342(isNaturalKind()) 0.00/0.08 , U342(tt()) -> U343(isLNat()) 0.00/0.08 , U343(tt()) -> U344(isLNatKind()) 0.00/0.08 , U41(tt()) -> U42(isNaturalKind()) 0.00/0.08 , U42(tt()) -> U43(isLNatKind()) 0.00/0.08 , U43(tt()) -> U44(isLNatKind()) 0.00/0.08 , U44(tt()) -> U45(isNatural()) 0.00/0.08 , U45(tt()) -> U46(isLNat()) 0.00/0.08 , U46(tt()) -> tt() 0.00/0.08 , U51(tt()) -> U52(isNaturalKind()) 0.00/0.08 , U52(tt()) -> U53(isLNatKind()) 0.00/0.08 , U53(tt()) -> U54(isLNatKind()) 0.00/0.08 , U54(tt()) -> U55(isNatural()) 0.00/0.08 , U55(tt()) -> U56(isLNat()) 0.00/0.08 , U56(tt()) -> tt() 0.00/0.08 , U61(tt()) -> U62(isPLNatKind()) 0.00/0.08 , U62(tt()) -> U63(isPLNat()) 0.00/0.08 , isPLNatKind() -> U261(isLNatKind()) 0.00/0.08 , isPLNatKind() -> U271(isNaturalKind()) 0.00/0.08 , U63(tt()) -> tt() 0.00/0.08 , isPLNat() -> U241(isLNatKind()) 0.00/0.08 , isPLNat() -> U251(isNaturalKind()) 0.00/0.08 , U71(tt()) -> U72(isNaturalKind()) 0.00/0.08 , U72(tt()) -> U73(isNatural()) 0.00/0.08 , U73(tt()) -> tt() 0.00/0.08 , U81(tt()) -> U82(isPLNatKind()) 0.00/0.08 , U82(tt()) -> U83(isPLNat()) 0.00/0.08 , U83(tt()) -> tt() 0.00/0.08 , U91(tt()) -> U92(isLNatKind()) 0.00/0.08 , U92(tt()) -> U93(isLNat()) 0.00/0.08 , U93(tt()) -> tt() 0.00/0.08 , natsFrom(N) -> U281(isNatural()) 0.00/0.08 , sel(N, XS) -> U291(isNatural()) 0.00/0.08 , tail(cons(N)) -> U331(isNatural()) 0.00/0.08 , take(N, XS) -> U341(isNatural()) } 0.00/0.08 StartTerms: basic terms 0.00/0.08 Strategy: none 0.00/0.08 EOF