(set-option :produce-models true)
(set-option :print-success false)
(set-logic QF_NRA)

(declare-fun a11r0 () Real)
(declare-fun a12r0 () Real)
(declare-fun a13r0 () Real)
(declare-fun a14r0 () Real)
(declare-fun a21r0 () Real)
(declare-fun a22r0 () Real)
(declare-fun a23r0 () Real)
(declare-fun a24r0 () Real)
(declare-fun b1r0 () Real)
(declare-fun b2r0 () Real)
(declare-fun c1r0 () Real)
(declare-fun c2r0 () Real)
(declare-fun c3r0 () Real)
(declare-fun c4r0 () Real)

(assert (>= b1r0 0))
(assert (>= b2r0 0))

; base: x1 x2 x3 x4 / x5 x6
; pivoting rule
(assert (< c1r0 0))
(assert (and (<= c1r0 c2r0) (<= c1r0 c3r0) (<= c1r0 c4r0)))
(assert (> a11r0 0))
;(assert (or (<= a12r0 0) (<= (* a12r0 b1r0) (* a11r0 b2r0))))
; pivoting step
(declare-fun a21r1 () Real) (assert (= a21r1 (/ a12r0 a11r0)))
(declare-fun a22r1 () Real) (assert (= a22r1 (/ a13r0 a11r0)))
(declare-fun a23r1 () Real) (assert (= a23r1 (/ a14r0 a11r0)))
(declare-fun a24r1 () Real) (assert (= a24r1 (/ 1 a11r0)))
(declare-fun b2r1 () Real) (assert (= b2r1 (/ b1r0 a11r0)))
(declare-fun a11r1 () Real) (assert (= a11r1 (- a22r0 (/ (* a21r0 a12r0) a11r0))))
(declare-fun a12r1 () Real) (assert (= a12r1 (- a23r0 (/ (* a21r0 a13r0) a11r0))))
(declare-fun a13r1 () Real) (assert (= a13r1 (- a24r0 (/ (* a21r0 a14r0) a11r0))))
(declare-fun a14r1 () Real) (assert (= a14r1 (- (/ a21r0 a11r0))))
(declare-fun b1r1 () Real) (assert (= b1r1 (- b2r0 (/ (* a21r0 b1r0) a11r0))))
(declare-fun c1r1 () Real) (assert (= c1r1 (- c2r0 (/ (* c1r0 a12r0) a11r0))))
(declare-fun c2r1 () Real) (assert (= c2r1 (- c3r0 (/ (* c1r0 a13r0) a11r0))))
(declare-fun c3r1 () Real) (assert (= c3r1 (- c4r0 (/ (* c1r0 a14r0) a11r0))))
(declare-fun c4r1 () Real) (assert (= c4r1 (- (/ c1r0 a11r0))))

; base: x2 x3 x4 x5 / x6 x1
; pivoting rule
(assert (< c1r1 0))
(assert (and (<= c1r1 c2r1) (<= c1r1 c3r1) (<= c1r1 c4r1)))
(assert (> a11r1 0))
;(assert (or (<= a12r1 0) (<= (* a12r1 b1r1) (* a11r1 b2r1))))
; pivoting step
(declare-fun a21r2 () Real) (assert (= a21r2 (/ a12r1 a11r1)))
(declare-fun a22r2 () Real) (assert (= a22r2 (/ a13r1 a11r1)))
(declare-fun a23r2 () Real) (assert (= a23r2 (/ a14r1 a11r1)))
(declare-fun a24r2 () Real) (assert (= a24r2 (/ 1 a11r1)))
(declare-fun b2r2 () Real) (assert (= b2r2 (/ b1r1 a11r1)))
(declare-fun a11r2 () Real) (assert (= a11r2 (- a22r1 (/ (* a21r1 a12r1) a11r1))))
(declare-fun a12r2 () Real) (assert (= a12r2 (- a23r1 (/ (* a21r1 a13r1) a11r1))))
(declare-fun a13r2 () Real) (assert (= a13r2 (- a24r1 (/ (* a21r1 a14r1) a11r1))))
(declare-fun a14r2 () Real) (assert (= a14r2 (- (/ a21r1 a11r1))))
(declare-fun b1r2 () Real) (assert (= b1r2 (- b2r1 (/ (* a21r1 b1r1) a11r1))))
(declare-fun c1r2 () Real) (assert (= c1r2 (- c2r1 (/ (* c1r1 a12r1) a11r1))))
(declare-fun c2r2 () Real) (assert (= c2r2 (- c3r1 (/ (* c1r1 a13r1) a11r1))))
(declare-fun c3r2 () Real) (assert (= c3r2 (- c4r1 (/ (* c1r1 a14r1) a11r1))))
(declare-fun c4r2 () Real) (assert (= c4r2 (- (/ c1r1 a11r1))))

