- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] zeros -> cons(0,n__zeros) [2] U101(tt,V1,V2) -> U102(isNatKind(activate(V1)),activate(V1),activate(V2)) [3] U102(tt,V1,V2) -> U103(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [4] U103(tt,V1,V2) -> U104(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [5] U104(tt,V1,V2) -> U105(isNat(activate(V1)),activate(V2)) [6] U105(tt,V2) -> U106(isNatIList(activate(V2))) [7] U106(tt) -> tt [8] U11(tt,V1) -> U12(isNatIListKind(activate(V1)),activate(V1)) [9] U111(tt,L,N) -> U112(isNatIListKind(activate(L)),activate(L),activate(N)) [10] U112(tt,L,N) -> U113(isNat(activate(N)),activate(L),activate(N)) [11] U113(tt,L,N) -> U114(isNatKind(activate(N)),activate(L)) [12] U114(tt,L) -> s(length(activate(L))) [13] U12(tt,V1) -> U13(isNatList(activate(V1))) [14] U121(tt,IL) -> U122(isNatIListKind(activate(IL))) [15] U122(tt) -> nil [16] U13(tt) -> tt [17] U131(tt,IL,M,N) -> U132(isNatIListKind(activate(IL)),activate(IL),activate(M),activate(N)) [18] U132(tt,IL,M,N) -> U133(isNat(activate(M)),activate(IL),activate(M),activate(N)) [19] U133(tt,IL,M,N) -> U134(isNatKind(activate(M)),activate(IL),activate(M),activate(N)) [20] U134(tt,IL,M,N) -> U135(isNat(activate(N)),activate(IL),activate(M),activate(N)) [21] U135(tt,IL,M,N) -> U136(isNatKind(activate(N)),activate(IL),activate(M),activate(N)) [22] U136(tt,IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL))) [23] U21(tt,V1) -> U22(isNatKind(activate(V1)),activate(V1)) [24] U22(tt,V1) -> U23(isNat(activate(V1))) [25] U23(tt) -> tt [26] U31(tt,V) -> U32(isNatIListKind(activate(V)),activate(V)) [27] U32(tt,V) -> U33(isNatList(activate(V))) [28] U33(tt) -> tt [29] U41(tt,V1,V2) -> U42(isNatKind(activate(V1)),activate(V1),activate(V2)) [30] U42(tt,V1,V2) -> U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [31] U43(tt,V1,V2) -> U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [32] U44(tt,V1,V2) -> U45(isNat(activate(V1)),activate(V2)) [33] U45(tt,V2) -> U46(isNatIList(activate(V2))) [34] U46(tt) -> tt [35] U51(tt,V2) -> U52(isNatIListKind(activate(V2))) [36] U52(tt) -> tt [37] U61(tt,V2) -> U62(isNatIListKind(activate(V2))) [38] U62(tt) -> tt [39] U71(tt) -> tt [40] U81(tt) -> tt [41] U91(tt,V1,V2) -> U92(isNatKind(activate(V1)),activate(V1),activate(V2)) [42] U92(tt,V1,V2) -> U93(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [43] U93(tt,V1,V2) -> U94(isNatIListKind(activate(V2)),activate(V1),activate(V2)) [44] U94(tt,V1,V2) -> U95(isNat(activate(V1)),activate(V2)) [45] U95(tt,V2) -> U96(isNatList(activate(V2))) [46] U96(tt) -> tt [47] isNat(n__0) -> tt [48] isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) [49] isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) [50] isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) [51] isNatIList(n__zeros) -> tt [52] isNatIList(n__cons(V1,V2)) -> U41(isNatKind(activate(V1)),activate(V1),activate(V2)) [53] isNatIListKind(n__nil) -> tt [54] isNatIListKind(n__zeros) -> tt [55] isNatIListKind(n__cons(V1,V2)) -> U51(isNatKind(activate(V1)),activate(V2)) [56] isNatIListKind(n__take(V1,V2)) -> U61(isNatKind(activate(V1)),activate(V2)) [57] isNatKind(n__0) -> tt [58] isNatKind(n__length(V1)) -> U71(isNatIListKind(activate(V1))) [59] isNatKind(n__s(V1)) -> U81(isNatKind(activate(V1))) [60] isNatList(n__nil) -> tt [61] isNatList(n__cons(V1,V2)) -> U91(isNatKind(activate(V1)),activate(V1),activate(V2)) [62] isNatList(n__take(V1,V2)) -> U101(isNatKind(activate(V1)),activate(V1),activate(V2)) [63] length(nil) -> 0 [64] length(cons(N,L)) -> U111(isNatList(activate(L)),activate(L),N) [65] take(0,IL) -> U121(isNatIList(IL),IL) [66] take(s(M),cons(N,IL)) -> U131(isNatIList(activate(IL)),activate(IL),M,N) [67] zeros -> n__zeros [68] take(X1,X2) -> n__take(X1,X2) [69] 0 -> n__0 [70] length(X) -> n__length(X) [71] s(X) -> n__s(X) [72] cons(X1,X2) -> n__cons(X1,X2) [73] nil -> n__nil [74] activate(n__zeros) -> zeros [75] activate(n__take(X1,X2)) -> take(X1,X2) [76] activate(n__0) -> 0 [77] activate(n__length(X)) -> length(X) [78] activate(n__s(X)) -> s(X) [79] activate(n__cons(X1,X2)) -> cons(X1,X2) [80] activate(n__nil) -> nil [81] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) ; isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) ; activate(n__zeros) >= zeros ; activate(n__take(X1,X2)) >= take(X1,X2) ; activate(n__0) >= 0 ; activate(n__length(X)) >= length(X) ; activate(n__s(X)) >= s(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(X) >= X ; U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__nil) >= tt ; U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) ; U105(tt,V2) >= U106(isNatIList(activate(V2))) ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U106(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U12(tt,V1) >= U13(isNatList(activate(V1))) ; U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) ; U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) ; U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L),activate(N)) ; U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) ; U114(tt,L) >= s(length(activate(L))) ; s(X) >= n__s(X) ; length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U13(tt) >= tt ; isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__nil) >= tt ; U122(tt) >= nil ; U121(tt,IL) >= U122(isNatIListKind(activate(IL))) ; nil >= n__nil ; U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL),activate(M), activate(N)) ; U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) ; U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL),activate(M), activate(N)) ; U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL),activate(M), activate(N)) ; U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL),activate(M), activate(N)) ; U136(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; U22(tt,V1) >= U23(isNat(activate(V1))) ; U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) ; U23(tt) >= tt ; U32(tt,V) >= U33(isNatList(activate(V))) ; U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) ; U33(tt) >= tt ; U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) ; U45(tt,V2) >= U46(isNatIList(activate(V2))) ; U46(tt) >= tt ; U52(tt) >= tt ; U51(tt,V2) >= U52(isNatIListKind(activate(V2))) ; U62(tt) >= tt ; U61(tt,V2) >= U62(isNatIListKind(activate(V2))) ; U71(tt) >= tt ; U81(tt) >= tt ; U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) ; U95(tt,V2) >= U96(isNatList(activate(V2))) ; U96(tt) >= tt ; take(0,IL) >= U121(isNatIList(IL),IL) ; take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)),activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_activate(n__take(X1,X2)) >= Marked_take(X1,X2) ; Marked_activate(n__length(X)) >= Marked_length(X) ; Marked_length(cons(N,L)) >= Marked_activate(L) ; Marked_length(cons(N,L)) >= Marked_U111(isNatList(activate(L)),activate(L),N) ; Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) ; Marked_take(0,IL) >= Marked_isNatIList(IL) ; Marked_take(0,IL) >= Marked_U121(isNatIList(IL),IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) ; Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) ; Marked_U131(tt,IL,M,N) >= Marked_activate(N) ; Marked_U131(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U131(tt,IL,M,N) >= Marked_activate(M) ; Marked_U131(tt,IL,M,N) >= Marked_isNatIListKind(activate(IL)) ; Marked_U131(tt,IL,M,N) >= Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isNatIList(V) >= Marked_activate(V) ; Marked_isNatIList(V) >= Marked_isNatIListKind(activate(V)) ; Marked_isNatIList(V) >= Marked_U31(isNatIListKind(activate(V)),activate(V)) ; Marked_U121(tt,IL) >= Marked_activate(IL) ; Marked_U121(tt,IL) >= Marked_isNatIListKind(activate(IL)) ; Marked_U111(tt,L,N) >= Marked_activate(L) ; Marked_U111(tt,L,N) >= Marked_activate(N) ; Marked_U111(tt,L,N) >= Marked_isNatIListKind(activate(L)) ; Marked_U111(tt,L,N) >= Marked_U112(isNatIListKind(activate(L)),activate(L), activate(N)) ; Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isNatList(n__take(V1,V2)) >= Marked_U101(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isNatList(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_U91(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U101(tt,V1,V2) >= Marked_activate(V1) ; Marked_U101(tt,V1,V2) >= Marked_activate(V2) ; Marked_U101(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U101(tt,V1,V2) >= Marked_U102(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_isNatKind(n__length(V1)) >= Marked_activate(V1) ; Marked_isNatKind(n__length(V1)) >= Marked_isNatIListKind(activate(V1)) ; Marked_isNatKind(n__s(V1)) >= Marked_activate(V1) ; Marked_isNatKind(n__s(V1)) >= Marked_isNatKind(activate(V1)) ; Marked_U91(tt,V1,V2) >= Marked_activate(V1) ; Marked_U91(tt,V1,V2) >= Marked_activate(V2) ; Marked_U91(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U91(tt,V1,V2) >= Marked_U92(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_U61(isNatKind(activate(V1)), activate(V2)) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_U51(isNatKind(activate(V1)), activate(V2)) ; Marked_U61(tt,V2) >= Marked_activate(V2) ; Marked_U61(tt,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U51(tt,V2) >= Marked_activate(V2) ; Marked_U51(tt,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_activate(V1) ; Marked_U41(tt,V1,V2) >= Marked_activate(V2) ; Marked_U41(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U31(tt,V) >= Marked_activate(V) ; Marked_U31(tt,V) >= Marked_isNatIListKind(activate(V)) ; Marked_U31(tt,V) >= Marked_U32(isNatIListKind(activate(V)),activate(V)) ; Marked_isNat(n__length(V1)) >= Marked_activate(V1) ; Marked_isNat(n__length(V1)) >= Marked_isNatIListKind(activate(V1)) ; Marked_isNat(n__length(V1)) >= Marked_U11(isNatIListKind(activate(V1)), activate(V1)) ; Marked_isNat(n__s(V1)) >= Marked_activate(V1) ; Marked_isNat(n__s(V1)) >= Marked_isNatKind(activate(V1)) ; Marked_isNat(n__s(V1)) >= Marked_U21(isNatKind(activate(V1)),activate(V1)) ; Marked_U21(tt,V1) >= Marked_activate(V1) ; Marked_U21(tt,V1) >= Marked_isNatKind(activate(V1)) ; Marked_U21(tt,V1) >= Marked_U22(isNatKind(activate(V1)),activate(V1)) ; Marked_U11(tt,V1) >= Marked_activate(V1) ; Marked_U11(tt,V1) >= Marked_isNatIListKind(activate(V1)) ; Marked_U11(tt,V1) >= Marked_U12(isNatIListKind(activate(V1)),activate(V1)) ; Marked_U95(tt,V2) >= Marked_activate(V2) ; Marked_U95(tt,V2) >= Marked_isNatList(activate(V2)) ; Marked_U94(tt,V1,V2) >= Marked_activate(V1) ; Marked_U94(tt,V1,V2) >= Marked_activate(V2) ; Marked_U94(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U94(tt,V1,V2) >= Marked_U95(isNat(activate(V1)),activate(V2)) ; Marked_U93(tt,V1,V2) >= Marked_activate(V1) ; Marked_U93(tt,V1,V2) >= Marked_activate(V2) ; Marked_U93(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U93(tt,V1,V2) >= Marked_U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U92(tt,V1,V2) >= Marked_activate(V1) ; Marked_U92(tt,V1,V2) >= Marked_activate(V2) ; Marked_U92(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U92(tt,V1,V2) >= Marked_U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U45(tt,V2) >= Marked_activate(V2) ; Marked_U45(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U44(tt,V1,V2) >= Marked_activate(V1) ; Marked_U44(tt,V1,V2) >= Marked_activate(V2) ; Marked_U44(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U44(tt,V1,V2) >= Marked_U45(isNat(activate(V1)),activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_activate(V1) ; Marked_U43(tt,V1,V2) >= Marked_activate(V2) ; Marked_U43(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_activate(V1) ; Marked_U42(tt,V1,V2) >= Marked_activate(V2) ; Marked_U42(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U32(tt,V) >= Marked_activate(V) ; Marked_U32(tt,V) >= Marked_isNatList(activate(V)) ; Marked_U22(tt,V1) >= Marked_activate(V1) ; Marked_U22(tt,V1) >= Marked_isNat(activate(V1)) ; Marked_U136(tt,IL,M,N) >= Marked_activate(N) ; Marked_U136(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U136(tt,IL,M,N) >= Marked_activate(M) ; Marked_U135(tt,IL,M,N) >= Marked_activate(N) ; Marked_U135(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U135(tt,IL,M,N) >= Marked_activate(M) ; Marked_U135(tt,IL,M,N) >= Marked_isNatKind(activate(N)) ; Marked_U135(tt,IL,M,N) >= Marked_U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) ; Marked_U134(tt,IL,M,N) >= Marked_activate(N) ; Marked_U134(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U134(tt,IL,M,N) >= Marked_activate(M) ; Marked_U134(tt,IL,M,N) >= Marked_isNat(activate(N)) ; Marked_U134(tt,IL,M,N) >= Marked_U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) ; Marked_U133(tt,IL,M,N) >= Marked_activate(N) ; Marked_U133(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U133(tt,IL,M,N) >= Marked_activate(M) ; Marked_U133(tt,IL,M,N) >= Marked_isNatKind(activate(M)) ; Marked_U133(tt,IL,M,N) >= Marked_U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) ; Marked_U132(tt,IL,M,N) >= Marked_activate(N) ; Marked_U132(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U132(tt,IL,M,N) >= Marked_activate(M) ; Marked_U132(tt,IL,M,N) >= Marked_isNat(activate(M)) ; Marked_U132(tt,IL,M,N) >= Marked_U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) ; Marked_U12(tt,V1) >= Marked_activate(V1) ; Marked_U12(tt,V1) >= Marked_isNatList(activate(V1)) ; Marked_U114(tt,L) >= Marked_activate(L) ; Marked_U114(tt,L) >= Marked_length(activate(L)) ; Marked_U113(tt,L,N) >= Marked_activate(L) ; Marked_U113(tt,L,N) >= Marked_activate(N) ; Marked_U113(tt,L,N) >= Marked_isNatKind(activate(N)) ; Marked_U113(tt,L,N) >= Marked_U114(isNatKind(activate(N)),activate(L)) ; Marked_U112(tt,L,N) >= Marked_activate(L) ; Marked_U112(tt,L,N) >= Marked_activate(N) ; Marked_U112(tt,L,N) >= Marked_isNat(activate(N)) ; Marked_U112(tt,L,N) >= Marked_U113(isNat(activate(N)),activate(L), activate(N)) ; Marked_U105(tt,V2) >= Marked_activate(V2) ; Marked_U105(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U104(tt,V1,V2) >= Marked_activate(V1) ; Marked_U104(tt,V1,V2) >= Marked_activate(V2) ; Marked_U104(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U104(tt,V1,V2) >= Marked_U105(isNat(activate(V1)),activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_activate(V1) ; Marked_U103(tt,V1,V2) >= Marked_activate(V2) ; Marked_U103(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_activate(V1) ; Marked_U102(tt,V1,V2) >= Marked_activate(V2) ; Marked_U102(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } + Disjunctions:{ { Marked_activate(n__take(X1,X2)) > Marked_take(X1,X2) ; } { Marked_activate(n__length(X)) > Marked_length(X) ; } { Marked_length(cons(N,L)) > Marked_activate(L) ; } { Marked_length(cons(N,L)) > Marked_U111(isNatList(activate(L)),activate(L),N) ; } { Marked_length(cons(N,L)) > Marked_isNatList(activate(L)) ; } { Marked_take(0,IL) > Marked_isNatIList(IL) ; } { Marked_take(0,IL) > Marked_U121(isNatIList(IL),IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_activate(IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) ; } { Marked_take(s(M),cons(N,IL)) > Marked_isNatIList(activate(IL)) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U131(tt,IL,M,N) > Marked_isNatIListKind(activate(IL)) ; } { Marked_U131(tt,IL,M,N) > Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isNatIList(V) > Marked_activate(V) ; } { Marked_isNatIList(V) > Marked_isNatIListKind(activate(V)) ; } { Marked_isNatIList(V) > Marked_U31(isNatIListKind(activate(V)),activate(V)) ; } { Marked_U121(tt,IL) > Marked_activate(IL) ; } { Marked_U121(tt,IL) > Marked_isNatIListKind(activate(IL)) ; } { Marked_U111(tt,L,N) > Marked_activate(L) ; } { Marked_U111(tt,L,N) > Marked_activate(N) ; } { Marked_U111(tt,L,N) > Marked_isNatIListKind(activate(L)) ; } { Marked_U111(tt,L,N) > Marked_U112(isNatIListKind(activate(L)),activate(L), activate(N)) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_U101(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_U91(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U101(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U101(tt,V1,V2) > Marked_U102(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_isNatKind(n__length(V1)) > Marked_activate(V1) ; } { Marked_isNatKind(n__length(V1)) > Marked_isNatIListKind(activate(V1)) ; } { Marked_isNatKind(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNatKind(n__s(V1)) > Marked_isNatKind(activate(V1)) ; } { Marked_U91(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U91(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U91(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U91(tt,V1,V2) > Marked_U92(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_U61(isNatKind(activate(V1)), activate(V2)) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_U51(isNatKind(activate(V1)), activate(V2)) ; } { Marked_U61(tt,V2) > Marked_activate(V2) ; } { Marked_U61(tt,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U51(tt,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U41(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U31(tt,V) > Marked_activate(V) ; } { Marked_U31(tt,V) > Marked_isNatIListKind(activate(V)) ; } { Marked_U31(tt,V) > Marked_U32(isNatIListKind(activate(V)),activate(V)) ; } { Marked_isNat(n__length(V1)) > Marked_activate(V1) ; } { Marked_isNat(n__length(V1)) > Marked_isNatIListKind(activate(V1)) ; } { Marked_isNat(n__length(V1)) > Marked_U11(isNatIListKind(activate(V1)), activate(V1)) ; } { Marked_isNat(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNat(n__s(V1)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNat(n__s(V1)) > Marked_U21(isNatKind(activate(V1)),activate(V1)) ; } { Marked_U21(tt,V1) > Marked_activate(V1) ; } { Marked_U21(tt,V1) > Marked_isNatKind(activate(V1)) ; } { Marked_U21(tt,V1) > Marked_U22(isNatKind(activate(V1)),activate(V1)) ; } { Marked_U11(tt,V1) > Marked_activate(V1) ; } { Marked_U11(tt,V1) > Marked_isNatIListKind(activate(V1)) ; } { Marked_U11(tt,V1) > Marked_U12(isNatIListKind(activate(V1)),activate(V1)) ; } { Marked_U95(tt,V2) > Marked_activate(V2) ; } { Marked_U95(tt,V2) > Marked_isNatList(activate(V2)) ; } { Marked_U94(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U94(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U94(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U94(tt,V1,V2) > Marked_U95(isNat(activate(V1)),activate(V2)) ; } { Marked_U93(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U93(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U93(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U93(tt,V1,V2) > Marked_U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U92(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U92(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U92(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U92(tt,V1,V2) > Marked_U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U45(tt,V2) > Marked_activate(V2) ; } { Marked_U45(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U44(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U44(tt,V1,V2) > Marked_U45(isNat(activate(V1)),activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U43(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U42(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U32(tt,V) > Marked_activate(V) ; } { Marked_U32(tt,V) > Marked_isNatList(activate(V)) ; } { Marked_U22(tt,V1) > Marked_activate(V1) ; } { Marked_U22(tt,V1) > Marked_isNat(activate(V1)) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U135(tt,IL,M,N) > Marked_isNatKind(activate(N)) ; } { Marked_U135(tt,IL,M,N) > Marked_U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U134(tt,IL,M,N) > Marked_isNat(activate(N)) ; } { Marked_U134(tt,IL,M,N) > Marked_U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U133(tt,IL,M,N) > Marked_isNatKind(activate(M)) ; } { Marked_U133(tt,IL,M,N) > Marked_U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U132(tt,IL,M,N) > Marked_isNat(activate(M)) ; } { Marked_U132(tt,IL,M,N) > Marked_U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) ; } { Marked_U12(tt,V1) > Marked_activate(V1) ; } { Marked_U12(tt,V1) > Marked_isNatList(activate(V1)) ; } { Marked_U114(tt,L) > Marked_activate(L) ; } { Marked_U114(tt,L) > Marked_length(activate(L)) ; } { Marked_U113(tt,L,N) > Marked_activate(L) ; } { Marked_U113(tt,L,N) > Marked_activate(N) ; } { Marked_U113(tt,L,N) > Marked_isNatKind(activate(N)) ; } { Marked_U113(tt,L,N) > Marked_U114(isNatKind(activate(N)),activate(L)) ; } { Marked_U112(tt,L,N) > Marked_activate(L) ; } { Marked_U112(tt,L,N) > Marked_activate(N) ; } { Marked_U112(tt,L,N) > Marked_isNat(activate(N)) ; } { Marked_U112(tt,L,N) > Marked_U113(isNat(activate(N)),activate(L),activate(N)) ; } { Marked_U105(tt,V2) > Marked_activate(V2) ; } { Marked_U105(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U104(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U104(tt,V1,V2) > Marked_U105(isNat(activate(V1)),activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U103(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U102(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(X1,X2) >= n__cons(X1,X2) constraint: 0 >= n__0 constraint: zeros >= cons(0,n__zeros) constraint: zeros >= n__zeros constraint: U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatKind(n__0) >= tt constraint: isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) constraint: isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) constraint: activate(n__zeros) >= zeros constraint: activate(n__take(X1,X2)) >= take(X1,X2) constraint: activate(n__0) >= 0 constraint: activate(n__length(X)) >= length(X) constraint: activate(n__s(X)) >= s(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(n__nil) >= nil constraint: activate(X) >= X constraint: U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatIListKind(n__zeros) >= tt constraint: isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__nil) >= tt constraint: U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) constraint: U105(tt,V2) >= U106(isNatIList(activate(V2))) constraint: isNat(n__0) >= tt constraint: isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)), activate(V1)) constraint: isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) constraint: U106(tt) >= tt constraint: isNatIList(n__zeros) >= tt constraint: isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) constraint: U12(tt,V1) >= U13(isNatList(activate(V1))) constraint: U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) constraint: U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) constraint: U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L), activate(N)) constraint: U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) constraint: U114(tt,L) >= s(length(activate(L))) constraint: s(X) >= n__s(X) constraint: length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) constraint: length(nil) >= 0 constraint: length(X) >= n__length(X) constraint: U13(tt) >= tt constraint: isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__nil) >= tt constraint: U122(tt) >= nil constraint: U121(tt,IL) >= U122(isNatIListKind(activate(IL))) constraint: nil >= n__nil constraint: U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) constraint: U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) constraint: U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) constraint: U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) constraint: U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) constraint: U136(tt,IL,M,N) >= cons(activate(N), n__take(activate(M),activate(IL))) constraint: U22(tt,V1) >= U23(isNat(activate(V1))) constraint: U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) constraint: U23(tt) >= tt constraint: U32(tt,V) >= U33(isNatList(activate(V))) constraint: U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) constraint: U33(tt) >= tt constraint: U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) constraint: U45(tt,V2) >= U46(isNatIList(activate(V2))) constraint: U46(tt) >= tt constraint: U52(tt) >= tt constraint: U51(tt,V2) >= U52(isNatIListKind(activate(V2))) constraint: U62(tt) >= tt constraint: U61(tt,V2) >= U62(isNatIListKind(activate(V2))) constraint: U71(tt) >= tt constraint: U81(tt) >= tt constraint: U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) constraint: U95(tt,V2) >= U96(isNatList(activate(V2))) constraint: U96(tt) >= tt constraint: take(0,IL) >= U121(isNatIList(IL),IL) constraint: take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)), activate(IL),M,N) constraint: take(X1,X2) >= n__take(X1,X2) constraint: Marked_activate(n__take(X1,X2)) >= Marked_take(X1,X2) constraint: Marked_activate(n__length(X)) >= Marked_length(X) constraint: Marked_length(cons(N,L)) >= Marked_activate(L) constraint: Marked_length(cons(N,L)) >= Marked_U111(isNatList(activate(L)), activate(L),N) constraint: Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) constraint: Marked_take(0,IL) >= Marked_isNatIList(IL) constraint: Marked_take(0,IL) >= Marked_U121(isNatIList(IL),IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U131(tt,IL,M,N) >= Marked_isNatIListKind(activate(IL)) constraint: Marked_U131(tt,IL,M,N) >= Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(isNatKind( activate( V1)), activate(V1),activate(V2)) constraint: Marked_isNatIList(V) >= Marked_activate(V) constraint: Marked_isNatIList(V) >= Marked_isNatIListKind(activate(V)) constraint: Marked_isNatIList(V) >= Marked_U31(isNatIListKind(activate(V)), activate(V)) constraint: Marked_U121(tt,IL) >= Marked_activate(IL) constraint: Marked_U121(tt,IL) >= Marked_isNatIListKind(activate(IL)) constraint: Marked_U111(tt,L,N) >= Marked_activate(L) constraint: Marked_U111(tt,L,N) >= Marked_activate(N) constraint: Marked_U111(tt,L,N) >= Marked_isNatIListKind(activate(L)) constraint: Marked_U111(tt,L,N) >= Marked_U112(isNatIListKind(activate(L)), activate(L),activate(N)) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_U101(isNatKind( activate( V1)), activate(V1),activate(V2)) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_U91(isNatKind( activate( V1)),activate(V1), activate(V2)) constraint: Marked_U101(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U101(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U101(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U101(tt,V1,V2) >= Marked_U102(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_isNatKind(n__length(V1)) >= Marked_activate(V1) constraint: Marked_isNatKind(n__length(V1)) >= Marked_isNatIListKind( activate(V1)) constraint: Marked_isNatKind(n__s(V1)) >= Marked_activate(V1) constraint: Marked_isNatKind(n__s(V1)) >= Marked_isNatKind(activate(V1)) constraint: Marked_U91(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U91(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U91(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U91(tt,V1,V2) >= Marked_U92(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_isNatKind( activate(V1)) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_U61(isNatKind( activate( V1)), activate(V2)) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_isNatKind( activate(V1)) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_U51(isNatKind( activate( V1)), activate(V2)) constraint: Marked_U61(tt,V2) >= Marked_activate(V2) constraint: Marked_U61(tt,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U51(tt,V2) >= Marked_activate(V2) constraint: Marked_U51(tt,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U41(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U41(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U41(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U41(tt,V1,V2) >= Marked_U42(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_U31(tt,V) >= Marked_activate(V) constraint: Marked_U31(tt,V) >= Marked_isNatIListKind(activate(V)) constraint: Marked_U31(tt,V) >= Marked_U32(isNatIListKind(activate(V)), activate(V)) constraint: Marked_isNat(n__length(V1)) >= Marked_activate(V1) constraint: Marked_isNat(n__length(V1)) >= Marked_isNatIListKind(activate(V1)) constraint: Marked_isNat(n__length(V1)) >= Marked_U11(isNatIListKind( activate(V1)), activate(V1)) constraint: Marked_isNat(n__s(V1)) >= Marked_activate(V1) constraint: Marked_isNat(n__s(V1)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNat(n__s(V1)) >= Marked_U21(isNatKind(activate(V1)), activate(V1)) constraint: Marked_U21(tt,V1) >= Marked_activate(V1) constraint: Marked_U21(tt,V1) >= Marked_isNatKind(activate(V1)) constraint: Marked_U21(tt,V1) >= Marked_U22(isNatKind(activate(V1)), activate(V1)) constraint: Marked_U11(tt,V1) >= Marked_activate(V1) constraint: Marked_U11(tt,V1) >= Marked_isNatIListKind(activate(V1)) constraint: Marked_U11(tt,V1) >= Marked_U12(isNatIListKind(activate(V1)), activate(V1)) constraint: Marked_U95(tt,V2) >= Marked_activate(V2) constraint: Marked_U95(tt,V2) >= Marked_isNatList(activate(V2)) constraint: Marked_U94(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U94(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U94(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U94(tt,V1,V2) >= Marked_U95(isNat(activate(V1)), activate(V2)) constraint: Marked_U93(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U93(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U93(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U93(tt,V1,V2) >= Marked_U94(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U92(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U92(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U92(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U92(tt,V1,V2) >= Marked_U93(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U45(tt,V2) >= Marked_activate(V2) constraint: Marked_U45(tt,V2) >= Marked_isNatIList(activate(V2)) constraint: Marked_U44(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U44(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U44(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U44(tt,V1,V2) >= Marked_U45(isNat(activate(V1)), activate(V2)) constraint: Marked_U43(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U43(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U43(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U43(tt,V1,V2) >= Marked_U44(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U42(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U42(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U42(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U42(tt,V1,V2) >= Marked_U43(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U32(tt,V) >= Marked_activate(V) constraint: Marked_U32(tt,V) >= Marked_isNatList(activate(V)) constraint: Marked_U22(tt,V1) >= Marked_activate(V1) constraint: Marked_U22(tt,V1) >= Marked_isNat(activate(V1)) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U135(tt,IL,M,N) >= Marked_isNatKind(activate(N)) constraint: Marked_U135(tt,IL,M,N) >= Marked_U136(isNatKind(activate(N)), activate(IL),activate(M),activate(N)) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U134(tt,IL,M,N) >= Marked_isNat(activate(N)) constraint: Marked_U134(tt,IL,M,N) >= Marked_U135(isNat(activate(N)), activate(IL),activate(M),activate(N)) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U133(tt,IL,M,N) >= Marked_isNatKind(activate(M)) constraint: Marked_U133(tt,IL,M,N) >= Marked_U134(isNatKind(activate(M)), activate(IL),activate(M),activate(N)) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U132(tt,IL,M,N) >= Marked_isNat(activate(M)) constraint: Marked_U132(tt,IL,M,N) >= Marked_U133(isNat(activate(M)), activate(IL),activate(M),activate(N)) constraint: Marked_U12(tt,V1) >= Marked_activate(V1) constraint: Marked_U12(tt,V1) >= Marked_isNatList(activate(V1)) constraint: Marked_U114(tt,L) >= Marked_activate(L) constraint: Marked_U114(tt,L) >= Marked_length(activate(L)) constraint: Marked_U113(tt,L,N) >= Marked_activate(L) constraint: Marked_U113(tt,L,N) >= Marked_activate(N) constraint: Marked_U113(tt,L,N) >= Marked_isNatKind(activate(N)) constraint: Marked_U113(tt,L,N) >= Marked_U114(isNatKind(activate(N)), activate(L)) constraint: Marked_U112(tt,L,N) >= Marked_activate(L) constraint: Marked_U112(tt,L,N) >= Marked_activate(N) constraint: Marked_U112(tt,L,N) >= Marked_isNat(activate(N)) constraint: Marked_U112(tt,L,N) >= Marked_U113(isNat(activate(N)),activate(L), activate(N)) constraint: Marked_U105(tt,V2) >= Marked_activate(V2) constraint: Marked_U105(tt,V2) >= Marked_isNatIList(activate(V2)) constraint: Marked_U104(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U104(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U104(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U104(tt,V1,V2) >= Marked_U105(isNat(activate(V1)), activate(V2)) constraint: Marked_U103(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U103(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U103(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U103(tt,V1,V2) >= Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U102(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U102(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U102(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U102(tt,V1,V2) >= Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) APPLY CRITERIA (Graph splitting) Found 2 components: { --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) ; isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) ; activate(n__zeros) >= zeros ; activate(n__take(X1,X2)) >= take(X1,X2) ; activate(n__0) >= 0 ; activate(n__length(X)) >= length(X) ; activate(n__s(X)) >= s(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(X) >= X ; U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__nil) >= tt ; U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) ; U105(tt,V2) >= U106(isNatIList(activate(V2))) ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U106(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U12(tt,V1) >= U13(isNatList(activate(V1))) ; U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) ; U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) ; U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L),activate(N)) ; U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) ; U114(tt,L) >= s(length(activate(L))) ; s(X) >= n__s(X) ; length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U13(tt) >= tt ; isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__nil) >= tt ; U122(tt) >= nil ; U121(tt,IL) >= U122(isNatIListKind(activate(IL))) ; nil >= n__nil ; U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL),activate(M), activate(N)) ; U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) ; U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL),activate(M), activate(N)) ; U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL),activate(M), activate(N)) ; U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL),activate(M), activate(N)) ; U136(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; U22(tt,V1) >= U23(isNat(activate(V1))) ; U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) ; U23(tt) >= tt ; U32(tt,V) >= U33(isNatList(activate(V))) ; U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) ; U33(tt) >= tt ; U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) ; U45(tt,V2) >= U46(isNatIList(activate(V2))) ; U46(tt) >= tt ; U52(tt) >= tt ; U51(tt,V2) >= U52(isNatIListKind(activate(V2))) ; U62(tt) >= tt ; U61(tt,V2) >= U62(isNatIListKind(activate(V2))) ; U71(tt) >= tt ; U81(tt) >= tt ; U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) ; U95(tt,V2) >= U96(isNatList(activate(V2))) ; U96(tt) >= tt ; take(0,IL) >= U121(isNatIList(IL),IL) ; take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)),activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_length(cons(N,L)) >= Marked_U111(isNatList(activate(L)),activate(L),N) ; Marked_U111(tt,L,N) >= Marked_U112(isNatIListKind(activate(L)),activate(L), activate(N)) ; Marked_U114(tt,L) >= Marked_length(activate(L)) ; Marked_U113(tt,L,N) >= Marked_U114(isNatKind(activate(N)),activate(L)) ; Marked_U112(tt,L,N) >= Marked_U113(isNat(activate(N)),activate(L), activate(N)) ; } + Disjunctions:{ { Marked_length(cons(N,L)) > Marked_U111(isNatList(activate(L)),activate(L),N) ; } { Marked_U111(tt,L,N) > Marked_U112(isNatIListKind(activate(L)),activate(L), activate(N)) ; } { Marked_U114(tt,L) > Marked_length(activate(L)) ; } { Marked_U113(tt,L,N) > Marked_U114(isNatKind(activate(N)),activate(L)) ; } { Marked_U112(tt,L,N) > Marked_U113(isNat(activate(N)),activate(L),activate(N)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(X1,X2) >= n__cons(X1,X2) constraint: 0 >= n__0 constraint: zeros >= cons(0,n__zeros) constraint: zeros >= n__zeros constraint: U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatKind(n__0) >= tt constraint: isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) constraint: isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) constraint: activate(n__zeros) >= zeros constraint: activate(n__take(X1,X2)) >= take(X1,X2) constraint: activate(n__0) >= 0 constraint: activate(n__length(X)) >= length(X) constraint: activate(n__s(X)) >= s(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(n__nil) >= nil constraint: activate(X) >= X constraint: U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatIListKind(n__zeros) >= tt constraint: isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__nil) >= tt constraint: U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) constraint: U105(tt,V2) >= U106(isNatIList(activate(V2))) constraint: isNat(n__0) >= tt constraint: isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)), activate(V1)) constraint: isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) constraint: U106(tt) >= tt constraint: isNatIList(n__zeros) >= tt constraint: isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) constraint: U12(tt,V1) >= U13(isNatList(activate(V1))) constraint: U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) constraint: U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) constraint: U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L), activate(N)) constraint: U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) constraint: U114(tt,L) >= s(length(activate(L))) constraint: s(X) >= n__s(X) constraint: length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) constraint: length(nil) >= 0 constraint: length(X) >= n__length(X) constraint: U13(tt) >= tt constraint: isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__nil) >= tt constraint: U122(tt) >= nil constraint: U121(tt,IL) >= U122(isNatIListKind(activate(IL))) constraint: nil >= n__nil constraint: U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) constraint: U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) constraint: U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) constraint: U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) constraint: U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) constraint: U136(tt,IL,M,N) >= cons(activate(N), n__take(activate(M),activate(IL))) constraint: U22(tt,V1) >= U23(isNat(activate(V1))) constraint: U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) constraint: U23(tt) >= tt constraint: U32(tt,V) >= U33(isNatList(activate(V))) constraint: U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) constraint: U33(tt) >= tt constraint: U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) constraint: U45(tt,V2) >= U46(isNatIList(activate(V2))) constraint: U46(tt) >= tt constraint: U52(tt) >= tt constraint: U51(tt,V2) >= U52(isNatIListKind(activate(V2))) constraint: U62(tt) >= tt constraint: U61(tt,V2) >= U62(isNatIListKind(activate(V2))) constraint: U71(tt) >= tt constraint: U81(tt) >= tt constraint: U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) constraint: U95(tt,V2) >= U96(isNatList(activate(V2))) constraint: U96(tt) >= tt constraint: take(0,IL) >= U121(isNatIList(IL),IL) constraint: take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)), activate(IL),M,N) constraint: take(X1,X2) >= n__take(X1,X2) constraint: Marked_length(cons(N,L)) >= Marked_U111(isNatList(activate(L)), activate(L),N) constraint: Marked_U111(tt,L,N) >= Marked_U112(isNatIListKind(activate(L)), activate(L),activate(N)) constraint: Marked_U114(tt,L) >= Marked_length(activate(L)) constraint: Marked_U113(tt,L,N) >= Marked_U114(isNatKind(activate(N)), activate(L)) constraint: Marked_U112(tt,L,N) >= Marked_U113(isNat(activate(N)),activate(L), activate(N)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) ; isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) ; activate(n__zeros) >= zeros ; activate(n__take(X1,X2)) >= take(X1,X2) ; activate(n__0) >= 0 ; activate(n__length(X)) >= length(X) ; activate(n__s(X)) >= s(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(X) >= X ; U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__nil) >= tt ; U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) ; U105(tt,V2) >= U106(isNatIList(activate(V2))) ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U106(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U12(tt,V1) >= U13(isNatList(activate(V1))) ; U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) ; U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) ; U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L),activate(N)) ; U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) ; U114(tt,L) >= s(length(activate(L))) ; s(X) >= n__s(X) ; length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U13(tt) >= tt ; isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__nil) >= tt ; U122(tt) >= nil ; U121(tt,IL) >= U122(isNatIListKind(activate(IL))) ; nil >= n__nil ; U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL),activate(M), activate(N)) ; U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) ; U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL),activate(M), activate(N)) ; U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL),activate(M), activate(N)) ; U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL),activate(M), activate(N)) ; U136(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; U22(tt,V1) >= U23(isNat(activate(V1))) ; U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) ; U23(tt) >= tt ; U32(tt,V) >= U33(isNatList(activate(V))) ; U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) ; U33(tt) >= tt ; U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) ; U45(tt,V2) >= U46(isNatIList(activate(V2))) ; U46(tt) >= tt ; U52(tt) >= tt ; U51(tt,V2) >= U52(isNatIListKind(activate(V2))) ; U62(tt) >= tt ; U61(tt,V2) >= U62(isNatIListKind(activate(V2))) ; U71(tt) >= tt ; U81(tt) >= tt ; U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) ; U95(tt,V2) >= U96(isNatList(activate(V2))) ; U96(tt) >= tt ; take(0,IL) >= U121(isNatIList(IL),IL) ; take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)),activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_activate(n__take(X1,X2)) >= Marked_take(X1,X2) ; Marked_take(0,IL) >= Marked_isNatIList(IL) ; Marked_take(0,IL) >= Marked_U121(isNatIList(IL),IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) ; Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) ; Marked_U131(tt,IL,M,N) >= Marked_activate(N) ; Marked_U131(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U131(tt,IL,M,N) >= Marked_activate(M) ; Marked_U131(tt,IL,M,N) >= Marked_isNatIListKind(activate(IL)) ; Marked_U131(tt,IL,M,N) >= Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isNatIList(V) >= Marked_activate(V) ; Marked_isNatIList(V) >= Marked_isNatIListKind(activate(V)) ; Marked_isNatIList(V) >= Marked_U31(isNatIListKind(activate(V)),activate(V)) ; Marked_U121(tt,IL) >= Marked_activate(IL) ; Marked_U121(tt,IL) >= Marked_isNatIListKind(activate(IL)) ; Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isNatList(n__take(V1,V2)) >= Marked_U101(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isNatList(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_U91(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U101(tt,V1,V2) >= Marked_activate(V1) ; Marked_U101(tt,V1,V2) >= Marked_activate(V2) ; Marked_U101(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U101(tt,V1,V2) >= Marked_U102(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_isNatKind(n__s(V1)) >= Marked_activate(V1) ; Marked_isNatKind(n__s(V1)) >= Marked_isNatKind(activate(V1)) ; Marked_U91(tt,V1,V2) >= Marked_activate(V1) ; Marked_U91(tt,V1,V2) >= Marked_activate(V2) ; Marked_U91(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U91(tt,V1,V2) >= Marked_U92(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIListKind(n__take(V1,V2)) >= Marked_U61(isNatKind(activate(V1)), activate(V2)) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) ; Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_U51(isNatKind(activate(V1)), activate(V2)) ; Marked_U61(tt,V2) >= Marked_activate(V2) ; Marked_U61(tt,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U51(tt,V2) >= Marked_activate(V2) ; Marked_U51(tt,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_activate(V1) ; Marked_U41(tt,V1,V2) >= Marked_activate(V2) ; Marked_U41(tt,V1,V2) >= Marked_isNatKind(activate(V1)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U31(tt,V) >= Marked_activate(V) ; Marked_U31(tt,V) >= Marked_isNatIListKind(activate(V)) ; Marked_U31(tt,V) >= Marked_U32(isNatIListKind(activate(V)),activate(V)) ; Marked_isNat(n__s(V1)) >= Marked_activate(V1) ; Marked_isNat(n__s(V1)) >= Marked_isNatKind(activate(V1)) ; Marked_isNat(n__s(V1)) >= Marked_U21(isNatKind(activate(V1)),activate(V1)) ; Marked_U21(tt,V1) >= Marked_activate(V1) ; Marked_U21(tt,V1) >= Marked_isNatKind(activate(V1)) ; Marked_U21(tt,V1) >= Marked_U22(isNatKind(activate(V1)),activate(V1)) ; Marked_U95(tt,V2) >= Marked_activate(V2) ; Marked_U95(tt,V2) >= Marked_isNatList(activate(V2)) ; Marked_U94(tt,V1,V2) >= Marked_activate(V1) ; Marked_U94(tt,V1,V2) >= Marked_activate(V2) ; Marked_U94(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U94(tt,V1,V2) >= Marked_U95(isNat(activate(V1)),activate(V2)) ; Marked_U93(tt,V1,V2) >= Marked_activate(V1) ; Marked_U93(tt,V1,V2) >= Marked_activate(V2) ; Marked_U93(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U93(tt,V1,V2) >= Marked_U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U92(tt,V1,V2) >= Marked_activate(V1) ; Marked_U92(tt,V1,V2) >= Marked_activate(V2) ; Marked_U92(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U92(tt,V1,V2) >= Marked_U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U45(tt,V2) >= Marked_activate(V2) ; Marked_U45(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U44(tt,V1,V2) >= Marked_activate(V1) ; Marked_U44(tt,V1,V2) >= Marked_activate(V2) ; Marked_U44(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U44(tt,V1,V2) >= Marked_U45(isNat(activate(V1)),activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_activate(V1) ; Marked_U43(tt,V1,V2) >= Marked_activate(V2) ; Marked_U43(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_activate(V1) ; Marked_U42(tt,V1,V2) >= Marked_activate(V2) ; Marked_U42(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U32(tt,V) >= Marked_activate(V) ; Marked_U32(tt,V) >= Marked_isNatList(activate(V)) ; Marked_U22(tt,V1) >= Marked_activate(V1) ; Marked_U22(tt,V1) >= Marked_isNat(activate(V1)) ; Marked_U136(tt,IL,M,N) >= Marked_activate(N) ; Marked_U136(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U136(tt,IL,M,N) >= Marked_activate(M) ; Marked_U135(tt,IL,M,N) >= Marked_activate(N) ; Marked_U135(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U135(tt,IL,M,N) >= Marked_activate(M) ; Marked_U135(tt,IL,M,N) >= Marked_isNatKind(activate(N)) ; Marked_U135(tt,IL,M,N) >= Marked_U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) ; Marked_U134(tt,IL,M,N) >= Marked_activate(N) ; Marked_U134(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U134(tt,IL,M,N) >= Marked_activate(M) ; Marked_U134(tt,IL,M,N) >= Marked_isNat(activate(N)) ; Marked_U134(tt,IL,M,N) >= Marked_U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) ; Marked_U133(tt,IL,M,N) >= Marked_activate(N) ; Marked_U133(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U133(tt,IL,M,N) >= Marked_activate(M) ; Marked_U133(tt,IL,M,N) >= Marked_isNatKind(activate(M)) ; Marked_U133(tt,IL,M,N) >= Marked_U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) ; Marked_U132(tt,IL,M,N) >= Marked_activate(N) ; Marked_U132(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U132(tt,IL,M,N) >= Marked_activate(M) ; Marked_U132(tt,IL,M,N) >= Marked_isNat(activate(M)) ; Marked_U132(tt,IL,M,N) >= Marked_U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) ; Marked_U105(tt,V2) >= Marked_activate(V2) ; Marked_U105(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U104(tt,V1,V2) >= Marked_activate(V1) ; Marked_U104(tt,V1,V2) >= Marked_activate(V2) ; Marked_U104(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U104(tt,V1,V2) >= Marked_U105(isNat(activate(V1)),activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_activate(V1) ; Marked_U103(tt,V1,V2) >= Marked_activate(V2) ; Marked_U103(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_activate(V1) ; Marked_U102(tt,V1,V2) >= Marked_activate(V2) ; Marked_U102(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } + Disjunctions:{ { Marked_activate(n__take(X1,X2)) > Marked_take(X1,X2) ; } { Marked_take(0,IL) > Marked_isNatIList(IL) ; } { Marked_take(0,IL) > Marked_U121(isNatIList(IL),IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_activate(IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) ; } { Marked_take(s(M),cons(N,IL)) > Marked_isNatIList(activate(IL)) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U131(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U131(tt,IL,M,N) > Marked_isNatIListKind(activate(IL)) ; } { Marked_U131(tt,IL,M,N) > Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isNatIList(V) > Marked_activate(V) ; } { Marked_isNatIList(V) > Marked_isNatIListKind(activate(V)) ; } { Marked_isNatIList(V) > Marked_U31(isNatIListKind(activate(V)),activate(V)) ; } { Marked_U121(tt,IL) > Marked_activate(IL) ; } { Marked_U121(tt,IL) > Marked_isNatIListKind(activate(IL)) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_U101(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_U91(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U101(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U101(tt,V1,V2) > Marked_U102(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_isNatKind(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNatKind(n__s(V1)) > Marked_isNatKind(activate(V1)) ; } { Marked_U91(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U91(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U91(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U91(tt,V1,V2) > Marked_U92(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIListKind(n__take(V1,V2)) > Marked_U61(isNatKind(activate(V1)), activate(V2)) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNatIListKind(n__cons(V1,V2)) > Marked_U51(isNatKind(activate(V1)), activate(V2)) ; } { Marked_U61(tt,V2) > Marked_activate(V2) ; } { Marked_U61(tt,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U51(tt,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U41(tt,V1,V2) > Marked_isNatKind(activate(V1)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U31(tt,V) > Marked_activate(V) ; } { Marked_U31(tt,V) > Marked_isNatIListKind(activate(V)) ; } { Marked_U31(tt,V) > Marked_U32(isNatIListKind(activate(V)),activate(V)) ; } { Marked_isNat(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNat(n__s(V1)) > Marked_isNatKind(activate(V1)) ; } { Marked_isNat(n__s(V1)) > Marked_U21(isNatKind(activate(V1)),activate(V1)) ; } { Marked_U21(tt,V1) > Marked_activate(V1) ; } { Marked_U21(tt,V1) > Marked_isNatKind(activate(V1)) ; } { Marked_U21(tt,V1) > Marked_U22(isNatKind(activate(V1)),activate(V1)) ; } { Marked_U95(tt,V2) > Marked_activate(V2) ; } { Marked_U95(tt,V2) > Marked_isNatList(activate(V2)) ; } { Marked_U94(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U94(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U94(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U94(tt,V1,V2) > Marked_U95(isNat(activate(V1)),activate(V2)) ; } { Marked_U93(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U93(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U93(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U93(tt,V1,V2) > Marked_U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U92(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U92(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U92(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U92(tt,V1,V2) > Marked_U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U45(tt,V2) > Marked_activate(V2) ; } { Marked_U45(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U44(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U44(tt,V1,V2) > Marked_U45(isNat(activate(V1)),activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U43(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U42(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U32(tt,V) > Marked_activate(V) ; } { Marked_U32(tt,V) > Marked_isNatList(activate(V)) ; } { Marked_U22(tt,V1) > Marked_activate(V1) ; } { Marked_U22(tt,V1) > Marked_isNat(activate(V1)) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U136(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U135(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U135(tt,IL,M,N) > Marked_isNatKind(activate(N)) ; } { Marked_U135(tt,IL,M,N) > Marked_U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U134(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U134(tt,IL,M,N) > Marked_isNat(activate(N)) ; } { Marked_U134(tt,IL,M,N) > Marked_U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U133(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U133(tt,IL,M,N) > Marked_isNatKind(activate(M)) ; } { Marked_U133(tt,IL,M,N) > Marked_U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(N) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U132(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U132(tt,IL,M,N) > Marked_isNat(activate(M)) ; } { Marked_U132(tt,IL,M,N) > Marked_U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) ; } { Marked_U105(tt,V2) > Marked_activate(V2) ; } { Marked_U105(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U104(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U104(tt,V1,V2) > Marked_U105(isNat(activate(V1)),activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U103(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U102(tt,V1,V2) > Marked_isNatIListKind(activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: cons(X1,X2) >= n__cons(X1,X2) constraint: 0 >= n__0 constraint: zeros >= cons(0,n__zeros) constraint: zeros >= n__zeros constraint: U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatKind(n__0) >= tt constraint: isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) constraint: isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) constraint: activate(n__zeros) >= zeros constraint: activate(n__take(X1,X2)) >= take(X1,X2) constraint: activate(n__0) >= 0 constraint: activate(n__length(X)) >= length(X) constraint: activate(n__s(X)) >= s(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(n__nil) >= nil constraint: activate(X) >= X constraint: U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: isNatIListKind(n__zeros) >= tt constraint: isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)), activate(V2)) constraint: isNatIListKind(n__nil) >= tt constraint: U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) constraint: U105(tt,V2) >= U106(isNatIList(activate(V2))) constraint: isNat(n__0) >= tt constraint: isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)), activate(V1)) constraint: isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) constraint: U106(tt) >= tt constraint: isNatIList(n__zeros) >= tt constraint: isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) constraint: U12(tt,V1) >= U13(isNatList(activate(V1))) constraint: U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) constraint: U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) constraint: U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L), activate(N)) constraint: U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) constraint: U114(tt,L) >= s(length(activate(L))) constraint: s(X) >= n__s(X) constraint: length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) constraint: length(nil) >= 0 constraint: length(X) >= n__length(X) constraint: U13(tt) >= tt constraint: isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: isNatList(n__nil) >= tt constraint: U122(tt) >= nil constraint: U121(tt,IL) >= U122(isNatIListKind(activate(IL))) constraint: nil >= n__nil constraint: U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL), activate(M),activate(N)) constraint: U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) constraint: U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL), activate(M),activate(N)) constraint: U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL), activate(M),activate(N)) constraint: U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL), activate(M),activate(N)) constraint: U136(tt,IL,M,N) >= cons(activate(N), n__take(activate(M),activate(IL))) constraint: U22(tt,V1) >= U23(isNat(activate(V1))) constraint: U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) constraint: U23(tt) >= tt constraint: U32(tt,V) >= U33(isNatList(activate(V))) constraint: U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) constraint: U33(tt) >= tt constraint: U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) constraint: U45(tt,V2) >= U46(isNatIList(activate(V2))) constraint: U46(tt) >= tt constraint: U52(tt) >= tt constraint: U51(tt,V2) >= U52(isNatIListKind(activate(V2))) constraint: U62(tt) >= tt constraint: U61(tt,V2) >= U62(isNatIListKind(activate(V2))) constraint: U71(tt) >= tt constraint: U81(tt) >= tt constraint: U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1), activate(V2)) constraint: U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1), activate(V2)) constraint: U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) constraint: U95(tt,V2) >= U96(isNatList(activate(V2))) constraint: U96(tt) >= tt constraint: take(0,IL) >= U121(isNatIList(IL),IL) constraint: take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)), activate(IL),M,N) constraint: take(X1,X2) >= n__take(X1,X2) constraint: Marked_activate(n__take(X1,X2)) >= Marked_take(X1,X2) constraint: Marked_take(0,IL) >= Marked_isNatIList(IL) constraint: Marked_take(0,IL) >= Marked_U121(isNatIList(IL),IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_U131(isNatIList(activate(IL)), activate(IL),M,N) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U131(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U131(tt,IL,M,N) >= Marked_isNatIListKind(activate(IL)) constraint: Marked_U131(tt,IL,M,N) >= Marked_U132(isNatIListKind(activate(IL)), activate(IL),activate(M),activate(N)) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(isNatKind( activate( V1)), activate(V1),activate(V2)) constraint: Marked_isNatIList(V) >= Marked_activate(V) constraint: Marked_isNatIList(V) >= Marked_isNatIListKind(activate(V)) constraint: Marked_isNatIList(V) >= Marked_U31(isNatIListKind(activate(V)), activate(V)) constraint: Marked_U121(tt,IL) >= Marked_activate(IL) constraint: Marked_U121(tt,IL) >= Marked_isNatIListKind(activate(IL)) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_U101(isNatKind( activate( V1)), activate(V1),activate(V2)) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_U91(isNatKind( activate( V1)),activate(V1), activate(V2)) constraint: Marked_U101(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U101(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U101(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U101(tt,V1,V2) >= Marked_U102(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_isNatKind(n__s(V1)) >= Marked_activate(V1) constraint: Marked_isNatKind(n__s(V1)) >= Marked_isNatKind(activate(V1)) constraint: Marked_U91(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U91(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U91(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U91(tt,V1,V2) >= Marked_U92(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_isNatKind( activate(V1)) constraint: Marked_isNatIListKind(n__take(V1,V2)) >= Marked_U61(isNatKind( activate( V1)), activate(V2)) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V1) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_activate(V2) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_isNatKind( activate(V1)) constraint: Marked_isNatIListKind(n__cons(V1,V2)) >= Marked_U51(isNatKind( activate( V1)), activate(V2)) constraint: Marked_U61(tt,V2) >= Marked_activate(V2) constraint: Marked_U61(tt,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U51(tt,V2) >= Marked_activate(V2) constraint: Marked_U51(tt,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U41(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U41(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U41(tt,V1,V2) >= Marked_isNatKind(activate(V1)) constraint: Marked_U41(tt,V1,V2) >= Marked_U42(isNatKind(activate(V1)), activate(V1),activate(V2)) constraint: Marked_U31(tt,V) >= Marked_activate(V) constraint: Marked_U31(tt,V) >= Marked_isNatIListKind(activate(V)) constraint: Marked_U31(tt,V) >= Marked_U32(isNatIListKind(activate(V)), activate(V)) constraint: Marked_isNat(n__s(V1)) >= Marked_activate(V1) constraint: Marked_isNat(n__s(V1)) >= Marked_isNatKind(activate(V1)) constraint: Marked_isNat(n__s(V1)) >= Marked_U21(isNatKind(activate(V1)), activate(V1)) constraint: Marked_U21(tt,V1) >= Marked_activate(V1) constraint: Marked_U21(tt,V1) >= Marked_isNatKind(activate(V1)) constraint: Marked_U21(tt,V1) >= Marked_U22(isNatKind(activate(V1)), activate(V1)) constraint: Marked_U95(tt,V2) >= Marked_activate(V2) constraint: Marked_U95(tt,V2) >= Marked_isNatList(activate(V2)) constraint: Marked_U94(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U94(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U94(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U94(tt,V1,V2) >= Marked_U95(isNat(activate(V1)), activate(V2)) constraint: Marked_U93(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U93(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U93(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U93(tt,V1,V2) >= Marked_U94(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U92(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U92(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U92(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U92(tt,V1,V2) >= Marked_U93(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U45(tt,V2) >= Marked_activate(V2) constraint: Marked_U45(tt,V2) >= Marked_isNatIList(activate(V2)) constraint: Marked_U44(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U44(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U44(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U44(tt,V1,V2) >= Marked_U45(isNat(activate(V1)), activate(V2)) constraint: Marked_U43(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U43(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U43(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U43(tt,V1,V2) >= Marked_U44(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U42(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U42(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U42(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U42(tt,V1,V2) >= Marked_U43(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U32(tt,V) >= Marked_activate(V) constraint: Marked_U32(tt,V) >= Marked_isNatList(activate(V)) constraint: Marked_U22(tt,V1) >= Marked_activate(V1) constraint: Marked_U22(tt,V1) >= Marked_isNat(activate(V1)) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U136(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U135(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U135(tt,IL,M,N) >= Marked_isNatKind(activate(N)) constraint: Marked_U135(tt,IL,M,N) >= Marked_U136(isNatKind(activate(N)), activate(IL),activate(M),activate(N)) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U134(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U134(tt,IL,M,N) >= Marked_isNat(activate(N)) constraint: Marked_U134(tt,IL,M,N) >= Marked_U135(isNat(activate(N)), activate(IL),activate(M),activate(N)) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U133(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U133(tt,IL,M,N) >= Marked_isNatKind(activate(M)) constraint: Marked_U133(tt,IL,M,N) >= Marked_U134(isNatKind(activate(M)), activate(IL),activate(M),activate(N)) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(N) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U132(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U132(tt,IL,M,N) >= Marked_isNat(activate(M)) constraint: Marked_U132(tt,IL,M,N) >= Marked_U133(isNat(activate(M)), activate(IL),activate(M),activate(N)) constraint: Marked_U105(tt,V2) >= Marked_activate(V2) constraint: Marked_U105(tt,V2) >= Marked_isNatIList(activate(V2)) constraint: Marked_U104(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U104(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U104(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U104(tt,V1,V2) >= Marked_U105(isNat(activate(V1)), activate(V2)) constraint: Marked_U103(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U103(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U103(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U103(tt,V1,V2) >= Marked_U104(isNatIListKind(activate(V2)), activate(V1),activate(V2)) constraint: Marked_U102(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U102(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U102(tt,V1,V2) >= Marked_isNatIListKind(activate(V2)) constraint: Marked_U102(tt,V1,V2) >= Marked_U103(isNatIListKind(activate(V2)), activate(V1),activate(V2)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 5 components: { --> --> --> --> --> --> } { --> --> --> --> --> --> } { --> --> --> } { --> --> } { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U102(tt,V1,V2) >= U103(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= U71(isNatIListKind(activate(V1))) ; isNatKind(n__s(V1)) >= U81(isNatKind(activate(V1))) ; activate(n__zeros) >= zeros ; activate(n__take(X1,X2)) >= take(X1,X2) ; activate(n__0) >= 0 ; activate(n__length(X)) >= length(X) ; activate(n__s(X)) >= s(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(X) >= X ; U101(tt,V1,V2) >= U102(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U103(tt,V1,V2) >= U104(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= U61(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__cons(V1,V2)) >= U51(isNatKind(activate(V1)),activate(V2)) ; isNatIListKind(n__nil) >= tt ; U104(tt,V1,V2) >= U105(isNat(activate(V1)),activate(V2)) ; U105(tt,V2) >= U106(isNatIList(activate(V2))) ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U106(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U12(tt,V1) >= U13(isNatList(activate(V1))) ; U11(tt,V1) >= U12(isNatIListKind(activate(V1)),activate(V1)) ; U112(tt,L,N) >= U113(isNat(activate(N)),activate(L),activate(N)) ; U111(tt,L,N) >= U112(isNatIListKind(activate(L)),activate(L),activate(N)) ; U113(tt,L,N) >= U114(isNatKind(activate(N)),activate(L)) ; U114(tt,L) >= s(length(activate(L))) ; s(X) >= n__s(X) ; length(cons(N,L)) >= U111(isNatList(activate(L)),activate(L),N) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U13(tt) >= tt ; isNatList(n__take(V1,V2)) >= U101(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__cons(V1,V2)) >= U91(isNatKind(activate(V1)),activate(V1), activate(V2)) ; isNatList(n__nil) >= tt ; U122(tt) >= nil ; U121(tt,IL) >= U122(isNatIListKind(activate(IL))) ; nil >= n__nil ; U132(tt,IL,M,N) >= U133(isNat(activate(M)),activate(IL),activate(M), activate(N)) ; U131(tt,IL,M,N) >= U132(isNatIListKind(activate(IL)),activate(IL), activate(M),activate(N)) ; U133(tt,IL,M,N) >= U134(isNatKind(activate(M)),activate(IL),activate(M), activate(N)) ; U134(tt,IL,M,N) >= U135(isNat(activate(N)),activate(IL),activate(M), activate(N)) ; U135(tt,IL,M,N) >= U136(isNatKind(activate(N)),activate(IL),activate(M), activate(N)) ; U136(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; U22(tt,V1) >= U23(isNat(activate(V1))) ; U21(tt,V1) >= U22(isNatKind(activate(V1)),activate(V1)) ; U23(tt) >= tt ; U32(tt,V) >= U33(isNatList(activate(V))) ; U31(tt,V) >= U32(isNatIListKind(activate(V)),activate(V)) ; U33(tt) >= tt ; U42(tt,V1,V2) >= U43(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U41(tt,V1,V2) >= U42(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U43(tt,V1,V2) >= U44(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U44(tt,V1,V2) >= U45(isNat(activate(V1)),activate(V2)) ; U45(tt,V2) >= U46(isNatIList(activate(V2))) ; U46(tt) >= tt ; U52(tt) >= tt ; U51(tt,V2) >= U52(isNatIListKind(activate(V2))) ; U62(tt) >= tt ; U61(tt,V2) >= U62(isNatIListKind(activate(V2))) ; U71(tt) >= tt ; U81(tt) >= tt ; U92(tt,V1,V2) >= U93(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U91(tt,V1,V2) >= U92(isNatKind(activate(V1)),activate(V1),activate(V2)) ; U93(tt,V1,V2) >= U94(isNatIListKind(activate(V2)),activate(V1),activate(V2)) ; U94(tt,V1,V2) >= U95(isNat(activate(V1)),activate(V2)) ; U95(tt,V2) >= U96(isNatList(activate(V2))) ; U96(tt) >= tt ; take(0,IL) >= U121(isNatIList(IL),IL) ; take(s(M),cons(N,IL)) >= U131(isNatIList(activate(IL)),activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U45(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U44(tt,V1,V2) >= Marked_U45(isNat(activate(V1)),activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } + Disjunctions:{ { Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(isNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U45(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U44(tt,V1,V2) > Marked_U45(isNat(activate(V1)),activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_U44(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_U43(isNatIListKind(activate(V2)),activate(V1), activate(V2)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 96.721409 seconds (real time) Cime Exit Status: 0