if z < -1.6846166027071804e+162 or 1.6780563391812001e+18 < z

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

if -1.6846166027071804e+162 < z < -22782720796029.24

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   61.5
2. Using strategy rm
   61.5
3. Applied add-cbrt-cube to get
   \[(x * y + z)_* - \left(1 + \color{red}{\left(x \cdot y + z\right)}\right) \leadsto (x * y + z)_* - \left(1 + \color{blue}{\sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right)\]
   62.3
4. Using strategy rm
   62.3
5. Applied add-log-exp to get
   \[\color{red}{(x * y + z)_* - \left(1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}\right)} \leadsto \color{blue}{\log \left(e^{(x * y + z)_* - \left(1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}\right)}\right)}\]
   62.5
6. Applied simplify to get
   \[\log \color{red}{\left(e^{(x * y + z)_* - \left(1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}\right)}\right)} \leadsto \log \color{blue}{\left(e^{\left((x * y + z)_* - z\right) - \left(y \cdot x + 1\right)}\right)}\]
   32.6

if -22782720796029.24 < z < 1.6780563391812001e+18

1. Started with
   \[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
   30.1
2. Using strategy rm
   30.1
3. Applied add-cbrt-cube to get
   \[(x * y + z)_* - \left(1 + \color{red}{\left(x \cdot y + z\right)}\right) \leadsto (x * y + z)_* - \left(1 + \color{blue}{\sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right)\]
   30.7
4. Using strategy rm
   30.7
5. Applied add-log-exp to get
   \[(x * y + z)_* - \color{red}{\left(1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}\right)} \leadsto (x * y + z)_* - \color{blue}{\log \left(e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right)}\]
   32.8
6. Applied add-log-exp to get
   \[\color{red}{(x * y + z)_*} - \log \left(e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right) \leadsto \color{blue}{\log \left(e^{(x * y + z)_*}\right)} - \log \left(e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right)\]
   33.2
7. Applied diff-log to get
   \[\color{red}{\log \left(e^{(x * y + z)_*}\right) - \log \left(e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}\right)} \leadsto \color{blue}{\log \left(\frac{e^{(x * y + z)_*}}{e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}}\right)}\]
   33.2
8. Applied simplify to get
   \[\log \color{red}{\left(\frac{e^{(x * y + z)_*}}{e^{1 + \sqrt[3]{{\left(x \cdot y + z\right)}^3}}}\right)} \leadsto \log \color{blue}{\left(e^{\left((x * y + z)_* - y \cdot x\right) - \left(z + 1\right)}\right)}\]
   10.1