2 (set-option :ag-miniscope-quant true)
3 (set-option :conjecture-gen true)
4 (set-option :int-wf-ind true)
5 (set-option :quant-model-ee true)
6 (set-option :sygus-inference true)
7 (set-option :uf-ho true)
8 (set-info :status unsat)
9 (declare-fun a () Real)
10 (declare-fun b () Real)
11 (declare-fun c () Real)
12 (declare-fun e () Real)
13 (assert (forall ((d Real)) (and (or (< (/ (* (- a) d) 0) c) (> b 0.0)) (= (= d 0) (= e 0)))))