(set-logic QF_BV)
(set-info :status unsat)
(assert (= #b1 (_ bv0 1)))
(declare-const v0 (_ BitVec 1))
(assert (= #b1 (ite (= (ite (= v0 (bvnot (_ bv0 1))) #b1 #b0) (bvnot (_ bv0 1))) #b1 #b0)))
(declare-const v1 (_ BitVec 1))
(assert (= #b1 (ite (= v1 v0) #b1 #b0)))
(declare-const v2 (_ BitVec 1))
(declare-const v3 (_ BitVec 1))
(assert (= #b1 (ite (= v2 (bvand v3 v1)) #b1 #b0)))
(declare-const v4 (_ BitVec 1))
(assert (= #b1 (ite (= v4 v2) #b1 #b0)))
(declare-const v5 (_ BitVec 1))
(declare-const v6 (_ BitVec 1))
(assert (= #b1 (ite (= (ite (= v5 (bvnot (_ bv0 1))) #b1 #b0) (bvnot (bvand (ite (= v4 (bvnot (_ bv0 1))) #b1 #b0) (bvnot v6)))) #b1 #b0)))
(declare-const v7 (_ BitVec 1))
(assert (= #b1 (ite (= v7 v5) #b1 #b0)))
(assert (= #b1 (ite (= (_ bv0 1) (ite (= v7 (bvnot (_ bv0 1))) #b1 #b0)) #b1 #b0)))
(check-sat)