(set-logic QF_FP)
(set-option :produce-models true)
(declare-const m (_ FloatingPoint 8 24))
(define-fun p () (_ FloatingPoint 11 53) (fp #b0 #b10000001000 #b1111010000000000000000000000000000000000000000000000))
(define-fun b () (_ FloatingPoint 8 24) ((_ to_fp 8 24) RNE 1.0))
(assert (fp.gt m (_ +zero 8 24)))
(assert (fp.leq m b))
(define-fun lo0 () (_ FloatingPoint 11 53) (_ +zero 11 53))
(define-fun hi0 () (_ FloatingPoint 11 53) (fp #b0 #b10000010111 #b0011000101101000000010100101101000101000111000101110))
(assert (fp.lt ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p hi0)))) m))
(define-fun mid0 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo0 hi0) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up0 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid0)))) m))
(define-fun lo1 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi0 lo0) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up0) mid0 lo0))
(define-fun hi1 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi0 lo0) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up0)) mid0 hi0))
(define-fun mid1 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo1 hi1) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up1 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid1)))) m))
(define-fun lo2 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi1 lo1) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up1) mid1 lo1))
(define-fun hi2 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi1 lo1) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up1)) mid1 hi1))
(define-fun mid2 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo2 hi2) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up2 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid2)))) m))
(define-fun lo3 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi2 lo2) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up2) mid2 lo2))
(define-fun hi3 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi2 lo2) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up2)) mid2 hi2))
(define-fun mid3 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo3 hi3) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up3 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid3)))) m))
(define-fun lo4 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi3 lo3) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up3) mid3 lo3))
(define-fun hi4 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi3 lo3) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up3)) mid3 hi3))
(define-fun mid4 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo4 hi4) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up4 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid4)))) m))
(define-fun lo5 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi4 lo4) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up4) mid4 lo4))
(define-fun hi5 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi4 lo4) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up4)) mid4 hi4))
(define-fun mid5 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo5 hi5) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up5 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid5)))) m))
(define-fun lo6 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi5 lo5) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up5) mid5 lo5))
(define-fun hi6 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi5 lo5) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up5)) mid5 hi5))
(define-fun mid6 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo6 hi6) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up6 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid6)))) m))
(define-fun lo7 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi6 lo6) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up6) mid6 lo6))
(define-fun hi7 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi6 lo6) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up6)) mid6 hi6))
(define-fun mid7 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo7 hi7) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up7 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid7)))) m))
(define-fun lo8 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi7 lo7) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up7) mid7 lo7))
(define-fun hi8 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi7 lo7) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up7)) mid7 hi7))
(define-fun mid8 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo8 hi8) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up8 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid8)))) m))
(define-fun lo9 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi8 lo8) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up8) mid8 lo8))
(define-fun hi9 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi8 lo8) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up8)) mid8 hi8))
(define-fun mid9 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo9 hi9) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up9 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid9)))) m))
(define-fun lo10 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi9 lo9) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up9) mid9 lo9))
(define-fun hi10 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi9 lo9) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up9)) mid9 hi9))
(define-fun mid10 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo10 hi10) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up10 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid10)))) m))
(define-fun lo11 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi10 lo10) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up10) mid10 lo10))
(define-fun hi11 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi10 lo10) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up10)) mid10 hi10))
(define-fun mid11 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo11 hi11) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up11 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid11)))) m))
(define-fun lo12 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi11 lo11) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up11) mid11 lo11))
(define-fun hi12 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi11 lo11) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up11)) mid11 hi11))
(define-fun mid12 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo12 hi12) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up12 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid12)))) m))
(define-fun lo13 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi12 lo12) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up12) mid12 lo12))
(define-fun hi13 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi12 lo12) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up12)) mid12 hi12))
(define-fun mid13 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo13 hi13) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up13 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid13)))) m))
(define-fun lo14 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi13 lo13) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up13) mid13 lo13))
(define-fun hi14 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi13 lo13) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up13)) mid13 hi13))
(define-fun mid14 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo14 hi14) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up14 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid14)))) m))
(define-fun lo15 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi14 lo14) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up14) mid14 lo14))
(define-fun hi15 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi14 lo14) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up14)) mid14 hi14))
(define-fun mid15 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo15 hi15) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up15 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid15)))) m))
(define-fun lo16 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi15 lo15) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up15) mid15 lo15))
(define-fun hi16 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi15 lo15) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up15)) mid15 hi15))
(define-fun mid16 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo16 hi16) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up16 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid16)))) m))
(define-fun lo17 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi16 lo16) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up16) mid16 lo16))
(define-fun hi17 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi16 lo16) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up16)) mid16 hi16))
(define-fun mid17 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo17 hi17) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up17 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid17)))) m))
(define-fun lo18 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi17 lo17) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up17) mid17 lo17))
(define-fun hi18 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi17 lo17) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up17)) mid17 hi17))
(define-fun mid18 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo18 hi18) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up18 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid18)))) m))
(define-fun lo19 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi18 lo18) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up18) mid18 lo18))
(define-fun hi19 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi18 lo18) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up18)) mid18 hi18))
(define-fun mid19 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo19 hi19) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up19 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid19)))) m))
(define-fun lo20 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi19 lo19) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up19) mid19 lo19))
(define-fun hi20 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi19 lo19) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up19)) mid19 hi19))
(define-fun mid20 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo20 hi20) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up20 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid20)))) m))
(define-fun lo21 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi20 lo20) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up20) mid20 lo20))
(define-fun hi21 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi20 lo20) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up20)) mid20 hi20))
(define-fun mid21 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo21 hi21) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up21 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid21)))) m))
(define-fun lo22 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi21 lo21) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up21) mid21 lo21))
(define-fun hi22 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi21 lo21) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up21)) mid21 hi21))
(define-fun mid22 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo22 hi22) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up22 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid22)))) m))
(define-fun lo23 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi22 lo22) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up22) mid22 lo22))
(define-fun hi23 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi22 lo22) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up22)) mid22 hi22))
(define-fun mid23 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo23 hi23) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up23 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid23)))) m))
(define-fun lo24 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi23 lo23) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up23) mid23 lo23))
(define-fun hi24 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi23 lo23) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up23)) mid23 hi23))
(define-fun mid24 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo24 hi24) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up24 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid24)))) m))
(define-fun lo25 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi24 lo24) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up24) mid24 lo24))
(define-fun hi25 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi24 lo24) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up24)) mid24 hi24))
(define-fun mid25 () (_ FloatingPoint 11 53) (fp.mul RNE (fp.add RNE lo25 hi25) ((_ to_fp 11 53) RNE 0.5)))
(define-fun up25 () Bool (fp.geq ((_ to_fp 8 24) RNE (fp.mul RNE ((_ to_fp 11 53) RNE b) (fp.div RNE p (fp.add RNE p mid25)))) m))
(define-fun lo26 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi25 lo25) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) up25) mid25 lo25))
(define-fun hi26 () (_ FloatingPoint 11 53) (ite (and (fp.gt (fp.sub RNE hi25 lo25) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)) (not up25)) mid25 hi25))
(assert (fp.gt (fp.sub RNE hi26 lo26) (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))
(check-sat)
(get-value (m lo26 hi26))