\[\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)\]

↓

\[\begin{array}{l} \mathbf{if}\;k \leq -5.352377399321279 \cdot 10^{-121}:\\ \;\;\;\;\left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right)\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y5 \cdot \left(a \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(c \cdot y4\right) \cdot \left(y \cdot y3 - t \cdot y2\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 1.4742294544187031 \cdot 10^{-186}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 2.5044263656925586 \cdot 10^{-159}:\\ \;\;\;\;\left(c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right) + \left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \left(a \cdot \left(\left(y \cdot x - t \cdot z\right) \cdot \sqrt[3]{b}\right)\right)\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 5.8370955327107604 \cdot 10^{-120}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right) - \left(t \cdot \left(y4 \cdot \left(c \cdot y2\right)\right) + y3 \cdot \left(a \cdot \left(y \cdot y5\right)\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 8.375037087757261 \cdot 10^{+37}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right) + \left(k \cdot \left(y \cdot \left(i \cdot y5\right)\right) - \left(t \cdot \left(j \cdot \left(i \cdot y5\right)\right) + y \cdot \left(k \cdot \left(b \cdot y4\right)\right)\right)\right)\right)\right)\right)\\ \end{array}\]

\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)

↓

\begin{array}{l}
\mathbf{if}\;k \leq -5.352377399321279 \cdot 10^{-121}:\\
\;\;\;\;\left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right)\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y5 \cdot \left(a \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(c \cdot y4\right) \cdot \left(y \cdot y3 - t \cdot y2\right)\right)\right)\right)\right)\right)\\

\mathbf{elif}\;k \leq 1.4742294544187031 \cdot 10^{-186}:\\
\;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\

\mathbf{elif}\;k \leq 2.5044263656925586 \cdot 10^{-159}:\\
\;\;\;\;\left(c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right) + \left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \left(a \cdot \left(\left(y \cdot x - t \cdot z\right) \cdot \sqrt[3]{b}\right)\right)\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\

\mathbf{elif}\;k \leq 5.8370955327107604 \cdot 10^{-120}:\\
\;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right) - \left(t \cdot \left(y4 \cdot \left(c \cdot y2\right)\right) + y3 \cdot \left(a \cdot \left(y \cdot y5\right)\right)\right)\right)\right)\right)\right)\right)\\

\mathbf{elif}\;k \leq 8.375037087757261 \cdot 10^{+37}:\\
\;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right) + \left(k \cdot \left(y \cdot \left(i \cdot y5\right)\right) - \left(t \cdot \left(j \cdot \left(i \cdot y5\right)\right) + y \cdot \left(k \cdot \left(b \cdot y4\right)\right)\right)\right)\right)\right)\right)\\

\end{array}

double code(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
	return ((double) (((double) (((double) (((double) (((double) (((double) (((double) (((double) (x * y)) - ((double) (z * t)))) * ((double) (((double) (a * b)) - ((double) (c * i)))))) - ((double) (((double) (((double) (x * j)) - ((double) (z * k)))) * ((double) (((double) (y0 * b)) - ((double) (y1 * i)))))))) + ((double) (((double) (((double) (x * y2)) - ((double) (z * y3)))) * ((double) (((double) (y0 * c)) - ((double) (y1 * a)))))))) + ((double) (((double) (((double) (t * j)) - ((double) (y * k)))) * ((double) (((double) (y4 * b)) - ((double) (y5 * i)))))))) - ((double) (((double) (((double) (t * y2)) - ((double) (y * y3)))) * ((double) (((double) (y4 * c)) - ((double) (y5 * a)))))))) + ((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y4 * y1)) - ((double) (y5 * y0))))))));
}

↓

