(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun i () Real)
(declare-fun e () Real)
(declare-fun ep () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(declare-fun g () Real)
(assert
  (or
    (not
      (exists
        ((h Real))
        (=>
          (and (= 0.0 (/ b j)) (< 0.0 e))
        (=> (= 0.0 i) (= (= (<= 0.0 h)  (<= h ep)) (= 1.0 2.0)))  ;; LINE 18
        )
    )
  )

    (not
      (exists
        ((h Real))
        (=> (<= 0.0 (/ a h)) (= 0 (/ c e)))
      )
    )
  )
)
(assert (= c (/ c g) g 0))
(assert (= ep (/ d f)))
(check-sat)