Cubic critical

Average Accuracy: 46.6% → 81.9%

Time: 28.6s

Precision: binary64

Cost: 20364

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) \]

↓

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, -20999999999999999892825751366275165687698317249138536736081263792459064345632643659636974437008550542481857618056144623311682081501011268411332755456\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-7597989933253771}{1013065324433836171511818326096474890383898005918563696288002277756507034036354527929615978746851512277392062160962106733983191180520452956027069051297354415786421338721071661056}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 3\right), c\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-7714861971741125}{42860344287450692837937001962400072422456192468221344297750015534814042044997444899727935152627834325103786916702125873007485811427692561743938310298794299215738271099296923941684298420249484567511816728612185899934327765069595070236662175784308251658284785910746168670641719326610497547348822672277504}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -3\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{7669960592712579}{93536104789177786765035829293842113257979682750464}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -3\right)\right)\right)\right)\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \end{array} \]

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
 (if (<=.f64
      b
      -20999999999999999892825751366275165687698317249138536736081263792459064345632643659636974437008550542481857618056144623311682081501011268411332755456)
   (/.f64 b (*.f64 a -3/2))
   (if (<=.f64
        b
        -7597989933253771/1013065324433836171511818326096474890383898005918563696288002277756507034036354527929615978746851512277392062160962106733983191180520452956027069051297354415786421338721071661056)
     (/.f64
      (-.f64 (sqrt.f64 (-.f64 (*.f64 b b) (*.f64 (*.f64 a 3) c))) b)
      (*.f64 a 3))
     (if (<=.f64
          b
          -7714861971741125/42860344287450692837937001962400072422456192468221344297750015534814042044997444899727935152627834325103786916702125873007485811427692561743938310298794299215738271099296923941684298420249484567511816728612185899934327765069595070236662175784308251658284785910746168670641719326610497547348822672277504)
       (/.f64
        -1/3
        (/.f64
         a
         (-.f64 b (hypot.f64 b (*.f64 (sqrt.f64 (*.f64 c -3)) (sqrt.f64 a))))))
       (if (<=.f64
            b
            7669960592712579/93536104789177786765035829293842113257979682750464)
         (/.f64
          (+.f64 b (hypot.f64 b (sqrt.f64 (*.f64 c (*.f64 a -3)))))
          (*.f64 a 3))
         (/.f64 (*.f64 c -1/2) b))))))

Derivation

1. Split input into 5 regimes

