Average Error: 26.6 → 29.8
Time: 1.1m
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}\;z \le -251600015590119898115307732992:\\ \;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-y1 \cdot i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right) - \left(y \cdot \left(y3 \cdot \left(y4 \cdot c\right)\right) + y5 \cdot \left(a \cdot \left(y2 \cdot t\right)\right)\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\ \mathbf{elif}\;z \le -2.972075418643144100874855017812060946209 \cdot 10^{-160}:\\ \;\;\;\;\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right) + \left(\left(-\left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b\right)\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(y1 \cdot i\right)\right)\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{elif}\;z \le -2.141578408042879697648173343065601427509 \cdot 10^{-273}:\\ \;\;\;\;\left(\left(\left(\left(\left(t \cdot \left(i \cdot \left(z \cdot c\right)\right) - \left(i \cdot \left(c \cdot \left(y \cdot x\right)\right) + a \cdot \left(t \cdot \left(z \cdot b\right)\right)\right)\right) - \left(\left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\ \mathbf{elif}\;z \le 2.695518215972674621510239531516560755776 \cdot 10^{-155}:\\ \;\;\;\;\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\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(y0 \cdot b\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-y1 \cdot i\right)\right)\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{elif}\;z \le 2.490460573128301389101354442913924902921 \cdot 10^{-117}:\\ \;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(y0 \cdot \left(z \cdot \left(y3 \cdot c\right)\right) + a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right)\right)\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)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\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}\;z \le -251600015590119898115307732992:\\
\;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-y1 \cdot i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right) - \left(y \cdot \left(y3 \cdot \left(y4 \cdot c\right)\right) + y5 \cdot \left(a \cdot \left(y2 \cdot t\right)\right)\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\

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

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

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

\mathbf{elif}\;z \le 2.490460573128301389101354442913924902921 \cdot 10^{-117}:\\
\;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(y0 \cdot \left(z \cdot \left(y3 \cdot c\right)\right) + a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right)\right)\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)\\

