; [1,2;0,-1]
; [3,0;-2,1]
; [1,2/3;0,1/3]
; [-1,0;2,1]
; [1,-2;-2,1;-1,0;0,-1] [True,False,False,True]
(set-option :produce-models true)
(set-option :print-success false)
(set-logic QF_LRA)
(declare-fun l0 () Real) (declare-fun u0 () Real) (assert (<= l0 u0))
(declare-fun l1 () Real) (declare-fun u1 () Real) (assert (<= l1 u1))
(declare-fun l2 () Real) (declare-fun u2 () Real) (assert (<= l2 u2))
(declare-fun l3 () Real) (declare-fun u3 () Real) (assert (<= l3 u3))
(declare-fun x0r0 () Real)
(declare-fun x1r0 () Real)
(declare-fun x2r0 () Real)
(declare-fun x3r0 () Real)
(assert (= 0 (+ (* 1 x0r0) (* (- 2) x1r0) (* (- 1) x2r0) (* 0 x3r0))))
(assert (= 0 (+ (* (- 2) x0r0) (* 1 x1r0) (* 0 x2r0) (* (- 1) x3r0))))
(assert (and (<= l0 x0r0) (<= x0r0 u0)))
(assert (and (<= l1 x1r0) (<= x1r0 u1)))
(declare-fun x0r1 () Real)
(declare-fun x1r1 () Real)
(declare-fun x2r1 () Real)
(declare-fun x3r1 () Real)
(assert (= 0 (+ (* 1 x0r1) (* (- 2) x1r1) (* (- 1) x2r1) (* 0 x3r1))))
(assert (= 0 (+ (* (- 2) x0r1) (* 1 x1r1) (* 0 x2r1) (* (- 1) x3r1))))
(assert (and (= x1r1 x1r0)))
(assert (ite (< x2r0 l2) (and (< x0r0 u0) (= x2r1 l2)) (ite (< u2 x2r0) (and (< l0 x0r0) (= x2r1 u2)) false)))
(declare-fun x0r2 () Real)
(declare-fun x1r2 () Real)
(declare-fun x2r2 () Real)
(declare-fun x3r2 () Real)
(assert (= 0 (+ (* 1 x0r2) (* (- 2) x1r2) (* (- 1) x2r2) (* 0 x3r2))))
(assert (= 0 (+ (* (- 2) x0r2) (* 1 x1r2) (* 0 x2r2) (* (- 1) x3r2))))
(assert (and (= x2r2 x2r1)))
(assert (ite (< x3r1 l3) (and (< l1 x1r1) (= x3r2 l3)) (ite (< u3 x3r1) (and (< x1r1 u1) (= x3r2 u3)) false)))
(declare-fun x0r3 () Real)
(declare-fun x1r3 () Real)
(declare-fun x2r3 () Real)
(declare-fun x3r3 () Real)
(assert (= 0 (+ (* 1 x0r3) (* (- 2) x1r3) (* (- 1) x2r3) (* 0 x3r3))))
(assert (= 0 (+ (* (- 2) x0r3) (* 1 x1r3) (* 0 x2r3) (* (- 1) x3r3))))
(assert (and (= x3r3 x3r2)))
(assert (ite (< x0r2 l0) (and (< l2 x2r2) (= x0r3 l0)) (ite (< u0 x0r2) (and (< x2r2 u2) (= x0r3 u0)) false)))
(declare-fun x0r4 () Real)
(declare-fun x1r4 () Real)
(declare-fun x2r4 () Real)
(declare-fun x3r4 () Real)
(assert (= 0 (+ (* 1 x0r4) (* (- 2) x1r4) (* (- 1) x2r4) (* 0 x3r4))))
(assert (= 0 (+ (* (- 2) x0r4) (* 1 x1r4) (* 0 x2r4) (* (- 1) x3r4))))
(assert (and (= x0r4 x0r3)))
(assert (ite (< x1r3 l1) (and (< x3r3 u3) (= x1r4 l1)) (ite (< u1 x1r3) (and (< l3 x3r3) (= x1r4 u1)) false)))
(declare-fun x0r5 () Real)
(declare-fun x1r5 () Real)
(declare-fun x2r5 () Real)
(declare-fun x3r5 () Real)
(assert (= 0 (+ (* 1 x0r5) (* (- 2) x1r5) (* (- 1) x2r5) (* 0 x3r5))))
(assert (= 0 (+ (* (- 2) x0r5) (* 1 x1r5) (* 0 x2r5) (* (- 1) x3r5))))
(assert (and (= x1r5 x1r4)))
(assert (ite (< x2r4 l2) (and (< x0r4 u0) (= x2r5 l2)) (ite (< u2 x2r4) (and (< l0 x0r4) (= x2r5 u2)) false)))
(declare-fun x0r6 () Real)
(declare-fun x1r6 () Real)
(declare-fun x2r6 () Real)
(declare-fun x3r6 () Real)
(assert (= 0 (+ (* 1 x0r6) (* (- 2) x1r6) (* (- 1) x2r6) (* 0 x3r6))))
(assert (= 0 (+ (* (- 2) x0r6) (* 1 x1r6) (* 0 x2r6) (* (- 1) x3r6))))
(assert (and (= x2r6 x2r5)))
(assert (ite (< x3r5 l3) (and (< l1 x1r5) (= x3r6 l3)) (ite (< u3 x3r5) (and (< x1r5 u1) (= x3r6 u3)) false)))
(declare-fun x0r7 () Real)
(declare-fun x1r7 () Real)
(declare-fun x2r7 () Real)
(declare-fun x3r7 () Real)
(assert (= 0 (+ (* 1 x0r7) (* (- 2) x1r7) (* (- 1) x2r7) (* 0 x3r7))))
(assert (= 0 (+ (* (- 2) x0r7) (* 1 x1r7) (* 0 x2r7) (* (- 1) x3r7))))
(assert (and (= x3r7 x3r6)))
(assert (ite (< x0r6 l0) (and (< l2 x2r6) (= x0r7 l0)) (ite (< u0 x0r6) (and (< x2r6 u2) (= x0r7 u0)) false)))
(declare-fun x0r8 () Real)
(declare-fun x1r8 () Real)
(declare-fun x2r8 () Real)
(declare-fun x3r8 () Real)
(assert (= 0 (+ (* 1 x0r8) (* (- 2) x1r8) (* (- 1) x2r8) (* 0 x3r8))))
(assert (= 0 (+ (* (- 2) x0r8) (* 1 x1r8) (* 0 x2r8) (* (- 1) x3r8))))
(assert (and (= x0r8 x0r7)))
(assert (ite (< x1r7 l1) (and (< x3r7 u3) (= x1r8 l1)) (ite (< u1 x1r7) (and (< l3 x3r7) (= x1r8 u1)) false)))
(assert (and (= x0r0 x0r8) (= x0r0 0)))
(assert (and (= x1r0 x1r8) (= x1r0 0)))
(assert (and (= x2r0 x2r8) (= x2r0 0)))
(assert (and (= x3r0 x3r8) (= x3r0 0)))
(declare-fun x0 () Real)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(assert (= 0 (+ (* 1 x0) (* (- 2) x1) (* (- 1) x2) (* 0 x3))))
(assert (= 0 (+ (* (- 2) x0) (* 1 x1) (* 0 x2) (* (- 1) x3))))
(assert (and (<= l0 x0) (<= x0 u0)))
(assert (and (<= l1 x1) (<= x1 u1)))
(assert (and (<= l2 x2) (<= x2 u2)))
(assert (and (<= l3 x3) (<= x3 u3)))
(check-sat)
(get-value (l0 l1 l2 l3))
(get-value (u0 u1 u2 u3))
(get-value (x0r0 x1r0 x2r0 x3r0))
(get-value (x0r1 x1r1 x2r1 x3r1))
(get-value (x0r2 x1r2 x2r2 x3r2))
(get-value (x0r3 x1r3 x2r3 x3r3))
(get-value (x0r4 x1r4 x2r4 x3r4))
(get-value (x0r5 x1r5 x2r5 x3r5))
(get-value (x0r6 x1r6 x2r6 x3r6))
(get-value (x0r7 x1r7 x2r7 x3r7))
(get-value (x0r8 x1r8 x2r8 x3r8))
(get-value (x0 x1 x2 x3))