MAYBE
0.00/0.04	 The problem does not contain well-formed TRSs:
0.00/0.04	   Strict Trs:
0.00/0.04	     { U11(tt()) -> snd(splitAt(N, XS))
0.00/0.04	     , snd(pair(X, Y)) -> U181(and(and(isLNat())))
0.00/0.04	     , splitAt(0(), XS) -> U191(and(isLNat()))
0.00/0.04	     , splitAt(s(N), cons(X)) -> U201(and(and(isNatural())))
0.00/0.04	     , U161(tt()) -> cons(N)
0.00/0.04	     , U171(tt()) -> head(afterNth(N, XS))
0.00/0.04	     , head(cons(N)) -> U31(and(and(isNatural())))
0.00/0.04	     , afterNth(N, XS) -> U11(and(and(isNatural())))
0.00/0.04	     , U181(tt()) -> Y
0.00/0.04	     , U191(tt()) -> pair(nil(), XS)
0.00/0.04	     , U201(tt()) -> U202(splitAt(N, XS))
0.00/0.04	     , U202(pair(YS, ZS)) -> pair(cons(X), ZS)
0.00/0.04	     , U21(tt()) -> X
0.00/0.04	     , U211(tt()) -> XS
0.00/0.04	     , U221(tt()) -> fst(splitAt(N, XS))
0.00/0.04	     , fst(pair(X, Y)) -> U21(and(and(isLNat())))
0.00/0.04	     , U31(tt()) -> N
0.00/0.04	     , and(tt()) -> X
0.00/0.04	     , U101(tt()) -> U102(isNatural())
0.00/0.04	     , U102(tt()) -> U103(isLNat())
0.00/0.04	     , isNatural() -> tt()
0.00/0.04	     , isNatural() -> U111(isLNatKind())
0.00/0.04	     , isNatural() -> U121(isNaturalKind())
0.00/0.04	     , isNatural() -> U131(and(isNaturalKind()))
0.00/0.04	     , U103(tt()) -> tt()
0.00/0.04	     , isLNat() -> tt()
0.00/0.04	     , isLNat() -> U101(and(isNaturalKind()))
0.00/0.04	     , isLNat() -> U41(and(isNaturalKind()))
0.00/0.04	     , isLNat() -> U51(and(isNaturalKind()))
0.00/0.04	     , isLNat() -> U61(isPLNatKind())
0.00/0.04	     , isLNat() -> U71(isNaturalKind())
0.00/0.04	     , isLNat() -> U81(isPLNatKind())
0.00/0.04	     , isLNat() -> U91(isLNatKind())
0.00/0.04	     , U111(tt()) -> U112(isLNat())
0.00/0.04	     , U112(tt()) -> tt()
0.00/0.04	     , U121(tt()) -> U122(isNatural())
0.00/0.04	     , U122(tt()) -> tt()
0.00/0.04	     , U131(tt()) -> U132(isNatural())
0.00/0.04	     , U132(tt()) -> U133(isLNat())
0.00/0.04	     , U133(tt()) -> tt()
0.00/0.04	     , U141(tt()) -> U142(isLNat())
0.00/0.04	     , U142(tt()) -> U143(isLNat())
0.00/0.04	     , U143(tt()) -> tt()
0.00/0.04	     , U151(tt()) -> U152(isNatural())
0.00/0.04	     , U152(tt()) -> U153(isLNat())
0.00/0.04	     , U153(tt()) -> tt()
0.00/0.04	     , U41(tt()) -> U42(isNatural())
0.00/0.04	     , U42(tt()) -> U43(isLNat())
0.00/0.04	     , U43(tt()) -> tt()
0.00/0.04	     , U51(tt()) -> U52(isNatural())
0.00/0.04	     , U52(tt()) -> U53(isLNat())
0.00/0.04	     , U53(tt()) -> tt()
0.00/0.04	     , U61(tt()) -> U62(isPLNat())
0.00/0.04	     , U62(tt()) -> tt()
0.00/0.04	     , isPLNat() -> U141(and(isLNatKind()))
0.00/0.04	     , isPLNat() -> U151(and(isNaturalKind()))
0.00/0.04	     , U71(tt()) -> U72(isNatural())
0.00/0.04	     , U72(tt()) -> tt()
0.00/0.04	     , U81(tt()) -> U82(isPLNat())
0.00/0.04	     , U82(tt()) -> tt()
0.00/0.04	     , U91(tt()) -> U92(isLNat())
0.00/0.04	     , U92(tt()) -> tt()
0.00/0.04	     , isNaturalKind() -> tt()
0.00/0.04	     , isNaturalKind() -> and(isNaturalKind())
0.00/0.04	     , isNaturalKind() -> isNaturalKind()
0.00/0.04	     , isNaturalKind() -> isLNatKind()
0.00/0.04	     , isPLNatKind() -> and(isNaturalKind())
0.00/0.04	     , isPLNatKind() -> and(isLNatKind())
0.00/0.04	     , isLNatKind() -> tt()
0.00/0.04	     , isLNatKind() -> and(isNaturalKind())
0.00/0.04	     , isLNatKind() -> isNaturalKind()
0.00/0.04	     , isLNatKind() -> isPLNatKind()
0.00/0.04	     , isLNatKind() -> isLNatKind()
0.00/0.04	     , natsFrom(N) -> U161(and(isNatural()))
0.00/0.04	     , sel(N, XS) -> U171(and(and(isNatural())))
0.00/0.04	     , tail(cons(N)) -> U211(and(and(isNatural())))
0.00/0.04	     , take(N, XS) -> U221(and(and(isNatural()))) }
0.00/0.04	   StartTerms: basic terms
0.00/0.04	   Strategy: none
0.00/0.04	EOF