Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.5

Time: 1.3m

Precision: 64

Math

\[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(x1 + \left(\left(\frac{\left(2 \cdot x2 + x1 \cdot \left(3 \cdot x1\right)\right) - x1}{1 + x1 \cdot x1} \cdot \left(x1 \cdot \left(3 \cdot x1\right)\right) + \left(1 + x1 \cdot x1\right) \cdot \left(\mathsf{fma}\left(\frac{1}{\sqrt[3]{1 + x1 \cdot x1} \cdot \sqrt[3]{1 + x1 \cdot x1}}, \frac{\left(2 \cdot x2 + x1 \cdot \left(3 \cdot x1\right)\right) - x1}{\sqrt[3]{1 + x1 \cdot x1}}, -3\right) \cdot \left(\left(x1 \cdot 2\right) \cdot \frac{\left(2 \cdot x2 + x1 \cdot \left(3 \cdot x1\right)\right) - x1}{1 + x1 \cdot x1}\right) + \mathsf{fma}\left(0, \frac{\mathsf{fma}\left(3, x1 \cdot x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}, \mathsf{fma}\left(\mathsf{fma}\left(4, \frac{\mathsf{fma}\left(3, x1 \cdot x1, 2 \cdot x2\right) - x1}{\mathsf{fma}\left(x1, x1, 1\right)}, -6\right), x1 \cdot x1, 0\right)\right)\right)\right) + x1 \cdot \left(x1 \cdot x1\right)\right)\right) + 3 \cdot \frac{\left(x1 \cdot \left(3 \cdot x1\right) - 2 \cdot x2\right) - x1}{1 + x1 \cdot x1}\right) + x1\]

C

double f(double x1, double x2) {
        double r2763804 = x1;
        double r2763805 = 2.0;
        double r2763806 = r2763805 * r2763804;
        double r2763807 = 3.0;
        double r2763808 = r2763807 * r2763804;
        double r2763809 = r2763808 * r2763804;
        double r2763810 = x2;
        double r2763811 = r2763805 * r2763810;
        double r2763812 = r2763809 + r2763811;
        double r2763813 = r2763812 - r2763804;
        double r2763814 = r2763804 * r2763804;
        double r2763815 = 1.0;
        double r2763816 = r2763814 + r2763815;
        double r2763817 = r2763813 / r2763816;
        double r2763818 = r2763806 * r2763817;
        double r2763819 = r2763817 - r2763807;
        double r2763820 = r2763818 * r2763819;
        double r2763821 = 4.0;
        double r2763822 = r2763821 * r2763817;
        double r2763823 = 6.0;
        double r2763824 = r2763822 - r2763823;
        double r2763825 = r2763814 * r2763824;
        double r2763826 = r2763820 + r2763825;
        double r2763827 = r2763826 * r2763816;
        double r2763828 = r2763809 * r2763817;
        double r2763829 = r2763827 + r2763828;
        double r2763830 = r2763814 * r2763804;
        double r2763831 = r2763829 + r2763830;
        double r2763832 = r2763831 + r2763804;
        double r2763833 = r2763809 - r2763811;
        double r2763834 = r2763833 - r2763804;
        double r2763835 = r2763834 / r2763816;
        double r2763836 = r2763807 * r2763835;
        double r2763837 = r2763832 + r2763836;
        double r2763838 = r2763804 + r2763837;
        return r2763838;
}

↓

