Simplified61.9
\[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(b, b, \left(a \cdot c\right) \cdot -4\right)} - b\right) \cdot \frac{0.5}{a}}
\]
Proof
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (*.f64 a c) -4))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (*.f64 (*.f64 a c) (Rewrite<= metadata-eval (neg.f64 4))))) b) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 a c) 4))))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 a c)))))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (fma.f64 b b (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 a) c))))) b) (/.f64 1/2 a)): 0 points increase in error, 16 points decrease in error
(*.f64 (-.f64 (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) b) (/.f64 1/2 a)): 16 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))) (neg.f64 b))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c))))) (/.f64 1/2 a)): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= metadata-eval (/.f64 1 2)) a)): 0 points increase in error, 16 points decrease in error
(*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 -1)) 2) a)): 6 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (neg.f64 -1) 2)) a)): 16 points increase in error, 0 points decrease in error
(Rewrite=> associate-/l*_binary64 (/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 a (/.f64 (neg.f64 -1) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a 2) (neg.f64 -1)))): 0 points increase in error, 16 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 a)) (neg.f64 -1))): 16 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (/.f64 (*.f64 2 a) (Rewrite=> metadata-eval 1))): 0 points increase in error, 16 points decrease in error
(/.f64 (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 4 a) c)))) (Rewrite=> /-rgt-identity_binary64 (*.f64 2 a))): 0 points increase in error, 6 points decrease in error