2. if b < -2.09999999999999999e148

   1. Initial program 4.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) \]

   2. Simplified 4.1%

      \[\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] 4.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) \]
      /-rgt-identity [<=] 4.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), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(3, a\right), 1\right)}\right) \]
      metadata-eval [<=] 4.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(\mathsf{*.f64}\left(3, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 4.1	\[ \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/ [<=] 4.1	\[ \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 [=>] 4.1	\[ \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/ [=>] 4.1	\[ \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/ [<=] 4.1	\[ \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 [=>] 4.1	\[ \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 [<=] 4.1	\[ \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 [<=] 4.1	\[ \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 [<=] 4.1	\[ \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 [=>] 4.1	\[ \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 [=>] 4.1	\[ \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 [=>] 4.1	\[ \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 [=>] 4.1	\[ \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 83.1%

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

   4. Simplified 83.1%

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

      [Start] 83.1	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{3}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, a\right), b\right)\right), \mathsf{*.f64}\left(-1, b\right)\right)\right), a\right)\right) \]
      mul-1-neg [=>] 83.1	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{3}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, a\right), b\right)\right), \color{blue}{\mathsf{neg.f64}\left(b\right)}\right)\right), a\right)\right) \]
      unsub-neg [=>] 83.1	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\frac{3}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(c, a\right), b\right)\right), b\right)}\right), a\right)\right) \]
      associate-*r/ [=>] 83.0	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{3}{2}, \mathsf{*.f64}\left(c, a\right)\right), b\right)}, b\right)\right), a\right)\right) \]
      associate-/l* [=>] 83.1	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(\frac{3}{2}, \mathsf{/.f64}\left(b, \mathsf{*.f64}\left(c, a\right)\right)\right)}, b\right)\right), a\right)\right) \]

   5. Taylor expanded in b around inf 95.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right)} \]

   6. Simplified 95.7%

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

      [Start] 95.7	\[ \mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right) \]
      associate-*r/ [=>] 95.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{-2}{3}, b\right), a\right)} \]
      associate-/l* [=>] 95.7	\[ \color{blue}{\mathsf{/.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(a, b\right)\right)} \]
      associate-/r/ [=>] 95.7	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{-2}{3}, a\right), b\right)} \]

   7. Applied egg-rr 95.8%

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

      [Start] 95.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{-2}{3}, a\right), b\right) \]
      *-commutative [=>] 95.7	\[ \color{blue}{\mathsf{*.f64}\left(b, \mathsf{/.f64}\left(\frac{-2}{3}, a\right)\right)} \]
      clear-num [=>] 95.6	\[ \mathsf{*.f64}\left(b, \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \frac{-2}{3}\right)\right)}\right) \]
      un-div-inv [=>] 95.7	\[ \color{blue}{\mathsf{/.f64}\left(b, \mathsf{/.f64}\left(a, \frac{-2}{3}\right)\right)} \]
      div-inv [=>] 95.8	\[ \mathsf{/.f64}\left(b, \color{blue}{\mathsf{*.f64}\left(a, \mathsf{/.f64}\left(1, \frac{-2}{3}\right)\right)}\right) \]
      metadata-eval [=>] 95.8	\[ \mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \color{blue}{\frac{-3}{2}}\right)\right) \]

   if -2.09999999999999999e148 < b < -7.49999999999999972e-162

   1. Initial program 90.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) \]

   if -7.49999999999999972e-162 < b < -1.80000000000000007e-286

   1. Initial program 73.7%

      \[\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 73.5%

      \[\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] 73.7	\[ \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 [<=] 73.7	\[ \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 [<=] 73.7	\[ \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* [<=] 73.7	\[ \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/ [<=] 73.7	\[ \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 [=>] 73.7	\[ \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/ [=>] 73.7	\[ \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/ [<=] 73.7	\[ \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 [=>] 73.7	\[ \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 [<=] 73.7	\[ \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 [<=] 73.7	\[ \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 [<=] 73.7	\[ \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 [=>] 73.7	\[ \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 [=>] 73.5	\[ \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 [=>] 73.5	\[ \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 [=>] 73.5	\[ \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. Applied egg-rr 80.9%

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

      [Start] 73.5	\[ \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) \]
      clear-num [=>] 73.4	\[ \mathsf{*.f64}\left(\frac{-1}{3}, \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, \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)\right)\right)}\right) \]
      un-div-inv [=>] 73.4	\[ \color{blue}{\mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \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)\right)\right)} \]
      fma-udef [=>] 73.4	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)}\right)\right)\right)\right) \]
      add-sqr-sqrt [=>] 73.4	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]
      hypot-def [=>] 80.9	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \color{blue}{\mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)\right)}\right)\right)\right) \]

   4. Applied egg-rr 49.0%

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

      [Start] 80.9	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)\right)\right)\right)\right) \]
      *-commutative [=>] 80.9	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c, -3\right), a\right)}\right)\right)\right)\right)\right) \]
      sqrt-prod [=>] 49.0	\[ \mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{hypot.f64}\left(b, \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -3\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)}\right)\right)\right)\right) \]

   if -1.80000000000000007e-286 < b < 8.20000000000000052e-35

   1. Initial program 65.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) \]

   2. Simplified 65.0%

      \[\leadsto \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(3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right)} \]
      Proof

      [Start] 65.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) \]
      neg-sub0 [=>] 65.1	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, 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) \]
      associate-+l- [=>] 65.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(b, \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) \]
      sub0-neg [=>] 65.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(b, \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) \]
      neg-mul-1 [=>] 65.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(b, \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/ [<=] 65.1	\[ \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \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 [<=] 65.1	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(1, -1\right)}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \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 [<=] 65.1	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(-1\right)}, -1\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \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 [<=] 65.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{\_.f64}\left(b, \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)} \]
      *-commutative [=>] 65.1	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{\_.f64}\left(b, \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(\mathsf{*.f64}\left(3, a\right), -1\right)}\right) \]
      times-frac [=>] 65.0	\[ \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{\_.f64}\left(b, \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), -1\right)\right)} \]
      associate-*l/ [=>] 65.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(-1\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \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), -1\right)\right), \mathsf{*.f64}\left(3, a\right)\right)} \]

   3. Applied egg-rr 35.9%

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

      [Start] 65.0	\[ \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(3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]
      expm1-log1p-u [=>] 62.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{expm1.f64}\left(\mathsf{log1p.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(3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right)\right)\right)}, \mathsf{*.f64}\left(3, a\right)\right) \]
      expm1-udef [=>] 36.3	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.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(3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right)\right)\right), 1\right)}, \mathsf{*.f64}\left(3, a\right)\right) \]

   4. Simplified 64.0%

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

      [Start] 35.9	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{exp.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-3, c\right), a\right)\right)\right)\right)\right)\right), 1\right), \mathsf{*.f64}\left(3, a\right)\right) \]
      expm1-def [=>] 61.4	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{expm1.f64}\left(\mathsf{log1p.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-3, c\right), a\right)\right)\right)\right)\right)\right)}, \mathsf{*.f64}\left(3, a\right)\right) \]
      expm1-log1p [=>] 63.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-3, c\right), a\right)\right)\right)\right)}, \mathsf{*.f64}\left(3, a\right)\right) \]
      *-commutative [=>] 63.7	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(c, -3\right)}, a\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]
      associate-*l* [=>] 64.0	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(-3, a\right)\right)}\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]
      *-commutative [=>] 64.0	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \color{blue}{\mathsf{*.f64}\left(a, -3\right)}\right)\right)\right)\right), \mathsf{*.f64}\left(3, a\right)\right) \]

   if 8.20000000000000052e-35 < b

   1. Initial program 15.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) \]

   2. Simplified 15.0%

      \[\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] 15.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) \]
      /-rgt-identity [<=] 15.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), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(3, a\right), 1\right)}\right) \]
      metadata-eval [<=] 15.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(\mathsf{*.f64}\left(3, a\right), \color{blue}{\mathsf{neg.f64}\left(-1\right)}\right)\right) \]
      associate-/l* [<=] 15.1	\[ \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/ [<=] 15.1	\[ \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 [=>] 15.1	\[ \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/ [=>] 15.1	\[ \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/ [<=] 15.1	\[ \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 [=>] 15.1	\[ \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 [<=] 15.1	\[ \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 [<=] 15.1	\[ \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 [<=] 15.1	\[ \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 [=>] 15.1	\[ \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 [=>] 15.1	\[ \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 [=>] 15.1	\[ \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 [=>] 15.1	\[ \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 88.0%

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

   4. Simplified 88.0%

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

      [Start] 88.0	\[ \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(c, b\right)\right) \]
      associate-*r/ [=>] 88.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{-1}{2}, c\right), b\right)} \]

3. Recombined 5 regimes into one program.

4. Final simplification 81.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, -20999999999999999892825751366275165687698317249138536736081263792459064345632643659636974437008550542481857618056144623311682081501011268411332755456\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-7597989933253771}{1013065324433836171511818326096474890383898005918563696288002277756507034036354527929615978746851512277392062160962106733983191180520452956027069051297354415786421338721071661056}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 3\right), c\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-7714861971741125}{42860344287450692837937001962400072422456192468221344297750015534814042044997444899727935152627834325103786916702125873007485811427692561743938310298794299215738271099296923941684298420249484567511816728612185899934327765069595070236662175784308251658284785910746168670641719326610497547348822672277504}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(a, \mathsf{\_.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, -3\right)\right), \mathsf{sqrt.f64}\left(a\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{7669960592712579}{93536104789177786765035829293842113257979682750464}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{+.f64}\left(b, \mathsf{hypot.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -3\right)\right)\right)\right)\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	76.1%
Cost	7888

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{4149515568880993}{2074757784440496479256203931845580575506223116121218449997828664845326405706454073199853524473551897144098943305650394591197575537705887653943437417056981843530590901700754761842688}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -3\right)\right)\right)\right), a\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{578960446186581}{28948022309329048855892746252171976963317496166410141009864396001978282409984}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(c, b\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{7378697629483821}{147573952589676412928}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(-3, \mathsf{*.f64}\left(a, c\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	83.6%
Cost	7752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(a, \mathsf{*.f64}\left(c, -3\right)\right)\right)\right)\right)\right), a\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	83.6%
Cost	7752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	83.7%
Cost	7752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), \frac{-7136238463529799}{1427247692705959881058285969449495136382746624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{neg.f64}\left(b\right), 99999999999999998278261272554585856747747644714015897553975120217811154108416\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(b, b\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(a, 3\right), c\right)\right)\right), b\right), \mathsf{*.f64}\left(a, 3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	76.9%
Cost	7632

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -3\right)\right)\right)\right), a\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{-3242591731706757}{72057594037927936}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-551821675271585}{904625697166532776746648320380374280103671755200316906558262375061821325312}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-8950677443466013}{51146728248377216718956089012931236753385031969422887335676427626502090568823039920051095192592252455482604439493126109519019633529459266458258243584}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(c, b\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{3086691458042867}{46768052394588893382517914646921056628989841375232}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \end{array} \]

