Average Error: 28.9 → 5.7
Time: 17.4s
Precision: binary64
Cost: 53376
\[\left(\left(1.0536712127723509 \cdot 10^{-8} < a \land a < 94906265.62425156\right) \land \left(1.0536712127723509 \cdot 10^{-8} < b \land b < 94906265.62425156\right)\right) \land \left(1.0536712127723509 \cdot 10^{-8} < c \land c < 94906265.62425156\right)\]
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a} \]
\[\mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \frac{{\left(c \cdot a\right)}^{4}}{\frac{\frac{a}{-1.0546875}}{{b}^{-7}}}\right)\right)\right) \]
(FPCore (a b c)
 :precision binary64
 (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))
(FPCore (a b c)
 :precision binary64
 (fma
  -0.5
  (/ c b)
  (fma
   -0.375
   (* (/ (* c c) (pow b 3.0)) a)
   (fma
    -0.5625
    (/ (pow c 3.0) (/ (pow b 5.0) (* a a)))
    (/ (pow (* c a) 4.0) (/ (/ a -1.0546875) (pow b -7.0)))))))
double code(double a, double b, double c) {
	return (-b + sqrt(((b * b) - ((3.0 * a) * c)))) / (3.0 * a);
}
double code(double a, double b, double c) {
	return fma(-0.5, (c / b), fma(-0.375, (((c * c) / pow(b, 3.0)) * a), fma(-0.5625, (pow(c, 3.0) / (pow(b, 5.0) / (a * a))), (pow((c * a), 4.0) / ((a / -1.0546875) / pow(b, -7.0))))));
}
function code(a, b, c)
	return Float64(Float64(Float64(-b) + sqrt(Float64(Float64(b * b) - Float64(Float64(3.0 * a) * c)))) / Float64(3.0 * a))
end
function code(a, b, c)
	return fma(-0.5, Float64(c / b), fma(-0.375, Float64(Float64(Float64(c * c) / (b ^ 3.0)) * a), fma(-0.5625, Float64((c ^ 3.0) / Float64((b ^ 5.0) / Float64(a * a))), Float64((Float64(c * a) ^ 4.0) / Float64(Float64(a / -1.0546875) / (b ^ -7.0))))))
