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)\]
Simplified0.5
\[\leadsto \color{blue}{x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} \cdot \left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right)\right) + 4 \cdot \left(x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)}\]
- Using strategy
rm Applied add-sqr-sqrt0.5
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{\color{blue}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}}} \cdot \left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right)\right) + 4 \cdot \left(x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
Applied *-un-lft-identity0.5
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\frac{\color{blue}{1 \cdot \left(x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)\right)}}{\sqrt{x1 \cdot x1 + 1} \cdot \sqrt{x1 \cdot x1 + 1}} \cdot \left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right)\right) + 4 \cdot \left(x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
Applied times-frac0.6
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\color{blue}{\left(\frac{1}{\sqrt{x1 \cdot x1 + 1}} \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{\sqrt{x1 \cdot x1 + 1}}\right)} \cdot \left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right)\right) + 4 \cdot \left(x1 \cdot x1\right)\right) + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
Applied associate-*l*0.6
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\color{blue}{\frac{1}{\sqrt{x1 \cdot x1 + 1}} \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{\sqrt{x1 \cdot x1 + 1}} \cdot \left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right)\right) + 4 \cdot \left(x1 \cdot x1\right)\right)\right)} + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
Simplified0.6
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\frac{1}{\sqrt{x1 \cdot x1 + 1}} \cdot \color{blue}{\left(\left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right) + x1 \cdot 4\right)\right) \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{\sqrt{x1 \cdot x1 + 1}}\right)} + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} + x1\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
Final simplification0.6
\[\leadsto x1 + \left(x1 + \left(\left(x1 \cdot x1 + 1\right) \cdot \left(\frac{1}{\sqrt{x1 \cdot x1 + 1}} \cdot \left(\left(x1 \cdot \left(2 \cdot \left(\frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1} - 3\right) + x1 \cdot 4\right)\right) \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{\sqrt{x1 \cdot x1 + 1}}\right) + x1 \cdot \left(x1 \cdot \left(-6\right)\right)\right) + \left(x1 \cdot \left(x1 \cdot \left(x1 + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) + \left(2 \cdot x2 - x1\right)}{x1 \cdot x1 + 1}\right)\right) + 3 \cdot \frac{x1 \cdot \left(x1 \cdot 3\right) - \left(x1 + 2 \cdot x2\right)}{x1 \cdot x1 + 1}\right)\right)\right)\]
