Cubic critical, wide range

Average Accuracy: 17.9% → 97.6%

Time: 17.7s

Precision: binary64

Cost: 53504

\[\left(\left(4.930380657631324 \cdot 10^{-32} < a \land a < 2.028240960365167 \cdot 10^{+31}\right) \land \left(4.930380657631324 \cdot 10^{-32} < b \land b < 2.028240960365167 \cdot 10^{+31}\right)\right) \land \left(4.930380657631324 \cdot 10^{-32} < c \land c < 2.028240960365167 \cdot 10^{+31}\right)\]

Math

\[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]

↓

\[\mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 4\right), \mathsf{/.f64}\left(\frac{405}{64}, \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

FPCore

(FPCore (a b c)
 :precision binary64
 (/.f64
  (+.f64 (neg.f64 b) (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 3 a) c))))
  (*.f64 3 a)))

↓

(FPCore (a b c)
 :precision binary64
 (fma.f64
  -9/16
  (/.f64 (pow.f64 c 3) (/.f64 (pow.f64 b 5) (*.f64 a a)))
  (fma.f64
   -1/6
   (*.f64 (pow.f64 (*.f64 c a) 4) (/.f64 405/64 (*.f64 a (pow.f64 b 7))))
   (fma.f64
    -1/2
    (/.f64 c b)
    (*.f64 -3/8 (/.f64 (*.f64 c c) (/.f64 (pow.f64 b 3) a)))))))

Derivation

1. Initial program 17.9%

   \[\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]

2. Simplified 17.9%

   \[\leadsto \color{blue}{\mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(b, b, \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)\right)\right), a\right)\right)} \]
   Proof

   [Start] 17.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]
   /-rgt-identity [<=] 17.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(3, a\right), 1\right)}\right) \]
   metadata-eval [<=] 17.9	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(3, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
   associate-/l* [<=] 17.9	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{neg.f64}\left(-1\right)\right), \mathsf{*.f64}\left(3, a\right)\right)} \]
   associate-*r/ [<=] 17.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(3, a\right)\right)\right)} \]
   *-commutative [=>] 17.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{*.f64}\left(3, a\right)\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right)\right)} \]
   associate-*l/ [=>] 17.9	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right)} \]
   associate-*r/ [<=] 17.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right)\right)} \]
   metadata-eval [=>] 17.9	\[ \mathsf{*.f64}\left(\color{blue}{1}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right)\right) \]
   metadata-eval [<=] 17.9	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(-1, -1\right)}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right)\right) \]
   times-frac [<=] 17.9	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(3, a\right)\right)\right)} \]
   neg-mul-1 [<=] 17.9	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(3, a\right)\right)}\right) \]
   distribute-rgt-neg-in [=>] 17.9	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(3, \mathsf{neg.f64}\left(a\right)\right)}\right) \]
   times-frac [=>] 17.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(-1, 3\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{neg.f64}\left(a\right)\right)\right)} \]
   metadata-eval [=>] 17.9	\[ \mathsf{*.f64}\left(\color{blue}{\frac{-1}{3}}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \mathsf{neg.f64}\left(a\right)\right)\right) \]
   neg-mul-1 [=>] 17.9	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{neg.f64}\left(b\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(3, a\right), c\right)\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(-1, a\right)}\right)\right) \]

3. Taylor expanded in b around inf 97.6%

   \[\leadsto \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{pow.f64}\left(a, 2\right)\right), \mathsf{pow.f64}\left(b, 5\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)\right)} \]

4. Simplified 97.6%

   \[\leadsto \color{blue}{\mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(a, a\right)\right), \frac{-9}{8}\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right)} \]
   Proof

   [Start] 97.6	\[ \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{pow.f64}\left(a, 2\right)\right), \mathsf{pow.f64}\left(b, 5\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)\right) \]
   fma-def [=>] 97.6	\[ \color{blue}{\mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{pow.f64}\left(a, 2\right)\right), \mathsf{pow.f64}\left(b, 5\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)\right)} \]
   associate-/l* [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \color{blue}{\mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right)}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)\right) \]
   unpow2 [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \color{blue}{\mathsf{*.f64}\left(a, a\right)}\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)\right) \]
   fma-def [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \color{blue}{\mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{-9}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), 2\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 2\right), a\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right)\right)}\right) \]

5. Taylor expanded in c around 0 97.6%

   \[\leadsto \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)}, \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