; base: x3 x4 x5 x6 / x1 x2
; pivoting rule
(assert (< c1r2 0))
(assert (and (<= c1r2 c2r2) (<= c1r2 c3r2) (<= c1r2 c4r2)))
(assert (> a11r2 0))
;(assert (or (<= a12r2 0) (<= (* a12r2 b1r2) (* a11r2 b2r2))))
; pivoting step
(declare-fun a21r3 () Real) (assert (= a21r3 (/ a12r2 a11r2)))
(declare-fun a22r3 () Real) (assert (= a22r3 (/ a13r2 a11r2)))
(declare-fun a23r3 () Real) (assert (= a23r3 (/ a14r2 a11r2)))
(declare-fun a24r3 () Real) (assert (= a24r3 (/ 1 a11r2)))
(declare-fun b2r3 () Real) (assert (= b2r3 (/ b1r2 a11r2)))
(declare-fun a11r3 () Real) (assert (= a11r3 (- a22r2 (/ (* a21r2 a12r2) a11r2))))
(declare-fun a12r3 () Real) (assert (= a12r3 (- a23r2 (/ (* a21r2 a13r2) a11r2))))
(declare-fun a13r3 () Real) (assert (= a13r3 (- a24r2 (/ (* a21r2 a14r2) a11r2))))
(declare-fun a14r3 () Real) (assert (= a14r3 (- (/ a21r2 a11r2))))
(declare-fun b1r3 () Real) (assert (= b1r3 (- b2r2 (/ (* a21r2 b1r2) a11r2))))
(declare-fun c1r3 () Real) (assert (= c1r3 (- c2r2 (/ (* c1r2 a12r2) a11r2))))
(declare-fun c2r3 () Real) (assert (= c2r3 (- c3r2 (/ (* c1r2 a13r2) a11r2))))
(declare-fun c3r3 () Real) (assert (= c3r3 (- c4r2 (/ (* c1r2 a14r2) a11r2))))
(declare-fun c4r3 () Real) (assert (= c4r3 (- (/ c1r2 a11r2))))

; base: x4 x5 x6 x1 / x2 x3
; pivoting rule
(assert (< c1r3 0))
(assert (and (<= c1r3 c2r3) (<= c1r3 c3r3) (< c1r3 c4r3)))
(assert (> a11r3 0))
;(assert (or (<= a12r3 0) (<= (* a12r3 b1r3) (* a11r3 b2r3))))
; pivoting step
(declare-fun a21r4 () Real) (assert (= a21r4 (/ a12r3 a11r3)))
(declare-fun a22r4 () Real) (assert (= a22r4 (/ a13r3 a11r3)))
(declare-fun a23r4 () Real) (assert (= a23r4 (/ a14r3 a11r3)))
(declare-fun a24r4 () Real) (assert (= a24r4 (/ 1 a11r3)))
(declare-fun b2r4 () Real) (assert (= b2r4 (/ b1r3 a11r3)))
(declare-fun a11r4 () Real) (assert (= a11r4 (- a22r3 (/ (* a21r3 a12r3) a11r3))))
(declare-fun a12r4 () Real) (assert (= a12r4 (- a23r3 (/ (* a21r3 a13r3) a11r3))))
(declare-fun a13r4 () Real) (assert (= a13r4 (- a24r3 (/ (* a21r3 a14r3) a11r3))))
(declare-fun a14r4 () Real) (assert (= a14r4 (- (/ a21r3 a11r3))))
(declare-fun b1r4 () Real) (assert (= b1r4 (- b2r3 (/ (* a21r3 b1r3) a11r3))))
(declare-fun c1r4 () Real) (assert (= c1r4 (- c2r3 (/ (* c1r3 a12r3) a11r3))))
(declare-fun c2r4 () Real) (assert (= c2r4 (- c3r3 (/ (* c1r3 a13r3) a11r3))))
(declare-fun c3r4 () Real) (assert (= c3r4 (- c4r3 (/ (* c1r3 a14r3) a11r3))))
(declare-fun c4r4 () Real) (assert (= c4r4 (- (/ c1r3 a11r3))))

