- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(and(tt,T)) -> mark(T) [2] active(isNatIList(IL)) -> mark(isNatList(IL)) [3] active(isNat(0)) -> mark(tt) [4] active(isNat(s(N))) -> mark(isNat(N)) [5] active(isNat(length(L))) -> mark(isNatList(L)) [6] active(isNatIList(zeros)) -> mark(tt) [7] active(isNatIList(cons(N,IL))) -> mark(and(isNat(N),isNatIList(IL))) [8] active(isNatList(nil)) -> mark(tt) [9] active(isNatList(cons(N,L))) -> mark(and(isNat(N),isNatList(L))) [10] active(isNatList(take(N,IL))) -> mark(and(isNat(N),isNatIList(IL))) [11] active(zeros) -> mark(cons(0,zeros)) [12] active(take(0,IL)) -> mark(uTake1(isNatIList(IL))) [13] active(uTake1(tt)) -> mark(nil) [14] active(take(s(M),cons(N,IL))) -> mark(uTake2(and(isNat(M),and(isNat(N),isNatIList(IL))),M,N,IL)) [15] active(uTake2(tt,M,N,IL)) -> mark(cons(N,take(M,IL))) [16] active(length(cons(N,L))) -> mark(uLength(and(isNat(N),isNatList(L)),L)) [17] active(uLength(tt,L)) -> mark(s(length(L))) [18] mark(and(X1,X2)) -> active(and(mark(X1),mark(X2))) [19] mark(tt) -> active(tt) [20] mark(isNatIList(X)) -> active(isNatIList(X)) [21] mark(isNatList(X)) -> active(isNatList(X)) [22] mark(isNat(X)) -> active(isNat(X)) [23] mark(0) -> active(0) [24] mark(s(X)) -> active(s(mark(X))) [25] mark(length(X)) -> active(length(mark(X))) [26] mark(zeros) -> active(zeros) [27] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [28] mark(nil) -> active(nil) [29] mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) [30] mark(uTake1(X)) -> active(uTake1(mark(X))) [31] mark(uTake2(X1,X2,X3,X4)) -> active(uTake2(mark(X1),X2,X3,X4)) [32] mark(uLength(X1,X2)) -> active(uLength(mark(X1),X2)) [33] and(mark(X1),X2) -> and(X1,X2) [34] and(X1,mark(X2)) -> and(X1,X2) [35] and(active(X1),X2) -> and(X1,X2) [36] and(X1,active(X2)) -> and(X1,X2) [37] isNatIList(mark(X)) -> isNatIList(X) [38] isNatIList(active(X)) -> isNatIList(X) [39] isNatList(mark(X)) -> isNatList(X) [40] isNatList(active(X)) -> isNatList(X) [41] isNat(mark(X)) -> isNat(X) [42] isNat(active(X)) -> isNat(X) [43] s(mark(X)) -> s(X) [44] s(active(X)) -> s(X) [45] length(mark(X)) -> length(X) [46] length(active(X)) -> length(X) [47] cons(mark(X1),X2) -> cons(X1,X2) [48] cons(X1,mark(X2)) -> cons(X1,X2) [49] cons(active(X1),X2) -> cons(X1,X2) [50] cons(X1,active(X2)) -> cons(X1,X2) [51] take(mark(X1),X2) -> take(X1,X2) [52] take(X1,mark(X2)) -> take(X1,X2) [53] take(active(X1),X2) -> take(X1,X2) [54] take(X1,active(X2)) -> take(X1,X2) [55] uTake1(mark(X)) -> uTake1(X) [56] uTake1(active(X)) -> uTake1(X) [57] uTake2(mark(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4) [58] uTake2(X1,mark(X2),X3,X4) -> uTake2(X1,X2,X3,X4) [59] uTake2(X1,X2,mark(X3),X4) -> uTake2(X1,X2,X3,X4) [60] uTake2(X1,X2,X3,mark(X4)) -> uTake2(X1,X2,X3,X4) [61] uTake2(active(X1),X2,X3,X4) -> uTake2(X1,X2,X3,X4) [62] uTake2(X1,active(X2),X3,X4) -> uTake2(X1,X2,X3,X4) [63] uTake2(X1,X2,active(X3),X4) -> uTake2(X1,X2,X3,X4) [64] uTake2(X1,X2,X3,active(X4)) -> uTake2(X1,X2,X3,X4) [65] uLength(mark(X1),X2) -> uLength(X1,X2) [66] uLength(X1,mark(X2)) -> uLength(X1,X2) [67] uLength(active(X1),X2) -> uLength(X1,X2) [68] uLength(X1,active(X2)) -> uLength(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 12 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(and(X1,X2)) >= active(and(mark(X1),mark(X2))) ; mark(tt) >= active(tt) ; mark(isNatList(X)) >= active(isNatList(X)) ; mark(isNatIList(X)) >= active(isNatIList(X)) ; mark(isNat(X)) >= active(isNat(X)) ; mark(0) >= active(0) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(zeros) >= active(zeros) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(uTake1(X)) >= active(uTake1(mark(X))) ; mark(uTake2(X1,X2,X3,X4)) >= active(uTake2(mark(X1),X2,X3,X4)) ; mark(uLength(X1,X2)) >= active(uLength(mark(X1),X2)) ; active(and(tt,T)) >= mark(T) ; active(isNatList(cons(N,L))) >= mark(and(isNat(N),isNatList(L))) ; active(isNatList(nil)) >= mark(tt) ; active(isNatList(take(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) ; active(isNatIList(zeros)) >= mark(tt) ; active(isNatIList(cons(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) ; active(isNatIList(IL)) >= mark(isNatList(IL)) ; active(isNat(0)) >= mark(tt) ; active(isNat(s(N))) >= mark(isNat(N)) ; active(isNat(length(L))) >= mark(isNatList(L)) ; active(length(cons(N,L))) >= mark(uLength(and(isNat(N),isNatList(L)),L)) ; active(zeros) >= mark(cons(0,zeros)) ; active(take(0,IL)) >= mark(uTake1(isNatIList(IL))) ; active(take(s(M),cons(N,IL))) >= mark(uTake2(and(isNat(M), and(isNat(N),isNatIList(IL))), M,N,IL)) ; active(uTake1(tt)) >= mark(nil) ; active(uTake2(tt,M,N,IL)) >= mark(cons(N,take(M,IL))) ; active(uLength(tt,L)) >= mark(s(length(L))) ; and(mark(X1),X2) >= and(X1,X2) ; and(active(X1),X2) >= and(X1,X2) ; and(X1,mark(X2)) >= and(X1,X2) ; and(X1,active(X2)) >= and(X1,X2) ; isNatList(mark(X)) >= isNatList(X) ; isNatList(active(X)) >= isNatList(X) ; isNatIList(mark(X)) >= isNatIList(X) ; isNatIList(active(X)) >= isNatIList(X) ; isNat(mark(X)) >= isNat(X) ; isNat(active(X)) >= isNat(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; take(mark(X1),X2) >= take(X1,X2) ; take(active(X1),X2) >= take(X1,X2) ; take(X1,mark(X2)) >= take(X1,X2) ; take(X1,active(X2)) >= take(X1,X2) ; uTake1(mark(X)) >= uTake1(X) ; uTake1(active(X)) >= uTake1(X) ; uTake2(mark(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(active(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,mark(X2),X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,active(X2),X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,mark(X3),X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,active(X3),X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,X3,mark(X4)) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,X3,active(X4)) >= uTake2(X1,X2,X3,X4) ; uLength(mark(X1),X2) >= uLength(X1,X2) ; uLength(active(X1),X2) >= uLength(X1,X2) ; uLength(X1,mark(X2)) >= uLength(X1,X2) ; uLength(X1,active(X2)) >= uLength(X1,X2) ; Marked_mark(and(X1,X2)) >= Marked_mark(X1) ; Marked_mark(and(X1,X2)) >= Marked_mark(X2) ; Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),mark(X2))) ; Marked_mark(isNatList(X)) >= Marked_active(isNatList(X)) ; Marked_mark(isNatIList(X)) >= Marked_active(isNatIList(X)) ; Marked_mark(isNat(X)) >= Marked_active(isNat(X)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(length(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(uTake1(X)) >= Marked_mark(X) ; Marked_mark(uTake1(X)) >= Marked_active(uTake1(mark(X))) ; Marked_mark(uTake2(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(uTake2(X1,X2,X3,X4)) >= Marked_active(uTake2(mark(X1),X2,X3,X4)) ; Marked_mark(uLength(X1,X2)) >= Marked_mark(X1) ; Marked_mark(uLength(X1,X2)) >= Marked_active(uLength(mark(X1),X2)) ; Marked_active(and(tt,T)) >= Marked_mark(T) ; Marked_active(isNatList(cons(N,L))) >= Marked_mark(and(isNat(N),isNatList(L))) ; Marked_active(isNatList(take(N,IL))) >= Marked_mark(and(isNat(N), isNatIList(IL))) ; Marked_active(isNatIList(cons(N,IL))) >= Marked_mark(and(isNat(N), isNatIList(IL))) ; Marked_active(isNatIList(IL)) >= Marked_mark(isNatList(IL)) ; Marked_active(isNat(s(N))) >= Marked_mark(isNat(N)) ; Marked_active(isNat(length(L))) >= Marked_mark(isNatList(L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(uLength(and(isNat(N), isNatList(L)), L)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(take(0,IL)) >= Marked_mark(uTake1(isNatIList(IL))) ; Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M,N,IL)) ; Marked_active(uTake2(tt,M,N,IL)) >= Marked_mark(cons(N,take(M,IL))) ; Marked_active(uLength(tt,L)) >= Marked_mark(s(length(L))) ; } + Disjunctions:{ { Marked_mark(and(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(and(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(and(X1,X2)) > Marked_active(and(mark(X1),mark(X2))) ; } { Marked_mark(isNatList(X)) > Marked_active(isNatList(X)) ; } { Marked_mark(isNatIList(X)) > Marked_active(isNatIList(X)) ; } { Marked_mark(isNat(X)) > Marked_active(isNat(X)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(length(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(uTake1(X)) > Marked_mark(X) ; } { Marked_mark(uTake1(X)) > Marked_active(uTake1(mark(X))) ; } { Marked_mark(uTake2(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(uTake2(X1,X2,X3,X4)) > Marked_active(uTake2(mark(X1),X2,X3,X4)) ; } { Marked_mark(uLength(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(uLength(X1,X2)) > Marked_active(uLength(mark(X1),X2)) ; } { Marked_active(and(tt,T)) > Marked_mark(T) ; } { Marked_active(isNatList(cons(N,L))) > Marked_mark(and(isNat(N),isNatList(L))) ; } { Marked_active(isNatList(take(N,IL))) > Marked_mark(and(isNat(N), isNatIList(IL))) ; } { Marked_active(isNatIList(cons(N,IL))) > Marked_mark(and(isNat(N), isNatIList(IL))) ; } { Marked_active(isNatIList(IL)) > Marked_mark(isNatList(IL)) ; } { Marked_active(isNat(s(N))) > Marked_mark(isNat(N)) ; } { Marked_active(isNat(length(L))) > Marked_mark(isNatList(L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(uLength(and(isNat(N), isNatList(L)), L)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(take(0,IL)) > Marked_mark(uTake1(isNatIList(IL))) ; } { Marked_active(take(s(M),cons(N,IL))) > Marked_mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M,N,IL)) ; } { Marked_active(uTake2(tt,M,N,IL)) > Marked_mark(cons(N,take(M,IL))) ; } { Marked_active(uLength(tt,L)) > Marked_mark(s(length(L))) ; } } === 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: mark(and(X1,X2)) >= active(and(mark(X1),mark(X2))) constraint: mark(tt) >= active(tt) constraint: mark(isNatList(X)) >= active(isNatList(X)) constraint: mark(isNatIList(X)) >= active(isNatIList(X)) constraint: mark(isNat(X)) >= active(isNat(X)) constraint: mark(0) >= active(0) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(zeros) >= active(zeros) constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(uTake1(X)) >= active(uTake1(mark(X))) constraint: mark(uTake2(X1,X2,X3,X4)) >= active(uTake2(mark(X1),X2,X3,X4)) constraint: mark(uLength(X1,X2)) >= active(uLength(mark(X1),X2)) constraint: active(and(tt,T)) >= mark(T) constraint: active(isNatList(cons(N,L))) >= mark(and(isNat(N),isNatList(L))) constraint: active(isNatList(nil)) >= mark(tt) constraint: active(isNatList(take(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) constraint: active(isNatIList(zeros)) >= mark(tt) constraint: active(isNatIList(cons(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) constraint: active(isNatIList(IL)) >= mark(isNatList(IL)) constraint: active(isNat(0)) >= mark(tt) constraint: active(isNat(s(N))) >= mark(isNat(N)) constraint: active(isNat(length(L))) >= mark(isNatList(L)) constraint: active(length(cons(N,L))) >= mark(uLength(and(isNat(N), isNatList(L)), L)) constraint: active(zeros) >= mark(cons(0,zeros)) constraint: active(take(0,IL)) >= mark(uTake1(isNatIList(IL))) constraint: active(take(s(M),cons(N,IL))) >= mark(uTake2(and(isNat(M), and(isNat(N), isNatIList(IL))), M,N,IL)) constraint: active(uTake1(tt)) >= mark(nil) constraint: active(uTake2(tt,M,N,IL)) >= mark(cons(N,take(M,IL))) constraint: active(uLength(tt,L)) >= mark(s(length(L))) constraint: and(mark(X1),X2) >= and(X1,X2) constraint: and(active(X1),X2) >= and(X1,X2) constraint: and(X1,mark(X2)) >= and(X1,X2) constraint: and(X1,active(X2)) >= and(X1,X2) constraint: isNatList(mark(X)) >= isNatList(X) constraint: isNatList(active(X)) >= isNatList(X) constraint: isNatIList(mark(X)) >= isNatIList(X) constraint: isNatIList(active(X)) >= isNatIList(X) constraint: isNat(mark(X)) >= isNat(X) constraint: isNat(active(X)) >= isNat(X) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: length(mark(X)) >= length(X) constraint: length(active(X)) >= length(X) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: take(mark(X1),X2) >= take(X1,X2) constraint: take(active(X1),X2) >= take(X1,X2) constraint: take(X1,mark(X2)) >= take(X1,X2) constraint: take(X1,active(X2)) >= take(X1,X2) constraint: uTake1(mark(X)) >= uTake1(X) constraint: uTake1(active(X)) >= uTake1(X) constraint: uTake2(mark(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(active(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,mark(X2),X3,X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,active(X2),X3,X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,X2,mark(X3),X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,X2,active(X3),X4) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,X2,X3,mark(X4)) >= uTake2(X1,X2,X3,X4) constraint: uTake2(X1,X2,X3,active(X4)) >= uTake2(X1,X2,X3,X4) constraint: uLength(mark(X1),X2) >= uLength(X1,X2) constraint: uLength(active(X1),X2) >= uLength(X1,X2) constraint: uLength(X1,mark(X2)) >= uLength(X1,X2) constraint: uLength(X1,active(X2)) >= uLength(X1,X2) constraint: Marked_mark(and(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(and(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),mark(X2))) constraint: Marked_mark(isNatList(X)) >= Marked_active(isNatList(X)) constraint: Marked_mark(isNatIList(X)) >= Marked_active(isNatIList(X)) constraint: Marked_mark(isNat(X)) >= Marked_active(isNat(X)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(length(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(uTake1(X)) >= Marked_mark(X) constraint: Marked_mark(uTake1(X)) >= Marked_active(uTake1(mark(X))) constraint: Marked_mark(uTake2(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(uTake2(X1,X2,X3,X4)) >= Marked_active(uTake2( mark(X1), X2,X3, X4)) constraint: Marked_mark(uLength(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(uLength(X1,X2)) >= Marked_active(uLength(mark(X1),X2)) constraint: Marked_active(and(tt,T)) >= Marked_mark(T) constraint: Marked_active(isNatList(cons(N,L))) >= Marked_mark(and(isNat(N), isNatList(L))) constraint: Marked_active(isNatList(take(N,IL))) >= Marked_mark(and(isNat(N), isNatIList(IL))) constraint: Marked_active(isNatIList(cons(N,IL))) >= Marked_mark(and( isNat(N), isNatIList( IL))) constraint: Marked_active(isNatIList(IL)) >= Marked_mark(isNatList(IL)) constraint: Marked_active(isNat(s(N))) >= Marked_mark(isNat(N)) constraint: Marked_active(isNat(length(L))) >= Marked_mark(isNatList(L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(uLength(and( isNat( N), isNatList( L)), L)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(take(0,IL)) >= Marked_mark(uTake1(isNatIList(IL))) constraint: Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(uTake2( and( isNat(M), and( isNat(N), isNatIList( IL))), M,N, IL)) constraint: Marked_active(uTake2(tt,M,N,IL)) >= Marked_mark(cons(N,take(M,IL))) constraint: Marked_active(uLength(tt,L)) >= Marked_mark(s(length(L))) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(and(X1,X2)) >= active(and(mark(X1),mark(X2))) ; mark(tt) >= active(tt) ; mark(isNatList(X)) >= active(isNatList(X)) ; mark(isNatIList(X)) >= active(isNatIList(X)) ; mark(isNat(X)) >= active(isNat(X)) ; mark(0) >= active(0) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(zeros) >= active(zeros) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(uTake1(X)) >= active(uTake1(mark(X))) ; mark(uTake2(X1,X2,X3,X4)) >= active(uTake2(mark(X1),X2,X3,X4)) ; mark(uLength(X1,X2)) >= active(uLength(mark(X1),X2)) ; active(and(tt,T)) >= mark(T) ; active(isNatList(cons(N,L))) >= mark(and(isNat(N),isNatList(L))) ; active(isNatList(nil)) >= mark(tt) ; active(isNatList(take(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) ; active(isNatIList(zeros)) >= mark(tt) ; active(isNatIList(cons(N,IL))) >= mark(and(isNat(N),isNatIList(IL))) ; active(isNatIList(IL)) >= mark(isNatList(IL)) ; active(isNat(0)) >= mark(tt) ; active(isNat(s(N))) >= mark(isNat(N)) ; active(isNat(length(L))) >= mark(isNatList(L)) ; active(length(cons(N,L))) >= mark(uLength(and(isNat(N),isNatList(L)),L)) ; active(zeros) >= mark(cons(0,zeros)) ; active(take(0,IL)) >= mark(uTake1(isNatIList(IL))) ; active(take(s(M),cons(N,IL))) >= mark(uTake2(and(isNat(M), and(isNat(N),isNatIList(IL))), M,N,IL)) ; active(uTake1(tt)) >= mark(nil) ; active(uTake2(tt,M,N,IL)) >= mark(cons(N,take(M,IL))) ; active(uLength(tt,L)) >= mark(s(length(L))) ; and(mark(X1),X2) >= and(X1,X2) ; and(active(X1),X2) >= and(X1,X2) ; and(X1,mark(X2)) >= and(X1,X2) ; and(X1,active(X2)) >= and(X1,X2) ; isNatList(mark(X)) >= isNatList(X) ; isNatList(active(X)) >= isNatList(X) ; isNatIList(mark(X)) >= isNatIList(X) ; isNatIList(active(X)) >= isNatIList(X) ; isNat(mark(X)) >= isNat(X) ; isNat(active(X)) >= isNat(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; take(mark(X1),X2) >= take(X1,X2) ; take(active(X1),X2) >= take(X1,X2) ; take(X1,mark(X2)) >= take(X1,X2) ; take(X1,active(X2)) >= take(X1,X2) ; uTake1(mark(X)) >= uTake1(X) ; uTake1(active(X)) >= uTake1(X) ; uTake2(mark(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(active(X1),X2,X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,mark(X2),X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,active(X2),X3,X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,mark(X3),X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,active(X3),X4) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,X3,mark(X4)) >= uTake2(X1,X2,X3,X4) ; uTake2(X1,X2,X3,active(X4)) >= uTake2(X1,X2,X3,X4) ; uLength(mark(X1),X2) >= uLength(X1,X2) ; uLength(active(X1),X2) >= uLength(X1,X2) ; uLength(X1,mark(X2)) >= uLength(X1,X2) ; uLength(X1,active(X2)) >= uLength(X1,X2) ; Marked_and(mark(X1),X2) >= Marked_and(X1,X2) ; Marked_and(active(X1),X2) >= Marked_and(X1,X2) ; Marked_and(X1,mark(X2)) >= Marked_and(X1,X2) ; Marked_and(X1,active(X2)) >= Marked_and(X1,X2) ; } + Disjunctions:{ { Marked_and(mark(X1),X2) > Marked_and(X1,X2) ; } { Marked_and(active(X1),X2) > Marked_and(X1,X2) ; } { Marked_and(X1,mark(X2)) > Marked_and(X1,X2) ; } { Marked_and(X1,active(X2)) > Marked_and(X1,X2) ; } } === 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 === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === 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 61.216722 seconds (real time) Cime Exit Status: 0