Alternative 6
Accuracy	77.1%
Cost	7632

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{-5312662293228351}{147573952589676412928}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-4052723123306067}{231584178474632390847141970017375815706539969331281128078915168015826259279872}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(-3, \mathsf{*.f64}\left(a, c\right)\right)\right)\right)\right), a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{-8950677443466013}{51146728248377216718956089012931236753385031969422887335676427626502090568823039920051095192592252455482604439493126109519019633529459266458258243584}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(c, b\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(b, \frac{4290987514424489}{3064991081731777716716694054300618367237478244367204352}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{-1}{3}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(b, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(c, \mathsf{*.f64}\left(a, -3\right)\right)\right)\right), a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \end{array} \]

Alternative 7
Accuracy	65.1%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{6712243105892569}{894965747452342537638086997927338702835054349130332891545045303197220750167278254979540133307019636732167484663093741252324901898658543021888907063798893113141027322124350378195837539421218086757657500257242038983622829800210549487979962097077321728}\right):\\ \;\;\;\;\mathsf{*.f64}\left(b, \mathsf{/.f64}\left(\frac{-2}{3}, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(c, \mathsf{/.f64}\left(\frac{-1}{2}, b\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	65.1%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{6586947901249241}{7159725979618740301104695983418709622680434793042663132360362425577766001338226039836321066456157093857339877304749930018599215189268344175111256510391144905128218576994803025566700315369744694061260002057936311868982638401684395903839696776618573824}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(b, a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(c, \mathsf{/.f64}\left(\frac{-1}{2}, b\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	65.1%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{475450553334057}{55935359215771408602380437370458668927190896820645805721565331449826296885454890936221258331688727295760467791443358828270306368666158938868056691487430819571314207632771898637239846213826130422353593766077627436476426862513159342998747631067332608}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\frac{-2}{3}, \mathsf{/.f64}\left(a, b\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(c, \mathsf{/.f64}\left(\frac{-1}{2}, b\right)\right)\\ \end{array} \]

Alternative 10
Accuracy	65.2%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{8949657474523425}{7159725979618740301104695983418709622680434793042663132360362425577766001338226039836321066456157093857339877304749930018599215189268344175111256510391144905128218576994803025566700315369744694061260002057936311868982638401684395903839696776618573824}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(c, \mathsf{/.f64}\left(\frac{-1}{2}, b\right)\right)\\ \end{array} \]

Alternative 11
Accuracy	65.3%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(b, \frac{7517712278599677}{7159725979618740301104695983418709622680434793042663132360362425577766001338226039836321066456157093857339877304749930018599215189268344175111256510391144905128218576994803025566700315369744694061260002057936311868982638401684395903839696776618573824}\right):\\ \;\;\;\;\mathsf{/.f64}\left(b, \mathsf{*.f64}\left(a, \frac{-3}{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(c, \frac{-1}{2}\right), b\right)\\ \end{array} \]

Alternative 12
Accuracy	37.8%
Cost	320

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

Reproduce

herbie shell --seed 2023144 
(FPCore (a b c)
  :name "Cubic critical"
  :precision binary64
  (/ (+ (- b) (sqrt (- (* b b) (* (* 3.0 a) c)))) (* 3.0 a)))