double code(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
	double VAR;
	if ((k <= -5.352377399321279e-121)) {
		VAR = ((double) (((double) (((double) (b * ((double) (a * ((double) (((double) (y * x)) - ((double) (t * z)))))))) + ((double) (c * ((double) (i * ((double) (((double) (t * z)) - ((double) (y * x)))))))))) + ((double) (((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * ((double) (((double) (i * y1)) - ((double) (b * y0)))))) + ((double) (((double) (((double) (c * ((double) (y0 * ((double) (((double) (x * y2)) - ((double) (z * y3)))))))) + ((double) (a * ((double) (y1 * ((double) (((double) (z * y3)) - ((double) (x * y2)))))))))) + ((double) (((double) (((double) (((double) (t * j)) - ((double) (k * y)))) * ((double) (((double) (b * y4)) - ((double) (i * y5)))))) + ((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (y5 * ((double) (a * ((double) (((double) (t * y2)) - ((double) (y * y3)))))))) + ((double) (((double) (c * y4)) * ((double) (((double) (y * y3)) - ((double) (t * y2))))))))))))))))));
	} else {
		double VAR_1;
		if ((k <= 1.4742294544187031e-186)) {
			VAR_1 = ((double) (((double) (((double) (((double) (y * x)) - ((double) (t * z)))) * ((double) (((double) (b * a)) - ((double) (c * i)))))) + ((double) (((double) (((double) (i * ((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * y1)))) + ((double) (b * ((double) (y0 * ((double) (((double) (k * z)) - ((double) (x * j)))))))))) + ((double) (((double) (((double) (((double) (x * y2)) - ((double) (z * y3)))) * ((double) (((double) (c * y0)) - ((double) (a * y1)))))) + ((double) (((double) (((double) (((double) (t * j)) - ((double) (k * y)))) * ((double) (((double) (b * y4)) - ((double) (i * y5)))))) + ((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (((double) (t * y2)) - ((double) (y * y3)))) * ((double) (((double) (a * y5)) - ((double) (c * y4))))))))))))))));
		} else {
			double VAR_2;
			if ((k <= 2.5044263656925586e-159)) {
				VAR_2 = ((double) (((double) (((double) (c * ((double) (i * ((double) (((double) (t * z)) - ((double) (y * x)))))))) + ((double) (((double) (((double) cbrt(b)) * ((double) cbrt(b)))) * ((double) (a * ((double) (((double) (((double) (y * x)) - ((double) (t * z)))) * ((double) cbrt(b)))))))))) + ((double) (((double) (((double) (i * ((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * y1)))) + ((double) (b * ((double) (y0 * ((double) (((double) (k * z)) - ((double) (x * j)))))))))) + ((double) (((double) (((double) (c * ((double) (y0 * ((double) (((double) (x * y2)) - ((double) (z * y3)))))))) + ((double) (a * ((double) (y1 * ((double) (((double) (z * y3)) - ((double) (x * y2)))))))))) + ((double) (((double) (((double) (((double) (t * j)) - ((double) (k * y)))) * ((double) (((double) (b * y4)) - ((double) (i * y5)))))) + ((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (((double) (t * y2)) - ((double) (y * y3)))) * ((double) (((double) (a * y5)) - ((double) (c * y4))))))))))))))));
			} else {
				double VAR_3;
				if ((k <= 5.8370955327107604e-120)) {
					VAR_3 = ((double) (((double) (((double) (((double) (y * x)) - ((double) (t * z)))) * ((double) (((double) (b * a)) - ((double) (c * i)))))) + ((double) (((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * ((double) (((double) (i * y1)) - ((double) (b * y0)))))) + ((double) (((double) (((double) (((double) (x * y2)) - ((double) (z * y3)))) * ((double) (((double) (c * y0)) - ((double) (a * y1)))))) + ((double) (((double) (((double) (((double) (t * j)) - ((double) (k * y)))) * ((double) (((double) (b * y4)) - ((double) (i * y5)))))) + ((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (y4 * ((double) (y * ((double) (c * y3)))))) - ((double) (((double) (t * ((double) (y4 * ((double) (c * y2)))))) + ((double) (y3 * ((double) (a * ((double) (y * y5))))))))))))))))))));
				} else {
					double VAR_4;
					if ((k <= 8.375037087757261e+37)) {
						VAR_4 = ((double) (((double) (((double) (((double) (y * x)) - ((double) (t * z)))) * ((double) (((double) (b * a)) - ((double) (c * i)))))) + ((double) (((double) (((double) (i * ((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * y1)))) + ((double) (b * ((double) (y0 * ((double) (((double) (k * z)) - ((double) (x * j)))))))))) + ((double) (((double) (((double) (((double) (x * y2)) - ((double) (z * y3)))) * ((double) (((double) (c * y0)) - ((double) (a * y1)))))) + ((double) (((double) (((double) (((double) (t * j)) - ((double) (k * y)))) * ((double) (((double) (b * y4)) - ((double) (i * y5)))))) + ((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (((double) (t * y2)) - ((double) (y * y3)))) * ((double) (((double) (a * y5)) - ((double) (c * y4))))))))))))))));
					} else {
						VAR_4 = ((double) (((double) (((double) (((double) (y * x)) - ((double) (t * z)))) * ((double) (((double) (b * a)) - ((double) (c * i)))))) + ((double) (((double) (((double) (((double) (x * j)) - ((double) (k * z)))) * ((double) (((double) (i * y1)) - ((double) (b * y0)))))) + ((double) (((double) (((double) (((double) (x * y2)) - ((double) (z * y3)))) * ((double) (((double) (c * y0)) - ((double) (a * y1)))))) + ((double) (((double) (((double) (((double) (((double) (k * y2)) - ((double) (j * y3)))) * ((double) (((double) (y1 * y4)) - ((double) (y0 * y5)))))) + ((double) (((double) (((double) (t * y2)) - ((double) (y * y3)))) * ((double) (((double) (a * y5)) - ((double) (c * y4)))))))) + ((double) (((double) (k * ((double) (y * ((double) (i * y5)))))) - ((double) (((double) (t * ((double) (j * ((double) (i * y5)))))) + ((double) (y * ((double) (k * ((double) (b * y4))))))))))))))))));
					}
					VAR_3 = VAR_4;
				}
				VAR_2 = VAR_3;
			}
			VAR_1 = VAR_2;
		}
		VAR = VAR_1;
	}
	return VAR;
}