end
code[a_, b_, c_] := N[(N[((-b) + N[Sqrt[N[(N[(b * b), $MachinePrecision] - N[(N[(3.0 * a), $MachinePrecision] * c), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] / N[(3.0 * a), $MachinePrecision]), $MachinePrecision]
code[a_, b_, c_] := N[(-0.5 * N[(c / b), $MachinePrecision] + N[(-0.375 * N[(N[(N[(c * c), $MachinePrecision] / N[Power[b, 3.0], $MachinePrecision]), $MachinePrecision] * a), $MachinePrecision] + N[(-0.5625 * N[(N[Power[c, 3.0], $MachinePrecision] / N[(N[Power[b, 5.0], $MachinePrecision] / N[(a * a), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(N[Power[N[(c * a), $MachinePrecision], 4.0], $MachinePrecision] / N[(N[(a / -1.0546875), $MachinePrecision] / N[Power[b, -7.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]
\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}
\mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \frac{{\left(c \cdot a\right)}^{4}}{\frac{\frac{a}{-1.0546875}}{{b}^{-7}}}\right)\right)\right)

Error

Derivation

  1. Initial program 28.9

    \[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a} \]
  2. Taylor expanded in b around inf 6.0

    \[\leadsto \frac{\color{blue}{-0.5 \cdot \frac{{\left(-1.125 \cdot \left({c}^{2} \cdot {a}^{2}\right)\right)}^{2} + 5.0625 \cdot \left({c}^{4} \cdot {a}^{4}\right)}{{b}^{7}} + \left(-1.125 \cdot \frac{{c}^{2} \cdot {a}^{2}}{{b}^{3}} + \left(-1.5 \cdot \frac{c \cdot a}{b} + -1.6875 \cdot \frac{{c}^{3} \cdot {a}^{3}}{{b}^{5}}\right)\right)}}{3 \cdot a} \]
  3. Simplified5.9

    \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(-0.5, \frac{\mathsf{fma}\left(5.0625, {c}^{4} \cdot {a}^{4}, \left({c}^{4} \cdot {a}^{4}\right) \cdot 1.265625\right)}{{b}^{7}}, \mathsf{fma}\left(-1.125, \frac{c \cdot c}{{b}^{3}} \cdot \left(a \cdot a\right), \mathsf{fma}\left(-1.6875, \frac{{\left(c \cdot a\right)}^{3}}{{b}^{5}}, -1.5 \cdot \left(\frac{c}{b} \cdot a\right)\right)\right)\right)}}{3 \cdot a} \]
    Proof
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (pow.f64 c (Rewrite<= metadata-eval (*.f64 2 2))) (pow.f64 a 4)) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 c 2) (pow.f64 c 2))) (pow.f64 a 4)) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 a (Rewrite<= metadata-eval (*.f64 2 2)))) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 a 2) (pow.f64 a 2)))) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (Rewrite=> unswap-sqr_binary64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (pow.f64 a 2)))) 81/64)) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (Rewrite<= metadata-eval (*.f64 -9/8 -9/8)))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) -9/8) (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) -9/8)))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2)))) (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) -9/8))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (*.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (Rewrite<= *-commutative_binary64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2)))))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (fma.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (pow.f64 b 3)) (*.f64 a a)) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (*.f64 (/.f64 (pow.f64 c 2) (pow.f64 b 3)) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 c 2) (/.f64 (pow.f64 b 3) (pow.f64 a 2)))) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 1 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (fma.f64 -27/16 (/.f64 (pow.f64 (*.f64 c a) 3) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (fma.f64 -27/16 (/.f64 (Rewrite=> cube-prod_binary64 (*.f64 (pow.f64 c 3) (pow.f64 a 3))) (pow.f64 b 5)) (*.f64 -3/2 (*.f64 (/.f64 c b) a))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (fma.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5)) (*.f64 -3/2 (Rewrite<= associate-/r/_binary64 (/.f64 c (/.f64 b a))))))): 33 points increase in error, 36 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (fma.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5)) (*.f64 -3/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c a) b)))))): 36 points increase in error, 36 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))) (*.f64 -3/2 (/.f64 (*.f64 c a) b)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (fma.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 1 points increase in error, 0 points decrease in error
    (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 (+.f64 (pow.f64 (*.f64 -9/8 (*.f64 (pow.f64 c 2) (pow.f64 a 2))) 2) (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (pow.f64 b 7))) (+.f64 (*.f64 -9/8 (/.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (pow.f64 b 3))) (+.f64 (*.f64 -3/2 (/.f64 (*.f64 c a) b)) (*.f64 -27/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 3)) (pow.f64 b 5))))))): 0 points increase in error, 0 points decrease in error
  4. Taylor expanded in c around 0 5.7

    \[\leadsto \color{blue}{-0.5625 \cdot \frac{{c}^{3} \cdot {a}^{2}}{{b}^{5}} + \left(-0.16666666666666666 \cdot \frac{{c}^{4} \cdot \left(1.265625 \cdot {a}^{4} + 5.0625 \cdot {a}^{4}\right)}{a \cdot {b}^{7}} + \left(-0.5 \cdot \frac{c}{b} + -0.375 \cdot \frac{{c}^{2} \cdot a}{{b}^{3}}\right)\right)} \]
  5. Simplified5.7

    \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \frac{{\left(c \cdot a\right)}^{4}}{\frac{a}{6.328125}} \cdot \frac{-0.16666666666666666}{{b}^{7}}\right)\right)\right)} \]
    Proof
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (*.f64 (/.f64 (*.f64 c c) (pow.f64 b 3)) a) (fma.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (pow.f64 b 3)) a) (fma.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 c 2) (/.f64 (pow.f64 b 3) a))) (fma.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (fma.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 1 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (pow.f64 (*.f64 c a) (Rewrite<= metadata-eval (*.f64 2 2))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (*.f64 c a) 2) (pow.f64 (*.f64 c a) 2))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a))) (pow.f64 (*.f64 c a) 2)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a))) (pow.f64 (*.f64 c a) 2)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a)) (pow.f64 (*.f64 c a) 2)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (pow.f64 (*.f64 c a) 2)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a)))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a)))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 1 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (*.f64 (pow.f64 a 2) (pow.f64 a 2)))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite=> pow-sqr_binary64 (pow.f64 a (*.f64 2 2)))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 1 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 a (Rewrite=> metadata-eval 4))) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 c (*.f64 2 2))) (pow.f64 a 4)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 c (Rewrite=> metadata-eval 4)) (pow.f64 a 4)) (/.f64 a 405/64)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (/.f64 a (Rewrite<= metadata-eval (+.f64 81/16 81/64)))) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (+.f64 81/16 81/64)) a)) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 c (Rewrite<= metadata-eval (*.f64 2 2))) (pow.f64 a 4)) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 c 2) (pow.f64 c 2))) (pow.f64 a 4)) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 a (Rewrite<= metadata-eval (*.f64 2 2)))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 a 2) (pow.f64 a 2)))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 1 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (Rewrite=> unswap-sqr_binary64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (pow.f64 a 2)))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 c c)) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 c c) (Rewrite=> unpow2_binary64 (*.f64 a a))) (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 c a) (*.f64 c a))) (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 1 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 c a) 2)) (*.f64 (pow.f64 c 2) (pow.f64 a 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 (*.f64 c a) 2) (*.f64 (Rewrite=> unpow2_binary64 (*.f64 c c)) (pow.f64 a 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 (*.f64 c a) 2) (*.f64 (*.f64 c c) (Rewrite=> unpow2_binary64 (*.f64 a a)))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 (*.f64 c a) 2) (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 c a) (*.f64 c a)))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (*.f64 (pow.f64 (*.f64 c a) 2) (Rewrite<= unpow2_binary64 (pow.f64 (*.f64 c a) 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 (*.f64 c a) (*.f64 2 2))) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (*.f64 (pow.f64 (*.f64 c a) (Rewrite=> metadata-eval 4)) (+.f64 81/16 81/64)) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/16 (pow.f64 (*.f64 c a) 4)) (*.f64 81/64 (pow.f64 (*.f64 c a) 4)))) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (+.f64 (*.f64 81/16 (pow.f64 (*.f64 c a) 4)) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 (*.f64 c a) 4) 81/64))) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (*.f64 (/.f64 (Rewrite<= fma-udef_binary64 (fma.f64 81/16 (pow.f64 (*.f64 c a) 4) (*.f64 (pow.f64 (*.f64 c a) 4) 81/64))) a) (/.f64 -1/6 (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (fma.f64 81/16 (pow.f64 (*.f64 c a) 4) (*.f64 (pow.f64 (*.f64 c a) 4) 81/64)) -1/6) (*.f64 a (pow.f64 b 7))))))): 0 points increase in error, 1 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 81/16 (pow.f64 (*.f64 c a) 4)) (*.f64 (pow.f64 (*.f64 c a) 4) 81/64))) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (+.f64 (*.f64 81/16 (pow.f64 (*.f64 c a) 4)) (Rewrite=> *-commutative_binary64 (*.f64 81/64 (pow.f64 (*.f64 c a) 4)))) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (Rewrite=> distribute-rgt-out_binary64 (*.f64 (pow.f64 (*.f64 c a) 4) (+.f64 81/16 81/64))) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (pow.f64 (*.f64 c a) (Rewrite<= metadata-eval (*.f64 2 2))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 (*.f64 c a) 2) (pow.f64 (*.f64 c a) 2))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a))) (pow.f64 (*.f64 c a) 2)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a))) (pow.f64 (*.f64 c a) 2)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a)) (pow.f64 (*.f64 c a) 2)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (pow.f64 (*.f64 c a) 2)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (Rewrite=> unpow2_binary64 (*.f64 (*.f64 c a) (*.f64 c a)))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 c c) (*.f64 a a)))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 c 2)) (*.f64 a a))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 a 2)) (*.f64 (pow.f64 c 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (*.f64 (pow.f64 a 2) (pow.f64 a 2)))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (Rewrite=> pow-sqr_binary64 (pow.f64 a (*.f64 2 2)))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c 2) (pow.f64 c 2)) (pow.f64 a (Rewrite=> metadata-eval 4))) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 c (*.f64 2 2))) (pow.f64 a 4)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 1 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (*.f64 (*.f64 (pow.f64 c (Rewrite=> metadata-eval 4)) (pow.f64 a 4)) (+.f64 81/16 81/64)) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (/.f64 (*.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4))))) -1/6) (*.f64 a (pow.f64 b 7)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))) -1/6))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (fma.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)) (Rewrite<= *-commutative_binary64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (fma.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))))): 0 points increase in error, 1 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))))): 0 points increase in error, 0 points decrease in error
    (fma.f64 -1/2 (/.f64 c b) (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 1 points decrease in error
    (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (*.f64 -1/2 (/.f64 c b)) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (+.f64 (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 27 points increase in error, 13 points decrease in error
    (+.f64 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))): 8 points increase in error, 10 points decrease in error
    (Rewrite=> associate-+l+_binary64 (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -1/6 (/.f64 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7))))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))))): 18 points increase in error, 22 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1/6 (+.f64 (*.f64 81/16 (*.f64 (pow.f64 c 4) (pow.f64 a 4))) (*.f64 81/64 (*.f64 (pow.f64 c 4) (pow.f64 a 4))))) (*.f64 a (pow.f64 b 7))))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (/.f64 (*.f64 -1/6 (Rewrite=> distribute-rgt-out_binary64 (*.f64 (*.f64 (pow.f64 c 4) (pow.f64 a 4)) (+.f64 81/16 81/64)))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (/.f64 (*.f64 -1/6 (Rewrite=> associate-*l*_binary64 (*.f64 (pow.f64 c 4) (*.f64 (pow.f64 a 4) (+.f64 81/16 81/64))))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (/.f64 (*.f64 -1/6 (*.f64 (pow.f64 c 4) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 81/16 (pow.f64 a 4)) (*.f64 81/64 (pow.f64 a 4)))))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (/.f64 (*.f64 -1/6 (*.f64 (pow.f64 c 4) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (*.f64 -1/2 (/.f64 c b)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -1/2 (/.f64 c b)))) (+.f64 (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (*.f64 -1/2 (/.f64 c b))) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))))): 22 points increase in error, 18 points decrease in error
    (+.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3)))))) (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5)))): 0 points increase in error, 3 points decrease in error
    (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -9/16 (/.f64 (*.f64 (pow.f64 c 3) (pow.f64 a 2)) (pow.f64 b 5))) (+.f64 (*.f64 -1/6 (/.f64 (*.f64 (pow.f64 c 4) (+.f64 (*.f64 81/64 (pow.f64 a 4)) (*.f64 81/16 (pow.f64 a 4)))) (*.f64 a (pow.f64 b 7)))) (+.f64 (*.f64 -1/2 (/.f64 c b)) (*.f64 -3/8 (/.f64 (*.f64 (pow.f64 c 2) a) (pow.f64 b 3))))))): 0 points increase in error, 0 points decrease in error
  6. Applied egg-rr5.7

    \[\leadsto \mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \color{blue}{0 + \left(\frac{{\left(c \cdot a\right)}^{4}}{a} \cdot -1.0546875\right) \cdot {b}^{-7}}\right)\right)\right) \]
  7. Simplified5.7

    \[\leadsto \mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \color{blue}{\frac{{\left(c \cdot a\right)}^{4}}{\frac{\frac{a}{-1.0546875}}{{b}^{-7}}}}\right)\right)\right) \]
    Proof
    (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (/.f64 a -135/128) (pow.f64 b -7))): 0 points increase in error, 0 points decrease in error
    (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (/.f64 a (Rewrite<= metadata-eval (/.f64 -1/6 64/405))) (pow.f64 b -7))): 0 points increase in error, 0 points decrease in error
    (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 a 64/405) -1/6)) (pow.f64 b -7))): 35 points increase in error, 10 points decrease in error
    (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) (/.f64 (*.f64 a 64/405) -1/6)) (pow.f64 b -7))): 42 points increase in error, 36 points decrease in error
    (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 (*.f64 c a) 4) -1/6) (*.f64 a 64/405))) (pow.f64 b -7)): 38 points increase in error, 33 points decrease in error
    (*.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) a) (/.f64 -1/6 64/405))) (pow.f64 b -7)): 38 points increase in error, 56 points decrease in error
    (*.f64 (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) a) (Rewrite=> metadata-eval -135/128)) (pow.f64 b -7)): 0 points increase in error, 0 points decrease in error
    (Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 (*.f64 (/.f64 (pow.f64 (*.f64 c a) 4) a) -135/128) (pow.f64 b -7)))): 0 points increase in error, 0 points decrease in error
  8. Final simplification5.7

    \[\leadsto \mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.375, \frac{c \cdot c}{{b}^{3}} \cdot a, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \frac{{\left(c \cdot a\right)}^{4}}{\frac{\frac{a}{-1.0546875}}{{b}^{-7}}}\right)\right)\right) \]

