Diagrams.Solve.Polynomial:cubForm from diagrams-solve-0.1, K

Average Error: 20.4 → 18.6

Time: 58.0s

Precision: 64

Math

\[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]

↓

\[\begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9957133982267296623547281342325732111931:\\ \;\;\;\;\sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\sqrt[3]{3} \cdot \sqrt[3]{3}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \left(\sin \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \cos \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) + \cos \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \sin \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)\right)\right)}^{3}} \cdot \left(2 \cdot \sqrt{x}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{1 - \frac{3}{2} \cdot {y}^{2}} - \frac{a}{b \cdot 3}\\ \end{array}\]

C

double f(double x, double y, double z, double t, double a, double b) {
        double r567745 = 2.0;
        double r567746 = x;
        double r567747 = sqrt(r567746);
        double r567748 = r567745 * r567747;
        double r567749 = y;
        double r567750 = z;
        double r567751 = t;
        double r567752 = r567750 * r567751;
        double r567753 = 3.0;
        double r567754 = r567752 / r567753;
        double r567755 = r567749 - r567754;
        double r567756 = cos(r567755);
        double r567757 = r567748 * r567756;
        double r567758 = a;
        double r567759 = b;
        double r567760 = r567759 * r567753;
        double r567761 = r567758 / r567760;
        double r567762 = r567757 - r567761;
        return r567762;
}

↓

