1 2 3 4 5
(set-logic QF_UF) (set-info :status sat) (declare-sort U 0) (declare-fun Constraint () U) (check-sat)