; EXPECT: sat
(set-logic ALL)
(set-option :incremental false)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Bool)
(declare-fun x_3 () Bool)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Bool)
(declare-fun x_7 () Bool)
(declare-fun x_8 () Bool)
(declare-fun x_9 () Bool)
(declare-fun x_10 () Bool)
(declare-fun x_11 () Bool)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Bool)
(declare-fun x_19 () Bool)
(declare-fun x_20 () Bool)
(assert (or (or (not x_9) x_3) (not x_15)))
(assert (or (or (not x_12) (not x_4)) (not x_15)))
(assert (or (or x_6 x_14) (not x_17)))
(assert (or (or x_10 x_16) x_11))
(assert (or (or (not x_15) x_20) (not x_7)))
(assert (or (or (not x_1) x_10) x_16))
(assert (or (or x_13 x_17) (not x_7)))
(assert (or (or (not x_2) (not x_14)) (not x_13)))
(assert (or (or x_13 (not x_6)) x_15))
(assert (or (or (not x_9) x_3) x_16))
(assert (or (or (not x_20) (not x_13)) x_4))
(assert (or (or (not x_7) x_15) (not x_14)))
(assert (or (or (not x_15) (not x_16)) x_6))
(assert (or (or x_5 (not x_18)) x_20))
(assert (or (or (not x_16) (not x_19)) x_7))
(assert (or (or x_20 (not x_18)) (not x_2)))
(assert (or (or x_10 (not x_19)) (not x_14)))
(assert (or (or x_16 (not x_7)) x_12))
(assert (or (or x_6 (not x_5)) (not x_1)))
(assert (or (or (not x_9) x_11) x_15))
(assert (or (or x_19 (not x_6)) x_7))
(assert (or (or (not x_11) x_17) (not x_19)))
(assert (or (or x_9 (not x_16)) x_6))
(assert (or (or x_15 (not x_20)) x_10))
(assert (or (or x_9 (not x_1)) (not x_11)))
(assert (or (or (not x_8) (not x_19)) x_5))
(assert (or (or (not x_19) x_11) x_20))
(assert (or (or (not x_12) x_13) (not x_3)))
(assert (or (or (not x_7) (not x_17)) (not x_19)))
(assert (or (or x_17 x_6) (not x_11)))
(assert (or (or (not x_7) (not x_17)) x_10))
(assert (or (or (not x_14) x_9) x_20))
(assert (or (or x_1 (not x_18)) (not x_16)))
(assert (or (or (not x_2) (not x_15)) x_20))
(assert (or (or x_14 x_18) (not x_1)))
(assert (or (or (not x_8) (not x_4)) x_1))
(assert (or (or x_13 x_3) (not x_9)))
(assert (or (or x_5 x_7) x_8))
(assert (or (or x_9 x_4) (not x_20)))
(assert (or (or (not x_18) (not x_15)) (not x_10)))
(assert (or (or x_10 x_3) (not x_20)))
(assert (or (or x_20 (not x_14)) x_16))
(assert (or (or x_20 (not x_3)) (not x_11)))
(assert (or (or (not x_12) x_19) (not x_16)))
(assert (or (or (not x_3) x_5) x_10))
(assert (or (or x_8 x_13) (not x_7)))
(assert (or (or (not x_2) (not x_15)) x_10))
(assert (or (or (not x_3) x_9) x_16))
(assert (or (or (not x_12) (not x_16)) (not x_18)))
(assert (or (or x_3 x_1) (not x_12)))
(assert (or (or (not x_18) x_13) x_5))
(assert (or (or x_1 x_3) (not x_19)))
(assert (or (or (not x_19) (not x_5)) x_6))
(assert (or (or (not x_20) x_8) (not x_2)))
(assert (or (or x_17 (not x_8)) (not x_13)))
(assert (or (or x_7 (not x_11)) (not x_12)))
(assert (or (or (not x_10) (not x_14)) (not x_20)))
(assert (or (or (not x_1) x_16) (not x_12)))
(assert (or (or x_5 (not x_3)) x_9))
(assert (or (or (not x_18) x_8) x_14))
(assert (or (or x_1 x_16) x_12))
(assert (or (or x_20 (not x_1)) (not x_16)))
(assert (or (or x_5 x_10) (not x_13)))
(assert (or (or x_9 (not x_10)) x_6))
(assert (or (or (not x_12) x_10) (not x_14)))
(assert (or (or (not x_13) x_1) x_4))
(assert (or (or (not x_20) (not x_7)) x_3))
(assert (or (or x_12 x_1) (not x_10)))
(assert (or (or (not x_1) (not x_16)) x_7))
(assert (or (or x_11 (not x_6)) (not x_4)))
(assert (or (or x_1 x_16) (not x_20)))
(assert (or (or x_9 x_7) x_15))
(assert (or (or (not x_6) x_17) x_10))
(assert (or (or x_8 x_9) x_17))
(assert (or (or x_18 x_11) x_10))
(assert (or (or x_7 x_1) (not x_8)))
(assert (or (or (not x_5) (not x_12)) x_18))
(assert (or (or (not x_6) x_2) x_15))
(assert (or (or x_2 x_18) x_1))
(assert (or (or (not x_7) (not x_13)) x_16))
(assert (or (or x_18 x_19) x_9))
(assert (or (or x_9 (not x_14)) x_18))
(assert (or (or x_14 x_12) (not x_5)))
(assert (or (or (not x_13) (not x_7)) (not x_14)))
(assert (or (or (not x_1) x_8) (not x_16)))
(assert (or (or (not x_11) x_4) x_7))
(assert (or (or (not x_4) x_20) x_5))
(assert (or (or (not x_5) x_2) x_12))
(assert (or (or (not x_5) x_13) (not x_18)))
(assert (or (or (not x_18) x_9) x_1))
(assert (or (or x_10 (not x_11)) x_16))
(check-sat)