Average Error: 0.5 → 0.6
Time: 1.2m
Precision: 64
\[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
↓
\[\left(\left(\left(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(1 + x1 \cdot x1\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + \left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}, \sqrt{6} \cdot \left(-\sqrt{6}\right)\right) \cdot \left(x1 \cdot x1\right) + \left(x1 \cdot 0\right) \cdot x1\right)\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right)\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + x1\]
x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)
↓
\left(\left(\left(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(1 + x1 \cdot x1\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + \left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}, \sqrt{6} \cdot \left(-\sqrt{6}\right)\right) \cdot \left(x1 \cdot x1\right) + \left(x1 \cdot 0\right) \cdot x1\right)\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right)\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + x1
double f(double x1, double x2) {
        double r2728244 = x1;
        double r2728245 = 2.0;
        double r2728246 = r2728245 * r2728244;
        double r2728247 = 3.0;
        double r2728248 = r2728247 * r2728244;
        double r2728249 = r2728248 * r2728244;
        double r2728250 = x2;
        double r2728251 = r2728245 * r2728250;
        double r2728252 = r2728249 + r2728251;
        double r2728253 = r2728252 - r2728244;
        double r2728254 = r2728244 * r2728244;
        double r2728255 = 1.0;
        double r2728256 = r2728254 + r2728255;
        double r2728257 = r2728253 / r2728256;
        double r2728258 = r2728246 * r2728257;
        double r2728259 = r2728257 - r2728247;
        double r2728260 = r2728258 * r2728259;
        double r2728261 = 4.0;
        double r2728262 = r2728261 * r2728257;
        double r2728263 = 6.0;
        double r2728264 = r2728262 - r2728263;
        double r2728265 = r2728254 * r2728264;
        double r2728266 = r2728260 + r2728265;
        double r2728267 = r2728266 * r2728256;
        double r2728268 = r2728249 * r2728257;
        double r2728269 = r2728267 + r2728268;
        double r2728270 = r2728254 * r2728244;
        double r2728271 = r2728269 + r2728270;
        double r2728272 = r2728271 + r2728244;
        double r2728273 = r2728249 - r2728251;
        double r2728274 = r2728273 - r2728244;
        double r2728275 = r2728274 / r2728256;
        double r2728276 = r2728247 * r2728275;
        double r2728277 = r2728272 + r2728276;
        double r2728278 = r2728244 + r2728277;
        return r2728278;
}
↓
double f(double x1, double x2) {
        double r2728279 = x1;
        double r2728280 = r2728279 * r2728279;
        double r2728281 = r2728279 * r2728280;
        double r2728282 = 1.0;
        double r2728283 = r2728282 + r2728280;
        double r2728284 = 3.0;
        double r2728285 = x2;
        double r2728286 = 2.0;
        double r2728287 = r2728285 * r2728286;
        double r2728288 = r2728287 - r2728279;
        double r2728289 = fma(r2728284, r2728280, r2728288);
        double r2728290 = fma(r2728281, r2728281, r2728282);
        double r2728291 = r2728289 / r2728290;
        double r2728292 = fma(r2728280, r2728280, r2728282);
        double r2728293 = r2728292 - r2728280;
        double r2728294 = -3.0;
        double r2728295 = fma(r2728291, r2728293, r2728294);
        double r2728296 = r2728279 * r2728286;
        double r2728297 = r2728284 * r2728279;
        double r2728298 = r2728297 * r2728279;
        double r2728299 = r2728298 + r2728287;
        double r2728300 = r2728299 - r2728279;
        double r2728301 = r2728300 / r2728283;
        double r2728302 = r2728296 * r2728301;
        double r2728303 = r2728295 * r2728302;
        double r2728304 = 4.0;
        double r2728305 = 6.0;
        double r2728306 = sqrt(r2728305);
        double r2728307 = -r2728306;
        double r2728308 = r2728306 * r2728307;
        double r2728309 = fma(r2728304, r2728301, r2728308);
        double r2728310 = r2728309 * r2728280;
        double r2728311 = 0.0;
        double r2728312 = r2728279 * r2728311;
        double r2728313 = r2728312 * r2728279;
        double r2728314 = r2728310 + r2728313;
        double r2728315 = r2728303 + r2728314;
        double r2728316 = r2728283 * r2728315;
        double r2728317 = r2728298 * r2728301;
        double r2728318 = r2728316 + r2728317;
        double r2728319 = r2728281 + r2728318;
        double r2728320 = r2728319 + r2728279;
        double r2728321 = r2728298 - r2728287;
        double r2728322 = r2728321 - r2728279;
        double r2728323 = r2728322 / r2728283;
        double r2728324 = r2728284 * r2728323;
        double r2728325 = r2728320 + r2728324;
        double r2728326 = r2728325 + r2728279;
        return r2728326;
}

