(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)
(declare-fun x_13 () Int)
(declare-fun x_14 () Int)
(declare-fun x_15 () Int)
(declare-fun x_16 () 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 (>= x_13 0))
(assert (>= x_14 0))
(assert (>= x_15 0))
(assert (>= x_16 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) (* (- 404) x_11) (* 37 x_12) (* 37 x_13) (* 37 x_14) (* 37 x_15) (* 37 x_16)) 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) (* (- 400) x_12) (* 41 x_13) (* 41 x_14) (* 41 x_15) (* 41 x_16)) 0))
(assert (<= (+ (* 43 x_0) (* 43 x_1) (* 43 x_2) (* 43 x_3) (* 43 x_4) (* 43 x_5) (* 43 x_6) (* 43 x_7) (* 43 x_8) (* 43 x_9) (* 43 x_10) (* 43 x_11) (* 43 x_12) (* (- 398) x_13) (* 43 x_14) (* 43 x_15) (* 43 x_16)) 0))
(assert (<= (+ (* 47 x_0) (* 47 x_1) (* 47 x_2) (* 47 x_3) (* 47 x_4) (* 47 x_5) (* 47 x_6) (* 47 x_7) (* 47 x_8) (* 47 x_9) (* 47 x_10) (* 47 x_11) (* 47 x_12) (* 47 x_13) (* (- 394) x_14) (* 47 x_15) (* 47 x_16)) 0))
(assert (<= (+ (* 53 x_0) (* 53 x_1) (* 53 x_2) (* 53 x_3) (* 53 x_4) (* 53 x_5) (* 53 x_6) (* 53 x_7) (* 53 x_8) (* 53 x_9) (* 53 x_10) (* 53 x_11) (* 53 x_12) (* 53 x_13) (* 53 x_14) (* (- 388) x_15) (* 53 x_16)) 0))
(assert (<= (+ (* 59 x_0) (* 59 x_1) (* 59 x_2) (* 59 x_3) (* 59 x_4) (* 59 x_5) (* 59 x_6) (* 59 x_7) (* 59 x_8) (* 59 x_9) (* 59 x_10) (* 59 x_11) (* 59 x_12) (* 59 x_13) (* 59 x_14) (* 59 x_15) (* (- 382) x_16)) 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 x_13 x_14 x_15 x_16) 1))
(check-sat)
(exit)