; base: x5 x6 x1 x2 / x3 x4
; pivoting rule
(assert (< c1r4 0))
(assert (and (<= c1r4 c2r4) (< c1r4 c3r4) (< c1r4 c4r4)))
(assert (> a11r4 0))
;(assert (or (<= a12r4 0) (<= (* a12r4 b1r4) (* a11r4 b2r4))))
; pivoting step
(declare-fun a21r5 () Real) (assert (= a21r5 (/ a12r4 a11r4)))
(declare-fun a22r5 () Real) (assert (= a22r5 (/ a13r4 a11r4)))
(declare-fun a23r5 () Real) (assert (= a23r5 (/ a14r4 a11r4)))
(declare-fun a24r5 () Real) (assert (= a24r5 (/ 1 a11r4)))
(declare-fun b2r5 () Real) (assert (= b2r5 (/ b1r4 a11r4)))
(declare-fun a11r5 () Real) (assert (= a11r5 (- a22r4 (/ (* a21r4 a12r4) a11r4))))
(declare-fun a12r5 () Real) (assert (= a12r5 (- a23r4 (/ (* a21r4 a13r4) a11r4))))
(declare-fun a13r5 () Real) (assert (= a13r5 (- a24r4 (/ (* a21r4 a14r4) a11r4))))
(declare-fun a14r5 () Real) (assert (= a14r5 (- (/ a21r4 a11r4))))
(declare-fun b1r5 () Real) (assert (= b1r5 (- b2r4 (/ (* a21r4 b1r4) a11r4))))
(declare-fun c1r5 () Real) (assert (= c1r5 (- c2r4 (/ (* c1r4 a12r4) a11r4))))
(declare-fun c2r5 () Real) (assert (= c2r5 (- c3r4 (/ (* c1r4 a13r4) a11r4))))
(declare-fun c3r5 () Real) (assert (= c3r5 (- c4r4 (/ (* c1r4 a14r4) a11r4))))
(declare-fun c4r5 () Real) (assert (= c4r5 (- (/ c1r4 a11r4))))

; base: x6 x1 x2 x3 / x4 x5
; pivoting rule
(assert (< c1r5 0))
(assert (and (< c1r5 c2r5) (< c1r5 c3r5) (< c1r5 c4r5)))
(assert (> a11r5 0))
;(assert (or (<= a12r5 0) (<= (* a12r5 b1r5) (* a11r5 b2r5))))
; pivoting step
(declare-fun a21r6 () Real) (assert (= a21r6 (/ a12r5 a11r5)))
(declare-fun a22r6 () Real) (assert (= a22r6 (/ a13r5 a11r5)))
(declare-fun a23r6 () Real) (assert (= a23r6 (/ a14r5 a11r5)))
(declare-fun a24r6 () Real) (assert (= a24r6 (/ 1 a11r5)))
(declare-fun b2r6 () Real) (assert (= b2r6 (/ b1r5 a11r5)))
(declare-fun a11r6 () Real) (assert (= a11r6 (- a22r5 (/ (* a21r5 a12r5) a11r5))))
(declare-fun a12r6 () Real) (assert (= a12r6 (- a23r5 (/ (* a21r5 a13r5) a11r5))))
(declare-fun a13r6 () Real) (assert (= a13r6 (- a24r5 (/ (* a21r5 a14r5) a11r5))))
(declare-fun a14r6 () Real) (assert (= a14r6 (- (/ a21r5 a11r5))))
(declare-fun b1r6 () Real) (assert (= b1r6 (- b2r5 (/ (* a21r5 b1r5) a11r5))))
(declare-fun c1r6 () Real) (assert (= c1r6 (- c2r5 (/ (* c1r5 a12r5) a11r5))))
(declare-fun c2r6 () Real) (assert (= c2r6 (- c3r5 (/ (* c1r5 a13r5) a11r5))))
(declare-fun c3r6 () Real) (assert (= c3r6 (- c4r5 (/ (* c1r5 a14r5) a11r5))))
(declare-fun c4r6 () Real) (assert (= c4r6 (- (/ c1r5 a11r5))))

(check-sat)
(get-value (a11r0 a12r0 a13r0 a14r0 b1r0))
(get-value (a21r0 a22r0 a23r0 a24r0 b2r0))
(get-value (c1r0 c2r0 c3r0 c4r0))

(get-value (a11r1 a12r1 a13r1 a14r1 b1r1))
(get-value (a21r1 a22r1 a23r1 a24r1 b2r1))
(get-value (c1r1 c2r1 c3r1 c4r1))