; advent of code 2025.10 pt2 piemērs
;
; (0,1,2,5,6,7,8) (1,4,6,7,8) (0,5,7) (0,1,2,6,7) (0,1,2,3,5,7,8) (0,1,5,7) (0,1,3,7,8)
; {138,150,10,13,17,127,25,155,38}

(declare-fun x1 () Int) ; x1 (0,1,2,5,6,7,8)
(declare-fun x2 () Int) ; x2 (1,4,6,7,8)
(declare-fun x3 () Int) ; x3 (0,5,7)
(declare-fun x4 () Int) ; x4 (0,1,2,6,7)
(declare-fun x5 () Int) ; x5 (0,1,2,3,5,7,8)
(declare-fun x6 () Int) ; x6 (0,1,5,7)
(declare-fun x7 () Int) ; x7 (0,1,3,7,8)
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (>= x4 0))
(assert (>= x5 0))
(assert (>= x6 0))
(assert (>= x7 0))

(assert (= 138 (+ x1 x3 x4 x5 x6 x7)))    ; 0
(assert (= 150 (+ x1 x2 x4 x5 x6 x7)))    ; 1
(assert (= 10 (+ x1 x4 x5)))              ; 2
(assert (= 13 (+ x5 x7)))                 ; 3
(assert (= 17 x2))                        ; 4
(assert (= 127 (+ x1 x3 x5 x6)))          ; 5
(assert (= 25 (+ x1 x2 x4)))              ; 6
(assert (= 155 (+ x1 x2 x3 x4 x5 x6 x7))) ; 7
(assert (= 38 (+ x1 x2 x5 x7)))           ; 8

(check-sat)
(get-model)