- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(zeros) -> mark(cons(0,zeros)) [2] active(U11(tt,L)) -> mark(U12(tt,L)) [3] active(U12(tt,L)) -> mark(s(length(L))) [4] active(U21(tt,IL,M,N)) -> mark(U22(tt,IL,M,N)) [5] active(U22(tt,IL,M,N)) -> mark(U23(tt,IL,M,N)) [6] active(U23(tt,IL,M,N)) -> mark(cons(N,take(M,IL))) [7] active(length(nil)) -> mark(0) [8] active(length(cons(N,L))) -> mark(U11(tt,L)) [9] active(take(0,IL)) -> mark(nil) [10] active(take(s(M),cons(N,IL))) -> mark(U21(tt,IL,M,N)) [11] mark(zeros) -> active(zeros) [12] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [13] mark(0) -> active(0) [14] mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) [15] mark(tt) -> active(tt) [16] mark(U12(X1,X2)) -> active(U12(mark(X1),X2)) [17] mark(s(X)) -> active(s(mark(X))) [18] mark(length(X)) -> active(length(mark(X))) [19] mark(U21(X1,X2,X3,X4)) -> active(U21(mark(X1),X2,X3,X4)) [20] mark(U22(X1,X2,X3,X4)) -> active(U22(mark(X1),X2,X3,X4)) [21] mark(U23(X1,X2,X3,X4)) -> active(U23(mark(X1),X2,X3,X4)) [22] mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) [23] mark(nil) -> active(nil) [24] cons(mark(X1),X2) -> cons(X1,X2) [25] cons(X1,mark(X2)) -> cons(X1,X2) [26] cons(active(X1),X2) -> cons(X1,X2) [27] cons(X1,active(X2)) -> cons(X1,X2) [28] U11(mark(X1),X2) -> U11(X1,X2) [29] U11(X1,mark(X2)) -> U11(X1,X2) [30] U11(active(X1),X2) -> U11(X1,X2) [31] U11(X1,active(X2)) -> U11(X1,X2) [32] U12(mark(X1),X2) -> U12(X1,X2) [33] U12(X1,mark(X2)) -> U12(X1,X2) [34] U12(active(X1),X2) -> U12(X1,X2) [35] U12(X1,active(X2)) -> U12(X1,X2) [36] s(mark(X)) -> s(X) [37] s(active(X)) -> s(X) [38] length(mark(X)) -> length(X) [39] length(active(X)) -> length(X) [40] U21(mark(X1),X2,X3,X4) -> U21(X1,X2,X3,X4) [41] U21(X1,mark(X2),X3,X4) -> U21(X1,X2,X3,X4) [42] U21(X1,X2,mark(X3),X4) -> U21(X1,X2,X3,X4) [43] U21(X1,X2,X3,mark(X4)) -> U21(X1,X2,X3,X4) [44] U21(active(X1),X2,X3,X4) -> U21(X1,X2,X3,X4) [45] U21(X1,active(X2),X3,X4) -> U21(X1,X2,X3,X4) [46] U21(X1,X2,active(X3),X4) -> U21(X1,X2,X3,X4) [47] U21(X1,X2,X3,active(X4)) -> U21(X1,X2,X3,X4) [48] U22(mark(X1),X2,X3,X4) -> U22(X1,X2,X3,X4) [49] U22(X1,mark(X2),X3,X4) -> U22(X1,X2,X3,X4) [50] U22(X1,X2,mark(X3),X4) -> U22(X1,X2,X3,X4) [51] U22(X1,X2,X3,mark(X4)) -> U22(X1,X2,X3,X4) [52] U22(active(X1),X2,X3,X4) -> U22(X1,X2,X3,X4) [53] U22(X1,active(X2),X3,X4) -> U22(X1,X2,X3,X4) [54] U22(X1,X2,active(X3),X4) -> U22(X1,X2,X3,X4) [55] U22(X1,X2,X3,active(X4)) -> U22(X1,X2,X3,X4) [56] U23(mark(X1),X2,X3,X4) -> U23(X1,X2,X3,X4) [57] U23(X1,mark(X2),X3,X4) -> U23(X1,X2,X3,X4) [58] U23(X1,X2,mark(X3),X4) -> U23(X1,X2,X3,X4) [59] U23(X1,X2,X3,mark(X4)) -> U23(X1,X2,X3,X4) [60] U23(active(X1),X2,X3,X4) -> U23(X1,X2,X3,X4) [61] U23(X1,active(X2),X3,X4) -> U23(X1,X2,X3,X4) [62] U23(X1,X2,active(X3),X4) -> U23(X1,X2,X3,X4) [63] U23(X1,X2,X3,active(X4)) -> U23(X1,X2,X3,X4) [64] take(mark(X1),X2) -> take(X1,X2) [65] take(X1,mark(X2)) -> take(X1,X2) [66] take(active(X1),X2) -> take(X1,X2) [67] take(X1,active(X2)) -> take(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 10 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; 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(U22(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; 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_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { 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(U22(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { 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_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } { Marked_active(take(s(M),cons(N,IL))) > Marked_mark(U21(tt,IL,M,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: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) 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(U22(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) 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_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) constraint: Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U11 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_U12 -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_s -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_length -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 4 APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 4 APPLY CRITERIA (Subterm criterion) ST: Marked_U23 -> 4 APPLY CRITERIA (Subterm criterion) ST: Marked_take -> 2 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; 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_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { 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_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } { Marked_active(take(s(M),cons(N,IL))) > Marked_mark(U21(tt,IL,M,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: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) 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_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) constraint: Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } { Marked_active(take(s(M),cons(N,IL))) > Marked_mark(U21(tt,IL,M,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: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) constraint: Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } { Marked_active(take(s(M),cons(N,IL))) > Marked_mark(U21(tt,IL,M,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: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) constraint: Marked_active(take(s(M),cons(N,IL))) >= Marked_mark(U21(tt,IL,M,N)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } } === 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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U21(tt,IL,M,N)) > Marked_mark(U22(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } } === 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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U21(tt,IL,M,N)) >= Marked_mark(U22(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U22(tt,IL,M,N)) > Marked_mark(U23(tt,IL,M,N)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } } === 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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U22(tt,IL,M,N)) >= Marked_mark(U23(tt,IL,M,N)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } { Marked_active(U23(tt,IL,M,N)) > Marked_mark(cons(N,take(M,IL))) ; } } === 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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) constraint: Marked_active(U23(tt,IL,M,N)) >= Marked_mark(cons(N,take(M,IL))) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1),X2,X3,X4)) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U22(X1,X2,X3,X4)) > Marked_active(U22(mark(X1),X2,X3,X4)) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U22(X1,X2,X3,X4)) >= Marked_active(U22(mark(X1), X2,X3,X4)) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1),X2,X3,X4)) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U21(X1,X2,X3,X4)) > Marked_active(U21(mark(X1),X2,X3,X4)) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U21(X1,X2,X3,X4)) >= Marked_active(U21(mark(X1), X2,X3,X4)) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1),X2,X3,X4)) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_mark(U23(X1,X2,X3,X4)) > Marked_active(U23(mark(X1),X2,X3,X4)) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_mark(U23(X1,X2,X3,X4)) >= Marked_active(U23(mark(X1), X2,X3,X4)) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zeros) >= Marked_active(zeros) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zeros) > Marked_active(zeros) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zeros) >= Marked_active(zeros) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(zeros) >= Marked_mark(cons(0,zeros)) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_active(zeros) > Marked_mark(cons(0,zeros)) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_active(zeros) >= Marked_mark(cons(0,zeros)) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(zeros) >= active(zeros) constraint: mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) constraint: mark(tt) >= active(tt) constraint: mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(length(X)) >= active(length(mark(X))) constraint: mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) constraint: mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) constraint: mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) 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: active(zeros) >= mark(cons(0,zeros)) constraint: active(U12(tt,L)) >= mark(s(length(L))) constraint: active(U11(tt,L)) >= mark(U12(tt,L)) constraint: active(length(cons(N,L))) >= mark(U11(tt,L)) constraint: active(length(nil)) >= mark(0) constraint: active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) constraint: active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) constraint: active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) constraint: active(take(0,IL)) >= mark(nil) constraint: active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) constraint: U12(mark(X1),X2) >= U12(X1,X2) constraint: U12(active(X1),X2) >= U12(X1,X2) constraint: U12(X1,mark(X2)) >= U12(X1,X2) constraint: U12(X1,active(X2)) >= U12(X1,X2) constraint: U11(mark(X1),X2) >= U11(X1,X2) constraint: U11(active(X1),X2) >= U11(X1,X2) constraint: U11(X1,mark(X2)) >= U11(X1,X2) constraint: U11(X1,active(X2)) >= U11(X1,X2) 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: U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) constraint: U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) constraint: U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) constraint: U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) constraint: U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) constraint: U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) 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: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) constraint: Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(length(X)) >= Marked_active(length(mark(X))) constraint: Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) constraint: Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) constraint: Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(U12(X1,X2)) >= Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) >= Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(U12(tt,L)) >= Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) >= Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) >= Marked_mark(U11(tt,L)) ; } + Disjunctions:{ { Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; } { Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(length(X)) > Marked_active(length(mark(X))) ; } { Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; } { Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; } { Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,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 === 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 (Simple graph) Found the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(zeros) >= active(zeros) ; mark(U12(X1,X2)) >= active(U12(mark(X1),X2)) ; mark(tt) >= active(tt) ; mark(U11(X1,X2)) >= active(U11(mark(X1),X2)) ; mark(s(X)) >= active(s(mark(X))) ; mark(length(X)) >= active(length(mark(X))) ; mark(U22(X1,X2,X3,X4)) >= active(U22(mark(X1),X2,X3,X4)) ; mark(U21(X1,X2,X3,X4)) >= active(U21(mark(X1),X2,X3,X4)) ; mark(U23(X1,X2,X3,X4)) >= active(U23(mark(X1),X2,X3,X4)) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; 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) ; active(zeros) >= mark(cons(0,zeros)) ; active(U12(tt,L)) >= mark(s(length(L))) ; active(U11(tt,L)) >= mark(U12(tt,L)) ; active(length(cons(N,L))) >= mark(U11(tt,L)) ; active(length(nil)) >= mark(0) ; active(U22(tt,IL,M,N)) >= mark(U23(tt,IL,M,N)) ; active(U21(tt,IL,M,N)) >= mark(U22(tt,IL,M,N)) ; active(U23(tt,IL,M,N)) >= mark(cons(N,take(M,IL))) ; active(take(0,IL)) >= mark(nil) ; active(take(s(M),cons(N,IL))) >= mark(U21(tt,IL,M,N)) ; U12(mark(X1),X2) >= U12(X1,X2) ; U12(active(X1),X2) >= U12(X1,X2) ; U12(X1,mark(X2)) >= U12(X1,X2) ; U12(X1,active(X2)) >= U12(X1,X2) ; U11(mark(X1),X2) >= U11(X1,X2) ; U11(active(X1),X2) >= U11(X1,X2) ; U11(X1,mark(X2)) >= U11(X1,X2) ; U11(X1,active(X2)) >= U11(X1,X2) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; length(mark(X)) >= length(X) ; length(active(X)) >= length(X) ; U22(mark(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(active(X1),X2,X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,mark(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,active(X2),X3,X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,mark(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,active(X3),X4) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,mark(X4)) >= U22(X1,X2,X3,X4) ; U22(X1,X2,X3,active(X4)) >= U22(X1,X2,X3,X4) ; U21(mark(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(active(X1),X2,X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,mark(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,active(X2),X3,X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,mark(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,active(X3),X4) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,mark(X4)) >= U21(X1,X2,X3,X4) ; U21(X1,X2,X3,active(X4)) >= U21(X1,X2,X3,X4) ; U23(mark(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(active(X1),X2,X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,mark(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,active(X2),X3,X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,mark(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,active(X3),X4) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,mark(X4)) >= U23(X1,X2,X3,X4) ; U23(X1,X2,X3,active(X4)) >= U23(X1,X2,X3,X4) ; 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) ; Marked_mark(U12(X1,X2)) > Marked_active(U12(mark(X1),X2)) ; Marked_mark(U11(X1,X2)) > Marked_active(U11(mark(X1),X2)) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(length(X)) >= Marked_active(length(mark(X))) ; Marked_active(U12(tt,L)) > Marked_mark(s(length(L))) ; Marked_active(U11(tt,L)) > Marked_mark(U12(tt,L)) ; Marked_active(length(cons(N,L))) > Marked_mark(U11(tt,L)) ; } + 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 === No solution found for these parameters.(83326 bt (60605) [41]) === 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) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U11 -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U12 -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 3 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U21 -> 2 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 3 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U22 -> 2 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U23 -> 3 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U23 -> 1 APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_U23 -> 2 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_take -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: NOT SOLVED No proof found Cime worked for 153.627419 seconds (real time) Cime Exit Status: 0