- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] zeros -> cons(0,n__zeros) [2] U11(tt,V1) -> U12(isNatList(activate(V1))) [3] U12(tt) -> tt [4] U21(tt,V1) -> U22(isNat(activate(V1))) [5] U22(tt) -> tt [6] U31(tt,V) -> U32(isNatList(activate(V))) [7] U32(tt) -> tt [8] U41(tt,V1,V2) -> U42(isNat(activate(V1)),activate(V2)) [9] U42(tt,V2) -> U43(isNatIList(activate(V2))) [10] U43(tt) -> tt [11] U51(tt,V1,V2) -> U52(isNat(activate(V1)),activate(V2)) [12] U52(tt,V2) -> U53(isNatList(activate(V2))) [13] U53(tt) -> tt [14] U61(tt,V1,V2) -> U62(isNat(activate(V1)),activate(V2)) [15] U62(tt,V2) -> U63(isNatIList(activate(V2))) [16] U63(tt) -> tt [17] U71(tt,L) -> s(length(activate(L))) [18] U81(tt) -> nil [19] U91(tt,IL,M,N) -> cons(activate(N),n__take(activate(M),activate(IL))) [20] and(tt,X) -> activate(X) [21] isNat(n__0) -> tt [22] isNat(n__length(V1)) -> U11(isNatIListKind(activate(V1)),activate(V1)) [23] isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1)) [24] isNatIList(V) -> U31(isNatIListKind(activate(V)),activate(V)) [25] isNatIList(n__zeros) -> tt [26] isNatIList(n__cons(V1,V2)) -> U41(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1), activate(V2)) [27] isNatIListKind(n__nil) -> tt [28] isNatIListKind(n__zeros) -> tt [29] isNatIListKind(n__cons(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))) [30] isNatIListKind(n__take(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))) [31] isNatKind(n__0) -> tt [32] isNatKind(n__length(V1)) -> isNatIListKind(activate(V1)) [33] isNatKind(n__s(V1)) -> isNatKind(activate(V1)) [34] isNatList(n__nil) -> tt [35] isNatList(n__cons(V1,V2)) -> U51(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1), activate(V2)) [36] isNatList(n__take(V1,V2)) -> U61(and(isNatKind(activate(V1)),n__isNatIListKind(activate(V2))),activate(V1), activate(V2)) [37] length(nil) -> 0 [38] length(cons(N,L)) -> U71(and(and(isNatList(activate(L)),n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))),activate(L)) [39] take(0,IL) -> U81(and(isNatIList(IL),n__isNatIListKind(IL))) [40] take(s(M),cons(N,IL)) -> U91(and(and(isNatIList(activate(IL)),n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N)))), activate(IL),M,N) [41] zeros -> n__zeros [42] take(X1,X2) -> n__take(X1,X2) [43] 0 -> n__0 [44] length(X) -> n__length(X) [45] s(X) -> n__s(X) [46] cons(X1,X2) -> n__cons(X1,X2) [47] isNatIListKind(X) -> n__isNatIListKind(X) [48] nil -> n__nil [49] and(X1,X2) -> n__and(X1,X2) [50] isNatKind(X) -> n__isNatKind(X) [51] activate(n__zeros) -> zeros [52] activate(n__take(X1,X2)) -> take(X1,X2) [53] activate(n__0) -> 0 [54] activate(n__length(X)) -> length(X) [55] activate(n__s(X)) -> s(X) [56] activate(n__cons(X1,X2)) -> cons(X1,X2) [57] activate(n__isNatIListKind(X)) -> isNatIListKind(X) [58] activate(n__nil) -> nil [59] activate(n__and(X1,X2)) -> and(X1,X2) [60] activate(n__isNatKind(X)) -> isNatKind(X) [61] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) 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 ; U12(tt) >= tt ; isNatList(n__take(V1,V2)) >= U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__nil) >= tt ; 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__isNatIListKind(X)) >= isNatIListKind(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(n__and(X1,X2)) >= and(X1,X2) ; activate(n__isNatKind(X)) >= isNatKind(X) ; activate(X) >= X ; U11(tt,V1) >= U12(isNatList(activate(V1))) ; U22(tt) >= tt ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U21(tt,V1) >= U22(isNat(activate(V1))) ; U32(tt) >= tt ; U31(tt,V) >= U32(isNatList(activate(V))) ; U42(tt,V2) >= U43(isNatIList(activate(V2))) ; U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ; U43(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U52(tt,V2) >= U53(isNatList(activate(V2))) ; U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ; U53(tt) >= tt ; U62(tt,V2) >= U63(isNatIList(activate(V2))) ; U61(tt,V1,V2) >= U62(isNat(activate(V1)),activate(V2)) ; U63(tt) >= tt ; s(X) >= n__s(X) ; length(cons(N,L)) >= U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))),activate(L)) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U71(tt,L) >= s(length(activate(L))) ; nil >= n__nil ; U81(tt) >= nil ; U91(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__nil) >= tt ; isNatIListKind(X) >= n__isNatIListKind(X) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ; isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ; isNatKind(X) >= n__isNatKind(X) ; take(0,IL) >= U81(and(isNatIList(IL),n__isNatIListKind(IL))) ; take(s(M),cons(N,IL)) >= U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), 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_activate(n__isNatIListKind(X)) >= Marked_isNatIListKind(X) ; Marked_activate(n__and(X1,X2)) >= Marked_and(X1,X2) ; Marked_activate(n__isNatKind(X)) >= Marked_isNatKind(X) ; 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_and(tt,X) >= Marked_activate(X) ; 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_and(isNatKind(activate(V1)), n__isNatIListKind(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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; Marked_length(cons(N,L)) >= Marked_activate(L) ; Marked_length(cons(N,L)) >= Marked_and(isNatList(activate(L)), n__isNatIListKind(activate(L))) ; Marked_length(cons(N,L)) >= Marked_and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))) ; Marked_length(cons(N,L)) >= Marked_isNat(N) ; Marked_length(cons(N,L)) >= Marked_U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))), activate(L)) ; Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) ; Marked_take(0,IL) >= Marked_and(isNatIList(IL),n__isNatIListKind(IL)) ; Marked_take(0,IL) >= Marked_isNatIList(IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) ; Marked_take(s(M),cons(N,IL)) >= Marked_and(isNat(M),n__isNatKind(M)) ; Marked_take(s(M),cons(N,IL)) >= Marked_and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))) ; Marked_take(s(M),cons(N,IL)) >= Marked_and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))) ; Marked_take(s(M),cons(N,IL)) >= Marked_U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate( IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))) ,activate(IL),M,N) ; Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) ; Marked_take(s(M),cons(N,IL)) >= Marked_isNat(M) ; Marked_take(s(M),cons(N,IL)) >= Marked_isNat(N) ; Marked_U91(tt,IL,M,N) >= Marked_activate(IL) ; Marked_U91(tt,IL,M,N) >= Marked_activate(M) ; Marked_U91(tt,IL,M,N) >= Marked_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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind( activate(V2))), 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_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_U71(tt,L) >= Marked_activate(L) ; Marked_U71(tt,L) >= Marked_length(activate(L)) ; 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_isNatKind(activate(V1)) ; Marked_isNatList(n__take(V1,V2)) >= Marked_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; Marked_isNatList(n__take(V1,V2)) >= Marked_U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate( V2))), activate(V1),activate(V2)) ; 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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; Marked_isNatList(n__cons(V1,V2)) >= Marked_U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate( V2))), activate(V1),activate(V2)) ; Marked_U61(tt,V1,V2) >= Marked_activate(V1) ; Marked_U61(tt,V1,V2) >= Marked_activate(V2) ; Marked_U61(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U61(tt,V1,V2) >= Marked_U62(isNat(activate(V1)),activate(V2)) ; Marked_U51(tt,V1,V2) >= Marked_activate(V1) ; Marked_U51(tt,V1,V2) >= Marked_activate(V2) ; Marked_U51(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U51(tt,V1,V2) >= Marked_U52(isNat(activate(V1)),activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_activate(V1) ; Marked_U41(tt,V1,V2) >= Marked_activate(V2) ; Marked_U41(tt,V1,V2) >= Marked_isNat(activate(V1)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ; Marked_U31(tt,V) >= Marked_activate(V) ; Marked_U31(tt,V) >= Marked_isNatList(activate(V)) ; Marked_U21(tt,V1) >= Marked_activate(V1) ; Marked_U21(tt,V1) >= Marked_isNat(activate(V1)) ; Marked_U11(tt,V1) >= Marked_activate(V1) ; Marked_U11(tt,V1) >= Marked_isNatList(activate(V1)) ; Marked_U62(tt,V2) >= Marked_activate(V2) ; Marked_U62(tt,V2) >= Marked_isNatIList(activate(V2)) ; Marked_U52(tt,V2) >= Marked_activate(V2) ; Marked_U52(tt,V2) >= Marked_isNatList(activate(V2)) ; Marked_U42(tt,V2) >= Marked_activate(V2) ; Marked_U42(tt,V2) >= Marked_isNatIList(activate(V2)) ; } + Disjunctions:{ { Marked_activate(n__take(X1,X2)) > Marked_take(X1,X2) ; } { Marked_activate(n__length(X)) > Marked_length(X) ; } { Marked_activate(n__isNatIListKind(X)) > Marked_isNatIListKind(X) ; } { Marked_activate(n__and(X1,X2)) > Marked_and(X1,X2) ; } { Marked_activate(n__isNatKind(X)) > Marked_isNatKind(X) ; } { 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_and(tt,X) > Marked_activate(X) ; } { 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_and(isNatKind(activate(V1)), n__isNatIListKind(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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; } { Marked_length(cons(N,L)) > Marked_activate(L) ; } { Marked_length(cons(N,L)) > Marked_and(isNatList(activate(L)), n__isNatIListKind(activate(L))) ; } { Marked_length(cons(N,L)) > Marked_and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))) ; } { Marked_length(cons(N,L)) > Marked_isNat(N) ; } { Marked_length(cons(N,L)) > Marked_U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))), activate(L)) ; } { Marked_length(cons(N,L)) > Marked_isNatList(activate(L)) ; } { Marked_take(0,IL) > Marked_and(isNatIList(IL),n__isNatIListKind(IL)) ; } { Marked_take(0,IL) > Marked_isNatIList(IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_activate(IL) ; } { Marked_take(s(M),cons(N,IL)) > Marked_and(isNat(M),n__isNatKind(M)) ; } { Marked_take(s(M),cons(N,IL)) > Marked_and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))) ; } { Marked_take(s(M),cons(N,IL)) > Marked_and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))) ; } { Marked_take(s(M),cons(N,IL)) > Marked_U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))) , n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), activate(IL),M,N) ; } { Marked_take(s(M),cons(N,IL)) > Marked_isNatIList(activate(IL)) ; } { Marked_take(s(M),cons(N,IL)) > Marked_isNat(M) ; } { Marked_take(s(M),cons(N,IL)) > Marked_isNat(N) ; } { Marked_U91(tt,IL,M,N) > Marked_activate(IL) ; } { Marked_U91(tt,IL,M,N) > Marked_activate(M) ; } { Marked_U91(tt,IL,M,N) > Marked_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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; } { Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate( V2))), 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_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_U71(tt,L) > Marked_activate(L) ; } { Marked_U71(tt,L) > Marked_length(activate(L)) ; } { 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_isNatKind(activate(V1)) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; } { Marked_isNatList(n__take(V1,V2)) > Marked_U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ,activate(V1),activate(V2)) ; } { 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_and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; } { Marked_isNatList(n__cons(V1,V2)) > Marked_U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ,activate(V1),activate(V2)) ; } { Marked_U61(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U61(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U61(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U61(tt,V1,V2) > Marked_U62(isNat(activate(V1)),activate(V2)) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U51(tt,V1,V2) > Marked_U52(isNat(activate(V1)),activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U41(tt,V1,V2) > Marked_isNat(activate(V1)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNat(activate(V1)),activate(V2)) ; } { Marked_U31(tt,V) > Marked_activate(V) ; } { Marked_U31(tt,V) > Marked_isNatList(activate(V)) ; } { Marked_U21(tt,V1) > Marked_activate(V1) ; } { Marked_U21(tt,V1) > Marked_isNat(activate(V1)) ; } { Marked_U11(tt,V1) > Marked_activate(V1) ; } { Marked_U11(tt,V1) > Marked_isNatList(activate(V1)) ; } { Marked_U62(tt,V2) > Marked_activate(V2) ; } { Marked_U62(tt,V2) > Marked_isNatIList(activate(V2)) ; } { Marked_U52(tt,V2) > Marked_activate(V2) ; } { Marked_U52(tt,V2) > Marked_isNatList(activate(V2)) ; } { Marked_U42(tt,V2) > Marked_activate(V2) ; } { Marked_U42(tt,V2) > Marked_isNatIList(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: U12(tt) >= tt constraint: isNatList(n__take(V1,V2)) >= U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) constraint: isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) constraint: isNatList(n__nil) >= tt 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__isNatIListKind(X)) >= isNatIListKind(X) constraint: activate(n__cons(X1,X2)) >= cons(X1,X2) constraint: activate(n__nil) >= nil constraint: activate(n__and(X1,X2)) >= and(X1,X2) constraint: activate(n__isNatKind(X)) >= isNatKind(X) constraint: activate(X) >= X constraint: U11(tt,V1) >= U12(isNatList(activate(V1))) constraint: U22(tt) >= tt 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: U21(tt,V1) >= U22(isNat(activate(V1))) constraint: U32(tt) >= tt constraint: U31(tt,V) >= U32(isNatList(activate(V))) constraint: U42(tt,V2) >= U43(isNatIList(activate(V2))) constraint: U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) constraint: U43(tt) >= tt constraint: isNatIList(n__zeros) >= tt constraint: isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) constraint: isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) constraint: U52(tt,V2) >= U53(isNatList(activate(V2))) constraint: U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) constraint: U53(tt) >= tt constraint: U62(tt,V2) >= U63(isNatIList(activate(V2))) constraint: U61(tt,V1,V2) >= U62(isNat(activate(V1)),activate(V2)) constraint: U63(tt) >= tt constraint: s(X) >= n__s(X) constraint: length(cons(N,L)) >= U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))), activate(L)) constraint: length(nil) >= 0 constraint: length(X) >= n__length(X) constraint: U71(tt,L) >= s(length(activate(L))) constraint: nil >= n__nil constraint: U81(tt) >= nil constraint: U91(tt,IL,M,N) >= cons(activate(N), n__take(activate(M),activate(IL))) constraint: and(tt,X) >= activate(X) constraint: and(X1,X2) >= n__and(X1,X2) constraint: isNatIListKind(n__zeros) >= tt constraint: isNatIListKind(n__take(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) constraint: isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) constraint: isNatIListKind(n__nil) >= tt constraint: isNatIListKind(X) >= n__isNatIListKind(X) constraint: isNatKind(n__0) >= tt constraint: isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) constraint: isNatKind(n__s(V1)) >= isNatKind(activate(V1)) constraint: isNatKind(X) >= n__isNatKind(X) constraint: take(0,IL) >= U81(and(isNatIList(IL),n__isNatIListKind(IL))) constraint: take(s(M),cons(N,IL)) >= U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), 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_activate(n__isNatIListKind(X)) >= Marked_isNatIListKind(X) constraint: Marked_activate(n__and(X1,X2)) >= Marked_and(X1,X2) constraint: Marked_activate(n__isNatKind(X)) >= Marked_isNatKind(X) 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_and(tt,X) >= Marked_activate(X) 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_and(isNatKind( activate( V1)), n__isNatIListKind( 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_and(isNatKind( activate( V1)), n__isNatIListKind( activate(V2))) constraint: Marked_length(cons(N,L)) >= Marked_activate(L) constraint: Marked_length(cons(N,L)) >= Marked_and(isNatList(activate(L)), n__isNatIListKind(activate(L))) constraint: Marked_length(cons(N,L)) >= Marked_and(and(isNatList(activate(L)), n__isNatIListKind( activate(L))), n__and(isNat(N),n__isNatKind(N))) constraint: Marked_length(cons(N,L)) >= Marked_isNat(N) constraint: Marked_length(cons(N,L)) >= Marked_U71(and(and(isNatList( activate( L)), n__isNatIListKind( activate(L))), n__and(isNat(N), n__isNatKind(N))), activate(L)) constraint: Marked_length(cons(N,L)) >= Marked_isNatList(activate(L)) constraint: Marked_take(0,IL) >= Marked_and(isNatIList(IL), n__isNatIListKind(IL)) constraint: Marked_take(0,IL) >= Marked_isNatIList(IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_activate(IL) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_and(isNat(M), n__isNatKind(M)) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_and(and(isNatIList( activate( IL)), n__isNatIListKind( activate(IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_U91(and(and(isNatIList( activate( IL)), n__isNatIListKind( activate( IL))), n__and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N)))), activate(IL),M,N) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_isNatIList(activate(IL)) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_isNat(M) constraint: Marked_take(s(M),cons(N,IL)) >= Marked_isNat(N) constraint: Marked_U91(tt,IL,M,N) >= Marked_activate(IL) constraint: Marked_U91(tt,IL,M,N) >= Marked_activate(M) constraint: Marked_U91(tt,IL,M,N) >= Marked_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_and(isNatKind( activate( V1)), n__isNatIListKind(activate( V2))) constraint: Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind( activate( V1)), n__isNatIListKind( activate( V2))), 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_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_U71(tt,L) >= Marked_activate(L) constraint: Marked_U71(tt,L) >= Marked_length(activate(L)) 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_isNatKind(activate(V1)) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_and(isNatKind( activate( V1)), n__isNatIListKind(activate(V2))) constraint: Marked_isNatList(n__take(V1,V2)) >= Marked_U61(and(isNatKind( activate( V1)), n__isNatIListKind( activate( V2))), activate(V1),activate(V2)) 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_and(isNatKind( activate( V1)), n__isNatIListKind(activate(V2))) constraint: Marked_isNatList(n__cons(V1,V2)) >= Marked_U51(and(isNatKind( activate( V1)), n__isNatIListKind( activate( V2))), activate(V1),activate(V2)) constraint: Marked_U61(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U61(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U61(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U61(tt,V1,V2) >= Marked_U62(isNat(activate(V1)), activate(V2)) constraint: Marked_U51(tt,V1,V2) >= Marked_activate(V1) constraint: Marked_U51(tt,V1,V2) >= Marked_activate(V2) constraint: Marked_U51(tt,V1,V2) >= Marked_isNat(activate(V1)) constraint: Marked_U51(tt,V1,V2) >= Marked_U52(isNat(activate(V1)), 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_isNat(activate(V1)) constraint: Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)), activate(V2)) constraint: Marked_U31(tt,V) >= Marked_activate(V) constraint: Marked_U31(tt,V) >= Marked_isNatList(activate(V)) constraint: Marked_U21(tt,V1) >= Marked_activate(V1) constraint: Marked_U21(tt,V1) >= Marked_isNat(activate(V1)) constraint: Marked_U11(tt,V1) >= Marked_activate(V1) constraint: Marked_U11(tt,V1) >= Marked_isNatList(activate(V1)) constraint: Marked_U62(tt,V2) >= Marked_activate(V2) constraint: Marked_U62(tt,V2) >= Marked_isNatIList(activate(V2)) constraint: Marked_U52(tt,V2) >= Marked_activate(V2) constraint: Marked_U52(tt,V2) >= Marked_isNatList(activate(V2)) constraint: Marked_U42(tt,V2) >= Marked_activate(V2) constraint: Marked_U42(tt,V2) >= Marked_isNatIList(activate(V2)) APPLY CRITERIA (Graph splitting) Found 5 components: { --> --> --> } { --> --> --> } { --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> } APPLY CRITERIA (Subterm criterion) 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 ; U12(tt) >= tt ; isNatList(n__take(V1,V2)) >= U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__nil) >= tt ; 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__isNatIListKind(X)) >= isNatIListKind(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(n__and(X1,X2)) >= and(X1,X2) ; activate(n__isNatKind(X)) >= isNatKind(X) ; activate(X) >= X ; U11(tt,V1) >= U12(isNatList(activate(V1))) ; U22(tt) >= tt ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U21(tt,V1) >= U22(isNat(activate(V1))) ; U32(tt) >= tt ; U31(tt,V) >= U32(isNatList(activate(V))) ; U42(tt,V2) >= U43(isNatIList(activate(V2))) ; U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ; U43(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U52(tt,V2) >= U53(isNatList(activate(V2))) ; U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ; U53(tt) >= tt ; U62(tt,V2) >= U63(isNatIList(activate(V2))) ; U61(tt,V1,V2) >= U62(isNat(activate(V1)),activate(V2)) ; U63(tt) >= tt ; s(X) >= n__s(X) ; length(cons(N,L)) >= U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))),activate(L)) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U71(tt,L) >= s(length(activate(L))) ; nil >= n__nil ; U81(tt) >= nil ; U91(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__nil) >= tt ; isNatIListKind(X) >= n__isNatIListKind(X) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ; isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ; isNatKind(X) >= n__isNatKind(X) ; take(0,IL) >= U81(and(isNatIList(IL),n__isNatIListKind(IL))) ; take(s(M),cons(N,IL)) >= U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind( activate(V2))), activate(V1),activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ; Marked_U42(tt,V2) >= Marked_isNatIList(activate(V2)) ; } + Disjunctions:{ { Marked_isNatIList(n__cons(V1,V2)) > Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate( V2))), activate(V1),activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNat(activate(V1)),activate(V2)) ; } { Marked_U42(tt,V2) > Marked_isNatIList(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 === STOPING TIMER virtual === Time out 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 (Simple graph) Found the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U12(tt) >= tt ; isNatList(n__take(V1,V2)) >= U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__nil) >= tt ; 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__isNatIListKind(X)) >= isNatIListKind(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(n__and(X1,X2)) >= and(X1,X2) ; activate(n__isNatKind(X)) >= isNatKind(X) ; activate(X) >= X ; U11(tt,V1) >= U12(isNatList(activate(V1))) ; U22(tt) >= tt ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U21(tt,V1) >= U22(isNat(activate(V1))) ; U32(tt) >= tt ; U31(tt,V) >= U32(isNatList(activate(V))) ; U42(tt,V2) >= U43(isNatIList(activate(V2))) ; U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ; U43(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U52(tt,V2) >= U53(isNatList(activate(V2))) ; U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ; U53(tt) >= tt ; U62(tt,V2) >= U63(isNatIList(activate(V2))) ; U61(tt,V1,V2) >= U62(isNat(activate(V1)),activate(V2)) ; U63(tt) >= tt ; s(X) >= n__s(X) ; length(cons(N,L)) >= U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))),activate(L)) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U71(tt,L) >= s(length(activate(L))) ; nil >= n__nil ; U81(tt) >= nil ; U91(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__nil) >= tt ; isNatIListKind(X) >= n__isNatIListKind(X) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ; isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ; isNatKind(X) >= n__isNatKind(X) ; take(0,IL) >= U81(and(isNatIList(IL),n__isNatIListKind(IL))) ; take(s(M),cons(N,IL)) >= U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind( activate(V2))), activate(V1),activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ; Marked_U42(tt,V2) > Marked_isNatIList(activate(V2)) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { cons(X1,X2) >= n__cons(X1,X2) ; 0 >= n__0 ; zeros >= cons(0,n__zeros) ; zeros >= n__zeros ; U12(tt) >= tt ; isNatList(n__take(V1,V2)) >= U61(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__cons(V1,V2)) >= U51(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatList(n__nil) >= tt ; 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__isNatIListKind(X)) >= isNatIListKind(X) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__nil) >= nil ; activate(n__and(X1,X2)) >= and(X1,X2) ; activate(n__isNatKind(X)) >= isNatKind(X) ; activate(X) >= X ; U11(tt,V1) >= U12(isNatList(activate(V1))) ; U22(tt) >= tt ; isNat(n__0) >= tt ; isNat(n__length(V1)) >= U11(isNatIListKind(activate(V1)),activate(V1)) ; isNat(n__s(V1)) >= U21(isNatKind(activate(V1)),activate(V1)) ; U21(tt,V1) >= U22(isNat(activate(V1))) ; U32(tt) >= tt ; U31(tt,V) >= U32(isNatList(activate(V))) ; U42(tt,V2) >= U43(isNatIList(activate(V2))) ; U41(tt,V1,V2) >= U42(isNat(activate(V1)),activate(V2)) ; U43(tt) >= tt ; isNatIList(n__zeros) >= tt ; isNatIList(n__cons(V1,V2)) >= U41(and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))), activate(V1),activate(V2)) ; isNatIList(V) >= U31(isNatIListKind(activate(V)),activate(V)) ; U52(tt,V2) >= U53(isNatList(activate(V2))) ; U51(tt,V1,V2) >= U52(isNat(activate(V1)),activate(V2)) ; U53(tt) >= tt ; U62(tt,V2) >= U63(isNatIList(activate(V2))) ; U61(tt,V1,V2) >= U62(isNat(activate(V1)),activate(V2)) ; U63(tt) >= tt ; s(X) >= n__s(X) ; length(cons(N,L)) >= U71(and(and(isNatList(activate(L)), n__isNatIListKind(activate(L))), n__and(isNat(N),n__isNatKind(N))),activate(L)) ; length(nil) >= 0 ; length(X) >= n__length(X) ; U71(tt,L) >= s(length(activate(L))) ; nil >= n__nil ; U81(tt) >= nil ; U91(tt,IL,M,N) >= cons(activate(N),n__take(activate(M),activate(IL))) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNatIListKind(n__zeros) >= tt ; isNatIListKind(n__take(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__cons(V1,V2)) >= and(isNatKind(activate(V1)), n__isNatIListKind(activate(V2))) ; isNatIListKind(n__nil) >= tt ; isNatIListKind(X) >= n__isNatIListKind(X) ; isNatKind(n__0) >= tt ; isNatKind(n__length(V1)) >= isNatIListKind(activate(V1)) ; isNatKind(n__s(V1)) >= isNatKind(activate(V1)) ; isNatKind(X) >= n__isNatKind(X) ; take(0,IL) >= U81(and(isNatIList(IL),n__isNatIListKind(IL))) ; take(s(M),cons(N,IL)) >= U91(and(and(isNatIList(activate(IL)), n__isNatIListKind(activate(IL))), n__and(and(isNat(M),n__isNatKind(M)), n__and(isNat(N),n__isNatKind(N)))), activate(IL),M,N) ; take(X1,X2) >= n__take(X1,X2) ; Marked_isNatIList(n__cons(V1,V2)) >= Marked_U41(and(isNatKind(activate(V1)), n__isNatIListKind( activate(V2))), activate(V1),activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNat(activate(V1)),activate(V2)) ; Marked_U42(tt,V2) > Marked_isNatIList(activate(V2)) ; } + Disjunctions:{ } === 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 === STOPING TIMER virtual === Time out 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 220.652299 seconds (real time) Cime Exit Status: 0