MAYBE 1045.52/297.32 MAYBE 1045.52/297.32 1045.52/297.32 We are left with following problem, upon which TcT provides the 1045.52/297.32 certificate MAYBE. 1045.52/297.32 1045.52/297.32 Strict Trs: 1045.52/297.32 { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U102(tt(), V2) -> U103(isLNat(activate(V2))) 1045.52/297.32 , isNatural(X) -> n__isNatural(X) 1045.52/297.32 , isNatural(n__s(V1)) -> 1045.52/297.32 U121(isNaturalKind(activate(V1)), activate(V1)) 1045.52/297.32 , isNatural(n__0()) -> tt() 1045.52/297.32 , isNatural(n__head(V1)) -> 1045.52/297.32 U111(isLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isNatural(n__sel(V1, V2)) -> 1045.52/297.32 U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , activate(X) -> X 1045.52/297.32 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 1045.52/297.32 , activate(n__s(X)) -> s(activate(X)) 1045.52/297.32 , activate(n__isNaturalKind(X)) -> isNaturalKind(X) 1045.52/297.32 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1045.52/297.32 , activate(n__isLNat(X)) -> isLNat(X) 1045.52/297.32 , activate(n__isLNatKind(X)) -> isLNatKind(X) 1045.52/297.32 , activate(n__nil()) -> nil() 1045.52/297.32 , activate(n__afterNth(X1, X2)) -> 1045.52/297.32 afterNth(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1045.52/297.32 , activate(n__fst(X)) -> fst(activate(X)) 1045.52/297.32 , activate(n__snd(X)) -> snd(activate(X)) 1045.52/297.32 , activate(n__tail(X)) -> tail(activate(X)) 1045.52/297.32 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__0()) -> 0() 1045.52/297.32 , activate(n__head(X)) -> head(activate(X)) 1045.52/297.32 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__splitAt(X1, X2)) -> 1045.52/297.32 splitAt(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__isNatural(X)) -> isNatural(X) 1045.52/297.32 , U103(tt()) -> tt() 1045.52/297.32 , isLNat(X) -> n__isLNat(X) 1045.52/297.32 , isLNat(n__natsFrom(V1)) -> 1045.52/297.32 U71(isNaturalKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__nil()) -> tt() 1045.52/297.32 , isLNat(n__afterNth(V1, V2)) -> 1045.52/297.32 U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isLNat(n__cons(V1, V2)) -> 1045.52/297.32 U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isLNat(n__fst(V1)) -> 1045.52/297.32 U61(isPLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__snd(V1)) -> 1045.52/297.32 U81(isPLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__tail(V1)) -> 1045.52/297.32 U91(isLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__take(V1, V2)) -> 1045.52/297.32 U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 1045.52/297.32 , snd(X) -> n__snd(X) 1045.52/297.32 , snd(pair(X, Y)) -> 1045.52/297.32 U181(and(and(isLNat(X), n__isLNatKind(X)), 1045.52/297.32 n__and(n__isLNat(Y), n__isLNatKind(Y))), 1045.52/297.32 Y) 1045.52/297.32 , splitAt(X1, X2) -> n__splitAt(X1, X2) 1045.52/297.32 , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) 1045.52/297.32 , splitAt(s(N), cons(X, XS)) -> 1045.52/297.32 U201(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), 1045.52/297.32 N, 1045.52/297.32 X, 1045.52/297.32 activate(XS)) 1045.52/297.32 , U111(tt(), V1) -> U112(isLNat(activate(V1))) 1045.52/297.32 , U112(tt()) -> tt() 1045.52/297.32 , U121(tt(), V1) -> U122(isNatural(activate(V1))) 1045.52/297.32 , U122(tt()) -> tt() 1045.52/297.32 , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U132(tt(), V2) -> U133(isLNat(activate(V2))) 1045.52/297.32 , U133(tt()) -> tt() 1045.52/297.32 , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) 1045.52/297.32 , U142(tt(), V2) -> U143(isLNat(activate(V2))) 1045.52/297.32 , U143(tt()) -> tt() 1045.52/297.32 , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U152(tt(), V2) -> U153(isLNat(activate(V2))) 1045.52/297.32 , U153(tt()) -> tt() 1045.52/297.32 , U161(tt(), N) -> 1045.52/297.32 cons(activate(N), n__natsFrom(n__s(activate(N)))) 1045.52/297.32 , cons(X1, X2) -> n__cons(X1, X2) 1045.52/297.32 , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 1045.52/297.32 , head(X) -> n__head(X) 1045.52/297.32 , head(cons(N, XS)) -> 1045.52/297.32 U31(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), 1045.52/297.32 N) 1045.52/297.32 , afterNth(N, XS) -> 1045.52/297.32 U11(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , afterNth(X1, X2) -> n__afterNth(X1, X2) 1045.52/297.32 , U181(tt(), Y) -> activate(Y) 1045.52/297.32 , U191(tt(), XS) -> pair(nil(), activate(XS)) 1045.52/297.32 , pair(X1, X2) -> n__pair(X1, X2) 1045.52/297.32 , nil() -> n__nil() 1045.52/297.32 , U201(tt(), N, X, XS) -> 1045.52/297.32 U202(splitAt(activate(N), activate(XS)), activate(X)) 1045.52/297.32 , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 1045.52/297.32 , U21(tt(), X) -> activate(X) 1045.52/297.32 , U211(tt(), XS) -> activate(XS) 1045.52/297.32 , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 1045.52/297.32 , fst(X) -> n__fst(X) 1045.52/297.32 , fst(pair(X, Y)) -> 1045.52/297.32 U21(and(and(isLNat(X), n__isLNatKind(X)), 1045.52/297.32 n__and(n__isLNat(Y), n__isLNatKind(Y))), 1045.52/297.32 X) 1045.52/297.32 , U31(tt(), N) -> activate(N) 1045.52/297.32 , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U42(tt(), V2) -> U43(isLNat(activate(V2))) 1045.52/297.32 , U43(tt()) -> tt() 1045.52/297.32 , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U52(tt(), V2) -> U53(isLNat(activate(V2))) 1045.52/297.32 , U53(tt()) -> tt() 1045.52/297.32 , U61(tt(), V1) -> U62(isPLNat(activate(V1))) 1045.52/297.32 , U62(tt()) -> tt() 1045.52/297.32 , isPLNat(n__pair(V1, V2)) -> 1045.52/297.32 U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isPLNat(n__splitAt(V1, V2)) -> 1045.52/297.32 U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , U71(tt(), V1) -> U72(isNatural(activate(V1))) 1045.52/297.32 , U72(tt()) -> tt() 1045.52/297.32 , U81(tt(), V1) -> U82(isPLNat(activate(V1))) 1045.52/297.32 , U82(tt()) -> tt() 1045.52/297.32 , U91(tt(), V1) -> U92(isLNat(activate(V1))) 1045.52/297.32 , U92(tt()) -> tt() 1045.52/297.32 , and(X1, X2) -> n__and(X1, X2) 1045.52/297.32 , and(tt(), X) -> activate(X) 1045.52/297.32 , isNaturalKind(X) -> n__isNaturalKind(X) 1045.52/297.32 , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) 1045.52/297.32 , isNaturalKind(n__0()) -> tt() 1045.52/297.32 , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) 1045.52/297.32 , isNaturalKind(n__sel(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isPLNatKind(n__pair(V1, V2)) -> 1045.52/297.32 and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isPLNatKind(n__splitAt(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(X) -> n__isLNatKind(X) 1045.52/297.32 , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__nil()) -> tt() 1045.52/297.32 , isLNatKind(n__afterNth(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(n__cons(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__take(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) 1045.52/297.32 , natsFrom(X) -> n__natsFrom(X) 1045.52/297.32 , sel(N, XS) -> 1045.52/297.32 U171(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , sel(X1, X2) -> n__sel(X1, X2) 1045.52/297.32 , 0() -> n__0() 1045.52/297.32 , s(X) -> n__s(X) 1045.52/297.32 , tail(X) -> n__tail(X) 1045.52/297.32 , tail(cons(N, XS)) -> 1045.52/297.32 U211(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), 1045.52/297.32 activate(XS)) 1045.52/297.32 , take(N, XS) -> 1045.52/297.32 U221(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , take(X1, X2) -> n__take(X1, X2) } 1045.52/297.32 Obligation: 1045.52/297.32 innermost runtime complexity 1045.52/297.32 Answer: 1045.52/297.32 MAYBE 1045.52/297.32 1045.52/297.32 Arguments of following rules are not normal-forms: 1045.52/297.32 1045.52/297.32 { snd(pair(X, Y)) -> 1045.52/297.32 U181(and(and(isLNat(X), n__isLNatKind(X)), 1045.52/297.32 n__and(n__isLNat(Y), n__isLNatKind(Y))), 1045.52/297.32 Y) 1045.52/297.32 , splitAt(0(), XS) -> U191(and(isLNat(XS), n__isLNatKind(XS)), XS) 1045.52/297.32 , splitAt(s(N), cons(X, XS)) -> 1045.52/297.32 U201(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__and(n__isNatural(X), n__isNaturalKind(X)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS))))), 1045.52/297.32 N, 1045.52/297.32 X, 1045.52/297.32 activate(XS)) 1045.52/297.32 , head(cons(N, XS)) -> 1045.52/297.32 U31(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), 1045.52/297.32 N) 1045.52/297.32 , U202(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS) 1045.52/297.32 , fst(pair(X, Y)) -> 1045.52/297.32 U21(and(and(isLNat(X), n__isLNatKind(X)), 1045.52/297.32 n__and(n__isLNat(Y), n__isLNatKind(Y))), 1045.52/297.32 X) 1045.52/297.32 , tail(cons(N, XS)) -> 1045.52/297.32 U211(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(activate(XS)), n__isLNatKind(activate(XS)))), 1045.52/297.32 activate(XS)) } 1045.52/297.32 1045.52/297.32 All above mentioned rules can be savely removed. 1045.52/297.32 1045.52/297.32 We are left with following problem, upon which TcT provides the 1045.52/297.32 certificate MAYBE. 1045.52/297.32 1045.52/297.32 Strict Trs: 1045.52/297.32 { U101(tt(), V1, V2) -> U102(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U102(tt(), V2) -> U103(isLNat(activate(V2))) 1045.52/297.32 , isNatural(X) -> n__isNatural(X) 1045.52/297.32 , isNatural(n__s(V1)) -> 1045.52/297.32 U121(isNaturalKind(activate(V1)), activate(V1)) 1045.52/297.32 , isNatural(n__0()) -> tt() 1045.52/297.32 , isNatural(n__head(V1)) -> 1045.52/297.32 U111(isLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isNatural(n__sel(V1, V2)) -> 1045.52/297.32 U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , activate(X) -> X 1045.52/297.32 , activate(n__natsFrom(X)) -> natsFrom(activate(X)) 1045.52/297.32 , activate(n__s(X)) -> s(activate(X)) 1045.52/297.32 , activate(n__isNaturalKind(X)) -> isNaturalKind(X) 1045.52/297.32 , activate(n__and(X1, X2)) -> and(activate(X1), X2) 1045.52/297.32 , activate(n__isLNat(X)) -> isLNat(X) 1045.52/297.32 , activate(n__isLNatKind(X)) -> isLNatKind(X) 1045.52/297.32 , activate(n__nil()) -> nil() 1045.52/297.32 , activate(n__afterNth(X1, X2)) -> 1045.52/297.32 afterNth(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__cons(X1, X2)) -> cons(activate(X1), X2) 1045.52/297.32 , activate(n__fst(X)) -> fst(activate(X)) 1045.52/297.32 , activate(n__snd(X)) -> snd(activate(X)) 1045.52/297.32 , activate(n__tail(X)) -> tail(activate(X)) 1045.52/297.32 , activate(n__take(X1, X2)) -> take(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__0()) -> 0() 1045.52/297.32 , activate(n__head(X)) -> head(activate(X)) 1045.52/297.32 , activate(n__sel(X1, X2)) -> sel(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__pair(X1, X2)) -> pair(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__splitAt(X1, X2)) -> 1045.52/297.32 splitAt(activate(X1), activate(X2)) 1045.52/297.32 , activate(n__isNatural(X)) -> isNatural(X) 1045.52/297.32 , U103(tt()) -> tt() 1045.52/297.32 , isLNat(X) -> n__isLNat(X) 1045.52/297.32 , isLNat(n__natsFrom(V1)) -> 1045.52/297.32 U71(isNaturalKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__nil()) -> tt() 1045.52/297.32 , isLNat(n__afterNth(V1, V2)) -> 1045.52/297.32 U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isLNat(n__cons(V1, V2)) -> 1045.52/297.32 U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isLNat(n__fst(V1)) -> 1045.52/297.32 U61(isPLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__snd(V1)) -> 1045.52/297.32 U81(isPLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__tail(V1)) -> 1045.52/297.32 U91(isLNatKind(activate(V1)), activate(V1)) 1045.52/297.32 , isLNat(n__take(V1, V2)) -> 1045.52/297.32 U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))) 1045.52/297.32 , snd(X) -> n__snd(X) 1045.52/297.32 , splitAt(X1, X2) -> n__splitAt(X1, X2) 1045.52/297.32 , U111(tt(), V1) -> U112(isLNat(activate(V1))) 1045.52/297.32 , U112(tt()) -> tt() 1045.52/297.32 , U121(tt(), V1) -> U122(isNatural(activate(V1))) 1045.52/297.32 , U122(tt()) -> tt() 1045.52/297.32 , U131(tt(), V1, V2) -> U132(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U132(tt(), V2) -> U133(isLNat(activate(V2))) 1045.52/297.32 , U133(tt()) -> tt() 1045.52/297.32 , U141(tt(), V1, V2) -> U142(isLNat(activate(V1)), activate(V2)) 1045.52/297.32 , U142(tt(), V2) -> U143(isLNat(activate(V2))) 1045.52/297.32 , U143(tt()) -> tt() 1045.52/297.32 , U151(tt(), V1, V2) -> U152(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U152(tt(), V2) -> U153(isLNat(activate(V2))) 1045.52/297.32 , U153(tt()) -> tt() 1045.52/297.32 , U161(tt(), N) -> 1045.52/297.32 cons(activate(N), n__natsFrom(n__s(activate(N)))) 1045.52/297.32 , cons(X1, X2) -> n__cons(X1, X2) 1045.52/297.32 , U171(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))) 1045.52/297.32 , head(X) -> n__head(X) 1045.52/297.32 , afterNth(N, XS) -> 1045.52/297.32 U11(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , afterNth(X1, X2) -> n__afterNth(X1, X2) 1045.52/297.32 , U181(tt(), Y) -> activate(Y) 1045.52/297.32 , U191(tt(), XS) -> pair(nil(), activate(XS)) 1045.52/297.32 , pair(X1, X2) -> n__pair(X1, X2) 1045.52/297.32 , nil() -> n__nil() 1045.52/297.32 , U201(tt(), N, X, XS) -> 1045.52/297.32 U202(splitAt(activate(N), activate(XS)), activate(X)) 1045.52/297.32 , U21(tt(), X) -> activate(X) 1045.52/297.32 , U211(tt(), XS) -> activate(XS) 1045.52/297.32 , U221(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))) 1045.52/297.32 , fst(X) -> n__fst(X) 1045.52/297.32 , U31(tt(), N) -> activate(N) 1045.52/297.32 , U41(tt(), V1, V2) -> U42(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U42(tt(), V2) -> U43(isLNat(activate(V2))) 1045.52/297.32 , U43(tt()) -> tt() 1045.52/297.32 , U51(tt(), V1, V2) -> U52(isNatural(activate(V1)), activate(V2)) 1045.52/297.32 , U52(tt(), V2) -> U53(isLNat(activate(V2))) 1045.52/297.32 , U53(tt()) -> tt() 1045.52/297.32 , U61(tt(), V1) -> U62(isPLNat(activate(V1))) 1045.52/297.32 , U62(tt()) -> tt() 1045.52/297.32 , isPLNat(n__pair(V1, V2)) -> 1045.52/297.32 U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , isPLNat(n__splitAt(V1, V2)) -> 1045.52/297.32 U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 1045.52/297.32 activate(V1), 1045.52/297.32 activate(V2)) 1045.52/297.32 , U71(tt(), V1) -> U72(isNatural(activate(V1))) 1045.52/297.32 , U72(tt()) -> tt() 1045.52/297.32 , U81(tt(), V1) -> U82(isPLNat(activate(V1))) 1045.52/297.32 , U82(tt()) -> tt() 1045.52/297.32 , U91(tt(), V1) -> U92(isLNat(activate(V1))) 1045.52/297.32 , U92(tt()) -> tt() 1045.52/297.32 , and(X1, X2) -> n__and(X1, X2) 1045.52/297.32 , and(tt(), X) -> activate(X) 1045.52/297.32 , isNaturalKind(X) -> n__isNaturalKind(X) 1045.52/297.32 , isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) 1045.52/297.32 , isNaturalKind(n__0()) -> tt() 1045.52/297.32 , isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) 1045.52/297.32 , isNaturalKind(n__sel(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isPLNatKind(n__pair(V1, V2)) -> 1045.52/297.32 and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isPLNatKind(n__splitAt(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(X) -> n__isLNatKind(X) 1045.52/297.32 , isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__nil()) -> tt() 1045.52/297.32 , isLNatKind(n__afterNth(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(n__cons(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) 1045.52/297.32 , isLNatKind(n__take(V1, V2)) -> 1045.52/297.32 and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) 1045.52/297.32 , natsFrom(N) -> U161(and(isNatural(N), n__isNaturalKind(N)), N) 1045.52/297.32 , natsFrom(X) -> n__natsFrom(X) 1045.52/297.32 , sel(N, XS) -> 1045.52/297.32 U171(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , sel(X1, X2) -> n__sel(X1, X2) 1045.52/297.32 , 0() -> n__0() 1045.52/297.32 , s(X) -> n__s(X) 1045.52/297.32 , tail(X) -> n__tail(X) 1045.52/297.32 , take(N, XS) -> 1045.52/297.32 U221(and(and(isNatural(N), n__isNaturalKind(N)), 1045.52/297.32 n__and(n__isLNat(XS), n__isLNatKind(XS))), 1045.52/297.32 N, 1045.52/297.32 XS) 1045.52/297.32 , take(X1, X2) -> n__take(X1, X2) } 1045.52/297.32 Obligation: 1045.52/297.32 innermost runtime complexity 1045.52/297.32 Answer: 1045.52/297.32 MAYBE 1045.52/297.32 1045.52/297.32 None of the processors succeeded. 1045.52/297.32 1045.52/297.32 Details of failed attempt(s): 1045.52/297.32 ----------------------------- 1045.52/297.32 1) 'empty' failed due to the following reason: 1045.52/297.32 1045.52/297.32 Empty strict component of the problem is NOT empty. 1045.52/297.32 1045.52/297.32 2) 'Best' failed due to the following reason: 1045.52/297.32 1045.52/297.32 None of the processors succeeded. 1045.52/297.32 1045.52/297.32 Details of failed attempt(s): 1045.52/297.32 ----------------------------- 1045.52/297.32 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1045.52/297.32 following reason: 1045.52/297.32 1045.52/297.32 Computation stopped due to timeout after 297.0 seconds. 1045.52/297.32 1045.52/297.32 2) 'Best' failed due to the following reason: 1045.52/297.32 1045.52/297.32 None of the processors succeeded. 1045.52/297.32 1045.52/297.32 Details of failed attempt(s): 1045.52/297.32 ----------------------------- 1045.52/297.32 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1045.52/297.32 seconds)' failed due to the following reason: 1045.52/297.32 1045.52/297.32 Computation stopped due to timeout after 148.0 seconds. 1045.52/297.32 1045.52/297.32 2) 'Best' failed due to the following reason: 1045.52/297.32 1045.52/297.32 None of the processors succeeded. 1045.52/297.32 1045.52/297.32 Details of failed attempt(s): 1045.52/297.32 ----------------------------- 1045.52/297.32 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1045.52/297.32 to the following reason: 1045.52/297.32 1045.52/297.32 The input cannot be shown compatible 1045.52/297.32 1045.52/297.32 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1045.52/297.32 following reason: 1045.52/297.32 1045.52/297.32 The input cannot be shown compatible 1045.52/297.32 1045.52/297.32 1045.52/297.32 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1045.52/297.32 failed due to the following reason: 1045.52/297.32 1045.52/297.32 None of the processors succeeded. 1045.52/297.32 1045.52/297.32 Details of failed attempt(s): 1045.52/297.32 ----------------------------- 1045.52/297.32 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1045.52/297.32 failed due to the following reason: 1045.52/297.32 1045.52/297.32 match-boundness of the problem could not be verified. 1045.52/297.32 1045.52/297.32 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1045.52/297.32 failed due to the following reason: 1045.52/297.32 1045.52/297.32 match-boundness of the problem could not be verified. 1045.52/297.32 1045.52/297.32 1045.52/297.32 1045.52/297.32 1045.52/297.32 1045.52/297.32 Arrrr.. 1046.69/298.41 EOF