Average Error: 27.3 → 30.0
Time: 1.5m
Precision: 64
\[\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}\;y0 \le -1.667790877689636481505521901403068103115 \cdot 10^{90}:\\ \;\;\;\;\left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.198705992458895702428916734917044414201 \cdot 10^{-162}:\\ \;\;\;\;\left(\left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(\left(i \cdot z\right) \cdot y1\right) \cdot k - y1 \cdot \left(\left(i \cdot j\right) \cdot x\right)\right) - \left(\left(z \cdot k\right) \cdot b\right) \cdot y0\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.869614940909926097226067307549077145402 \cdot 10^{-227}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{elif}\;y0 \le 3.486128712704299101676819382240846478502 \cdot 10^{-82}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(z \cdot y1\right) \cdot y3 - \left(y1 \cdot y2\right) \cdot x\right) \cdot a - \left(c \cdot z\right) \cdot \left(y0 \cdot y3\right)\right) + \left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\\ \mathbf{elif}\;y0 \le 5.69000333338126936863636307941908438558 \cdot 10^{54}:\\ \;\;\;\;\left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(y0 \cdot b - i \cdot y1\right) \cdot x\right) \cdot j + \left(z \cdot \left(-\left(y0 \cdot b - i \cdot y1\right)\right)\right) \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le 6.576128619084347295996967330841980145855 \cdot 10^{77}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - 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(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\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}\;y0 \le -1.667790877689636481505521901403068103115 \cdot 10^{90}:\\
\;\;\;\;\left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\

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

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

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

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

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

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

\end{array}
double f(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 r149231 = x;
        double r149232 = y;
        double r149233 = r149231 * r149232;
        double r149234 = z;
        double r149235 = t;
        double r149236 = r149234 * r149235;
        double r149237 = r149233 - r149236;
        double r149238 = a;
        double r149239 = b;
        double r149240 = r149238 * r149239;
        double r149241 = c;
        double r149242 = i;
        double r149243 = r149241 * r149242;
        double r149244 = r149240 - r149243;
        double r149245 = r149237 * r149244;
        double r149246 = j;
        double r149247 = r149231 * r149246;
        double r149248 = k;
        double r149249 = r149234 * r149248;
        double r149250 = r149247 - r149249;
        double r149251 = y0;
        double r149252 = r149251 * r149239;
        double r149253 = y1;
        double r149254 = r149253 * r149242;
        double r149255 = r149252 - r149254;
        double r149256 = r149250 * r149255;
        double r149257 = r149245 - r149256;
        double r149258 = y2;
        double r149259 = r149231 * r149258;
        double r149260 = y3;
        double r149261 = r149234 * r149260;
        double r149262 = r149259 - r149261;
        double r149263 = r149251 * r149241;
        double r149264 = r149253 * r149238;
        double r149265 = r149263 - r149264;
        double r149266 = r149262 * r149265;
        double r149267 = r149257 + r149266;
        double r149268 = r149235 * r149246;
        double r149269 = r149232 * r149248;
        double r149270 = r149268 - r149269;
        double r149271 = y4;
        double r149272 = r149271 * r149239;
        double r149273 = y5;
        double r149274 = r149273 * r149242;
        double r149275 = r149272 - r149274;
        double r149276 = r149270 * r149275;
        double r149277 = r149267 + r149276;
        double r149278 = r149235 * r149258;
        double r149279 = r149232 * r149260;
        double r149280 = r149278 - r149279;
        double r149281 = r149271 * r149241;
        double r149282 = r149273 * r149238;
        double r149283 = r149281 - r149282;
        double r149284 = r149280 * r149283;
        double r149285 = r149277 - r149284;
        double r149286 = r149248 * r149258;
        double r149287 = r149246 * r149260;
        double r149288 = r149286 - r149287;
        double r149289 = r149271 * r149253;
        double r149290 = r149273 * r149251;
        double r149291 = r149289 - r149290;
        double r149292 = r149288 * r149291;
        double r149293 = r149285 + r149292;
        return r149293;
}

