\[1.053671212772350866701172186984739043147 \cdot 10^{-8} \lt a \lt 94906265.62425155937671661376953125 \land 1.053671212772350866701172186984739043147 \cdot 10^{-8} \lt b \lt 94906265.62425155937671661376953125 \land 1.053671212772350866701172186984739043147 \cdot 10^{-8} \lt c \lt 94906265.62425155937671661376953125\]

\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}\]

↓

\[\frac{1}{-\left(\frac{1}{c} \cdot b + \frac{\sqrt{\frac{{b}^{6} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}{\mathsf{fma}\left(\left(3 \cdot a\right) \cdot c, \mathsf{fma}\left(b, b, c \cdot \left(3 \cdot a\right)\right), {b}^{4}\right)}}}{c}\right)}\]

\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}

↓

\frac{1}{-\left(\frac{1}{c} \cdot b + \frac{\sqrt{\frac{{b}^{6} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}{\mathsf{fma}\left(\left(3 \cdot a\right) \cdot c, \mathsf{fma}\left(b, b, c \cdot \left(3 \cdot a\right)\right), {b}^{4}\right)}}}{c}\right)}

double f(double a, double b, double c) {
        double r64018 = b;
        double r64019 = -r64018;
        double r64020 = r64018 * r64018;
        double r64021 = 3.0;
        double r64022 = a;
        double r64023 = r64021 * r64022;
        double r64024 = c;
        double r64025 = r64023 * r64024;
        double r64026 = r64020 - r64025;
        double r64027 = sqrt(r64026);
        double r64028 = r64019 + r64027;
        double r64029 = r64028 / r64023;
        return r64029;
}

↓

double f(double a, double b, double c) {
        double r64030 = 1.0;
        double r64031 = c;
        double r64032 = r64030 / r64031;
        double r64033 = b;
        double r64034 = r64032 * r64033;
        double r64035 = 6.0;
        double r64036 = pow(r64033, r64035);
        double r64037 = 3.0;
        double r64038 = a;
        double r64039 = r64037 * r64038;
        double r64040 = r64039 * r64031;
        double r64041 = 3.0;
        double r64042 = pow(r64040, r64041);
        double r64043 = r64036 - r64042;
        double r64044 = r64031 * r64039;
        double r64045 = fma(r64033, r64033, r64044);
        double r64046 = 4.0;
        double r64047 = pow(r64033, r64046);
        double r64048 = fma(r64040, r64045, r64047);
        double r64049 = r64043 / r64048;
        double r64050 = sqrt(r64049);
        double r64051 = r64050 / r64031;
        double r64052 = r64034 + r64051;
        double r64053 = -r64052;
        double r64054 = r64030 / r64053;
        return r64054;
}

Derivation

Initial program 28.7
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{3 \cdot a}\]
Using strategy rm
Applied flip-+28.7
\[\leadsto \frac{\color{blue}{\frac{\left(-b\right) \cdot \left(-b\right) - \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c} \cdot \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{\left(-b\right) - \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}}}{3 \cdot a}\]
Simplified0.5
\[\leadsto \frac{\frac{\color{blue}{0 + \left(3 \cdot a\right) \cdot c}}{\left(-b\right) - \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}}{3 \cdot a}\]
Using strategy rm
Applied clear-num0.5
\[\leadsto \color{blue}{\frac{1}{\frac{3 \cdot a}{\frac{0 + \left(3 \cdot a\right) \cdot c}{\left(-b\right) - \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}}}}\]
Simplified0.6
\[\leadsto \frac{1}{\color{blue}{\frac{3 \cdot a}{3 \cdot \left(a \cdot c\right)} \cdot \left(\left(-b\right) - \sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}\right)}}\]
Using strategy rm
Applied sub-neg0.6
\[\leadsto \frac{1}{\frac{3 \cdot a}{3 \cdot \left(a \cdot c\right)} \cdot \color{blue}{\left(\left(-b\right) + \left(-\sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}\right)\right)}}\]
Applied distribute-lft-in0.6
\[\leadsto \frac{1}{\color{blue}{\frac{3 \cdot a}{3 \cdot \left(a \cdot c\right)} \cdot \left(-b\right) + \frac{3 \cdot a}{3 \cdot \left(a \cdot c\right)} \cdot \left(-\sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}\right)}}\]
Simplified0.5
\[\leadsto \frac{1}{\color{blue}{\frac{1}{c} \cdot \left(-b\right)} + \frac{3 \cdot a}{3 \cdot \left(a \cdot c\right)} \cdot \left(-\sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}\right)}\]
Simplified0.4
\[\leadsto \frac{1}{\frac{1}{c} \cdot \left(-b\right) + \color{blue}{\frac{-\sqrt{b \cdot b - \left(3 \cdot a\right) \cdot c}}{\frac{c}{1}}}}\]
Using strategy rm
Applied flip3--0.4
\[\leadsto \frac{1}{\frac{1}{c} \cdot \left(-b\right) + \frac{-\sqrt{\color{blue}{\frac{{\left(b \cdot b\right)}^{3} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}{\left(b \cdot b\right) \cdot \left(b \cdot b\right) + \left(\left(\left(3 \cdot a\right) \cdot c\right) \cdot \left(\left(3 \cdot a\right) \cdot c\right) + \left(b \cdot b\right) \cdot \left(\left(3 \cdot a\right) \cdot c\right)\right)}}}}{\frac{c}{1}}}\]
Simplified0.4
\[\leadsto \frac{1}{\frac{1}{c} \cdot \left(-b\right) + \frac{-\sqrt{\frac{\color{blue}{{b}^{6} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}}{\left(b \cdot b\right) \cdot \left(b \cdot b\right) + \left(\left(\left(3 \cdot a\right) \cdot c\right) \cdot \left(\left(3 \cdot a\right) \cdot c\right) + \left(b \cdot b\right) \cdot \left(\left(3 \cdot a\right) \cdot c\right)\right)}}}{\frac{c}{1}}}\]
Simplified0.4
\[\leadsto \frac{1}{\frac{1}{c} \cdot \left(-b\right) + \frac{-\sqrt{\frac{{b}^{6} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}{\color{blue}{\mathsf{fma}\left(\left(3 \cdot a\right) \cdot c, \mathsf{fma}\left(b, b, c \cdot \left(3 \cdot a\right)\right), {b}^{4}\right)}}}}{\frac{c}{1}}}\]
Final simplification0.4
\[\leadsto \frac{1}{-\left(\frac{1}{c} \cdot b + \frac{\sqrt{\frac{{b}^{6} - {\left(\left(3 \cdot a\right) \cdot c\right)}^{3}}{\mathsf{fma}\left(\left(3 \cdot a\right) \cdot c, \mathsf{fma}\left(b, b, c \cdot \left(3 \cdot a\right)\right), {b}^{4}\right)}}}{c}\right)}\]

Error

Derivation

Reproduce