Original	27.1
Target	31.0
Herbie	26.9

Derivation

Split input into 5 regimes
if k < -5.3523773993212786e-121
1. Initial program 28.5
  \[\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)\]
2. Simplified28.5
  \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg28.5
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{blue}{\left(c \cdot y0 + \left(-a \cdot y1\right)\right)} + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
5. Applied distribute-lft-in28.5
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right)} + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
6. Simplified28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(\color{blue}{c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)} + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
7. Simplified28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \color{blue}{a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)}\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
8. Using strategy rm
9. Applied sub-neg28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \color{blue}{\left(a \cdot b + \left(-c \cdot i\right)\right)} + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
10. Applied distribute-lft-in28.7
  \[\leadsto \color{blue}{\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b\right) + \left(x \cdot y - z \cdot t\right) \cdot \left(-c \cdot i\right)\right)} + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
11. Simplified28.6
  \[\leadsto \left(\color{blue}{b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right)} + \left(x \cdot y - z \cdot t\right) \cdot \left(-c \cdot i\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
12. Simplified28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)}\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
13. Using strategy rm
14. Applied sub-neg28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \color{blue}{\left(a \cdot y5 + \left(-c \cdot y4\right)\right)}\right)\right)\right)\right)\]
15. Applied distribute-lft-in28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \color{blue}{\left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-c \cdot y4\right)\right)}\right)\right)\right)\right)\]
16. Simplified28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(\color{blue}{y5 \cdot \left(a \cdot \left(t \cdot y2 - y \cdot y3\right)\right)} + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-c \cdot y4\right)\right)\right)\right)\right)\right)\]
17. Simplified28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y5 \cdot \left(a \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \color{blue}{\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot \left(-c\right)\right)}\right)\right)\right)\right)\right)\]
if -5.3523773993212786e-121 < k < 1.474229454418703e-186 or 5.8370955327107604e-120 < k < 8.37503708775726056e37
1. Initial program 26.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)\]
2. Simplified26.1
  \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg26.1
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \color{blue}{\left(i \cdot y1 + \left(-b \cdot y0\right)\right)} + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
5. Applied distribute-lft-in26.1
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\color{blue}{\left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-b \cdot y0\right)\right)} + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
6. Simplified25.8
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(\color{blue}{i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right)} + \left(x \cdot j - z \cdot k\right) \cdot \left(-b \cdot y0\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
7. Simplified25.5
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right) + \color{blue}{b \cdot \left(\left(-y0\right) \cdot \left(j \cdot x - k \cdot z\right)\right)}\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
if 1.474229454418703e-186 < k < 2.50442636569255858e-159
1. Initial program 28.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)\]
2. Simplified28.7
  \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{blue}{\left(c \cdot y0 + \left(-a \cdot y1\right)\right)} + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
