- Split input into 4 regimes
if (+ (- (+ (+ (- (- (* z (* c (* t i))) (+ (* y (* c (* i x))) (* z (* b (* a t))))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) < -1.053436419897432e+306
Initial program 49.8
\[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
Taylor expanded around inf 48.8
\[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \color{blue}{\left(z \cdot \left(y1 \cdot \left(k \cdot i\right)\right) - \left(z \cdot \left(b \cdot \left(y0 \cdot k\right)\right) + y1 \cdot \left(j \cdot \left(i \cdot x\right)\right)\right)\right)}\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if -1.053436419897432e+306 < (+ (- (+ (+ (- (- (* z (* c (* t i))) (+ (* y (* c (* i x))) (* z (* b (* a t))))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) < -5.91172691841533e+183 or 5.089140033083518e+108 < (+ (- (+ (+ (- (- (* z (* c (* t i))) (+ (* y (* c (* i x))) (* z (* b (* a t))))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) < 4.835321378996754e+300
Initial program 5.1
\[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
Taylor expanded around inf 2.4
\[\leadsto \left(\left(\left(\left(\color{blue}{\left(z \cdot \left(c \cdot \left(t \cdot i\right)\right) - \left(y \cdot \left(c \cdot \left(i \cdot x\right)\right) + z \cdot \left(b \cdot \left(a \cdot t\right)\right)\right)\right)} - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if -5.91172691841533e+183 < (+ (- (+ (+ (- (- (* z (* c (* t i))) (+ (* y (* c (* i x))) (* z (* b (* a t))))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))) < 5.089140033083518e+108
Initial program 3.7
\[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
- Using strategy
rm Applied add-cube-cbrt3.8
\[\leadsto \left(\left(\left(\left(\color{blue}{\left(\sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)} \cdot \sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)}\right) \cdot \sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)}} - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
- Using strategy
rm Applied add-cube-cbrt3.8
\[\leadsto \left(\left(\left(\left(\left(\sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)} \cdot \sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \color{blue}{\left(\left(\sqrt[3]{a \cdot b - c \cdot i} \cdot \sqrt[3]{a \cdot b - c \cdot i}\right) \cdot \sqrt[3]{a \cdot b - c \cdot i}\right)}}\right) \cdot \sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)} - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
Applied associate-*r*3.8
\[\leadsto \left(\left(\left(\left(\left(\sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)} \cdot \sqrt[3]{\color{blue}{\left(\left(x \cdot y - z \cdot t\right) \cdot \left(\sqrt[3]{a \cdot b - c \cdot i} \cdot \sqrt[3]{a \cdot b - c \cdot i}\right)\right) \cdot \sqrt[3]{a \cdot b - c \cdot i}}}\right) \cdot \sqrt[3]{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right)} - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if 4.835321378996754e+300 < (+ (- (+ (+ (- (- (* z (* c (* t i))) (+ (* y (* c (* i x))) (* z (* b (* a t))))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))
Initial program 53.7
\[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
Taylor expanded around 0 51.8
\[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \color{blue}{0}\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
- Recombined 4 regimes into one program.
Final simplification24.3
\[\leadsto \begin{array}{l}
\mathbf{if}\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) \le -1.053436419897432 \cdot 10^{+306}:\\
\;\;\;\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(i \cdot k\right) \cdot y1\right) \cdot z - \left(\left(\left(y0 \cdot k\right) \cdot b\right) \cdot z + \left(j \cdot \left(x \cdot i\right)\right) \cdot y1\right)\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\
\mathbf{elif}\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) \le -5.91172691841533 \cdot 10^{+183}:\\
\;\;\;\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\
\mathbf{elif}\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) \le 5.089140033083518 \cdot 10^{+108}:\\
\;\;\;\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right) + \left(\left(\left(\sqrt[3]{\left(a \cdot b - i \cdot c\right) \cdot \left(x \cdot y - z \cdot t\right)} \cdot \sqrt[3]{\left(\left(\sqrt[3]{a \cdot b - i \cdot c} \cdot \sqrt[3]{a \cdot b - i \cdot c}\right) \cdot \left(x \cdot y - z \cdot t\right)\right) \cdot \sqrt[3]{a \cdot b - i \cdot c}}\right) \cdot \sqrt[3]{\left(a \cdot b - i \cdot c\right) \cdot \left(x \cdot y - z \cdot t\right)} - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\
\mathbf{elif}\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) \le 4.835321378996754 \cdot 10^{+300}:\\
\;\;\;\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(\left(\left(\left(c \cdot \left(t \cdot i\right)\right) \cdot z - \left(\left(b \cdot \left(a \cdot t\right)\right) \cdot z + \left(\left(x \cdot i\right) \cdot c\right) \cdot y\right)\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\left(y4 \cdot y1 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(\left(\left(b \cdot y4 - i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\
\end{array}\]