(set-option :auto_config false)
(set-option :smt.case_split 3)
(set-option :smt.delay_units true)
(declare-sort U)
(declare-sort T)
(declare-const bb Bool)
(declare-fun a () U)
(declare-fun b () T)
(declare-fun e (U) U)
(declare-fun f (U) U)
(declare-fun g (T) U)
(declare-fun h (U) U)
(declare-fun D (U) Int)
(declare-fun E (U Bool U) U)
(declare-fun F (U) U)
(declare-fun Q (U Bool U) Bool)
(declare-fun P (U U) Bool)
(assert (forall ((x U) (y Bool) (z U)) (! (not (Q x y z)) :pattern ((E x y z)))))
(assert (forall ((x U)) (and (Q (f a) false (F (e (g b)))) (= (h a) (ite (P (f a) (E (f a) (< 0 (D a)) (F (e (g b))))) (f a) (h x))))))
(assert (or (=> bb (P a (h a)))))
(check-sat)