(set-logic QF_UFC)
(set-info :status sat)
(declare-sort S0 0)
(declare-const S0-0 S0)
(assert (fmf.card S0-0 1))
(assert (fmf.card S0-0 4))
(check-sat)