Skip to content

Instantly share code, notes, and snippets.

@zenna

zenna/gist:ad60335a22f05e66cdb4

Created June 4, 2015 08:18
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save zenna/ad60335a22f05e66cdb4 to your computer and use it in GitHub Desktop.
Save zenna/ad60335a22f05e66cdb4 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
(set-logic QF_NRA)
(declare-fun omega0 () Real)
(declare-fun omega1 () Real)
(push 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.25))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.25))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.375))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.375))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 0.9375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 0.9375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.40625 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.40625 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.9375 omega1))
(assert(<= omega1 0.96875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.9375 omega1))
(assert(<= omega1 0.96875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.390625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.390625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.398438 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.398438 omega0))
(assert(<= omega0 0.40625))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.984375 omega1))
(assert(<= omega1 0.992188))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.984375 omega1))
(assert(<= omega1 0.992188))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.394531 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.394531 omega0))
(assert(<= omega0 0.398438))
(assert(<= 0.992188 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.996094 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.996094 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.392578))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.390625 omega0))
(assert(<= omega0 0.392578))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.996094))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.994141 omega1))
(assert(<= omega1 0.996094))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.994141 omega1))
(assert(<= omega1 0.996094))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.393555))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.392578 omega0))
(assert(<= omega0 0.393555))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.994141))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.993164))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.992188 omega1))
(assert(<= omega1 0.993164))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.993164 omega1))
(assert(<= omega1 0.994141))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.393555 omega0))
(assert(<= omega0 0.394531))
(assert(<= 0.993164 omega1))
(assert(<= omega1 0.994141))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
;Initial satisfying point found!, starting MH chain
;box = Dict(0=>[0.0 1.0],1=>[0.0 1.0])
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 0.75))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 0.75))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 1))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.875 omega0))
(assert(<= omega0 1))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.875 omega0))
(assert(<= omega0 1))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.8125 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.8125 omega0))
(assert(<= omega0 0.875))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.8125 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.8125 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.78125 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.78125 omega0))
(assert(<= omega0 0.8125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.8125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.78125 omega1))
(assert(<= omega1 0.8125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.78125 omega1))
(assert(<= omega1 0.8125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.765625 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.765625 omega0))
(assert(<= omega0 0.78125))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.78125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.765625 omega1))
(assert(<= omega1 0.78125))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.765625 omega1))
(assert(<= omega1 0.78125))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.757812))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.75 omega0))
(assert(<= omega0 0.757812))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.765625))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.757813 omega1))
(assert(<= omega1 0.765625))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.757813 omega1))
(assert(<= omega1 0.765625))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.761719 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.761719 omega0))
(assert(<= omega0 0.765625))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.757812))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.753906 omega1))
(assert(<= omega1 0.757812))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.753906 omega1))
(assert(<= omega1 0.757812))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.759766 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.759766 omega0))
(assert(<= omega0 0.761719))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.753906))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.751953 omega1))
(assert(<= omega1 0.753906))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.751953 omega1))
(assert(<= omega1 0.753906))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.758789 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.758789 omega0))
(assert(<= omega0 0.759766))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.751953))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.750977))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.750977))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.750977 omega1))
(assert(<= omega1 0.751953))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.757813 omega0))
(assert(<= omega0 0.758789))
(assert(<= 0.750977 omega1))
(assert(<= omega1 0.751953))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
;box = Dict(0=>[0.0 1.0],1=>[0.0 1.0])
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.5 omega0))
(assert(<= omega0 1))
(assert(<= 0 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0 omega1))
(assert(<= omega1 0.5))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.25))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0 omega0))
(assert(<= omega0 0.25))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.5 omega1))
(assert(<= omega1 0.75))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.375))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.25 omega0))
(assert(<= omega0 0.375))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.75 omega1))
(assert(<= omega1 0.875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.375 omega0))
(assert(<= omega0 0.4375))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 0.9375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.875 omega1))
(assert(<= omega1 0.9375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.46875))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.4375 omega0))
(assert(<= omega0 0.46875))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 0.96875))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.9375 omega1))
(assert(<= omega1 0.96875))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.484375))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.46875 omega0))
(assert(<= omega0 0.484375))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.984375 omega1))
(assert(<= omega1 1))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.492188 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.492188 omega0))
(assert(<= omega0 0.5))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.984375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.976563 omega1))
(assert(<= omega1 0.984375))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.976563 omega1))
(assert(<= omega1 0.984375))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.488281))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.484375 omega0))
(assert(<= omega0 0.488281))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
; end
(push 1)
(assert(<= 0.488281 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577)))
(check-sat)
(pop 1)
(push 1)
(assert(<= 0.488281 omega0))
(assert(<= omega0 0.492188))
(assert(<= 0.96875 omega1))
(assert(<= omega1 0.976562))
(assert(not (and (and (<= (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5) 3) (<= 1 (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5))) (= (+ (* (log (/ omega1 (+ 1 (* -1 omega1)))) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) (/ (+ 0 (* -1 (log (+ 1 (* -1 omega0))))) 0.5)) 5.97577))))
(check-sat)
(pop 1)
(push 1)
(exit)
; end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment