(set-option :produce-models true) (set-logic QF_LRA) (declare-fun r () Real) (assert (>= r ( / 3 4 ) )) (declare-fun x1 () Real) (declare-fun y1 () Real) (assert (>= x1 0)) (assert (>= y1 0)) (assert (<= (+ x1 y1) 1)) (declare-fun x2 () Real) (declare-fun y2 () Real) (assert (>= x2 0)) (assert (>= y2 0)) (assert (<= (+ x2 y2) 1)) (declare-fun x3 () Real) (declare-fun y3 () Real) (assert (>= x3 0)) (assert (>= y3 0)) (assert (<= (+ x3 y3) 1)) (declare-fun x4 () Real) (declare-fun y4 () Real) (assert (>= x4 0)) (assert (>= y4 0)) (assert (<= (+ x4 y4) 1)) (declare-fun x5 () Real) (declare-fun y5 () Real) (assert (>= x5 0)) (assert (>= y5 0)) (assert (<= (+ x5 y5) 1)) (declare-fun x6 () Real) (declare-fun y6 () Real) (assert (>= x6 0)) (assert (>= y6 0)) (assert (<= (+ x6 y6) 1)) (declare-fun x7 () Real) (declare-fun y7 () Real) (assert (>= x7 0)) (assert (>= y7 0)) (assert (<= (+ x7 y7) 1)) (declare-fun x8 () Real) (declare-fun y8 () Real) (assert (>= x8 0)) (assert (>= y8 0)) (assert (<= (+ x8 y8) 1)) (assert (<= x1 x2)) (assert (or (< x1 x2 ) (< y1 y2 ) ) ) (assert (<= x2 x3)) (assert (or (< x2 x3 ) (< y2 y3 ) ) ) (assert (<= x3 x4)) (assert (or (< x3 x4 ) (< y3 y4 ) ) ) (assert (<= x4 x5)) (assert (or (< x4 x5 ) (< y4 y5 ) ) ) (assert (<= x5 x6)) (assert (or (< x5 x6 ) (< y5 y6 ) ) ) (assert (<= x6 x7)) (assert (or (< x6 x7 ) (< y6 y7 ) ) ) (assert (<= x7 x8)) (assert (or (< x7 x8 ) (< y7 y8 ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x2 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y2 ) ) ) ( <= r ( - ( + ( * 2 x2 ) ( * 2 y2 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x3 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y3 ) ) ) ( <= r ( - ( + ( * 2 x3 ) ( * 2 y3 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x4 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y4 ) ) ) ( <= r ( - ( + ( * 2 x4 ) ( * 2 y4 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x5 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y5 ) ) ) ( <= r ( - ( + ( * 2 x5 ) ( * 2 y5 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x6 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y6 ) ) ) ( <= r ( - ( + ( * 2 x6 ) ( * 2 y6 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x1 ) ) ) ( or ( <= r ( - ( * 2 y1 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x1 ) ( * 2 y1 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x3 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y3 ) ) ) ( <= r ( - ( + ( * 2 x3 ) ( * 2 y3 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x4 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y4 ) ) ) ( <= r ( - ( + ( * 2 x4 ) ( * 2 y4 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x5 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y5 ) ) ) ( <= r ( - ( + ( * 2 x5 ) ( * 2 y5 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x6 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y6 ) ) ) ( <= r ( - ( + ( * 2 x6 ) ( * 2 y6 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x2 ) ) ) ( or ( <= r ( - ( * 2 y2 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x2 ) ( * 2 y2 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x4 ) ( * 2 x3 ) ) ) ( or ( <= r ( - ( * 2 y3 ) ( * 2 y4 ) ) ) ( <= r ( - ( + ( * 2 x4 ) ( * 2 y4 ) ) ( + ( * 2 x3 ) ( * 2 y3 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x5 ) ( * 2 x3 ) ) ) ( or ( <= r ( - ( * 2 y3 ) ( * 2 y5 ) ) ) ( <= r ( - ( + ( * 2 x5 ) ( * 2 y5 ) ) ( + ( * 2 x3 ) ( * 2 y3 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x6 ) ( * 2 x3 ) ) ) ( or ( <= r ( - ( * 2 y3 ) ( * 2 y6 ) ) ) ( <= r ( - ( + ( * 2 x6 ) ( * 2 y6 ) ) ( + ( * 2 x3 ) ( * 2 y3 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x3 ) ) ) ( or ( <= r ( - ( * 2 y3 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x3 ) ( * 2 y3 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x3 ) ) ) ( or ( <= r ( - ( * 2 y3 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x3 ) ( * 2 y3 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x5 ) ( * 2 x4 ) ) ) ( or ( <= r ( - ( * 2 y4 ) ( * 2 y5 ) ) ) ( <= r ( - ( + ( * 2 x5 ) ( * 2 y5 ) ) ( + ( * 2 x4 ) ( * 2 y4 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x6 ) ( * 2 x4 ) ) ) ( or ( <= r ( - ( * 2 y4 ) ( * 2 y6 ) ) ) ( <= r ( - ( + ( * 2 x6 ) ( * 2 y6 ) ) ( + ( * 2 x4 ) ( * 2 y4 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x4 ) ) ) ( or ( <= r ( - ( * 2 y4 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x4 ) ( * 2 y4 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x4 ) ) ) ( or ( <= r ( - ( * 2 y4 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x4 ) ( * 2 y4 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x6 ) ( * 2 x5 ) ) ) ( or ( <= r ( - ( * 2 y5 ) ( * 2 y6 ) ) ) ( <= r ( - ( + ( * 2 x6 ) ( * 2 y6 ) ) ( + ( * 2 x5 ) ( * 2 y5 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x5 ) ) ) ( or ( <= r ( - ( * 2 y5 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x5 ) ( * 2 y5 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x5 ) ) ) ( or ( <= r ( - ( * 2 y5 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x5 ) ( * 2 y5 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x7 ) ( * 2 x6 ) ) ) ( or ( <= r ( - ( * 2 y6 ) ( * 2 y7 ) ) ) ( <= r ( - ( + ( * 2 x7 ) ( * 2 y7 ) ) ( + ( * 2 x6 ) ( * 2 y6 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x6 ) ) ) ( or ( <= r ( - ( * 2 y6 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x6 ) ( * 2 y6 ) ) ) ) ) ) ) ) (assert ( or ( <= r 0 ) ( or ( <= r ( - ( * 2 x8 ) ( * 2 x7 ) ) ) ( or ( <= r ( - ( * 2 y7 ) ( * 2 y8 ) ) ) ( <= r ( - ( + ( * 2 x8 ) ( * 2 y8 ) ) ( + ( * 2 x7 ) ( * 2 y7 ) ) ) ) ) ) ) ) (check-sat) (get-value ( x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 x7 y7 x8 y8 )) (push 1) (assert (> r ( / 3 4 ) )) (check-sat) (get-value ( r )) (get-value ( x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 x7 y7 x8 y8 ))