; Encoding based on Peter Zörnig's work

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

(declare-fun a11 () Real) (assert (= a11 (/ 1 3)))
(declare-fun a12 () Real) (assert (= a12 (- 2)))
(declare-fun a13 () Real) (assert (= a13 (/ (- 2) 3)))
(declare-fun a14 () Real) (assert (= a14 (/ (- 1) 3)))
(declare-fun a15 () Real) (assert (= a15 1))
(declare-fun a16 () Real) (assert (= a16 0))
(declare-fun a21 () Real) ;(assert (= a21 0))
(declare-fun a22 () Real) ;(assert (= a22 2))
(declare-fun a23 () Real) ;(assert (= a23 1))
(declare-fun a24 () Real) (assert (= a24 (/ 6 13)))
(declare-fun a25 () Real) (assert (= a25 0))
(declare-fun a26 () Real) (assert (= a26 1))
(declare-fun b1 () Real) (assert (= b1 0))
(declare-fun b2 () Real) (assert (= b2 0))
(declare-fun c1 () Real)
(declare-fun c2 () Real)
(declare-fun c3 () Real)
(declare-fun c4 () Real)
(declare-fun c5 () Real) (assert (= c5 0))
(declare-fun c6 () Real) (assert (= c6 0))

(define-fun det2
 ((c11 Real) (c12 Real) (c21 Real) (c22 Real))
 Real
 (- (* c11 c22) (* c21 c12)))
(define-fun det3
 ((c11 Real) (c12 Real) (c13 Real)
  (c21 Real) (c22 Real) (c23 Real)
  (c31 Real) (c32 Real) (c33 Real))
 Real
 (- (+ (* c11 c22 c33) (* c12 c23 c31) (* c13 c21 c32))
    (+ (* c11 c23 c32) (* c12 c21 c33) (* c13 c22 c31))))

; cycle: (1,2) (2,3) (3,4) (4,5) (5,6) (6,1)

; linearly independent columns
(assert (< 0 (det2 a11 a12 a21 a22)))
(assert (> 0 (det2 a12 a13 a22 a23)))
(assert (< 0 (det2 a13 a14 a23 a24)))
(assert (> 0 (det2 a14 a15 a24 a25)))
(assert (< 0 (det2 a15 a16 a25 a26)))
(assert (> 0 (det2 a16 a11 a26 a21)))

; positive pivot element (follows from above)
;(assert (< 0 (det2 a13 a12 a23 a22)))
;(assert (> 0 (det2 a14 a13 a24 a23)))
;(assert (< 0 (det2 a15 a14 a25 a24)))
;(assert (> 0 (det2 a16 a15 a26 a25)))
;(assert (< 0 (det2 a11 a16 a21 a26)))
;(assert (> 0 (det2 a12 a11 a22 a21)))

; negative cost factor

; 1,2 -> 2,3
(assert (> 0 (det3 a11 a12 a13 a21 a22 a23 c1 c2 c3)))
(assert (<= (det3 a11 a12 a13 a21 a22 a23 c1 c2 c3) (det3 a11 a12 a14 a21 a22 a24 c1 c2 c4)))
(assert (<= (det3 a11 a12 a13 a21 a22 a23 c1 c2 c3) (det3 a11 a12 a15 a21 a22 a25 c1 c2 c5)))
(assert (<= (det3 a11 a12 a13 a21 a22 a23 c1 c2 c3) (det3 a11 a12 a16 a21 a22 a26 c1 c2 c6)))

; 2,3 -> 3,4
(assert (< 0 (det3 a12 a13 a14 a22 a23 a24 c2 c3 c4)))
(assert (>= (det3 a12 a13 a14 a22 a23 a24 c2 c3 c4) (det3 a12 a13 a15 a22 a23 a25 c2 c3 c5)))
(assert (>= (det3 a12 a13 a14 a22 a23 a24 c2 c3 c4) (det3 a12 a13 a16 a22 a23 a26 c2 c3 c6)))
(assert (> (det3 a12 a13 a14 a22 a23 a24 c2 c3 c4) (det3 a12 a13 a11 a22 a23 a21 c2 c3 c1)))

; 3,4 -> 4,5
(assert (> 0 (det3 a13 a14 a15 a23 a24 a25 c3 c4 c5)))
(assert (<= (det3 a13 a14 a15 a23 a24 a25 c3 c4 c5) (det3 a13 a14 a16 a23 a24 a26 c3 c4 c6)))
(assert (< (det3 a13 a14 a15 a23 a24 a25 c3 c4 c5) (det3 a13 a14 a11 a23 a24 a21 c3 c4 c1)))
(assert (< (det3 a13 a14 a15 a23 a24 a25 c3 c4 c5) (det3 a13 a14 a12 a23 a24 a22 c3 c4 c2)))

; 4,5 -> 5,6
(assert (< 0 (det3 a14 a15 a16 a24 a25 a26 c4 c5 c6)))
(assert (> (det3 a14 a15 a16 a24 a25 a26 c4 c5 c6) (det3 a14 a15 a11 a24 a25 a21 c4 c5 c1)))
(assert (> (det3 a14 a15 a16 a24 a25 a26 c4 c5 c6) (det3 a14 a15 a12 a24 a25 a22 c4 c5 c2)))
(assert (> (det3 a14 a15 a16 a24 a25 a26 c4 c5 c6) (det3 a14 a15 a13 a24 a25 a23 c4 c5 c3)))

; 5,6 -> 6,1
(assert (> 0 (det3 a15 a16 a11 a25 a26 a21 c5 c6 c1)))
(assert (<= (det3 a15 a16 a11 a25 a26 a21 c5 c6 c1) (det3 a15 a16 a12 a25 a26 a22 c5 c6 c2)))
(assert (<= (det3 a15 a16 a11 a25 a26 a21 c5 c6 c1) (det3 a15 a16 a13 a25 a26 a23 c5 c6 c3)))
(assert (<= (det3 a15 a16 a11 a25 a26 a21 c5 c6 c1) (det3 a15 a16 a14 a25 a26 a24 c5 c6 c4)))

; 6,1 -> 1,2
(assert (< 0 (det3 a16 a11 a12 a26 a21 a22 c6 c1 c2)))
(assert (>= (det3 a16 a11 a12 a26 a21 a22 c6 c1 c2) (det3 a16 a11 a13 a26 a21 a23 c6 c1 c3)))
(assert (>= (det3 a16 a11 a12 a26 a21 a22 c6 c1 c2) (det3 a16 a11 a14 a26 a21 a24 c6 c1 c4)))
(assert (>= (det3 a16 a11 a12 a26 a21 a22 c6 c1 c2) (det3 a16 a11 a15 a26 a21 a25 c6 c1 c5)))
; ensure that x1 is not allowed to enter the basis:
(assert (> 0 (det2 a12 a16 a22 a26)))

(check-sat)
(get-value (a11 a12 a13 a14 a15 a16 b1))
(get-value (a21 a22 a23 a24 a25 a26 b2))
(get-value (c1 c2 c3 c4 c5 c6))