(set-info :smt-lib-version 2.6) (set-logic QF_LIA) (set-info :category "crafted") (set-info :status sat) (declare-fun x_0 () Int) (declare-fun x_1 () Int) (declare-fun x_2 () Int) (declare-fun x_3 () Int) (declare-fun x_4 () Int) (declare-fun x_5 () Int) (declare-fun x_6 () Int) (declare-fun x_7 () Int) (declare-fun x_8 () Int) (declare-fun x_9 () Int) (declare-fun x_10 () Int) (declare-fun x_11 () Int) (declare-fun x_12 () Int) (assert (>= x_0 0)) (assert (>= x_1 0)) (assert (>= x_2 0)) (assert (>= x_3 0)) (assert (>= x_4 0)) (assert (>= x_5 0)) (assert (>= x_6 0)) (assert (>= x_7 0)) (assert (>= x_8 0)) (assert (>= x_9 0)) (assert (>= x_10 0)) (assert (>= x_11 0)) (assert (>= x_12 0)) (assert (<= (+ (* (- 237) x_0) (* 2 x_1) (* 2 x_2) (* 2 x_3) (* 2 x_4) (* 2 x_5) (* 2 x_6) (* 2 x_7) (* 2 x_8) (* 2 x_9) (* 2 x_10) (* 2 x_11) (* 2 x_12)) 0)) (assert (<= (+ (* 3 x_0) (* (- 236) x_1) (* 3 x_2) (* 3 x_3) (* 3 x_4) (* 3 x_5) (* 3 x_6) (* 3 x_7) (* 3 x_8) (* 3 x_9) (* 3 x_10) (* 3 x_11) (* 3 x_12)) 0)) (assert (<= (+ (* 5 x_0) (* 5 x_1) (* (- 234) x_2) (* 5 x_3) (* 5 x_4) (* 5 x_5) (* 5 x_6) (* 5 x_7) (* 5 x_8) (* 5 x_9) (* 5 x_10) (* 5 x_11) (* 5 x_12)) 0)) (assert (<= (+ (* 7 x_0) (* 7 x_1) (* 7 x_2) (* (- 232) x_3) (* 7 x_4) (* 7 x_5) (* 7 x_6) (* 7 x_7) (* 7 x_8) (* 7 x_9) (* 7 x_10) (* 7 x_11) (* 7 x_12)) 0)) (assert (<= (+ (* 11 x_0) (* 11 x_1) (* 11 x_2) (* 11 x_3) (* (- 228) x_4) (* 11 x_5) (* 11 x_6) (* 11 x_7) (* 11 x_8) (* 11 x_9) (* 11 x_10) (* 11 x_11) (* 11 x_12)) 0)) (assert (<= (+ (* 13 x_0) (* 13 x_1) (* 13 x_2) (* 13 x_3) (* 13 x_4) (* (- 226) x_5) (* 13 x_6) (* 13 x_7) (* 13 x_8) (* 13 x_9) (* 13 x_10) (* 13 x_11) (* 13 x_12)) 0)) (assert (<= (+ (* 17 x_0) (* 17 x_1) (* 17 x_2) (* 17 x_3) (* 17 x_4) (* 17 x_5) (* (- 222) x_6) (* 17 x_7) (* 17 x_8) (* 17 x_9) (* 17 x_10) (* 17 x_11) (* 17 x_12)) 0)) (assert (<= (+ (* 19 x_0) (* 19 x_1) (* 19 x_2) (* 19 x_3) (* 19 x_4) (* 19 x_5) (* 19 x_6) (* (- 220) x_7) (* 19 x_8) (* 19 x_9) (* 19 x_10) (* 19 x_11) (* 19 x_12)) 0)) (assert (<= (+ (* 23 x_0) (* 23 x_1) (* 23 x_2) (* 23 x_3) (* 23 x_4) (* 23 x_5) (* 23 x_6) (* 23 x_7) (* (- 216) x_8) (* 23 x_9) (* 23 x_10) (* 23 x_11) (* 23 x_12)) 0)) (assert (<= (+ (* 29 x_0) (* 29 x_1) (* 29 x_2) (* 29 x_3) (* 29 x_4) (* 29 x_5) (* 29 x_6) (* 29 x_7) (* 29 x_8) (* (- 210) x_9) (* 29 x_10) (* 29 x_11) (* 29 x_12)) 0)) (assert (<= (+ (* 31 x_0) (* 31 x_1) (* 31 x_2) (* 31 x_3) (* 31 x_4) (* 31 x_5) (* 31 x_6) (* 31 x_7) (* 31 x_8) (* 31 x_9) (* (- 208) x_10) (* 31 x_11) (* 31 x_12)) 0)) (assert (<= (+ (* 37 x_0) (* 37 x_1) (* 37 x_2) (* 37 x_3) (* 37 x_4) (* 37 x_5) (* 37 x_6) (* 37 x_7) (* 37 x_8) (* 37 x_9) (* 37 x_10) (* (- 202) x_11) (* 37 x_12)) 0)) (assert (<= (+ (* 41 x_0) (* 41 x_1) (* 41 x_2) (* 41 x_3) (* 41 x_4) (* 41 x_5) (* 41 x_6) (* 41 x_7) (* 41 x_8) (* 41 x_9) (* 41 x_10) (* 41 x_11) (* (- 198) x_12)) 0)) (assert (>= (+ x_0 x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8 x_9 x_10 x_11 x_12) 1)) (check-sat) (exit)