Error

Bits error versus x1

Bits error versus x2

Derivation

  1. Initial program 0.5

    \[x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
  2. Using strategy rm

  3. Applied *-un-lft-identity0.5

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - \color{blue}{1 \cdot 3}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  4. Applied flip3-+0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\color{blue}{\frac{{\left(x1 \cdot x1\right)}^{3} + {1}^{3}}{\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right) + \left(1 \cdot 1 - \left(x1 \cdot x1\right) \cdot 1\right)}}} - 1 \cdot 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  5. Applied associate-/r/0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\color{blue}{\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{{\left(x1 \cdot x1\right)}^{3} + {1}^{3}} \cdot \left(\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right) + \left(1 \cdot 1 - \left(x1 \cdot x1\right) \cdot 1\right)\right)} - 1 \cdot 3\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  6. Applied prod-diff0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \color{blue}{\left(\mathsf{fma}\left(\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{{\left(x1 \cdot x1\right)}^{3} + {1}^{3}}, \left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right) + \left(1 \cdot 1 - \left(x1 \cdot x1\right) \cdot 1\right), -3 \cdot 1\right) + \mathsf{fma}\left(-3, 1, 3 \cdot 1\right)\right)} + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  7. Simplified0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\color{blue}{\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right)} + \mathsf{fma}\left(-3, 1, 3 \cdot 1\right)\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  8. Simplified0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) + \color{blue}{0}\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - 6\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]
  9. Using strategy rm

  10. Applied add-sqr-sqrt0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) + 0\right) + \left(x1 \cdot x1\right) \cdot \left(4 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1} - \color{blue}{\sqrt{6} \cdot \sqrt{6}}\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  11. Applied prod-diff0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) + 0\right) + \left(x1 \cdot x1\right) \cdot \color{blue}{\left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \mathsf{fma}\left(-\sqrt{6}, \sqrt{6}, \sqrt{6} \cdot \sqrt{6}\right)\right)}\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  12. Applied distribute-lft-in0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) + 0\right) + \color{blue}{\left(\left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(-\sqrt{6}, \sqrt{6}, \sqrt{6} \cdot \sqrt{6}\right)\right)}\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  13. Simplified0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\left(\left(2 \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) + 0\right) + \left(\left(x1 \cdot x1\right) \cdot \mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}, -\sqrt{6} \cdot \sqrt{6}\right) + \color{blue}{\left(x1 \cdot 0\right) \cdot x1}\right)\right) \cdot \left(x1 \cdot x1 + 1\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right) + \left(x1 \cdot x1\right) \cdot x1\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - 2 \cdot x2\right) - x1}{x1 \cdot x1 + 1}\right)\]

  14. Final simplification0.6

    \[\leadsto \left(\left(\left(x1 \cdot \left(x1 \cdot x1\right) + \left(\left(1 + x1 \cdot x1\right) \cdot \left(\mathsf{fma}\left(\frac{\mathsf{fma}\left(3, x1 \cdot x1, x2 \cdot 2 - x1\right)}{\mathsf{fma}\left(x1 \cdot \left(x1 \cdot x1\right), x1 \cdot \left(x1 \cdot x1\right), 1\right)}, \mathsf{fma}\left(x1 \cdot x1, x1 \cdot x1, 1\right) - x1 \cdot x1, -3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + \left(\mathsf{fma}\left(4, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}, \sqrt{6} \cdot \left(-\sqrt{6}\right)\right) \cdot \left(x1 \cdot x1\right) + \left(x1 \cdot 0\right) \cdot x1\right)\right) + \left(\left(3 \cdot x1\right) \cdot x1\right) \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right)\right) + x1\right) + 3 \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 - x2 \cdot 2\right) - x1}{1 + x1 \cdot x1}\right) + x1\]

Reproduce

herbie shell --seed 2019151 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  (+ x1 (+ (+ (+ (+ (* (+ (* (* (* 2 x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) (- (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)) 3)) (* (* x1 x1) (- (* 4 (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))) 6))) (+ (* x1 x1) 1)) (* (* (* 3 x1) x1) (/ (- (+ (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1)))) (* (* x1 x1) x1)) x1) (* 3 (/ (- (- (* (* 3 x1) x1) (* 2 x2)) x1) (+ (* x1 x1) 1))))))