MAYBE 0.00/0.03 The problem does not contain well-formed TRSs: 0.00/0.03 Strict Trs: 0.00/0.03 { U12(tt()) -> snd(splitAt(N, XS)) 0.00/0.03 , snd(pair(X, Y)) -> U181(isLNat()) 0.00/0.03 , splitAt(0(), XS) -> U191(isLNat()) 0.00/0.03 , splitAt(s(N), cons(X)) -> U201(isNatural()) 0.00/0.03 , U161(tt()) -> cons(N) 0.00/0.03 , U172(tt()) -> head(afterNth(N, XS)) 0.00/0.03 , head(cons(N)) -> U31(isNatural()) 0.00/0.03 , afterNth(N, XS) -> U11(isNatural()) 0.00/0.03 , U182(tt()) -> Y 0.00/0.03 , U191(tt()) -> pair(nil(), XS) 0.00/0.03 , U203(tt()) -> U204(splitAt(N, XS)) 0.00/0.03 , U204(pair(YS, ZS)) -> pair(cons(X), ZS) 0.00/0.03 , U212(tt()) -> XS 0.00/0.03 , U22(tt()) -> X 0.00/0.03 , U222(tt()) -> fst(splitAt(N, XS)) 0.00/0.03 , fst(pair(X, Y)) -> U21(isLNat()) 0.00/0.03 , U32(tt()) -> N 0.00/0.03 , U101(tt()) -> U102(isLNat()) 0.00/0.03 , U102(tt()) -> tt() 0.00/0.03 , isLNat() -> tt() 0.00/0.03 , isLNat() -> U101(isNatural()) 0.00/0.03 , isLNat() -> U41(isNatural()) 0.00/0.03 , isLNat() -> U51(isNatural()) 0.00/0.03 , isLNat() -> U61(isPLNat()) 0.00/0.03 , isLNat() -> U71(isNatural()) 0.00/0.03 , isLNat() -> U81(isPLNat()) 0.00/0.03 , isLNat() -> U91(isLNat()) 0.00/0.03 , U11(tt()) -> U12(isLNat()) 0.00/0.03 , U111(tt()) -> tt() 0.00/0.03 , U121(tt()) -> tt() 0.00/0.03 , U131(tt()) -> U132(isLNat()) 0.00/0.03 , U132(tt()) -> tt() 0.00/0.04 , U141(tt()) -> U142(isLNat()) 0.00/0.04 , U142(tt()) -> tt() 0.00/0.04 , U151(tt()) -> U152(isLNat()) 0.00/0.04 , U152(tt()) -> tt() 0.00/0.04 , U171(tt()) -> U172(isLNat()) 0.00/0.04 , U181(tt()) -> U182(isLNat()) 0.00/0.04 , U201(tt()) -> U202(isNatural()) 0.00/0.04 , U202(tt()) -> U203(isLNat()) 0.00/0.04 , isNatural() -> tt() 0.00/0.04 , isNatural() -> U111(isLNat()) 0.00/0.04 , isNatural() -> U121(isNatural()) 0.00/0.04 , isNatural() -> U131(isNatural()) 0.00/0.04 , U21(tt()) -> U22(isLNat()) 0.00/0.04 , U211(tt()) -> U212(isLNat()) 0.00/0.04 , U221(tt()) -> U222(isLNat()) 0.00/0.04 , U31(tt()) -> U32(isLNat()) 0.00/0.04 , U41(tt()) -> U42(isLNat()) 0.00/0.04 , U42(tt()) -> tt() 0.00/0.04 , U51(tt()) -> U52(isLNat()) 0.00/0.04 , U52(tt()) -> tt() 0.00/0.04 , U61(tt()) -> tt() 0.00/0.04 , U71(tt()) -> tt() 0.00/0.04 , U81(tt()) -> tt() 0.00/0.04 , U91(tt()) -> tt() 0.00/0.04 , isPLNat() -> U141(isLNat()) 0.00/0.04 , isPLNat() -> U151(isNatural()) 0.00/0.04 , natsFrom(N) -> U161(isNatural()) 0.00/0.04 , sel(N, XS) -> U171(isNatural()) 0.00/0.04 , tail(cons(N)) -> U211(isNatural()) 0.00/0.04 , take(N, XS) -> U221(isNatural()) } 0.00/0.04 StartTerms: all 0.00/0.04 Strategy: none 0.00/0.04 EOF