(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 _let_0))) (let ((_let_2 (f _let_1))) (and (not (= x y)) (= _let_1 _let_2) (= _let_1 y) (= (f _let_2) z) (= _let_0 z) (not (= _let_0 y)))))) ))