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