Initial program 29.1
\[\left(\left(\left(\left(\left(\left(x \cdot 18.0\right) \cdot y\right) \cdot z\right) \cdot t - \left(a \cdot 4.0\right) \cdot t\right) + b \cdot c\right) - \left(x \cdot 4.0\right) \cdot i\right) - \left(j \cdot 27.0\right) \cdot k\]
Applied simplify11.4
\[\leadsto \color{blue}{(\left(\left(t \cdot x\right) \cdot \left(y \cdot 18.0\right)\right) \cdot z + \left((\left(-a\right) \cdot \left(4.0 \cdot t\right) + \left(b \cdot c\right))_*\right))_* - (i \cdot \left(x \cdot 4.0\right) + \left(\left(27.0 \cdot k\right) \cdot j\right))_*}\]
Taylor expanded around inf 11.1
\[\leadsto \color{blue}{\left(\left(18.0 \cdot \left(z \cdot \left(y \cdot \left(t \cdot x\right)\right)\right) + b \cdot c\right) - 4.0 \cdot \left(a \cdot t\right)\right)} - (i \cdot \left(x \cdot 4.0\right) + \left(\left(27.0 \cdot k\right) \cdot j\right))_*\]
Applied simplify10.8
\[\leadsto \color{blue}{(\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_* - (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*}\]
- Using strategy
rm Applied *-un-lft-identity10.8
\[\leadsto (\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_* - \color{blue}{1 \cdot (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*}\]
Applied *-un-lft-identity10.8
\[\leadsto \color{blue}{1 \cdot (\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_*} - 1 \cdot (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\]
Applied prod-diff10.8
\[\leadsto \color{blue}{(1 \cdot \left((\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_*\right) + \left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_* + (\left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\right) \cdot 1 + \left((4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_*}\]
Applied simplify58.8
\[\leadsto \color{blue}{\left((18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_* - (\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right)} + (\left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\right) \cdot 1 + \left((4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_*\]
Applied simplify58.8
\[\leadsto \left((18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_* - (\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right) + \color{blue}{0}\]
- Using strategy
rm Applied add-sqr-sqrt60.3
\[\leadsto \left((18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_* - \color{blue}{\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*} \cdot \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}}\right) + 0\]
Applied add-cube-cbrt60.3
\[\leadsto \left(\color{blue}{\left(\sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*} \cdot \sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*}\right) \cdot \sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*}} - \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*} \cdot \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right) + 0\]
Applied prod-diff60.3
\[\leadsto \color{blue}{\left((\left(\sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*} \cdot \sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*}\right) \cdot \left(\sqrt[3]{(18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_*}\right) + \left(-\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*} \cdot \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right))_* + (\left(-\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right) \cdot \left(\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right) + \left(\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*} \cdot \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right))_*\right)} + 0\]
Applied simplify37.6
\[\leadsto \left(\color{blue}{\left((t \cdot \left(\left(18.0 \cdot y\right) \cdot \left(z \cdot x\right)\right) + \left(b \cdot c\right))_* - (4.0 \cdot \left((a \cdot t + \left(x \cdot i\right))_*\right) + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right)} + (\left(-\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right) \cdot \left(\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right) + \left(\sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*} \cdot \sqrt{(\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*}\right))_*\right) + 0\]
Applied simplify11.8
\[\leadsto \left(\left((t \cdot \left(\left(18.0 \cdot y\right) \cdot \left(z \cdot x\right)\right) + \left(b \cdot c\right))_* - (4.0 \cdot \left((a \cdot t + \left(x \cdot i\right))_*\right) + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right) + \color{blue}{0}\right) + 0\]
Initial program 2.9
\[\left(\left(\left(\left(\left(\left(x \cdot 18.0\right) \cdot y\right) \cdot z\right) \cdot t - \left(a \cdot 4.0\right) \cdot t\right) + b \cdot c\right) - \left(x \cdot 4.0\right) \cdot i\right) - \left(j \cdot 27.0\right) \cdot k\]
Applied simplify3.5
\[\leadsto \color{blue}{(\left(\left(t \cdot x\right) \cdot \left(y \cdot 18.0\right)\right) \cdot z + \left((\left(-a\right) \cdot \left(4.0 \cdot t\right) + \left(b \cdot c\right))_*\right))_* - (i \cdot \left(x \cdot 4.0\right) + \left(\left(27.0 \cdot k\right) \cdot j\right))_*}\]
Taylor expanded around inf 3.4
\[\leadsto \color{blue}{\left(\left(18.0 \cdot \left(z \cdot \left(y \cdot \left(t \cdot x\right)\right)\right) + b \cdot c\right) - 4.0 \cdot \left(a \cdot t\right)\right)} - (i \cdot \left(x \cdot 4.0\right) + \left(\left(27.0 \cdot k\right) \cdot j\right))_*\]
Applied simplify3.8
\[\leadsto \color{blue}{(\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_* - (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*}\]
- Using strategy
rm Applied *-un-lft-identity3.8
\[\leadsto (\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_* - \color{blue}{1 \cdot (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*}\]
Applied *-un-lft-identity3.8
\[\leadsto \color{blue}{1 \cdot (\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_*} - 1 \cdot (4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\]
Applied prod-diff3.8
\[\leadsto \color{blue}{(1 \cdot \left((\left(z \cdot 18.0\right) \cdot \left(\left(y \cdot t\right) \cdot x\right) + \left(c \cdot b\right))_*\right) + \left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_* + (\left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\right) \cdot 1 + \left((4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_*}\]
Applied simplify0.2
\[\leadsto \color{blue}{\left((18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_* - (\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right)} + (\left(-(4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_*\right) \cdot 1 + \left((4.0 \cdot \left((t \cdot a + \left(x \cdot i\right))_*\right) + \left(\left(k \cdot j\right) \cdot 27.0\right))_* \cdot 1\right))_*\]
Applied simplify0.2
\[\leadsto \left((18.0 \cdot \left(\left(x \cdot y\right) \cdot \left(t \cdot z\right)\right) + \left(b \cdot c\right))_* - (\left((t \cdot a + \left(x \cdot i\right))_*\right) \cdot 4.0 + \left(\left(j \cdot k\right) \cdot 27.0\right))_*\right) + \color{blue}{0}\]