[644] % z3 rewriter.eq2ineq=true small.smt2 
sat
[645] % z3 small.smt2
unsat
[646] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(assert
 (forall ((e Real))
 (not
  (=>
  (= (<= (- 2) e b) (>= c (* e e)))
  (= c (* (- (+ a 1) d) (- (+ a 1) d)))
  (= d 0)))))
(check-sat)
[647] %