5. Applied distribute-lft-in28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right)} + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
6. Simplified28.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(\color{blue}{c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)} + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
7. Simplified29.0
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \color{blue}{a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)}\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
8. Using strategy rm
9. Applied sub-neg29.0
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \color{blue}{\left(a \cdot b + \left(-c \cdot i\right)\right)} + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
10. Applied distribute-lft-in29.0
  \[\leadsto \color{blue}{\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b\right) + \left(x \cdot y - z \cdot t\right) \cdot \left(-c \cdot i\right)\right)} + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
11. Simplified29.0
  \[\leadsto \left(\color{blue}{b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right)} + \left(x \cdot y - z \cdot t\right) \cdot \left(-c \cdot i\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
12. Simplified29.3
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)}\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
13. Using strategy rm
14. Applied sub-neg29.3
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \color{blue}{\left(i \cdot y1 + \left(-b \cdot y0\right)\right)} + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
15. Applied distribute-lft-in29.3
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\color{blue}{\left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-b \cdot y0\right)\right)} + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
16. Simplified29.5
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(\color{blue}{i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right)} + \left(x \cdot j - z \cdot k\right) \cdot \left(-b \cdot y0\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
17. Simplified28.0
  \[\leadsto \left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right) + \color{blue}{b \cdot \left(\left(-y0\right) \cdot \left(j \cdot x - k \cdot z\right)\right)}\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
18. Using strategy rm
19. Applied add-cube-cbrt28.1
  \[\leadsto \left(\color{blue}{\left(\left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \sqrt[3]{b}\right)} \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right) + b \cdot \left(\left(-y0\right) \cdot \left(j \cdot x - k \cdot z\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
20. Applied associate-*l*28.1
  \[\leadsto \left(\color{blue}{\left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \left(\sqrt[3]{b} \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right)\right)} + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right) + b \cdot \left(\left(-y0\right) \cdot \left(j \cdot x - k \cdot z\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
21. Simplified27.8
  \[\leadsto \left(\left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \color{blue}{\left(a \cdot \left(\left(y \cdot x - t \cdot z\right) \cdot \sqrt[3]{b}\right)\right)} + c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)\right) + \left(\left(i \cdot \left(y1 \cdot \left(j \cdot x - k \cdot z\right)\right) + b \cdot \left(\left(-y0\right) \cdot \left(j \cdot x - k \cdot z\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + a \cdot \left(\left(-y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
if 2.50442636569255858e-159 < k < 5.8370955327107604e-120
1. Initial program 23.3
  \[\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)\]
2. Simplified23.3
  \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)}\]
3. Taylor expanded around inf 27.7
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \color{blue}{\left(y4 \cdot \left(y3 \cdot \left(y \cdot c\right)\right) - \left(t \cdot \left(y2 \cdot \left(y4 \cdot c\right)\right) + a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right)\right)\right)}\right)\right)\right)\right)\]
4. Simplified27.9
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \color{blue}{\left(y4 \cdot \left(y \cdot \left(y3 \cdot c\right)\right) - \left(t \cdot \left(y4 \cdot \left(c \cdot y2\right)\right) + y3 \cdot \left(\left(y \cdot y5\right) \cdot a\right)\right)\right)}\right)\right)\right)\right)\]
if 8.37503708775726056e37 < k
1. Initial program 28.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)\]
2. Simplified28.8
  \[\leadsto \color{blue}{\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)}\]