double f(double x, double y, double z, double t, double a, double b) {
        double r567763 = y;
        double r567764 = z;
        double r567765 = t;
        double r567766 = r567764 * r567765;
        double r567767 = 3.0;
        double r567768 = r567766 / r567767;
        double r567769 = r567763 - r567768;
        double r567770 = cos(r567769);
        double r567771 = 0.9957133982267297;
        bool r567772 = r567770 <= r567771;
        double r567773 = 1.0;
        double r567774 = r567767 / r567764;
        double r567775 = cbrt(r567774);
        double r567776 = r567775 * r567775;
        double r567777 = r567773 / r567776;
        double r567778 = r567765 / r567775;
        double r567779 = -r567778;
        double r567780 = r567779 + r567778;
        double r567781 = r567777 * r567780;
        double r567782 = cos(r567781);
        double r567783 = r567778 / r567776;
        double r567784 = r567763 - r567783;
        double r567785 = cos(r567784);
        double r567786 = r567782 * r567785;
        double r567787 = cbrt(r567765);
        double r567788 = r567787 * r567787;
        double r567789 = cbrt(r567767);
        double r567790 = r567789 * r567789;
        double r567791 = cbrt(r567790);
        double r567792 = r567788 / r567791;
        double r567793 = r567789 / r567764;
        double r567794 = cbrt(r567793);
        double r567795 = r567787 / r567794;
        double r567796 = -r567795;
        double r567797 = fma(r567792, r567796, r567778);
        double r567798 = r567777 * r567797;
        double r567799 = sin(r567798);
        double r567800 = cbrt(r567763);
        double r567801 = r567800 * r567800;
        double r567802 = cbrt(r567764);
        double r567803 = r567802 * r567802;
        double r567804 = -r567803;
        double r567805 = 2.0;
        double r567806 = pow(r567789, r567805);
        double r567807 = r567778 / r567806;
        double r567808 = r567804 * r567807;
        double r567809 = fma(r567801, r567800, r567808);
        double r567810 = sin(r567809);
        double r567811 = r567804 + r567803;
        double r567812 = r567807 * r567811;
        double r567813 = cos(r567812);
        double r567814 = r567810 * r567813;
        double r567815 = cos(r567809);
        double r567816 = sin(r567812);
        double r567817 = r567815 * r567816;
        double r567818 = r567814 + r567817;
        double r567819 = r567799 * r567818;
        double r567820 = r567786 - r567819;
        double r567821 = 3.0;
        double r567822 = pow(r567820, r567821);
        double r567823 = cbrt(r567822);
        double r567824 = 2.0;
        double r567825 = x;
        double r567826 = sqrt(r567825);
        double r567827 = r567824 * r567826;
        double r567828 = r567823 * r567827;
        double r567829 = a;
        double r567830 = b;
        double r567831 = r567830 * r567767;
        double r567832 = r567829 / r567831;
        double r567833 = r567828 - r567832;
        double r567834 = 1.5;
        double r567835 = pow(r567763, r567805);
        double r567836 = r567834 * r567835;
        double r567837 = r567773 - r567836;
        double r567838 = cbrt(r567837);
        double r567839 = r567827 * r567838;
        double r567840 = r567839 - r567832;
        double r567841 = r567772 ? r567833 : r567840;
        return r567841;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Target

Original	20.4
Target	18.5
Herbie	18.6

\[\begin{array}{l} \mathbf{if}\;z \lt -1.379333748723514136852843173740882251575 \cdot 10^{129}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(\frac{1}{y} - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{elif}\;z \lt 3.516290613555987147199887107423758623887 \cdot 10^{106}:\\ \;\;\;\;\left(\sqrt{x} \cdot 2\right) \cdot \cos \left(y - \frac{t}{3} \cdot z\right) - \frac{\frac{a}{3}}{b}\\ \mathbf{else}:\\ \;\;\;\;\cos \left(y - \frac{\frac{0.3333333333333333148296162562473909929395}{z}}{t}\right) \cdot \left(2 \cdot \sqrt{x}\right) - \frac{\frac{a}{b}}{3}\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if (cos (- y (/ (* z t) 3.0))) < 0.9957133982267297

   1. Initial program 20.0

      \[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]
   2. Using strategy rm

   3. Applied add-cbrt-cube 20.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\sqrt[3]{\left(\cos \left(y - \frac{z \cdot t}{3}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right)\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right)}} - \frac{a}{b \cdot 3}\]

   4. Simplified 20.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{\color{blue}{{\left(\cos \left(y - \frac{t}{\frac{3}{z}}\right)\right)}^{3}}} - \frac{a}{b \cdot 3}\]
   5. Using strategy rm

   6. Applied add-cube-cbrt 20.0

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(y - \frac{t}{\color{blue}{\left(\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}\right) \cdot \sqrt[3]{\frac{3}{z}}}}\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   7. Applied add-sqr-sqrt 42.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(y - \frac{\color{blue}{\sqrt{t} \cdot \sqrt{t}}}{\left(\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}\right) \cdot \sqrt[3]{\frac{3}{z}}}\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   8. Applied times-frac 42.1

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(y - \color{blue}{\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}}\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   9. Applied add-sqr-sqrt 54.6

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\color{blue}{\sqrt{y} \cdot \sqrt{y}} - \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   10. Applied prod-diff 54.6

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \color{blue}{\left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) + \mathsf{fma}\left(-\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right)}\right)}^{3}} - \frac{a}{b \cdot 3}\]

   11. Applied cos-sum 54.6

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\color{blue}{\left(\cos \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right) - \sin \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right)\right)}}^{3}} - \frac{a}{b \cdot 3}\]

   12. Simplified 53.0

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\color{blue}{\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)} - \sin \left(\mathsf{fma}\left(\sqrt{y}, \sqrt{y}, -\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}, \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}}} \cdot \frac{\sqrt{t}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   13. Simplified 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \color{blue}{\sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)}\right)}^{3}} - \frac{a}{b \cdot 3}\]
   14. Using strategy rm

   15. Applied *-un-lft-identity 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{\color{blue}{1 \cdot z}}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   16. Applied add-cube-cbrt 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{\color{blue}{\left(\sqrt[3]{3} \cdot \sqrt[3]{3}\right) \cdot \sqrt[3]{3}}}{1 \cdot z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   17. Applied times-frac 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\color{blue}{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1} \cdot \frac{\sqrt[3]{3}}{z}}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   18. Applied cbrt-prod 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\color{blue}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}} \cdot \sqrt[3]{\frac{\sqrt[3]{3}}{z}}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   19. Applied add-cube-cbrt 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{\color{blue}{\left(\sqrt[3]{t} \cdot \sqrt[3]{t}\right) \cdot \sqrt[3]{t}}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}} \cdot \sqrt[3]{\frac{\sqrt[3]{3}}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   20. Applied times-frac 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\color{blue}{\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}} \cdot \frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   21. Applied distribute-rgt-neg-in 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\color{blue}{\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}} \cdot \left(-\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}\right)} + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   22. Applied fma-def 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \color{blue}{\mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)}\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]
   23. Using strategy rm

   24. Applied cbrt-div 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \color{blue}{\frac{\sqrt[3]{3}}{\sqrt[3]{z}}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   25. Applied cbrt-div 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\color{blue}{\frac{\sqrt[3]{3}}{\sqrt[3]{z}}} \cdot \frac{\sqrt[3]{3}}{\sqrt[3]{z}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   26. Applied frac-times 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\color{blue}{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{\sqrt[3]{z} \cdot \sqrt[3]{z}}}}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   27. Applied associate-/r/ 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(y - \color{blue}{\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   28. Applied add-cube-cbrt 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(\color{blue}{\left(\sqrt[3]{y} \cdot \sqrt[3]{y}\right) \cdot \sqrt[3]{y}} - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}} \cdot \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   29. Applied prod-diff 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \color{blue}{\left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, -\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right) + \mathsf{fma}\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}, \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}, \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right)} \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   30. Applied sin-sum 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \color{blue}{\left(\sin \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, -\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right) \cdot \cos \left(\mathsf{fma}\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}, \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}, \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right) + \cos \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, -\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}, \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}, \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right)\right)} \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   31. Simplified 20.1

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \left(\color{blue}{\sin \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \cos \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)} + \cos \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, -\left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right) \cdot \sin \left(\mathsf{fma}\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}, \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}, \left(\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{3} \cdot \sqrt[3]{3}}\right)\right)\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   32. Simplified 20.2

       \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \left(\sin \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \cos \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) + \color{blue}{\cos \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \sin \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)}\right) \cdot \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3} \cdot \sqrt[3]{3}}{1}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right)\right)}^{3}} - \frac{a}{b \cdot 3}\]

   if 0.9957133982267297 < (cos (- y (/ (* z t) 3.0)))

   1. Initial program 20.9

      \[\left(2 \cdot \sqrt{x}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right) - \frac{a}{b \cdot 3}\]
   2. Using strategy rm

   3. Applied add-cbrt-cube 20.9

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \color{blue}{\sqrt[3]{\left(\cos \left(y - \frac{z \cdot t}{3}\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right)\right) \cdot \cos \left(y - \frac{z \cdot t}{3}\right)}} - \frac{a}{b \cdot 3}\]

   4. Simplified 20.9

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{\color{blue}{{\left(\cos \left(y - \frac{t}{\frac{3}{z}}\right)\right)}^{3}}} - \frac{a}{b \cdot 3}\]

   5. Taylor expanded around 0 16.3

      \[\leadsto \left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{\color{blue}{1 - \frac{3}{2} \cdot {y}^{2}}} - \frac{a}{b \cdot 3}\]
