(set-logic QF_UF)
(set-info :status unsat)
(declare-sort U 0)

(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun a () U)
(declare-fun b () U)
(declare-fun c () U)
(declare-fun d () U)
(declare-fun e () U)
(declare-fun h () U)
(declare-fun i () U)

(assert (or 
(= a c)
(= h c)
(not (= h d))
(not (= h e))
(= h i)
(= (= (f a) d) (= d (f b)))
(= (not (= (f a) d)) (not (= d (f b))))
(not (= (not (= d (f b))) (= (f a) d)))
(not (= (= d (f b)) (not (= (f a) d))))
(xor (= (f a) d) (not (= d (f b))))
(xor (not (= (f a) d)) (= d (f b)))
(not (xor (= (f a) d) (= d (f b))))
(not (xor (not (= (f a) d)) (not (= d (f b)))))
))
(assert (not (= h i)))
(assert (or (not (= (f a) d)) (not (= d (f b)))))
(assert (or (= (f a) d) (= d (f b))))
(assert (and (not (= b e)) (not (= c a))))
(assert (and (= h e) (not (= b e))))

(assert (not (or (= b h) (= c h))))
(assert (not (or (= b h) (not (= d h)))))
(check-sat)