(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 z () U)
(declare-fun f (U) U)
(declare-fun g (U) U)
(declare-fun H (U U) U)
(declare-fun J (U U) U)
(check-sat-assuming ( (let ((_let_0 (f x))) (let ((_let_1 (f z))) (let ((_let_2 (g y))) (let ((_let_3 (g z))) (let ((_let_4 (= _let_2 _let_3))) (and (not (= x y)) (= _let_0 _let_1) _let_4 _let_4 (= _let_2 y) (= _let_0 x) (= _let_1 z) (= _let_3 z) (or (not (= x z)) (not (= y z))))))))) ))