1 2 3 4 5 6 7 8 9 10
; EXPECT: unsat (set-logic HO_ALL) (set-info :status unsat) (declare-sort U 0) (declare-fun f (U) U) (declare-fun a () U) (declare-fun b () U) (assert (forall ((x (-> U U))) (= (x a) b))) (assert (not (= (f a) b))) (check-sat)