6. Simplified 97.6%

   \[\leadsto \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 4\right)\right)}, \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   Proof

   [Start] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   metadata-eval [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, \color{blue}{\mathsf{+.f64}\left(3, 1\right)}\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   pow-plus [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 3\right), c\right)}, \mathsf{pow.f64}\left(a, 4\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unpow3 [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), c\right)}, c\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   associate-*r* [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(c, c\right)\right)}, \mathsf{pow.f64}\left(a, 4\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   metadata-eval [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(c, c\right)\right), \mathsf{pow.f64}\left(a, \color{blue}{\mathsf{*.f64}\left(2, 2\right)}\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   pow-sqr [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(c, c\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), \mathsf{pow.f64}\left(a, 2\right)\right)}\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unpow2 [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(c, c\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(a, a\right)}, \mathsf{pow.f64}\left(a, 2\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unpow2 [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(c, c\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, a\right), \color{blue}{\mathsf{*.f64}\left(a, a\right)}\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unswap-sqr [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(a, a\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(a, a\right)\right)\right)}\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   swap-sqr [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, a\right), \mathsf{*.f64}\left(c, a\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(a, a\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unpow2 [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\color{blue}{\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 2\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{*.f64}\left(a, a\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   swap-sqr [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, a\right), \mathsf{*.f64}\left(c, a\right)\right)}\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   unpow2 [<=] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 2\right), \color{blue}{\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 2\right)}\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   pow-sqr [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \color{blue}{\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), \mathsf{*.f64}\left(2, 2\right)\right)}\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   metadata-eval [=>] 97.6	\[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), \color{blue}{4}\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

7. Taylor expanded in c around 0 97.6%

   \[\leadsto \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{pow.f64}\left(a, 4\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)}, \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

8. Simplified 97.6%

   \[\leadsto \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 4\right), \mathsf{/.f64}\left(\frac{405}{64}, \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right)}, \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]
   Proof

   [Start] 97.6

   \[ \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c, 4\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{81}{64}, \mathsf{pow.f64}\left(a, 4\right)\right), \mathsf{*.f64}\left(\frac{81}{16}, \mathsf{pow.f64}\left(a, 4\right)\right)\right)\right), \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

9. Final simplification 97.6%

   \[\leadsto \mathsf{fma.f64}\left(\frac{-9}{16}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 5\right), \mathsf{*.f64}\left(a, a\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{6}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(c, a\right), 4\right), \mathsf{/.f64}\left(\frac{405}{64}, \mathsf{*.f64}\left(a, \mathsf{pow.f64}\left(b, 7\right)\right)\right)\right), \mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, c\right), \mathsf{/.f64}\left(\mathsf{pow.f64}\left(b, 3\right), a\right)\right)\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	96.8%
Cost	33536

\[\mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\frac{-9}{16}, \mathsf{*.f64}\left(a, \mathsf{/.f64}\left(a, \mathsf{pow.f64}\left(b, 5\right)\right)\right)\right), \mathsf{pow.f64}\left(c, 3\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{-3}{8}, \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(c, a\right)\right)\right), \mathsf{pow.f64}\left(b, 3\right)\right)\right)\right) \]

Alternative 2
Accuracy	96.8%
Cost	27328

\[\mathsf{fma.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(\frac{-9}{16}, \mathsf{*.f64}\left(a, \mathsf{/.f64}\left(a, \mathsf{pow.f64}\left(b, 5\right)\right)\right)\right), \mathsf{pow.f64}\left(c, 3\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(c, a\right)\right), \mathsf{*.f64}\left(b, b\right)\right), \mathsf{/.f64}\left(\frac{-3}{8}, b\right)\right)\right)\right) \]

Alternative 3
Accuracy	95.1%
Cost	7424

\[\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(a, \frac{-3}{8}\right), \mathsf{*.f64}\left(c, \mathsf{*.f64}\left(c, \mathsf{pow.f64}\left(b, -3\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right)\right) \]

Alternative 4
Accuracy	95.1%
Cost	960

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(c, b\right), \mathsf{+.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, \frac{-3}{8}\right)\right), \mathsf{*.f64}\left(b, b\right)\right)\right)\right) \]

Alternative 5
Accuracy	90.0%
Cost	320

\[\mathsf{*.f64}\left(c, \mathsf{/.f64}\left(\frac{-1}{2}, b\right)\right) \]

Alternative 6
Accuracy	90.3%
Cost	320

\[\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right) \]

Alternative 7
Accuracy	3.3%
Cost	64

\[0 \]

Reproduce

herbie shell --seed 2023144 
(FPCore (a b c)
  :name "Cubic critical, wide range"
  :precision binary64
  :pre (and (and (and (< 4.930380657631324e-32 a) (< a 2.028240960365167e+31)) (and (< 4.930380657631324e-32 b) (< b 2.028240960365167e+31))) (and (< 4.930380657631324e-32 c) (< c 2.028240960365167e+31)))
  (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))