(set-logic QF_UF) (set-info :status sat) (declare-sort U 0) (declare-fun Constraint () U) (check-sat)