if z < -76168393706.3139 or 3.1224846592363346e+28 < z

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   62.4
2. Using strategy rm
   62.4
3. Applied add-cbrt-cube to get
   \[(x * y + z)_* - \color{red}{\left(1 + \left(x \cdot y + z\right)\right)} \leadsto (x * y + z)_* - \color{blue}{\sqrt[3]{{\left(1 + \left(x \cdot y + z\right)\right)}^3}}\]
   62.6
4. Applied taylor to get
   \[(x * y + z)_* - \sqrt[3]{{\left(1 + \left(x \cdot y + z\right)\right)}^3} \leadsto (\left(\frac{1}{x}\right) * \left(\frac{1}{y}\right) + \left(\frac{1}{z}\right))_* - 1\]
   0.2
5. Taylor expanded around inf to get
   \[\color{red}{(\left(\frac{1}{x}\right) * \left(\frac{1}{y}\right) + \left(\frac{1}{z}\right))_* - 1} \leadsto \color{blue}{(\left(\frac{1}{x}\right) * \left(\frac{1}{y}\right) + \left(\frac{1}{z}\right))_* - 1}\]
   0.2
6. Applied simplify to get
   \[(\left(\frac{1}{x}\right) * \left(\frac{1}{y}\right) + \left(\frac{1}{z}\right))_* - 1 \leadsto (\left(\frac{1}{x}\right) * \left(\frac{1}{y}\right) + \left(\frac{1}{z}\right))_* - 1\]
   0.2

---

7. Applied final simplification

if -76168393706.3139 < z < 3.1224846592363346e+28

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   30.6
2. Using strategy rm
   30.6
3. Applied flip-+ to get
   \[(x * y + z)_* - \color{red}{\left(1 + \left(x \cdot y + z\right)\right)} \leadsto (x * y + z)_* - \color{blue}{\frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}}\]
   30.8
4. Using strategy rm
   30.8
5. Applied flip-- to get
   \[\color{red}{(x * y + z)_* - \frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}} \leadsto \color{blue}{\frac{{\left((x * y + z)_*\right)}^2 - {\left(\frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}\right)}^2}{(x * y + z)_* + \frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}}}\]
   31.7
6. Applied simplify to get
   \[\frac{{\left((x * y + z)_*\right)}^2 - {\left(\frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}\right)}^2}{\color{red}{(x * y + z)_* + \frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}}} \leadsto \frac{{\left((x * y + z)_*\right)}^2 - {\left(\frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}\right)}^2}{\color{blue}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*}}\]
   31.7
7. Applied taylor to get
   \[\frac{{\left((x * y + z)_*\right)}^2 - {\left(\frac{{1}^2 - {\left(x \cdot y + z\right)}^2}{1 - \left(x \cdot y + z\right)}\right)}^2}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*} \leadsto \frac{{\left((x * y + z)_*\right)}^2 - {\left(y \cdot x + \left(1 + z\right)\right)}^2}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*}\]
   31.7
8. Taylor expanded around 0 to get
   \[\frac{{\left((x * y + z)_*\right)}^2 - {\color{red}{\left(y \cdot x + \left(1 + z\right)\right)}}^2}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*} \leadsto \frac{{\left((x * y + z)_*\right)}^2 - {\color{blue}{\left(y \cdot x + \left(1 + z\right)\right)}}^2}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*}\]
   31.7
9. Applied simplify to get
   \[\frac{{\left((x * y + z)_*\right)}^2 - {\left(y \cdot x + \left(1 + z\right)\right)}^2}{\left(y \cdot x + \left(1 + z\right)\right) + (x * y + z)_*} \leadsto \frac{\left(y \cdot x + \left(z + 1\right)\right) + (x * y + z)_*}{\frac{\left(y \cdot x + \left(z + 1\right)\right) + (x * y + z)_*}{\left((x * y + z)_* - y \cdot x\right) - \left(z + 1\right)}}\]
   10.5

---

10. Applied final simplification
11. Applied simplify to get
    \[\color{red}{\frac{\left(y \cdot x + \left(z + 1\right)\right) + (x * y + z)_*}{\frac{\left(y \cdot x + \left(z + 1\right)\right) + (x * y + z)_*}{\left((x * y + z)_* - y \cdot x\right) - \left(z + 1\right)}}} \leadsto \color{blue}{\left((x * y + z)_* - x \cdot y\right) - \left(1 + z\right)}\]
    10.4