double f(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 r149294 = y0;
        double r149295 = -1.6677908776896365e+90;
        bool r149296 = r149294 <= r149295;
        double r149297 = a;
        double r149298 = b;
        double r149299 = r149297 * r149298;
        double r149300 = i;
        double r149301 = c;
        double r149302 = r149300 * r149301;
        double r149303 = r149299 - r149302;
        double r149304 = y;
        double r149305 = x;
        double r149306 = r149304 * r149305;
        double r149307 = t;
        double r149308 = z;
        double r149309 = r149307 * r149308;
        double r149310 = r149306 - r149309;
        double r149311 = r149303 * r149310;
        double r149312 = r149294 * r149298;
        double r149313 = y1;
        double r149314 = r149300 * r149313;
        double r149315 = r149312 - r149314;
        double r149316 = j;
        double r149317 = r149316 * r149305;
        double r149318 = k;
        double r149319 = r149308 * r149318;
        double r149320 = r149317 - r149319;
        double r149321 = r149315 * r149320;
        double r149322 = r149311 - r149321;
        double r149323 = r149301 * r149294;
        double r149324 = r149313 * r149297;
        double r149325 = r149323 - r149324;
        double r149326 = y2;
        double r149327 = r149305 * r149326;
        double r149328 = y3;
        double r149329 = r149328 * r149308;
        double r149330 = r149327 - r149329;
        double r149331 = r149325 * r149330;
        double r149332 = r149322 + r149331;
        double r149333 = r149307 * r149316;
        double r149334 = r149304 * r149318;
        double r149335 = r149333 - r149334;
        double r149336 = y4;
        double r149337 = r149298 * r149336;
        double r149338 = y5;
        double r149339 = r149300 * r149338;
        double r149340 = r149337 - r149339;
        double r149341 = r149335 * r149340;
        double r149342 = r149301 * r149336;
        double r149343 = r149338 * r149297;
        double r149344 = r149342 - r149343;
        double r149345 = r149307 * r149326;
        double r149346 = r149328 * r149304;
        double r149347 = r149345 - r149346;
        double r149348 = r149344 * r149347;
        double r149349 = r149341 - r149348;
        double r149350 = r149332 + r149349;
        double r149351 = -1.1987059924588957e-162;
        bool r149352 = r149294 <= r149351;
        double r149353 = r149313 * r149336;
        double r149354 = r149338 * r149294;
        double r149355 = r149353 - r149354;
        double r149356 = r149355 * r149318;
        double r149357 = r149326 * r149356;
        double r149358 = r149316 * r149328;
        double r149359 = -r149358;
        double r149360 = r149359 * r149355;
        double r149361 = r149357 + r149360;
        double r149362 = r149361 + r149331;
        double r149363 = r149300 * r149308;
        double r149364 = r149363 * r149313;
        double r149365 = r149364 * r149318;
        double r149366 = r149300 * r149316;
        double r149367 = r149366 * r149305;
        double r149368 = r149313 * r149367;
        double r149369 = r149365 - r149368;
        double r149370 = r149319 * r149298;
        double r149371 = r149370 * r149294;
        double r149372 = r149369 - r149371;
        double r149373 = r149311 - r149372;
        double r149374 = r149362 + r149373;
        double r149375 = r149374 + r149349;
        double r149376 = -1.869614940909926e-227;
        bool r149377 = r149294 <= r149376;
        double r149378 = r149311 + r149362;
        double r149379 = r149349 + r149378;
        double r149380 = 3.486128712704299e-82;
        bool r149381 = r149294 <= r149380;
        double r149382 = r149308 * r149313;
        double r149383 = r149382 * r149328;
        double r149384 = r149313 * r149326;
        double r149385 = r149384 * r149305;
        double r149386 = r149383 - r149385;
        double r149387 = r149386 * r149297;
        double r149388 = r149301 * r149308;
        double r149389 = r149294 * r149328;
        double r149390 = r149388 * r149389;
        double r149391 = r149387 - r149390;
        double r149392 = r149391 + r149361;
        double r149393 = r149392 + r149322;
        double r149394 = r149349 + r149393;
        double r149395 = 5.6900033333812694e+54;
        bool r149396 = r149294 <= r149395;
        double r149397 = r149326 * r149318;
        double r149398 = r149397 - r149358;
        double r149399 = r149355 * r149398;
        double r149400 = r149399 + r149331;
        double r149401 = r149315 * r149305;
        double r149402 = r149401 * r149316;
        double r149403 = -r149315;
        double r149404 = r149308 * r149403;
        double r149405 = r149404 * r149318;
        double r149406 = r149402 + r149405;
        double r149407 = r149311 - r149406;
        double r149408 = r149400 + r149407;
        double r149409 = r149408 + r149349;
        double r149410 = 6.576128619084347e+77;
        bool r149411 = r149294 <= r149410;
        double r149412 = -r149321;
        double r149413 = r149412 + r149362;
        double r149414 = r149413 + r149349;
        double r149415 = r149411 ? r149379 : r149414;
        double r149416 = r149396 ? r149409 : r149415;
        double r149417 = r149381 ? r149394 : r149416;
        double r149418 = r149377 ? r149379 : r149417;
        double r149419 = r149352 ? r149375 : r149418;
        double r149420 = r149296 ? r149350 : r149419;
        return r149420;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Bits error versus c

Bits error versus i

Bits error versus j

Bits error versus k

Bits error versus y0

Bits error versus y1

Bits error versus y2

Bits error versus y3

Bits error versus y4

Bits error versus y5

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 6 regimes
  2. if y0 < -1.6677908776896365e+90

    1. Initial program 32.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. Simplified32.5

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Taylor expanded around 0 38.2

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{0} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    if -1.6677908776896365e+90 < y0 < -1.1987059924588957e-162

    1. Initial program 26.4

      \[\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.4

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Using strategy rm
    4. Applied sub-neg26.4

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    5. Applied distribute-lft-in26.4

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    6. Simplified27.1

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    7. Simplified27.1

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Taylor expanded around inf 28.9

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(i \cdot \left(z \cdot \left(y1 \cdot k\right)\right) - \left(x \cdot \left(y1 \cdot \left(j \cdot i\right)\right) + y0 \cdot \left(z \cdot \left(b \cdot k\right)\right)\right)\right)}\right)\right)\]
    9. Simplified29.6

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(\left(\left(i \cdot z\right) \cdot y1\right) \cdot k - \left(x \cdot \left(i \cdot j\right)\right) \cdot y1\right) - y0 \cdot \left(\left(k \cdot z\right) \cdot b\right)\right)}\right)\right)\]

    if -1.1987059924588957e-162 < y0 < -1.869614940909926e-227 or 5.6900033333812694e+54 < y0 < 6.576128619084347e+77

    1. Initial program 23.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. Simplified23.7

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Using strategy rm
    4. Applied sub-neg23.7

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    5. Applied distribute-lft-in23.7

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    6. Simplified23.9

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    7. Simplified23.9

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Taylor expanded around 0 28.7

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{0}\right)\right)\]

    if -1.869614940909926e-227 < y0 < 3.486128712704299e-82

    1. Initial program 26.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. Simplified26.7

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Using strategy rm
    4. Applied sub-neg26.7

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    5. Applied distribute-lft-in26.7

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    6. Simplified26.4

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    7. Simplified26.4

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Taylor expanded around inf 27.1

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right) + c \cdot \left(z \cdot \left(y3 \cdot y0\right)\right)\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    9. Simplified28.2

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(a \cdot \left(\left(y1 \cdot z\right) \cdot y3 - x \cdot \left(y2 \cdot y1\right)\right) - \left(z \cdot c\right) \cdot \left(y0 \cdot y3\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    if 3.486128712704299e-82 < y0 < 5.6900033333812694e+54

    1. Initial program 24.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. Simplified24.3

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Using strategy rm
    4. Applied sub-neg24.3

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
    5. Applied distribute-lft-in24.3

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
    6. Simplified25.0

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{j \cdot \left(x \cdot \left(y0 \cdot b - y1 \cdot i\right)\right)} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
    7. Simplified25.3

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(j \cdot \left(x \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \color{blue}{\left(\left(y0 \cdot b - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]

    if 6.576128619084347e+77 < y0

    1. Initial program 31.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. Simplified31.5

      \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
    3. Using strategy rm
    4. Applied sub-neg31.5

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    5. Applied distribute-lft-in31.5

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    6. Simplified33.3

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    7. Simplified33.3

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Taylor expanded around 0 34.5

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\color{blue}{0} - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
  3. Recombined 6 regimes into one program.
  4. Final simplification30.0

    \[\leadsto \begin{array}{l} \mathbf{if}\;y0 \le -1.667790877689636481505521901403068103115 \cdot 10^{90}:\\ \;\;\;\;\left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.198705992458895702428916734917044414201 \cdot 10^{-162}:\\ \;\;\;\;\left(\left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(\left(i \cdot z\right) \cdot y1\right) \cdot k - y1 \cdot \left(\left(i \cdot j\right) \cdot x\right)\right) - \left(\left(z \cdot k\right) \cdot b\right) \cdot y0\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.869614940909926097226067307549077145402 \cdot 10^{-227}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{elif}\;y0 \le 3.486128712704299101676819382240846478502 \cdot 10^{-82}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(z \cdot y1\right) \cdot y3 - \left(y1 \cdot y2\right) \cdot x\right) \cdot a - \left(c \cdot z\right) \cdot \left(y0 \cdot y3\right)\right) + \left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\\ \mathbf{elif}\;y0 \le 5.69000333338126936863636307941908438558 \cdot 10^{54}:\\ \;\;\;\;\left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(y0 \cdot b - i \cdot y1\right) \cdot x\right) \cdot j + \left(z \cdot \left(-\left(y0 \cdot b - i \cdot y1\right)\right)\right) \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le 6.576128619084347295996967330841980145855 \cdot 10^{77}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - 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(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019194 
(FPCore (x y z t a b c i j k y0 y1 y2 y3 y4 y5)
  :name "Linear.Matrix:det44 from linear-1.19.1.3"
  (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* 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)))))