Linear.Matrix:det44 from linear-1.19.1.3

Average Error: 27.0 → 30.1

Time: 1.6m

Precision: 64

Math

\[\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}\;y4 \le -617175255753787705220435928565733478367200:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(i \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot \left(-c\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot a\right) \cdot b\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \mathbf{elif}\;y4 \le -2.176428204282215683286541428526422284872 \cdot 10^{-125}:\\ \;\;\;\;\left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right) + \left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\\ \mathbf{elif}\;y4 \le -2.567061354010687248637387810560011604782 \cdot 10^{-254}:\\ \;\;\;\;\left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right) + \left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right)\\ \mathbf{elif}\;y4 \le 7.742023117024128236838563930215200024067 \cdot 10^{-208}:\\ \;\;\;\;\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right) + \left(\left(\left(y5 \cdot \left(\left(-i\right) \cdot \mathsf{fma}\left(t, j, y \cdot \left(-k\right)\right)\right) + \mathsf{fma}\left(t, j, y \cdot \left(-k\right)\right) \cdot \left(b \cdot y4\right)\right) + \left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\\ \mathbf{elif}\;y4 \le 1.687477064286342108432003547396676662615 \cdot 10^{-164}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(i \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot \left(-c\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot a\right) \cdot b\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \mathbf{elif}\;y4 \le 7.586217188176184986289740850066189488425 \cdot 10^{-103}:\\ \;\;\;\;\left(\left(\left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le 1146684347183370447338978607628288:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(-\left(j \cdot x - z \cdot k\right)\right) \cdot \left(b \cdot y0 - y1 \cdot i\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le 5.0685232286476560290775075501477904359 \cdot 10^{142}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \mathsf{fma}\left(y0 \cdot \left(j \cdot y5\right), y3, -\mathsf{fma}\left(y2 \cdot \left(y0 \cdot y5\right), k, y1 \cdot \left(\left(y3 \cdot j\right) \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y5 \cdot \left(-\left(y2 \cdot t - y \cdot y3\right) \cdot a\right) + \left(y4 \cdot c\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \end{array}\]

C

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 r182452 = x;
        double r182453 = y;
        double r182454 = r182452 * r182453;
        double r182455 = z;
        double r182456 = t;
        double r182457 = r182455 * r182456;
        double r182458 = r182454 - r182457;
        double r182459 = a;
        double r182460 = b;
        double r182461 = r182459 * r182460;
        double r182462 = c;
        double r182463 = i;
        double r182464 = r182462 * r182463;
        double r182465 = r182461 - r182464;
        double r182466 = r182458 * r182465;
        double r182467 = j;
        double r182468 = r182452 * r182467;
        double r182469 = k;
        double r182470 = r182455 * r182469;
        double r182471 = r182468 - r182470;
        double r182472 = y0;
        double r182473 = r182472 * r182460;
        double r182474 = y1;
        double r182475 = r182474 * r182463;
        double r182476 = r182473 - r182475;
        double r182477 = r182471 * r182476;
        double r182478 = r182466 - r182477;
        double r182479 = y2;
        double r182480 = r182452 * r182479;
        double r182481 = y3;
        double r182482 = r182455 * r182481;
        double r182483 = r182480 - r182482;
        double r182484 = r182472 * r182462;
        double r182485 = r182474 * r182459;
        double r182486 = r182484 - r182485;
        double r182487 = r182483 * r182486;
        double r182488 = r182478 + r182487;
        double r182489 = r182456 * r182467;
        double r182490 = r182453 * r182469;
        double r182491 = r182489 - r182490;
        double r182492 = y4;
        double r182493 = r182492 * r182460;
        double r182494 = y5;
        double r182495 = r182494 * r182463;
        double r182496 = r182493 - r182495;
        double r182497 = r182491 * r182496;
        double r182498 = r182488 + r182497;
        double r182499 = r182456 * r182479;
        double r182500 = r182453 * r182481;
        double r182501 = r182499 - r182500;
        double r182502 = r182492 * r182462;
        double r182503 = r182494 * r182459;
        double r182504 = r182502 - r182503;
        double r182505 = r182501 * r182504;
        double r182506 = r182498 - r182505;
        double r182507 = r182469 * r182479;
        double r182508 = r182467 * r182481;
        double r182509 = r182507 - r182508;
        double r182510 = r182492 * r182474;
        double r182511 = r182494 * r182472;
        double r182512 = r182510 - r182511;
        double r182513 = r182509 * r182512;
        double r182514 = r182506 + r182513;
        return r182514;
}

↓

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 r182515 = y4;
        double r182516 = -6.171752557537877e+41;
        bool r182517 = r182515 <= r182516;
        double r182518 = i;
        double r182519 = x;
        double r182520 = y;
        double r182521 = r182519 * r182520;
        double r182522 = t;
        double r182523 = z;
        double r182524 = r182522 * r182523;
        double r182525 = r182521 - r182524;
        double r182526 = r182518 * r182525;
        double r182527 = c;
        double r182528 = -r182527;
        double r182529 = r182526 * r182528;
        double r182530 = a;
        double r182531 = r182525 * r182530;
        double r182532 = b;
        double r182533 = r182531 * r182532;
        double r182534 = r182529 + r182533;
        double r182535 = y1;
        double r182536 = r182535 * r182518;
        double r182537 = -r182536;
        double r182538 = j;
        double r182539 = r182538 * r182519;
        double r182540 = k;
        double r182541 = r182523 * r182540;
        double r182542 = r182539 - r182541;
        double r182543 = r182537 * r182542;
        double r182544 = y0;
        double r182545 = r182542 * r182544;
        double r182546 = r182545 * r182532;
        double r182547 = r182543 + r182546;
        double r182548 = r182534 - r182547;
        double r182549 = r182544 * r182527;
        double r182550 = r182530 * r182535;
        double r182551 = r182549 - r182550;
        double r182552 = y2;
        double r182553 = r182552 * r182519;
        double r182554 = y3;
        double r182555 = r182554 * r182523;
        double r182556 = r182553 - r182555;
        double r182557 = r182551 * r182556;
        double r182558 = r182548 + r182557;
        double r182559 = -r182540;
        double r182560 = r182520 * r182559;
        double r182561 = fma(r182538, r182522, r182560);
        double r182562 = r182515 * r182561;
        double r182563 = r182562 * r182532;
        double r182564 = y5;
        double r182565 = r182561 * r182564;
        double r182566 = -r182565;
        double r182567 = r182518 * r182566;
        double r182568 = r182563 + r182567;
        double r182569 = r182558 + r182568;
        double r182570 = r182515 * r182527;
        double r182571 = r182530 * r182564;
        double r182572 = r182570 - r182571;
        double r182573 = r182552 * r182522;
        double r182574 = r182520 * r182554;
        double r182575 = r182573 - r182574;
        double r182576 = r182572 * r182575;
        double r182577 = r182569 - r182576;
        double r182578 = r182552 * r182540;
        double r182579 = r182554 * r182538;
        double r182580 = r182578 - r182579;
        double r182581 = r182580 * r182564;
        double r182582 = -r182581;
        double r182583 = r182544 * r182582;
        double r182584 = r182515 * r182580;
        double r182585 = r182535 * r182584;
        double r182586 = r182583 + r182585;
        double r182587 = r182577 + r182586;
        double r182588 = -2.1764282042822157e-125;
        bool r182589 = r182515 <= r182588;
        double r182590 = r182532 * r182530;
        double r182591 = r182518 * r182527;
        double r182592 = r182590 - r182591;
        double r182593 = r182525 * r182592;
        double r182594 = r182593 - r182547;
        double r182595 = r182594 + r182557;
        double r182596 = r182595 - r182576;
        double r182597 = r182586 + r182596;
        double r182598 = -2.5670613540106872e-254;
        bool r182599 = r182515 <= r182598;
        double r182600 = r182595 + r182568;
        double r182601 = r182586 + r182600;
        double r182602 = 7.742023117024128e-208;
        bool r182603 = r182515 <= r182602;
        double r182604 = r182515 * r182535;
        double r182605 = r182544 * r182564;
        double r182606 = r182604 - r182605;
        double r182607 = r182606 * r182580;
        double r182608 = -r182518;
        double r182609 = fma(r182522, r182538, r182560);
        double r182610 = r182608 * r182609;
        double r182611 = r182564 * r182610;
        double r182612 = r182532 * r182515;
        double r182613 = r182609 * r182612;
        double r182614 = r182611 + r182613;
        double r182615 = r182614 + r182595;
        double r182616 = r182615 - r182576;
        double r182617 = r182607 + r182616;
        double r182618 = 1.6874770642863421e-164;
        bool r182619 = r182515 <= r182618;
        double r182620 = 7.586217188176185e-103;
        bool r182621 = r182515 <= r182620;
        double r182622 = r182518 * r182564;
        double r182623 = r182612 - r182622;
        double r182624 = r182538 * r182522;
        double r182625 = r182520 * r182540;
        double r182626 = r182624 - r182625;
        double r182627 = r182623 * r182626;
        double r182628 = r182557 + r182593;
        double r182629 = r182627 + r182628;
        double r182630 = r182629 - r182576;
        double r182631 = r182630 + r182607;
        double r182632 = 1.1466843471833704e+33;
        bool r182633 = r182515 <= r182632;
        double r182634 = -r182542;
        double r182635 = r182532 * r182544;
        double r182636 = r182635 - r182536;
        double r182637 = r182634 * r182636;
        double r182638 = r182557 + r182637;
        double r182639 = r182638 + r182627;
        double r182640 = r182639 - r182576;
        double r182641 = r182640 + r182607;
        double r182642 = 5.068523228647656e+142;
        bool r182643 = r182515 <= r182642;
        double r182644 = r182636 * r182542;
        double r182645 = r182593 - r182644;
        double r182646 = r182557 + r182645;
        double r182647 = r182646 + r182627;
        double r182648 = r182647 - r182576;
        double r182649 = r182538 * r182564;
        double r182650 = r182544 * r182649;
        double r182651 = r182552 * r182605;
        double r182652 = r182579 * r182515;
        double r182653 = r182535 * r182652;
        double r182654 = fma(r182651, r182540, r182653);
        double r182655 = -r182654;
        double r182656 = fma(r182650, r182554, r182655);
        double r182657 = r182648 + r182656;
        double r182658 = r182575 * r182530;
        double r182659 = -r182658;
        double r182660 = r182564 * r182659;
        double r182661 = r182570 * r182575;
        double r182662 = r182660 + r182661;
        double r182663 = r182600 - r182662;
        double r182664 = r182663 + r182586;
        double r182665 = r182643 ? r182657 : r182664;
        double r182666 = r182633 ? r182641 : r182665;
        double r182667 = r182621 ? r182631 : r182666;
        double r182668 = r182619 ? r182587 : r182667;
        double r182669 = r182603 ? r182617 : r182668;
        double r182670 = r182599 ? r182601 : r182669;
        double r182671 = r182589 ? r182597 : r182670;
        double r182672 = r182517 ? r182587 : r182671;
        return r182672;
}

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

Derivation

1. Split input into 8 regimes

2. if y4 < -6.171752557537877e+41 or 7.742023117024128e-208 < y4 < 1.6874770642863421e-164

   1. Initial program 28.8

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

   3. Applied sub-neg 28.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-in 28.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. Simplified 29.2

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

   6. Simplified 29.2

      \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\left(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \color{blue}{\left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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. Using strategy rm

   8. Applied sub-neg 29.2

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

   9. Applied distribute-lft-in 29.2

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

   10. Simplified 30.5

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

   11. Simplified 29.9

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

   13. Applied sub-neg 29.9

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

   14. Applied distribute-lft-in 29.9

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

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

   16. Simplified 29.5

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

   18. Applied sub-neg 29.5

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

   19. Applied distribute-lft-in 29.5

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

   20. Simplified 29.6

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

   21. Simplified 29.9

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

   if -6.171752557537877e+41 < y4 < -2.1764282042822157e-125

   1. Initial program 24.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-neg 24.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-in 24.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. Simplified 23.8

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

   6. Simplified 23.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \color{blue}{\left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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. Using strategy rm

   8. Applied sub-neg 23.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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 \color{blue}{\left(y4 \cdot y1 + \left(-y5 \cdot y0\right)\right)}\]

   9. Applied distribute-lft-in 23.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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) + \color{blue}{\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)}\]

   10. Simplified 23.9

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

   11. Simplified 23.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1 + \color{blue}{\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5\right)\right) \cdot y0}\right)\]

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

   if -2.1764282042822157e-125 < y4 < -2.5670613540106872e-254

   1. Initial program 26.2

      \[\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-neg 26.2

      \[\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-in 26.2

      \[\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. Simplified 26.1

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

   6. Simplified 26.1

      \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\left(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \color{blue}{\left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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. Using strategy rm

   8. Applied sub-neg 26.1

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

   9. Applied distribute-lft-in 26.1

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

   10. Simplified 26.1

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

   11. Simplified 26.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1 + \color{blue}{\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5\right)\right) \cdot y0}\right)\]
   12. Using strategy rm

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

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

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

   16. Simplified 27.2

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

   17. Taylor expanded around 0 31.2

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

   if -2.5670613540106872e-254 < y4 < 7.742023117024128e-208

   1. Initial program 28.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-neg 28.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-in 28.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. Simplified 28.0

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

   6. Simplified 28.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \color{blue}{\left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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. Using strategy rm

   8. Applied sub-neg 28.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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 \color{blue}{\left(y4 \cdot b + \left(-y5 \cdot i\right)\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)\]

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

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

   11. Simplified 28.5

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

   if 1.6874770642863421e-164 < y4 < 7.586217188176185e-103

   1. Initial program 25.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. Taylor expanded around 0 32.3

      \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \color{blue}{0}\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 7.586217188176185e-103 < y4 < 1.1466843471833704e+33

   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. Taylor expanded around 0 28.2

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

   if 1.1466843471833704e+33 < y4 < 5.068523228647656e+142

   1. Initial program 27.9

      \[\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. Taylor expanded around inf 32.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 \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) + \color{blue}{\left(y3 \cdot \left(j \cdot \left(y5 \cdot y0\right)\right) - \left(y1 \cdot \left(y3 \cdot \left(y4 \cdot j\right)\right) + k \cdot \left(y2 \cdot \left(y5 \cdot y0\right)\right)\right)\right)}\]

   3. Simplified 32.5

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

   if 5.068523228647656e+142 < y4

   1. Initial program 34.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-neg 34.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-in 34.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. Simplified 35.9

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

   6. Simplified 35.9

      \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\left(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \color{blue}{\left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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. Using strategy rm

   8. Applied sub-neg 35.9

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

   9. Applied distribute-lft-in 35.9

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

   10. Simplified 36.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\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(\color{blue}{\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1} + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)\]

   11. Simplified 35.1

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

   13. Applied sub-neg 35.1

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

   14. Applied distribute-lft-in 35.1

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

   15. Simplified 34.2

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

   16. Simplified 33.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y4\right) \cdot b + \color{blue}{\left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right) \cdot \left(-i\right)}\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1 + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5\right)\right) \cdot y0\right)\]
   17. Using strategy rm

   18. Applied sub-neg 33.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y4\right) \cdot b + \left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right) \cdot \left(-i\right)\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \color{blue}{\left(y4 \cdot c + \left(-y5 \cdot a\right)\right)}\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1 + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5\right)\right) \cdot y0\right)\]

   19. Applied distribute-lft-in 33.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(\left(x \cdot j - z \cdot k\right) \cdot y0\right) \cdot b + \left(-i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y4\right) \cdot b + \left(\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right) \cdot \left(-i\right)\right)\right) - \color{blue}{\left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-y5 \cdot a\right)\right)}\right) + \left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y4\right) \cdot y1 + \left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5\right)\right) \cdot y0\right)\]

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

   21. Simplified 32.9

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

