(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)