3. Recombined 2 regimes into one program.

4. Final simplification 18.6

   \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(y - \frac{z \cdot t}{3}\right) \le 0.9957133982267296623547281342325732111931:\\ \;\;\;\;\sqrt[3]{{\left(\cos \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \left(\left(-\frac{t}{\sqrt[3]{\frac{3}{z}}}\right) + \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \cos \left(y - \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}}\right) - \sin \left(\frac{1}{\sqrt[3]{\frac{3}{z}} \cdot \sqrt[3]{\frac{3}{z}}} \cdot \mathsf{fma}\left(\frac{\sqrt[3]{t} \cdot \sqrt[3]{t}}{\sqrt[3]{\sqrt[3]{3} \cdot \sqrt[3]{3}}}, -\frac{\sqrt[3]{t}}{\sqrt[3]{\frac{\sqrt[3]{3}}{z}}}, \frac{t}{\sqrt[3]{\frac{3}{z}}}\right)\right) \cdot \left(\sin \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \cos \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right) + \cos \left(\mathsf{fma}\left(\sqrt[3]{y} \cdot \sqrt[3]{y}, \sqrt[3]{y}, \left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) \cdot \frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}}\right)\right) \cdot \sin \left(\frac{\frac{t}{\sqrt[3]{\frac{3}{z}}}}{{\left(\sqrt[3]{3}\right)}^{2}} \cdot \left(\left(-\sqrt[3]{z} \cdot \sqrt[3]{z}\right) + \sqrt[3]{z} \cdot \sqrt[3]{z}\right)\right)\right)\right)}^{3}} \cdot \left(2 \cdot \sqrt{x}\right) - \frac{a}{b \cdot 3}\\ \mathbf{else}:\\ \;\;\;\;\left(2 \cdot \sqrt{x}\right) \cdot \sqrt[3]{1 - \frac{3}{2} \cdot {y}^{2}} - \frac{a}{b \cdot 3}\\ \end{array}\]

Reproduce

herbie shell --seed 2019347 +o rules:numerics
(FPCore (x y z t a b)
  :name "Diagrams.Solve.Polynomial:cubForm  from diagrams-solve-0.1, K"
  :precision binary64

  :herbie-target
  (if (< z -1.379333748723514e+129) (- (* (* 2 (sqrt x)) (cos (- (/ 1 y) (/ (/ 0.3333333333333333 z) t)))) (/ (/ a 3) b)) (if (< z 3.516290613555987e+106) (- (* (* (sqrt x) 2) (cos (- y (* (/ t 3) z)))) (/ (/ a 3) b)) (- (* (cos (- y (/ (/ 0.3333333333333333 z) t))) (* 2 (sqrt x))) (/ (/ a b) 3))))

  (- (* (* 2 (sqrt x)) (cos (- y (/ (* z t) 3)))) (/ a (* b 3))))