(set-logic QF_BV)
(declare-const c0 (_ BitVec 4))
(declare-const c1 (_ BitVec 4))
(declare-const c2 (_ BitVec 4))
(declare-const c3 (_ BitVec 4))
(declare-const c4 (_ BitVec 4))
(declare-const c5 (_ BitVec 4))
(declare-const c6 (_ BitVec 4))
(declare-const c7 (_ BitVec 4))
(declare-const c8 (_ BitVec 4))
(declare-const c9 (_ BitVec 4))
(declare-const c10 (_ BitVec 4))
(declare-const c11 (_ BitVec 4))
(declare-const c12 (_ BitVec 4))
(declare-const c13 (_ BitVec 4))
(declare-const c14 (_ BitVec 4))
(assert (= c0 (_ bv0 4)))
(assert (= c1 (_ bv1 4)))
(assert (let ((t (bvxor c0 c1))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c0 c2))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c1 c3))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c1 c4))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c2 c5))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c3 c6))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c4 c6))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c4 c7))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c5 c8))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c8 c9))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c9 c10))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c10 c11))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c10 c12))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c11 c13))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c12 c13))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (let ((t (bvxor c12 c14))) (and (distinct t (_ bv0 4)) (= (bvand t (bvsub t (_ bv1 4))) (_ bv0 4)))))
(assert (distinct c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14))
(check-sat)
(get-model)