(set-logic QF_UF) (set-info :status unsat) (declare-sort A 0) (declare-sort B 0) (declare-fun x () A) (declare-fun y () A) (declare-fun f (A) B) (assert (not (=> (= x y) (= (f x) (f y))))) (check-sat)