(set-logic QF_UFNIA)

(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)

(declare-fun f (Int) Int)
(declare-fun z () Bool)

;a ∗ (f (b) + f (c)) = d, b ∗ (f (a) + f (c)) ̸= d, a = b

(assert (= (* a (+ (f b) (f c))) d))
(assert (distinct (* b (+ (f a) (f c))) d))
(assert (= a b))
(check-sat)
(exit)