- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(pairNs) -> mark(cons(0,incr(oddNs))) [2] active(oddNs) -> mark(incr(pairNs)) [3] active(incr(cons(X,XS))) -> mark(cons(s(X),incr(XS))) [4] active(take(0,XS)) -> mark(nil) [5] active(take(s(N),cons(X,XS))) -> mark(cons(X,take(N,XS))) [6] active(zip(nil,XS)) -> mark(nil) [7] active(zip(X,nil)) -> mark(nil) [8] active(zip(cons(X,XS),cons(Y,YS))) -> mark(cons(pair(X,Y),zip(XS,YS))) [9] active(tail(cons(X,XS))) -> mark(XS) [10] active(repItems(nil)) -> mark(nil) [11] active(repItems(cons(X,XS))) -> mark(cons(X,cons(X,repItems(XS)))) [12] mark(pairNs) -> active(pairNs) [13] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [14] mark(0) -> active(0) [15] mark(incr(X)) -> active(incr(mark(X))) [16] mark(oddNs) -> active(oddNs) [17] mark(s(X)) -> active(s(mark(X))) [18] mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) [19] mark(nil) -> active(nil) [20] mark(zip(X1,X2)) -> active(zip(mark(X1),mark(X2))) [21] mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2))) [22] mark(tail(X)) -> active(tail(mark(X))) [23] mark(repItems(X)) -> active(repItems(mark(X))) [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] incr(mark(X)) -> incr(X) [29] incr(active(X)) -> incr(X) [30] s(mark(X)) -> s(X) [31] s(active(X)) -> s(X) [32] take(mark(X1),X2) -> take(X1,X2) [33] take(X1,mark(X2)) -> take(X1,X2) [34] take(active(X1),X2) -> take(X1,X2) [35] take(X1,active(X2)) -> take(X1,X2) [36] zip(mark(X1),X2) -> zip(X1,X2) [37] zip(X1,mark(X2)) -> zip(X1,X2) [38] zip(active(X1),X2) -> zip(X1,X2) [39] zip(X1,active(X2)) -> zip(X1,X2) [40] pair(mark(X1),X2) -> pair(X1,X2) [41] pair(X1,mark(X2)) -> pair(X1,X2) [42] pair(active(X1),X2) -> pair(X1,X2) [43] pair(X1,active(X2)) -> pair(X1,X2) [44] tail(mark(X)) -> tail(X) [45] tail(active(X)) -> tail(X) [46] repItems(mark(X)) -> repItems(X) [47] repItems(active(X)) -> repItems(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 9 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_active(pair(mark(X1),mark(X2))) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_mark(X) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_active(pair(mark(X1),mark(X2))) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_mark(X) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(tail(cons(X,XS))) > Marked_mark(XS) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_active(pair(mark(X1),mark(X2))) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_mark(X) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) APPLY CRITERIA (Subterm criterion) ST: Marked_cons -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_incr -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_s -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_take -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_zip -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_pair -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_tail -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_repItems -> 1 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_mark(X) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_mark(X) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(tail(cons(X,XS))) > Marked_mark(XS) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_mark(X) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(tail(cons(X,XS))) > Marked_mark(XS) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(tail(cons(X,XS))) > Marked_mark(XS) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(tail(cons(X,XS))) > Marked_mark(XS) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(tail(cons(X,XS))) >= Marked_mark(XS) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons(X,take(N,XS))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(take(s(N),cons(X,XS))) > Marked_mark(cons(X,take(N,XS))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(take(s(N),cons(X,XS))) >= Marked_mark(cons( X,take(N,XS))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons(X,repItems(XS)))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } { Marked_active(repItems(cons(X,XS))) > Marked_mark(cons(X, cons(X,repItems(XS)))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) constraint: Marked_active(repItems(cons(X,XS))) >= Marked_mark(cons(X, cons( X, repItems(XS)))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_active(repItems(mark(X))) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(repItems(X)) >= Marked_active(repItems(mark(X))) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(zip(X1,X2)) > Marked_active(zip(mark(X1),mark(X2))) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(zip(X1,X2)) >= Marked_active(zip(mark(X1),mark(X2))) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } { Marked_active(zip(cons(X,XS),cons(Y,YS))) > Marked_mark(cons(pair(X,Y), zip(XS,YS))) ; } } === 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) constraint: Marked_active(zip(cons(X,XS),cons(Y,YS))) >= Marked_mark( cons(pair(X,Y), zip(XS,YS))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(pairNs) >= Marked_active(pairNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(pairNs) > Marked_active(pairNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } { Marked_active(pairNs) > Marked_mark(cons(0,incr(oddNs))) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat 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(incr(X)) >= active(incr(mark(X))) constraint: mark(oddNs) >= active(oddNs) constraint: mark(pairNs) >= active(pairNs) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(nil) >= active(nil) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(repItems(X)) >= active(repItems(mark(X))) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: incr(mark(X)) >= incr(X) constraint: incr(active(X)) >= incr(X) constraint: active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) constraint: active(oddNs) >= mark(incr(pairNs)) constraint: active(pairNs) >= mark(cons(0,incr(oddNs))) constraint: active(take(0,XS)) >= mark(nil) constraint: active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) constraint: active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y), zip(XS,YS))) constraint: active(zip(nil,XS)) >= mark(nil) constraint: active(zip(X,nil)) >= mark(nil) constraint: active(tail(cons(X,XS))) >= mark(XS) constraint: active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) constraint: active(repItems(nil)) >= mark(nil) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: zip(mark(X1),X2) >= zip(X1,X2) constraint: zip(active(X1),X2) >= zip(X1,X2) constraint: zip(X1,mark(X2)) >= zip(X1,X2) constraint: zip(X1,active(X2)) >= zip(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: repItems(mark(X)) >= repItems(X) constraint: repItems(active(X)) >= repItems(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) constraint: Marked_mark(oddNs) >= Marked_active(oddNs) constraint: Marked_mark(pairNs) >= Marked_active(pairNs) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) constraint: Marked_active(oddNs) >= Marked_mark(incr(pairNs)) constraint: Marked_active(pairNs) >= Marked_mark(cons(0,incr(oddNs))) 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(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(incr(X)) >= Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) >= Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) >= Marked_mark(incr(pairNs)) ; } + Disjunctions:{ { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; } { Marked_mark(oddNs) > Marked_active(oddNs) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; } { Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (Simple graph) Found the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(incr(X)) > Marked_mark(X) ; Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } APPLY CRITERIA (SOLVE_ORD) Trying to solve the following constraints: { mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(incr(X)) >= active(incr(mark(X))) ; mark(oddNs) >= active(oddNs) ; mark(pairNs) >= active(pairNs) ; mark(s(X)) >= active(s(mark(X))) ; mark(nil) >= active(nil) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(zip(X1,X2)) >= active(zip(mark(X1),mark(X2))) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(repItems(X)) >= active(repItems(mark(X))) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; incr(mark(X)) >= incr(X) ; incr(active(X)) >= incr(X) ; active(incr(cons(X,XS))) >= mark(cons(s(X),incr(XS))) ; active(oddNs) >= mark(incr(pairNs)) ; active(pairNs) >= mark(cons(0,incr(oddNs))) ; active(take(0,XS)) >= mark(nil) ; active(take(s(N),cons(X,XS))) >= mark(cons(X,take(N,XS))) ; active(zip(cons(X,XS),cons(Y,YS))) >= mark(cons(pair(X,Y),zip(XS,YS))) ; active(zip(nil,XS)) >= mark(nil) ; active(zip(X,nil)) >= mark(nil) ; active(tail(cons(X,XS))) >= mark(XS) ; active(repItems(cons(X,XS))) >= mark(cons(X,cons(X,repItems(XS)))) ; active(repItems(nil)) >= mark(nil) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; zip(mark(X1),X2) >= zip(X1,X2) ; zip(active(X1),X2) >= zip(X1,X2) ; zip(X1,mark(X2)) >= zip(X1,X2) ; zip(X1,active(X2)) >= zip(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; repItems(mark(X)) >= repItems(X) ; repItems(active(X)) >= repItems(X) ; Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; Marked_mark(incr(X)) > Marked_mark(X) ; Marked_mark(incr(X)) > Marked_active(incr(mark(X))) ; Marked_mark(oddNs) >= Marked_active(oddNs) ; Marked_mark(s(X)) > Marked_mark(X) ; Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; Marked_active(incr(cons(X,XS))) > Marked_mark(cons(s(X),incr(XS))) ; Marked_active(oddNs) > Marked_mark(incr(pairNs)) ; } + 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.(1873 bt (1776) [876]) === 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 solver returned === STOPING TIMER real === === 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 0 components: 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: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_zip -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) ST: Marked_pair -> 1 APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: NOT SOLVED No proof found Cime worked for 167.661082 seconds (real time) Cime Exit Status: 0