3. Taylor expanded around inf 28.2
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\color{blue}{\left(k \cdot \left(i \cdot \left(y \cdot y5\right)\right) - \left(t \cdot \left(i \cdot \left(j \cdot y5\right)\right) + k \cdot \left(y \cdot \left(y4 \cdot b\right)\right)\right)\right)} + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
4. Simplified28.9
  \[\leadsto \left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\color{blue}{\left(k \cdot \left(y \cdot \left(i \cdot y5\right)\right) - \left(t \cdot \left(j \cdot \left(i \cdot y5\right)\right) + y \cdot \left(k \cdot \left(b \cdot y4\right)\right)\right)\right)} + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\]
Recombined 5 regimes into one program.
Final simplification26.9
\[\leadsto \begin{array}{l} \mathbf{if}\;k \leq -5.352377399321279 \cdot 10^{-121}:\\ \;\;\;\;\left(b \cdot \left(a \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right)\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y5 \cdot \left(a \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(c \cdot y4\right) \cdot \left(y \cdot y3 - t \cdot y2\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 1.4742294544187031 \cdot 10^{-186}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 2.5044263656925586 \cdot 10^{-159}:\\ \;\;\;\;\left(c \cdot \left(i \cdot \left(t \cdot z - y \cdot x\right)\right) + \left(\sqrt[3]{b} \cdot \sqrt[3]{b}\right) \cdot \left(a \cdot \left(\left(y \cdot x - t \cdot z\right) \cdot \sqrt[3]{b}\right)\right)\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(c \cdot \left(y0 \cdot \left(x \cdot y2 - z \cdot y3\right)\right) + a \cdot \left(y1 \cdot \left(z \cdot y3 - x \cdot y2\right)\right)\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 5.8370955327107604 \cdot 10^{-120}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right) - \left(t \cdot \left(y4 \cdot \left(c \cdot y2\right)\right) + y3 \cdot \left(a \cdot \left(y \cdot y5\right)\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;k \leq 8.375037087757261 \cdot 10^{+37}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(i \cdot \left(\left(x \cdot j - k \cdot z\right) \cdot y1\right) + b \cdot \left(y0 \cdot \left(k \cdot z - x \cdot j\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y \cdot x - t \cdot z\right) \cdot \left(b \cdot a - c \cdot i\right) + \left(\left(x \cdot j - k \cdot z\right) \cdot \left(i \cdot y1 - b \cdot y0\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y0 \cdot y5\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(a \cdot y5 - c \cdot y4\right)\right) + \left(k \cdot \left(y \cdot \left(i \cdot y5\right)\right) - \left(t \cdot \left(j \cdot \left(i \cdot y5\right)\right) + y \cdot \left(k \cdot \left(b \cdot y4\right)\right)\right)\right)\right)\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if k < -5.3523773993212786e-121`

`if -5.3523773993212786e-121 < k < 1.474229454418703e-186 or 5.8370955327107604e-120 < k < 8.37503708775726056e37`

`if 1.474229454418703e-186 < k < 2.50442636569255858e-159`

`if 2.50442636569255858e-159 < k < 5.8370955327107604e-120`

`if 8.37503708775726056e37 < k`

Reproduce

In
Out