(set-logic QF_BV)
(set-info :status sat)
(declare-const v0 (_ BitVec 8))
(assert (distinct (_ bv0 8) v0))
(declare-const v1 (_ BitVec 8))
(assert (distinct (_ bv0 8) v1))
(declare-const v2 (_ BitVec 8))
(assert (distinct (_ bv0 8) v2))
(declare-const v3 (_ BitVec 8))
(assert (distinct (_ bv0 8) v3))
(declare-const v4 (_ BitVec 8))
(assert (distinct (_ bv0 8) v4))
(declare-const v5 (_ BitVec 8))
(assert (distinct (_ bv0 8) v5))
(declare-const v6 (_ BitVec 8))
(assert (distinct (_ bv0 8) v6))
(declare-const v7 (_ BitVec 8))
(assert (distinct (_ bv0 8) v7))
(declare-const v8 (_ BitVec 8))
(assert (distinct (_ bv0 8) v8))
(declare-const v9 (_ BitVec 8))
(assert (distinct (_ bv0 8) v9))
(declare-const v10 (_ BitVec 8))
(assert (distinct (_ bv0 8) v10))
(declare-const v11 (_ BitVec 8))
(assert (distinct (_ bv0 8) v11))
(declare-const v12 (_ BitVec 8))
(assert (distinct (_ bv0 8) v12))
(declare-const v13 (_ BitVec 8))
(assert (distinct (_ bv0 8) v13))
(declare-const v14 (_ BitVec 8))
(assert (distinct (_ bv0 8) v14))
(declare-const v15 (_ BitVec 8))
(assert (distinct (_ bv0 8) v15))
(declare-const v16 (_ BitVec 8))
(assert (distinct (_ bv0 8) v16))
(declare-const v17 (_ BitVec 8))
(assert (distinct (_ bv0 8) v17))
(declare-const v18 (_ BitVec 8))
(assert (distinct (_ bv0 8) v18))
(declare-const v19 (_ BitVec 8))
(assert (distinct (_ bv0 8) v19))
(declare-const v20 (_ BitVec 8))
(assert (distinct (_ bv0 8) v20))
(declare-const v21 (_ BitVec 8))
(assert (distinct (_ bv0 8) v21))
(declare-const v22 (_ BitVec 8))
(assert (distinct (_ bv0 8) v22))
(declare-const v23 (_ BitVec 8))
(assert (distinct (_ bv0 8) v23))
(declare-const v24 (_ BitVec 8))
(assert (distinct (_ bv0 8) v24))
(declare-const v25 (_ BitVec 8))
(assert (distinct (_ bv0 8) v25))
(declare-const v26 (_ BitVec 8))
(assert (distinct (_ bv0 8) v26))
(declare-const v27 (_ BitVec 8))
(assert (distinct (_ bv0 8) v27))
(declare-const v28 (_ BitVec 8))
(assert (distinct (_ bv0 8) v28))
(check-sat)