(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 h (Int Int) Int) (declare-fun g (Int Int) Int) (declare-fun z () Bool) ;a ∗ (f (b) + f (c)) = d, b ∗ (f (a) + f (c)) ̸= d, a = b (assert (= (h a (g (f b) (f c))) d)) (assert (distinct (h b (g (f a) (f c))) d)) (assert (= a b)) (check-sat) (exit)