reset.smt2

(set-option :produce-unsat-assumptions true)
(set-logic QF_UF)
(declare-fun x1 () Bool)
(declare-fun x2 () Bool)
(declare-fun x3 () Bool)
(assert (! x1 :named C1))
(assert (! (not x1) :named C2))
(assert (! (or (not x1) x2) :named C3))
(assert (! (not x2) :named C4))
(assert (! (or (not x1) x3) :named C5))
(assert (! (not x3) :named C6))
(check-sat)
(reset)
(check-sat)