Alternatives

Alternative 1
Error6.5
Cost40964
\[\begin{array}{l} t_0 := c \cdot \left(a \cdot -3\right)\\ \mathbf{if}\;\frac{\sqrt{b \cdot b + t_0} - b}{3 \cdot a} \leq -1.05:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b, b, t_0\right)} - b}{3 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \mathsf{fma}\left(-0.5, \frac{c}{b}, \frac{-0.375 \cdot \left(c \cdot \left(c \cdot a\right)\right)}{{b}^{3}}\right)\right)\\ \end{array} \]
Alternative 2
Error6.5
Cost40964
\[\begin{array}{l} t_0 := c \cdot \left(a \cdot -3\right)\\ \mathbf{if}\;\frac{\sqrt{b \cdot b + t_0} - b}{3 \cdot a} \leq -1.05:\\ \;\;\;\;\frac{\sqrt{\mathsf{fma}\left(b, b, t_0\right)} - b}{3 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.5, \frac{c}{b}, \mathsf{fma}\left(-0.5625, \frac{{c}^{3}}{\frac{{b}^{5}}{a \cdot a}}, \frac{\left(c \cdot c\right) \cdot \left(-0.375 \cdot a\right)}{{b}^{3}}\right)\right)\\ \end{array} \]
Alternative 3
Error9.5
Cost21124
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -0.0002:\\ \;\;\;\;\frac{b - \sqrt{\mathsf{fma}\left(b, b, \left(c \cdot a\right) \cdot -3\right)}}{a} \cdot -0.3333333333333333\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(-0.375, \frac{a}{\frac{{b}^{3}}{c \cdot c}}, -0.5 \cdot \frac{c}{b}\right)\\ \end{array} \]
Alternative 4
Error9.7
Cost21060
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -0.0002:\\ \;\;\;\;\left(b - \sqrt{\mathsf{fma}\left(b, b, a \cdot \left(c \cdot -3\right)\right)}\right) \cdot \frac{-0.3333333333333333}{a}\\ \mathbf{else}:\\ \;\;\;\;-0.3333333333333333 \cdot \mathsf{fma}\left(\frac{a}{\frac{b \cdot b}{c} \cdot \frac{b}{c}}, 1.125, \frac{c}{b} \cdot 1.5\right)\\ \end{array} \]
Alternative 5
Error9.7
Cost21060
\[\begin{array}{l} \mathbf{if}\;\frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a} \leq -0.0002:\\ \;\;\;\;\frac{b - \sqrt{\mathsf{fma}\left(b, b, \left(c \cdot a\right) \cdot -3\right)}}{a} \cdot -0.3333333333333333\\ \mathbf{else}:\\ \;\;\;\;-0.3333333333333333 \cdot \mathsf{fma}\left(\frac{a}{\frac{b \cdot b}{c} \cdot \frac{b}{c}}, 1.125, \frac{c}{b} \cdot 1.5\right)\\ \end{array} \]
Alternative 6
Error9.7
Cost15044
\[\begin{array}{l} t_0 := \frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a}\\ \mathbf{if}\;t_0 \leq -0.0002:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;-0.3333333333333333 \cdot \mathsf{fma}\left(\frac{a}{\frac{b \cdot b}{c} \cdot \frac{b}{c}}, 1.125, \frac{c}{b} \cdot 1.5\right)\\ \end{array} \]
Alternative 7
Error15.0
Cost14788
\[\begin{array}{l} t_0 := \frac{\sqrt{b \cdot b + c \cdot \left(a \cdot -3\right)} - b}{3 \cdot a}\\ \mathbf{if}\;t_0 \leq -2.7 \cdot 10^{-5}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \frac{c}{b}\\ \end{array} \]
Alternative 8
Error16.6
Cost7492
\[\begin{array}{l} \mathbf{if}\;b \leq 750:\\ \;\;\;\;\frac{\sqrt{b \cdot b + \left(c \cdot a\right) \cdot -3} - b}{3 \cdot a}\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \frac{c}{b}\\ \end{array} \]
Alternative 9
Error22.4
Cost320
\[-0.5 \cdot \frac{c}{b} \]

Error

Reproduce

herbie shell --seed 2022338 
(FPCore (a b c)
  :name "Cubic critical, narrow range"
  :precision binary64
  :pre (and (and (and (< 1.0536712127723509e-8 a) (< a 94906265.62425156)) (and (< 1.0536712127723509e-8 b) (< b 94906265.62425156))) (and (< 1.0536712127723509e-8 c) (< c 94906265.62425156)))
  (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))