(set-logic QF_UF)
(declare-sort S 0)
(declare-fun f (S) Bool)
(declare-fun g (S) S)
(declare-fun x1 () S)
(declare-fun x2 () S)
(assert (not (f (g x1))))
(assert (= x1 (g (g x2))))
(assert (= (g x1) (g x2)))
(assert (distinct (g x1) x1))
(assert (distinct x2 (g x1)))
(check-sat)