4. Final simplification 30.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;y4 \le -617175255753787705220435928565733478367200:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(i \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot \left(-c\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot a\right) \cdot b\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \mathbf{elif}\;y4 \le -2.176428204282215683286541428526422284872 \cdot 10^{-125}:\\ \;\;\;\;\left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right) + \left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\\ \mathbf{elif}\;y4 \le -2.567061354010687248637387810560011604782 \cdot 10^{-254}:\\ \;\;\;\;\left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right) + \left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right)\\ \mathbf{elif}\;y4 \le 7.742023117024128236838563930215200024067 \cdot 10^{-208}:\\ \;\;\;\;\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right) + \left(\left(\left(y5 \cdot \left(\left(-i\right) \cdot \mathsf{fma}\left(t, j, y \cdot \left(-k\right)\right)\right) + \mathsf{fma}\left(t, j, y \cdot \left(-k\right)\right) \cdot \left(b \cdot y4\right)\right) + \left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\\ \mathbf{elif}\;y4 \le 1.687477064286342108432003547396676662615 \cdot 10^{-164}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(i \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot \left(-c\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot a\right) \cdot b\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \mathbf{elif}\;y4 \le 7.586217188176184986289740850066189488425 \cdot 10^{-103}:\\ \;\;\;\;\left(\left(\left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le 1146684347183370447338978607628288:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(-\left(j \cdot x - z \cdot k\right)\right) \cdot \left(b \cdot y0 - y1 \cdot i\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le 5.0685232286476560290775075501477904359 \cdot 10^{142}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - y \cdot k\right)\right) - \left(y4 \cdot c - a \cdot y5\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \mathsf{fma}\left(y0 \cdot \left(j \cdot y5\right), y3, -\mathsf{fma}\left(y2 \cdot \left(y0 \cdot y5\right), k, y1 \cdot \left(\left(y3 \cdot j\right) \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(-y1 \cdot i\right) \cdot \left(j \cdot x - z \cdot k\right) + \left(\left(j \cdot x - z \cdot k\right) \cdot y0\right) \cdot b\right)\right) + \left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(y4 \cdot \mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right)\right) \cdot b + i \cdot \left(-\mathsf{fma}\left(j, t, y \cdot \left(-k\right)\right) \cdot y5\right)\right)\right) - \left(y5 \cdot \left(-\left(y2 \cdot t - y \cdot y3\right) \cdot a\right) + \left(y4 \cdot c\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right)\right) + \left(y0 \cdot \left(-\left(y2 \cdot k - y3 \cdot j\right) \cdot y5\right) + y1 \cdot \left(y4 \cdot \left(y2 \cdot k - y3 \cdot j\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019195 +o rules:numerics
(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)))))