(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun n () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun o () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(assert (not 
    (exists ((j Real)) 
        (let ((?k (- c))) 
        (let ((?l (+ (* ?k j) d)) (?p (* 2 c))) 
        (let ((m 0)) (=>  
            (and 
                (=> (<= 0 j f) (and (>= ?l 0) (<= j e)))  
                (>= d 0) 
                (= o (/ (* (/ (-  (*  3 g))  2) (/ (-  (*  3 g))  2)) ?p)) 
                (> (-  h) 0) 
                (<= (/ (-  (*  3 g))  2) n)) 
            (>= (+ (* ?k f) d) 0))))))))
(assert (= (+ c h) d (/ a i d  b n)))
(check-sat)
(get-model)

  (define-fun n () Real
    1.0)
  (define-fun b () Real
    0.0)
  (define-fun d () Real
    0.0)
  (define-fun a () Real
    (- (/ 1.0 8.0)))
  (define-fun i () Real
    0.0)
  (define-fun g () Real
    0.0)
  (define-fun c () Real
    (/ 1.0 2.0))
  (define-fun h () Real
    (- (/ 1.0 2.0)))
  (define-fun f () Real
    1.0)
  (define-fun o () Real
    0.0)
  (define-fun e () Real
    (- (/ 1.0 4.0)))