Rosa's FloatVsDoubleBenchmark

Average Error: 0.5 → 0.6

Time: 20.7s

Precision: 64

• Falling back on racket egraph because egg-herbie package not installed

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

↓

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

C

double f(double x1, double x2) {
        double r68922 = x1;
        double r68923 = 2.0;
        double r68924 = r68923 * r68922;
        double r68925 = 3.0;
        double r68926 = r68925 * r68922;
        double r68927 = r68926 * r68922;
        double r68928 = x2;
        double r68929 = r68923 * r68928;
        double r68930 = r68927 + r68929;
        double r68931 = r68930 - r68922;
        double r68932 = r68922 * r68922;
        double r68933 = 1.0;
        double r68934 = r68932 + r68933;
        double r68935 = r68931 / r68934;
        double r68936 = r68924 * r68935;
        double r68937 = r68935 - r68925;
        double r68938 = r68936 * r68937;
        double r68939 = 4.0;
        double r68940 = r68939 * r68935;
        double r68941 = 6.0;
        double r68942 = r68940 - r68941;
        double r68943 = r68932 * r68942;
        double r68944 = r68938 + r68943;
        double r68945 = r68944 * r68934;
        double r68946 = r68927 * r68935;
        double r68947 = r68945 + r68946;
        double r68948 = r68932 * r68922;
        double r68949 = r68947 + r68948;
        double r68950 = r68949 + r68922;
        double r68951 = r68927 - r68929;
        double r68952 = r68951 - r68922;
        double r68953 = r68952 / r68934;
        double r68954 = r68925 * r68953;
        double r68955 = r68950 + r68954;
        double r68956 = r68922 + r68955;
        return r68956;
}

↓

double f(double x1, double x2) {
        double r68957 = x1;
        double r68958 = 3.0;
        double r68959 = r68958 * r68957;
        double r68960 = r68959 * r68957;
        double r68961 = 2.0;
        double r68962 = x2;
        double r68963 = r68961 * r68962;
        double r68964 = r68960 + r68963;
        double r68965 = r68964 - r68957;
        double r68966 = r68957 * r68957;
        double r68967 = r68966 * r68966;
        double r68968 = 1.0;
        double r68969 = r68968 * r68968;
        double r68970 = r68967 - r68969;
        double r68971 = r68965 / r68970;
        double r68972 = r68966 - r68968;
        double r68973 = sqrt(r68958);
        double r68974 = r68973 * r68973;
        double r68975 = -r68974;
        double r68976 = fma(r68971, r68972, r68975);
        double r68977 = r68961 * r68957;
        double r68978 = r68966 + r68968;
        double r68979 = r68965 / r68978;
        double r68980 = r68977 * r68979;
        double r68981 = r68976 * r68980;
        double r68982 = -r68958;
        double r68983 = r68982 + r68958;
        double r68984 = fma(r68959, r68957, r68963);
        double r68985 = r68984 - r68957;
        double r68986 = r68985 * r68977;
        double r68987 = fma(r68957, r68957, r68968);
        double r68988 = r68986 / r68987;
        double r68989 = 4.0;
        double r68990 = r68985 / r68987;
        double r68991 = 6.0;
        double r68992 = -r68991;
        double r68993 = fma(r68989, r68990, r68992);
        double r68994 = cbrt(r68993);
        double r68995 = 3.0;
        double r68996 = pow(r68994, r68995);
        double r68997 = r68966 * r68996;
        double r68998 = cbrt(r68997);
        double r68999 = r68998 * r68998;
        double r69000 = r68999 * r68998;
        double r69001 = fma(r68983, r68988, r69000);
        double r69002 = r68981 + r69001;
        double r69003 = r69002 * r68978;
        double r69004 = r68960 * r68979;
        double r69005 = r69003 + r69004;
        double r69006 = r68966 * r68957;
        double r69007 = r69005 + r69006;
        double r69008 = r69007 + r68957;
        double r69009 = r68960 - r68963;
        double r69010 = r69009 - r68957;
        double r69011 = r69010 / r68978;
        double r69012 = r68958 * r69011;
        double r69013 = r69008 + r69012;
        double r69014 = r68957 + r69013;
        return r69014;
}

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} - \color{blue}{\sqrt{3} \cdot \sqrt{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 flip-+ 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}{\color{blue}{\frac{\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right) - 1 \cdot 1}{x1 \cdot x1 - 1}}} - \sqrt{3} \cdot \sqrt{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.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(\color{blue}{\frac{\left(\left(3 \cdot x1\right) \cdot x1 + 2 \cdot x2\right) - x1}{\left(x1 \cdot x1\right) \cdot \left(x1 \cdot x1\right) - 1 \cdot 1} \cdot \left(x1 \cdot x1 - 1\right)} - \sqrt{3} \cdot \sqrt{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-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 \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) \cdot \left(x1 \cdot x1\right) - 1 \cdot 1}, x1 \cdot x1 - 1, -\sqrt{3} \cdot \sqrt{3}\right) + \mathsf{fma}\left(-\sqrt{3}, \sqrt{3}, \sqrt{3} \cdot \sqrt{3}\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. Applied distribute-rgt-in 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\left(\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) \cdot \left(x1 \cdot x1\right) - 1 \cdot 1}, x1 \cdot x1 - 1, -\sqrt{3} \cdot \sqrt{3}\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(-\sqrt{3}, \sqrt{3}, \sqrt{3} \cdot \sqrt{3}\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(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. Applied associate-+l+ 0.5

   \[\leadsto x1 + \left(\left(\left(\left(\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) \cdot \left(x1 \cdot x1\right) - 1 \cdot 1}, x1 \cdot x1 - 1, -\sqrt{3} \cdot \sqrt{3}\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(-\sqrt{3}, \sqrt{3}, \sqrt{3} \cdot \sqrt{3}\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(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)\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. Simplified 0.5

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

11. Applied add-cube-cbrt 0.6

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

12. Applied associate-*l* 0.7

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

14. Applied add-cube-cbrt 0.7

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

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

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

17. Final simplification 0.6

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

Reproduce

herbie shell --seed 2020047 +o rules:numerics
(FPCore (x1 x2)
  :name "Rosa's FloatVsDoubleBenchmark"
  :precision binary64
  (+ 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))))))