(set-info :status unsat)
(declare-const x Bool)
(declare-const x1 Bool)
(declare-const x4 Bool)
(assert (distinct x x4))
(push 1)
(assert (= x1 (distinct x x4)))
(assert (and (distinct true x4) (= x1 x4)))
(check-sat)