if z < -1.7226329f+15 or 1.5366934f+17 < z

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   30.4
2. Using strategy rm
   30.4
3. Applied add-cube-cbrt to get
   \[(x * y + z)_* - \left(1 + \color{red}{\left(x \cdot y + z\right)}\right) \leadsto (x * y + z)_* - \left(1 + \color{blue}{{\left(\sqrt[3]{x \cdot y + z}\right)}^3}\right)\]
   30.1
4. Applied taylor to get
   \[(x * y + z)_* - \left(1 + {\left(\sqrt[3]{x \cdot y + z}\right)}^3\right) \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 -1.7226329f+15 < z < -4.1334874f-06

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   19.0
2. Using strategy rm
   19.0
3. Applied associate--r+ to get
   \[\color{red}{(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)} \leadsto \color{blue}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)}\]
   10.4
4. Using strategy rm
   10.4
5. Applied flip3-- to get
   \[\color{red}{\left((x * y + z)_* - 1\right)} - \left(x \cdot y + z\right) \leadsto \color{blue}{\frac{{\left((x * y + z)_*\right)}^{3} - {1}^{3}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)}} - \left(x \cdot y + z\right)\]
   21.2
6. Applied simplify to get
   \[\frac{\color{red}{{\left((x * y + z)_*\right)}^{3} - {1}^{3}}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right) \leadsto \frac{\color{blue}{{\left((x * y + z)_*\right)}^3 - 1}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)\]
   11.1
7. Using strategy rm
   11.1
8. Applied add-cube-cbrt to get
   \[\color{red}{\frac{{\left((x * y + z)_*\right)}^3 - 1}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)} \leadsto \color{blue}{{\left(\sqrt[3]{\frac{{\left((x * y + z)_*\right)}^3 - 1}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)}\right)}^3}\]
   11.1

if -4.1334874f-06 < z < 583.3768f0

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   12.6
2. Using strategy rm
   12.6
3. Applied associate--r+ to get
   \[\color{red}{(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)} \leadsto \color{blue}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)}\]
   9.6
4. Using strategy rm
   9.6
5. Applied associate--r+ to get
   \[\color{red}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)} \leadsto \color{blue}{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right) - z}\]
   9.7
6. Applied taylor to get
   \[\left(\left((x * y + z)_* - 1\right) - x \cdot y\right) - z \leadsto \left((x * y + z)_* - \left(y \cdot x + 1\right)\right) - z\]
   12.5
7. Taylor expanded around 0 to get
   \[\color{red}{\left((x * y + z)_* - \left(y \cdot x + 1\right)\right)} - z \leadsto \color{blue}{\left((x * y + z)_* - \left(y \cdot x + 1\right)\right)} - z\]
   12.5
8. Applied simplify to get
   \[\left((x * y + z)_* - \left(y \cdot x + 1\right)\right) - z \leadsto \left((x * y + z)_* - y \cdot x\right) - \left(z + 1\right)\]
   4.8

---

9. Applied final simplification

if 583.3768f0 < z < 1.5366934f+17

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   24.6
2. Using strategy rm
   24.6
3. Applied associate--r+ to get
   \[\color{red}{(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)} \leadsto \color{blue}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)}\]
   12.3
4. Using strategy rm
   12.3
5. Applied flip3-- to get
   \[\color{red}{\left((x * y + z)_* - 1\right)} - \left(x \cdot y + z\right) \leadsto \color{blue}{\frac{{\left((x * y + z)_*\right)}^{3} - {1}^{3}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)}} - \left(x \cdot y + z\right)\]
   27.3
6. Applied simplify to get
   \[\frac{\color{red}{{\left((x * y + z)_*\right)}^{3} - {1}^{3}}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right) \leadsto \frac{\color{blue}{{\left((x * y + z)_*\right)}^3 - 1}}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)\]
   13.3
7. Using strategy rm
   13.3
8. Applied add-cube-cbrt to get
   \[\color{red}{\frac{{\left((x * y + z)_*\right)}^3 - 1}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)} \leadsto \color{blue}{{\left(\sqrt[3]{\frac{{\left((x * y + z)_*\right)}^3 - 1}{{\left((x * y + z)_*\right)}^2 + \left({1}^2 + (x * y + z)_* \cdot 1\right)} - \left(x \cdot y + z\right)}\right)}^3}\]
   13.3