(set-option :incremental false) (set-info :status unsat) (set-info :category "crafted") (set-logic QF_UF) (declare-sort U 0) (declare-fun x () U) (declare-fun y () U) (declare-fun f (U) Bool) (check-sat-assuming ( (let ((_let_0 (f x))) (let ((_let_1 (f y))) (and _let_0 (= _let_0 _let_1) (not _let_1)))) ))