(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :category "crafted")
(set-info :status unsat)
(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)
(declare-fun x_17 () Int)
(declare-fun x_18 () Int)
(declare-fun x_19 () 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 (>= x_17 0))
(assert (>= x_18 0))
(assert (>= x_19 0))
(assert (<= (+ (* (- 638) 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) (* 2 x_13) (* 2 x_14) (* 2 x_15) (* 2 x_16) (* 2 x_17) (* 2 x_18) (* 2 x_19)) 0))
(assert (<= (+ (* 3 x_0) (* (- 637) 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) (* 3 x_13) (* 3 x_14) (* 3 x_15) (* 3 x_16) (* 3 x_17) (* 3 x_18) (* 3 x_19)) 0))
(assert (<= (+ (* 5 x_0) (* 5 x_1) (* (- 635) 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) (* 5 x_13) (* 5 x_14) (* 5 x_15) (* 5 x_16) (* 5 x_17) (* 5 x_18) (* 5 x_19)) 0))
(assert (<= (+ (* 7 x_0) (* 7 x_1) (* 7 x_2) (* (- 633) 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) (* 7 x_13) (* 7 x_14) (* 7 x_15) (* 7 x_16) (* 7 x_17) (* 7 x_18) (* 7 x_19)) 0))
(assert (<= (+ (* 11 x_0) (* 11 x_1) (* 11 x_2) (* 11 x_3) (* (- 629) 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) (* 11 x_13) (* 11 x_14) (* 11 x_15) (* 11 x_16) (* 11 x_17) (* 11 x_18) (* 11 x_19)) 0))
(assert (<= (+ (* 13 x_0) (* 13 x_1) (* 13 x_2) (* 13 x_3) (* 13 x_4) (* (- 627) x_5) (* 13 x_6) (* 13 x_7) (* 13 x_8) (* 13 x_9) (* 13 x_10) (* 13 x_11) (* 13 x_12) (* 13 x_13) (* 13 x_14) (* 13 x_15) (* 13 x_16) (* 13 x_17) (* 13 x_18) (* 13 x_19)) 0))
(assert (<= (+ (* 17 x_0) (* 17 x_1) (* 17 x_2) (* 17 x_3) (* 17 x_4) (* 17 x_5) (* (- 623) x_6) (* 17 x_7) (* 17 x_8) (* 17 x_9) (* 17 x_10) (* 17 x_11) (* 17 x_12) (* 17 x_13) (* 17 x_14) (* 17 x_15) (* 17 x_16) (* 17 x_17) (* 17 x_18) (* 17 x_19)) 0))
(assert (<= (+ (* 19 x_0) (* 19 x_1) (* 19 x_2) (* 19 x_3) (* 19 x_4) (* 19 x_5) (* 19 x_6) (* (- 621) x_7) (* 19 x_8) (* 19 x_9) (* 19 x_10) (* 19 x_11) (* 19 x_12) (* 19 x_13) (* 19 x_14) (* 19 x_15) (* 19 x_16) (* 19 x_17) (* 19 x_18) (* 19 x_19)) 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) (* (- 617) x_8) (* 23 x_9) (* 23 x_10) (* 23 x_11) (* 23 x_12) (* 23 x_13) (* 23 x_14) (* 23 x_15) (* 23 x_16) (* 23 x_17) (* 23 x_18) (* 23 x_19)) 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) (* (- 611) x_9) (* 29 x_10) (* 29 x_11) (* 29 x_12) (* 29 x_13) (* 29 x_14) (* 29 x_15) (* 29 x_16) (* 29 x_17) (* 29 x_18) (* 29 x_19)) 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) (* (- 609) x_10) (* 31 x_11) (* 31 x_12) (* 31 x_13) (* 31 x_14) (* 31 x_15) (* 31 x_16) (* 31 x_17) (* 31 x_18) (* 31 x_19)) 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) (* (- 603) x_11) (* 37 x_12) (* 37 x_13) (* 37 x_14) (* 37 x_15) (* 37 x_16) (* 37 x_17) (* 37 x_18) (* 37 x_19)) 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) (* (- 599) x_12) (* 41 x_13) (* 41 x_14) (* 41 x_15) (* 41 x_16) (* 41 x_17) (* 41 x_18) (* 41 x_19)) 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) (* (- 597) x_13) (* 43 x_14) (* 43 x_15) (* 43 x_16) (* 43 x_17) (* 43 x_18) (* 43 x_19)) 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) (* (- 593) x_14) (* 47 x_15) (* 47 x_16) (* 47 x_17) (* 47 x_18) (* 47 x_19)) 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) (* (- 587) x_15) (* 53 x_16) (* 53 x_17) (* 53 x_18) (* 53 x_19)) 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) (* (- 581) x_16) (* 59 x_17) (* 59 x_18) (* 59 x_19)) 0))
(assert (<= (+ (* 61 x_0) (* 61 x_1) (* 61 x_2) (* 61 x_3) (* 61 x_4) (* 61 x_5) (* 61 x_6) (* 61 x_7) (* 61 x_8) (* 61 x_9) (* 61 x_10) (* 61 x_11) (* 61 x_12) (* 61 x_13) (* 61 x_14) (* 61 x_15) (* 61 x_16) (* (- 579) x_17) (* 61 x_18) (* 61 x_19)) 0))
(assert (<= (+ (* 67 x_0) (* 67 x_1) (* 67 x_2) (* 67 x_3) (* 67 x_4) (* 67 x_5) (* 67 x_6) (* 67 x_7) (* 67 x_8) (* 67 x_9) (* 67 x_10) (* 67 x_11) (* 67 x_12) (* 67 x_13) (* 67 x_14) (* 67 x_15) (* 67 x_16) (* 67 x_17) (* (- 573) x_18) (* 67 x_19)) 0))
(assert (<= (+ (* 71 x_0) (* 71 x_1) (* 71 x_2) (* 71 x_3) (* 71 x_4) (* 71 x_5) (* 71 x_6) (* 71 x_7) (* 71 x_8) (* 71 x_9) (* 71 x_10) (* 71 x_11) (* 71 x_12) (* 71 x_13) (* 71 x_14) (* 71 x_15) (* 71 x_16) (* 71 x_17) (* 71 x_18) (* (- 569) x_19)) 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 x_17 x_18 x_19) 1))
(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 x_17 x_18 x_19) 638))
(check-sat)
(exit)