(set-logic QF_FP)
(declare-fun a () (_ FloatingPoint 8 24))
(declare-fun b () (_ FloatingPoint 8 24))
(declare-fun x () (_ FloatingPoint 8 24))
(assert (and (not (fp.isNaN a)) (not (fp.isInfinite a))))
(assert (and (not (fp.isNaN b)) (not (fp.isInfinite b))))
(assert (and (not (fp.isNaN x)) (not (fp.isInfinite x))))
(assert (or (fp.isNormal (fp.div roundNearestTiesToEven
                         (fp.sub roundNearestTiesToEven b a)
                         (fp #b0 #x82 #b11100000000000000000000)))
    (fp.eq a b)))
(assert (let ((a!1 (ite (and (fp.isZero x) (fp.isZero a))
                (ite (and (fp.isNegative x) (fp.isNegative a))
                     (_ -zero 8 24)
                     (_ +zero 8 24))
                (ite (fp.gt x a) x a))))
(let ((a!2 (fp.isNaN (ite (or (fp.isNaN x) (fp.isNaN a)) (_ NaN 8 24) a!1)))
      (a!3 (fp.isZero (ite (or (fp.isNaN x) (fp.isNaN a)) (_ NaN 8 24) a!1)))
      (a!4 (fp.isNegative (ite (or (fp.isNaN x) (fp.isNaN a)) (_ NaN 8 24) a!1)))
      (a!5 (fp.lt (ite (or (fp.isNaN x) (fp.isNaN a)) (_ NaN 8 24) a!1) b)))
(let ((a!6 (ite a!5 (ite (or (fp.isNaN x) (fp.isNaN a)) (_ NaN 8 24) a!1) b)))
(let ((a!7 (ite (and a!3 (fp.isZero b))
                (ite (or a!4 (fp.isNegative b)) (_ -zero 8 24) (_ +zero 8 24))
                a!6)))
(let ((a!8 (fp.sub roundNearestTiesToEven
                   (ite (or a!2 (fp.isNaN b)) (_ NaN 8 24) a!7)
                   a)))
(let ((a!9 (fp.div roundNearestTiesToEven
                   a!8
                   (fp.div roundNearestTiesToEven
                           (fp.sub roundNearestTiesToEven b a)
                           (fp #b0 #x82 #b11100000000000000000000)))))
  (and (not (fp.isNaN a!9))
       (or (fp.lt a!9 (fp #b1 #x7e #b00000000000000000000000))
           (fp.geq a!9 (fp #b0 #x82 #b11110000000000000000000)))))))))))
(check-sat)