double f(double x1, double x2) {
        double r2763839 = x1;
        double r2763840 = 2.0;
        double r2763841 = x2;
        double r2763842 = r2763840 * r2763841;
        double r2763843 = 3.0;
        double r2763844 = r2763843 * r2763839;
        double r2763845 = r2763839 * r2763844;
        double r2763846 = r2763842 + r2763845;
        double r2763847 = r2763846 - r2763839;
        double r2763848 = 1.0;
        double r2763849 = r2763839 * r2763839;
        double r2763850 = r2763848 + r2763849;
        double r2763851 = r2763847 / r2763850;
        double r2763852 = r2763851 * r2763845;
        double r2763853 = cbrt(r2763850);
        double r2763854 = r2763853 * r2763853;
        double r2763855 = r2763848 / r2763854;
        double r2763856 = r2763847 / r2763853;
        double r2763857 = -3.0;
        double r2763858 = fma(r2763855, r2763856, r2763857);
        double r2763859 = r2763839 * r2763840;
        double r2763860 = r2763859 * r2763851;
        double r2763861 = r2763858 * r2763860;
        double r2763862 = 0.0;
        double r2763863 = fma(r2763843, r2763849, r2763842);
        double r2763864 = r2763863 - r2763839;
        double r2763865 = fma(r2763839, r2763839, r2763848);
        double r2763866 = r2763864 / r2763865;
        double r2763867 = 4.0;
        double r2763868 = -6.0;
        double r2763869 = fma(r2763867, r2763866, r2763868);
        double r2763870 = fma(r2763869, r2763849, r2763862);
        double r2763871 = fma(r2763862, r2763866, r2763870);
        double r2763872 = r2763861 + r2763871;
        double r2763873 = r2763850 * r2763872;
        double r2763874 = r2763852 + r2763873;
        double r2763875 = r2763839 * r2763849;
        double r2763876 = r2763874 + r2763875;
        double r2763877 = r2763839 + r2763876;
        double r2763878 = r2763845 - r2763842;
        double r2763879 = r2763878 - r2763839;
        double r2763880 = r2763879 / r2763850;
        double r2763881 = r2763843 * r2763880;
        double r2763882 = r2763877 + r2763881;
        double r2763883 = r2763882 + r2763839;
        return r2763883;
}

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 add-sqr-sqrt 0.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} - 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} - \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)\]

4. Applied prod-diff 0.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} - 3\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)\]

5. Applied distribute-lft-in 0.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} - 3\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)\]

6. Simplified 0.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} - 3\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)\]
7. Using strategy rm

8. Applied *-un-lft-identity 0.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(\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 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)\]

9. Applied add-cube-cbrt 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}{\left(\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}\right) \cdot \sqrt[3]{x1 \cdot x1 + 1}}} - 1 \cdot 3\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) + \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)\]

10. Applied *-un-lft-identity 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{\color{blue}{1 \cdot \left(\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1\right)}}{\left(\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}\right) \cdot \sqrt[3]{x1 \cdot x1 + 1}} - 1 \cdot 3\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) + \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)\]

11. Applied times-frac 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{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}} \cdot \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}} - 1 \cdot 3\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) + \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)\]

12. Applied prod-diff 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 \color{blue}{\left(\mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}, -3 \cdot 1\right) + \mathsf{fma}\left(-3, 1, 3 \cdot 1\right)\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) + \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)\]

13. Applied distribute-rgt-in 0.6

    \[\leadsto x1 + \left(\left(\left(\left(\left(\color{blue}{\left(\mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}, -3 \cdot 1\right) \cdot \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) + \mathsf{fma}\left(-3, 1, 3 \cdot 1\right) \cdot \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)\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) + \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. Applied associate-+l+ 0.6

    \[\leadsto x1 + \left(\left(\left(\left(\color{blue}{\left(\mathsf{fma}\left(\frac{1}{\sqrt[3]{x1 \cdot x1 + 1} \cdot \sqrt[3]{x1 \cdot x1 + 1}}, \frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\sqrt[3]{x1 \cdot x1 + 1}}, -3 \cdot 1\right) \cdot \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) + \left(\mathsf{fma}\left(-3, 1, 3 \cdot 1\right) \cdot \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) + \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 0\right) \cdot x1\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)\]

15. Simplified 0.5

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

16. Final simplification 0.5

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

Reproduce

herbie shell --seed 2019144 +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))))))