\mathbf{else}:\\
\;\;\;\;\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\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 r153199 = x;
        double r153200 = y;
        double r153201 = r153199 * r153200;
        double r153202 = z;
        double r153203 = t;
        double r153204 = r153202 * r153203;
        double r153205 = r153201 - r153204;
        double r153206 = a;
        double r153207 = b;
        double r153208 = r153206 * r153207;
        double r153209 = c;
        double r153210 = i;
        double r153211 = r153209 * r153210;
        double r153212 = r153208 - r153211;
        double r153213 = r153205 * r153212;
        double r153214 = j;
        double r153215 = r153199 * r153214;
        double r153216 = k;
        double r153217 = r153202 * r153216;
        double r153218 = r153215 - r153217;
        double r153219 = y0;
        double r153220 = r153219 * r153207;
        double r153221 = y1;
        double r153222 = r153221 * r153210;
        double r153223 = r153220 - r153222;
        double r153224 = r153218 * r153223;
        double r153225 = r153213 - r153224;
        double r153226 = y2;
        double r153227 = r153199 * r153226;
        double r153228 = y3;
        double r153229 = r153202 * r153228;
        double r153230 = r153227 - r153229;
        double r153231 = r153219 * r153209;
        double r153232 = r153221 * r153206;
        double r153233 = r153231 - r153232;
        double r153234 = r153230 * r153233;
        double r153235 = r153225 + r153234;
        double r153236 = r153203 * r153214;
        double r153237 = r153200 * r153216;
        double r153238 = r153236 - r153237;
        double r153239 = y4;
        double r153240 = r153239 * r153207;
        double r153241 = y5;
        double r153242 = r153241 * r153210;
        double r153243 = r153240 - r153242;
        double r153244 = r153238 * r153243;
        double r153245 = r153235 + r153244;
        double r153246 = r153203 * r153226;
        double r153247 = r153200 * r153228;
        double r153248 = r153246 - r153247;
        double r153249 = r153239 * r153209;
        double r153250 = r153241 * r153206;
        double r153251 = r153249 - r153250;
        double r153252 = r153248 * r153251;
        double r153253 = r153245 - r153252;
        double r153254 = r153216 * r153226;
        double r153255 = r153214 * r153228;
        double r153256 = r153254 - r153255;
        double r153257 = r153239 * r153221;
        double r153258 = r153241 * r153219;
        double r153259 = r153257 - r153258;
        double r153260 = r153256 * r153259;
        double r153261 = r153253 + r153260;
        return r153261;
}
↓
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 r153262 = z;
        double r153263 = -2.516000155901199e+29;
        bool r153264 = r153262 <= r153263;
        double r153265 = x;
        double r153266 = y;
        double r153267 = r153265 * r153266;
        double r153268 = t;
        double r153269 = r153262 * r153268;
        double r153270 = r153267 - r153269;
        double r153271 = a;
        double r153272 = b;
        double r153273 = r153271 * r153272;
        double r153274 = c;
        double r153275 = i;
        double r153276 = r153274 * r153275;
        double r153277 = r153273 - r153276;
        double r153278 = r153270 * r153277;
        double r153279 = j;
        double r153280 = r153265 * r153279;
        double r153281 = k;
        double r153282 = r153262 * r153281;
        double r153283 = r153280 - r153282;
        double r153284 = y0;
        double r153285 = r153284 * r153272;
        double r153286 = r153283 * r153285;
        double r153287 = y1;
        double r153288 = r153287 * r153275;
        double r153289 = -r153288;
        double r153290 = r153283 * r153289;
        double r153291 = r153286 + r153290;
        double r153292 = r153278 - r153291;
        double r153293 = y2;
        double r153294 = r153265 * r153293;
        double r153295 = y3;
        double r153296 = r153262 * r153295;
        double r153297 = r153294 - r153296;
        double r153298 = r153284 * r153274;
        double r153299 = r153287 * r153271;
        double r153300 = r153298 - r153299;
        double r153301 = r153297 * r153300;
        double r153302 = r153292 + r153301;
        double r153303 = r153268 * r153279;
        double r153304 = r153266 * r153281;
        double r153305 = r153303 - r153304;
        double r153306 = y4;
        double r153307 = r153306 * r153272;
        double r153308 = y5;
        double r153309 = r153308 * r153275;
        double r153310 = r153307 - r153309;
        double r153311 = r153305 * r153310;
        double r153312 = r153302 + r153311;
        double r153313 = r153266 * r153308;
        double r153314 = r153295 * r153313;
        double r153315 = r153271 * r153314;
        double r153316 = r153306 * r153274;
        double r153317 = r153295 * r153316;
        double r153318 = r153266 * r153317;
        double r153319 = r153293 * r153268;
        double r153320 = r153271 * r153319;
        double r153321 = r153308 * r153320;
        double r153322 = r153318 + r153321;
        double r153323 = r153315 - r153322;
        double r153324 = r153312 - r153323;
        double r153325 = r153281 * r153293;
        double r153326 = r153279 * r153295;
        double r153327 = r153325 - r153326;
        double r153328 = r153306 * r153287;
        double r153329 = r153308 * r153284;
        double r153330 = r153328 - r153329;
        double r153331 = r153327 * r153330;
        double r153332 = r153324 + r153331;
        double r153333 = -2.972075418643144e-160;
        bool r153334 = r153262 <= r153333;
        double r153335 = -r153286;
        double r153336 = r153283 * r153288;
        double r153337 = r153335 + r153336;
        double r153338 = r153301 + r153337;
        double r153339 = r153311 + r153338;
        double r153340 = r153268 * r153293;
        double r153341 = r153266 * r153295;
        double r153342 = r153340 - r153341;
        double r153343 = r153308 * r153271;
        double r153344 = r153316 - r153343;
        double r153345 = r153342 * r153344;
        double r153346 = r153339 - r153345;
        double r153347 = r153331 + r153346;
        double r153348 = -2.1415784080428797e-273;
        bool r153349 = r153262 <= r153348;
        double r153350 = r153262 * r153274;
        double r153351 = r153275 * r153350;
        double r153352 = r153268 * r153351;
        double r153353 = r153266 * r153265;
        double r153354 = r153274 * r153353;
        double r153355 = r153275 * r153354;
        double r153356 = r153262 * r153272;
        double r153357 = r153268 * r153356;
        double r153358 = r153271 * r153357;
        double r153359 = r153355 + r153358;
        double r153360 = r153352 - r153359;
        double r153361 = r153283 * r153287;
        double r153362 = -r153275;
        double r153363 = r153361 * r153362;
        double r153364 = r153286 + r153363;
        double r153365 = r153360 - r153364;
        double r153366 = r153365 + r153301;
        double r153367 = r153366 + r153311;
        double r153368 = r153367 - r153345;
        double r153369 = r153368 + r153331;
        double r153370 = 2.6955182159726746e-155;
        bool r153371 = r153262 <= r153370;
        double r153372 = r153311 + r153292;
        double r153373 = r153372 - r153345;
        double r153374 = r153331 + r153373;
        double r153375 = 2.4904605731283014e-117;
        bool r153376 = r153262 <= r153375;
        double r153377 = r153278 - r153364;
        double r153378 = r153287 * r153262;
        double r153379 = r153295 * r153378;
        double r153380 = r153271 * r153379;
        double r153381 = r153295 * r153274;
        double r153382 = r153262 * r153381;
        double r153383 = r153284 * r153382;
        double r153384 = r153293 * r153287;
        double r153385 = r153265 * r153384;
        double r153386 = r153271 * r153385;
        double r153387 = r153383 + r153386;
        double r153388 = r153380 - r153387;
        double r153389 = r153377 + r153388;
        double r153390 = r153389 + r153311;
        double r153391 = r153390 - r153345;
        double r153392 = r153391 + r153331;
        double r153393 = r153377 + r153301;
        double r153394 = r153393 + r153311;
        double r153395 = r153394 + r153331;
        double r153396 = r153376 ? r153392 : r153395;
        double r153397 = r153371 ? r153374 : r153396;
        double r153398 = r153349 ? r153369 : r153397;
        double r153399 = r153334 ? r153347 : r153398;
        double r153400 = r153264 ? r153332 : r153399;
        return r153400;
}

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 z < -2.516000155901199e+29

    1. Initial program 29.6

      \[\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. Using strategy rm

    3. Applied sub-neg29.6

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

    4. Applied distribute-lft-in29.6

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

    5. Taylor expanded around inf 31.7

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

    if -2.516000155901199e+29 < z < -2.972075418643144e-160

    1. Initial program 23.0

      \[\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. Using strategy rm

    3. Applied sub-neg23.0

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

    4. Applied distribute-lft-in23.0

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

    5. Taylor expanded around 0 28.3

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

    if -2.972075418643144e-160 < z < -2.1415784080428797e-273

    1. Initial program 27.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. Using strategy rm

    3. Applied sub-neg27.7

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

    4. Applied distribute-lft-in27.7

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

    6. Applied distribute-rgt-neg-in27.7

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

    7. Applied associate-*r*27.3

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

    8. Taylor expanded around inf 27.2

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

    if -2.1415784080428797e-273 < z < 2.6955182159726746e-155

    1. Initial program 27.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. Using strategy rm

    3. Applied sub-neg27.8

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

    4. Applied distribute-lft-in27.8

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

    5. Taylor expanded around 0 30.0

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

    if 2.6955182159726746e-155 < z < 2.4904605731283014e-117

    1. Initial program 22.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. Using strategy rm

    3. Applied sub-neg22.8

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

    4. Applied distribute-lft-in22.8

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

    6. Applied distribute-rgt-neg-in22.8

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

    7. Applied associate-*r*21.6

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

    8. Taylor expanded around inf 23.4

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

    if 2.4904605731283014e-117 < z

    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. Using strategy rm

    3. Applied sub-neg26.4

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

    4. Applied distribute-lft-in26.4

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

    6. Applied distribute-rgt-neg-in26.4

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

    7. Applied associate-*r*27.4

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

    8. Taylor expanded around 0 31.4

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

  4. Final simplification29.8

    \[\leadsto \begin{array}{l} \mathbf{if}\;z \le -251600015590119898115307732992:\\ \;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-y1 \cdot i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right) - \left(y \cdot \left(y3 \cdot \left(y4 \cdot c\right)\right) + y5 \cdot \left(a \cdot \left(y2 \cdot t\right)\right)\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\ \mathbf{elif}\;z \le -2.972075418643144100874855017812060946209 \cdot 10^{-160}:\\ \;\;\;\;\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right) + \left(\left(-\left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b\right)\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(y1 \cdot i\right)\right)\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{elif}\;z \le -2.141578408042879697648173343065601427509 \cdot 10^{-273}:\\ \;\;\;\;\left(\left(\left(\left(\left(t \cdot \left(i \cdot \left(z \cdot c\right)\right) - \left(i \cdot \left(c \cdot \left(y \cdot x\right)\right) + a \cdot \left(t \cdot \left(z \cdot b\right)\right)\right)\right) - \left(\left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\ \mathbf{elif}\;z \le 2.695518215972674621510239531516560755776 \cdot 10^{-155}:\\ \;\;\;\;\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\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(y0 \cdot b\right) + \left(x \cdot j - z \cdot k\right) \cdot \left(-y1 \cdot i\right)\right)\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{elif}\;z \le 2.490460573128301389101354442913924902921 \cdot 10^{-117}:\\ \;\;\;\;\left(\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(y0 \cdot \left(z \cdot \left(y3 \cdot c\right)\right) + a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right)\right)\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)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\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(y0 \cdot b\right) + \left(\left(x \cdot j - z \cdot k\right) \cdot y1\right) \cdot \left(-i\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019347 
(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"
  :precision binary64
  (+ (- (+ (+ (- (* (- (* 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)))))