- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] a__pairNs -> cons(0,incr(oddNs)) [2] a__oddNs -> a__incr(a__pairNs) [3] a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) [4] a__take(0,XS) -> nil [5] a__take(s(N),cons(X,XS)) -> cons(mark(X),take(N,XS)) [6] a__zip(nil,XS) -> nil [7] a__zip(X,nil) -> nil [8] a__zip(cons(X,XS),cons(Y,YS)) -> cons(pair(mark(X),mark(Y)),zip(XS,YS)) [9] a__tail(cons(X,XS)) -> mark(XS) [10] a__repItems(nil) -> nil [11] a__repItems(cons(X,XS)) -> cons(mark(X),cons(X,repItems(XS))) [12] mark(pairNs) -> a__pairNs [13] mark(incr(X)) -> a__incr(mark(X)) [14] mark(oddNs) -> a__oddNs [15] mark(take(X1,X2)) -> a__take(mark(X1),mark(X2)) [16] mark(zip(X1,X2)) -> a__zip(mark(X1),mark(X2)) [17] mark(tail(X)) -> a__tail(mark(X)) [18] mark(repItems(X)) -> a__repItems(mark(X)) [19] mark(cons(X1,X2)) -> cons(mark(X1),X2) [20] mark(0) -> 0 [21] mark(s(X)) -> s(mark(X)) [22] mark(nil) -> nil [23] mark(pair(X1,X2)) -> pair(mark(X1),mark(X2)) [24] a__pairNs -> pairNs [25] a__incr(X) -> incr(X) [26] a__oddNs -> oddNs [27] a__take(X1,X2) -> take(X1,X2) [28] a__zip(X1,X2) -> zip(X1,X2) [29] a__tail(X) -> tail(X) [30] a__repItems(X) -> repItems(X) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) ; Marked_a__tail(cons(X,XS)) >= Marked_mark(XS) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__oddNs >= Marked_a__incr(a__pairNs) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(oddNs) >= Marked_a__oddNs ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_a__zip(mark(X1),mark(X2)) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_a__repItems(mark(X)) ; Marked_mark(repItems(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_a__tail(mark(X)) ; Marked_mark(tail(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__repItems(cons(X,XS)) > Marked_mark(X) ; } { Marked_a__tail(cons(X,XS)) > Marked_mark(XS) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(X) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(Y) ; } { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__oddNs > Marked_a__incr(a__pairNs) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(oddNs) > Marked_a__oddNs ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_a__zip(mark(X1),mark(X2)) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_a__repItems(mark(X)) ; } { Marked_mark(repItems(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_a__tail(mark(X)) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } } === 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: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__tail(cons(X,XS)) >= Marked_mark(XS) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__oddNs >= Marked_a__incr(a__pairNs) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(oddNs) >= Marked_a__oddNs constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_a__zip(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(repItems(X)) >= Marked_a__repItems(mark(X)) constraint: Marked_mark(repItems(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_a__tail(mark(X)) constraint: Marked_mark(tail(X)) >= Marked_mark(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) ; Marked_a__tail(cons(X,XS)) >= Marked_mark(XS) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_a__zip(mark(X1),mark(X2)) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_a__repItems(mark(X)) ; Marked_mark(repItems(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_a__tail(mark(X)) ; Marked_mark(tail(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__repItems(cons(X,XS)) > Marked_mark(X) ; } { Marked_a__tail(cons(X,XS)) > Marked_mark(XS) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(X) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(Y) ; } { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_a__zip(mark(X1),mark(X2)) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_a__repItems(mark(X)) ; } { Marked_mark(repItems(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_a__tail(mark(X)) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } } === 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: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__tail(cons(X,XS)) >= Marked_mark(XS) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_a__zip(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(repItems(X)) >= Marked_a__repItems(mark(X)) constraint: Marked_mark(repItems(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_a__tail(mark(X)) constraint: Marked_mark(tail(X)) >= Marked_mark(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_a__zip(mark(X1),mark(X2)) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; Marked_mark(repItems(X)) >= Marked_a__repItems(mark(X)) ; Marked_mark(repItems(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__repItems(cons(X,XS)) > Marked_mark(X) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(X) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(Y) ; } { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_a__zip(mark(X1),mark(X2)) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(repItems(X)) > Marked_a__repItems(mark(X)) ; } { Marked_mark(repItems(X)) > Marked_mark(X) ; } } === 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: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__repItems(cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_a__zip(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(repItems(X)) >= Marked_a__repItems(mark(X)) constraint: Marked_mark(repItems(X)) >= Marked_mark(X) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) ; Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(zip(X1,X2)) >= Marked_a__zip(mark(X1),mark(X2)) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X1) ; Marked_mark(zip(X1,X2)) >= Marked_mark(X2) ; } + Disjunctions:{ { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(X) ; } { Marked_a__zip(cons(X,XS),cons(Y,YS)) > Marked_mark(Y) ; } { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(zip(X1,X2)) > Marked_a__zip(mark(X1),mark(X2)) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(zip(X1,X2)) > Marked_mark(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(X) constraint: Marked_a__zip(cons(X,XS),cons(Y,YS)) >= Marked_mark(Y) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(zip(X1,X2)) >= Marked_a__zip(mark(X1),mark(X2)) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(zip(X1,X2)) >= Marked_mark(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; } + Disjunctions:{ { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; } + Disjunctions:{ { Marked_a__take(s(N),cons(X,XS)) > Marked_mark(X) ; } { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(take(X1,X2)) > Marked_a__take(mark(X1),mark(X2)) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat solver returned Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: a__pairNs >= cons(0,incr(oddNs)) constraint: a__pairNs >= pairNs constraint: a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) constraint: a__incr(X) >= incr(X) constraint: a__oddNs >= oddNs constraint: a__oddNs >= a__incr(a__pairNs) constraint: mark(cons(X1,X2)) >= cons(mark(X1),X2) constraint: mark(0) >= 0 constraint: mark(incr(X)) >= a__incr(mark(X)) constraint: mark(oddNs) >= a__oddNs constraint: mark(s(X)) >= s(mark(X)) constraint: mark(nil) >= nil constraint: mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) constraint: mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) constraint: mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) constraint: mark(repItems(X)) >= a__repItems(mark(X)) constraint: mark(pairNs) >= a__pairNs constraint: mark(tail(X)) >= a__tail(mark(X)) constraint: a__take(0,XS) >= nil constraint: a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) constraint: a__take(X1,X2) >= take(X1,X2) constraint: a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)), zip(XS,YS)) constraint: a__zip(nil,XS) >= nil constraint: a__zip(X,nil) >= nil constraint: a__zip(X1,X2) >= zip(X1,X2) constraint: a__tail(cons(X,XS)) >= mark(XS) constraint: a__tail(X) >= tail(X) constraint: a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) constraint: a__repItems(nil) >= nil constraint: a__repItems(X) >= repItems(X) constraint: Marked_a__take(s(N),cons(X,XS)) >= Marked_mark(X) constraint: Marked_a__incr(cons(X,XS)) >= Marked_mark(X) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) constraint: Marked_mark(incr(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(take(X1,X2)) >= Marked_a__take(mark(X1),mark(X2)) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { a__pairNs >= cons(0,incr(oddNs)) ; a__pairNs >= pairNs ; a__incr(cons(X,XS)) >= cons(s(mark(X)),incr(XS)) ; a__incr(X) >= incr(X) ; a__oddNs >= oddNs ; a__oddNs >= a__incr(a__pairNs) ; mark(cons(X1,X2)) >= cons(mark(X1),X2) ; mark(0) >= 0 ; mark(incr(X)) >= a__incr(mark(X)) ; mark(oddNs) >= a__oddNs ; mark(s(X)) >= s(mark(X)) ; mark(nil) >= nil ; mark(take(X1,X2)) >= a__take(mark(X1),mark(X2)) ; mark(pair(X1,X2)) >= pair(mark(X1),mark(X2)) ; mark(zip(X1,X2)) >= a__zip(mark(X1),mark(X2)) ; mark(repItems(X)) >= a__repItems(mark(X)) ; mark(pairNs) >= a__pairNs ; mark(tail(X)) >= a__tail(mark(X)) ; a__take(0,XS) >= nil ; a__take(s(N),cons(X,XS)) >= cons(mark(X),take(N,XS)) ; a__take(X1,X2) >= take(X1,X2) ; a__zip(cons(X,XS),cons(Y,YS)) >= cons(pair(mark(X),mark(Y)),zip(XS,YS)) ; a__zip(nil,XS) >= nil ; a__zip(X,nil) >= nil ; a__zip(X1,X2) >= zip(X1,X2) ; a__tail(cons(X,XS)) >= mark(XS) ; a__tail(X) >= tail(X) ; a__repItems(cons(X,XS)) >= cons(mark(X),cons(X,repItems(XS))) ; a__repItems(nil) >= nil ; a__repItems(X) >= repItems(X) ; Marked_a__incr(cons(X,XS)) >= Marked_mark(X) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(incr(X)) >= Marked_a__incr(mark(X)) ; Marked_mark(incr(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_mark(X) ; } + Disjunctions:{ { Marked_a__incr(cons(X,XS)) > Marked_mark(X) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(incr(X)) > Marked_a__incr(mark(X)) ; } { Marked_mark(incr(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } } === 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 : 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) NOT SOLVED No proof found Cime worked for 24.093434 seconds (real time) Cime Exit Status: 0