Initial program 0.5
\[\frac{2 + \left(\left(\sqrt{2} \cdot \left(\sin x - \frac{\sin y}{16}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 \cdot \left(\left(1 + \frac{\sqrt{5} - 1}{2} \cdot \cos x\right) + \frac{3 - \sqrt{5}}{2} \cdot \cos y\right)}\]
Simplified0.4
\[\leadsto \color{blue}{\frac{2 + \left(\left(\sqrt{2} \cdot \left(\sin x - \frac{\sin y}{16}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}}\]
- Using strategy
rm Applied add-cube-cbrt_binary64_82970.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \left(\sin x - \frac{\sin y}{\color{blue}{\left(\sqrt[3]{16} \cdot \sqrt[3]{16}\right) \cdot \sqrt[3]{16}}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied add-cube-cbrt_binary64_82970.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \left(\sin x - \frac{\color{blue}{\left(\sqrt[3]{\sin y} \cdot \sqrt[3]{\sin y}\right) \cdot \sqrt[3]{\sin y}}}{\left(\sqrt[3]{16} \cdot \sqrt[3]{16}\right) \cdot \sqrt[3]{16}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied times-frac_binary64_82680.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \left(\sin x - \color{blue}{\frac{\sqrt[3]{\sin y} \cdot \sqrt[3]{\sin y}}{\sqrt[3]{16} \cdot \sqrt[3]{16}} \cdot \frac{\sqrt[3]{\sin y}}{\sqrt[3]{16}}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied cancel-sign-sub-inv_binary64_82280.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \color{blue}{\left(\sin x + \left(-\frac{\sqrt[3]{\sin y} \cdot \sqrt[3]{\sin y}}{\sqrt[3]{16} \cdot \sqrt[3]{16}}\right) \cdot \frac{\sqrt[3]{\sin y}}{\sqrt[3]{16}}\right)}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied distribute-rgt-in_binary64_82120.4
\[\leadsto \frac{2 + \left(\color{blue}{\left(\sin x \cdot \sqrt{2} + \left(\left(-\frac{\sqrt[3]{\sin y} \cdot \sqrt[3]{\sin y}}{\sqrt[3]{16} \cdot \sqrt[3]{16}}\right) \cdot \frac{\sqrt[3]{\sin y}}{\sqrt[3]{16}}\right) \cdot \sqrt{2}\right)} \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Simplified0.4
\[\leadsto \frac{2 + \left(\left(\color{blue}{\sqrt{2} \cdot \sin x} + \left(\left(-\frac{\sqrt[3]{\sin y} \cdot \sqrt[3]{\sin y}}{\sqrt[3]{16} \cdot \sqrt[3]{16}}\right) \cdot \frac{\sqrt[3]{\sin y}}{\sqrt[3]{16}}\right) \cdot \sqrt{2}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Simplified0.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \color{blue}{\sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \left(3 - \sqrt{5}\right)\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
- Using strategy
rm Applied flip--_binary64_82370.5
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \color{blue}{\frac{3 \cdot 3 - \sqrt{5} \cdot \sqrt{5}}{3 + \sqrt{5}}}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Simplified0.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{\color{blue}{4}}{3 + \sqrt{5}}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Simplified0.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \cos y\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{4}{\color{blue}{\sqrt{5} + 3}}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
- Using strategy
rm Applied add-log-exp_binary64_83010.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\cos x - \color{blue}{\log \left(e^{\cos y}\right)}\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{4}{\sqrt{5} + 3}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied add-log-exp_binary64_83010.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \left(\color{blue}{\log \left(e^{\cos x}\right)} - \log \left(e^{\cos y}\right)\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{4}{\sqrt{5} + 3}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Applied diff-log_binary64_83540.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x + \sqrt{2} \cdot \left(-\frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right)\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \color{blue}{\log \left(\frac{e^{\cos x}}{e^{\cos y}}\right)}}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{4}{\sqrt{5} + 3}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]
Final simplification0.4
\[\leadsto \frac{2 + \left(\left(\sqrt{2} \cdot \sin x - \sqrt{2} \cdot \frac{\sin y}{{\left(\sqrt[3]{16}\right)}^{3}}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right) \cdot \log \left(\frac{e^{\cos x}}{e^{\cos y}}\right)}{3 + \left(\cos y \cdot \left(1.5 \cdot \frac{4}{3 + \sqrt{5}}\right) + 1.5 \cdot \left(\cos x \cdot \left(\sqrt{5} - 1\right)\right)\right)}\]