Linear.Matrix:det44 from linear-1.19.1.3

Average Error: 27.0 → 28.1

Time: 1.5m

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}\;j \le -5.423307827391987656847104322360977276686 \cdot 10^{-206} \lor \neg \left(j \le 6.591415557374126792319668655786595642762 \cdot 10^{-241}\right):\\ \;\;\;\;\left(\left(\left(\left(\left(\sqrt[3]{x \cdot y - z \cdot t} \cdot \sqrt[3]{x \cdot y - z \cdot t}\right) \cdot \left(\sqrt[3]{x \cdot y - z \cdot t} \cdot \left(a \cdot b - c \cdot i\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\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(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\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 r598544 = x;
        double r598545 = y;
        double r598546 = r598544 * r598545;
        double r598547 = z;
        double r598548 = t;
        double r598549 = r598547 * r598548;
        double r598550 = r598546 - r598549;
        double r598551 = a;
        double r598552 = b;
        double r598553 = r598551 * r598552;
        double r598554 = c;
        double r598555 = i;
        double r598556 = r598554 * r598555;
        double r598557 = r598553 - r598556;
        double r598558 = r598550 * r598557;
        double r598559 = j;
        double r598560 = r598544 * r598559;
        double r598561 = k;
        double r598562 = r598547 * r598561;
        double r598563 = r598560 - r598562;
        double r598564 = y0;
        double r598565 = r598564 * r598552;
        double r598566 = y1;
        double r598567 = r598566 * r598555;
        double r598568 = r598565 - r598567;
        double r598569 = r598563 * r598568;
        double r598570 = r598558 - r598569;
        double r598571 = y2;
        double r598572 = r598544 * r598571;
        double r598573 = y3;
        double r598574 = r598547 * r598573;
        double r598575 = r598572 - r598574;
        double r598576 = r598564 * r598554;
        double r598577 = r598566 * r598551;
        double r598578 = r598576 - r598577;
        double r598579 = r598575 * r598578;
        double r598580 = r598570 + r598579;
        double r598581 = r598548 * r598559;
        double r598582 = r598545 * r598561;
        double r598583 = r598581 - r598582;
        double r598584 = y4;
        double r598585 = r598584 * r598552;
        double r598586 = y5;
        double r598587 = r598586 * r598555;
        double r598588 = r598585 - r598587;
        double r598589 = r598583 * r598588;
        double r598590 = r598580 + r598589;
        double r598591 = r598548 * r598571;
        double r598592 = r598545 * r598573;
        double r598593 = r598591 - r598592;
        double r598594 = r598584 * r598554;
        double r598595 = r598586 * r598551;
        double r598596 = r598594 - r598595;
        double r598597 = r598593 * r598596;
        double r598598 = r598590 - r598597;
        double r598599 = r598561 * r598571;
        double r598600 = r598559 * r598573;
        double r598601 = r598599 - r598600;
        double r598602 = r598584 * r598566;
        double r598603 = r598586 * r598564;
        double r598604 = r598602 - r598603;
        double r598605 = r598601 * r598604;
        double r598606 = r598598 + r598605;
        return r598606;
}

↓

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 r598607 = j;
        double r598608 = -5.423307827391988e-206;
        bool r598609 = r598607 <= r598608;
        double r598610 = 6.591415557374127e-241;
        bool r598611 = r598607 <= r598610;
        double r598612 = !r598611;
        bool r598613 = r598609 || r598612;
        double r598614 = x;
        double r598615 = y;
        double r598616 = r598614 * r598615;
        double r598617 = z;
        double r598618 = t;
        double r598619 = r598617 * r598618;
        double r598620 = r598616 - r598619;
        double r598621 = cbrt(r598620);
        double r598622 = r598621 * r598621;
        double r598623 = a;
        double r598624 = b;
        double r598625 = r598623 * r598624;
        double r598626 = c;
        double r598627 = i;
        double r598628 = r598626 * r598627;
        double r598629 = r598625 - r598628;
        double r598630 = r598621 * r598629;
        double r598631 = r598622 * r598630;
        double r598632 = r598614 * r598607;
        double r598633 = k;
        double r598634 = r598617 * r598633;
        double r598635 = r598632 - r598634;
        double r598636 = y0;
        double r598637 = r598636 * r598624;
        double r598638 = y1;
        double r598639 = r598638 * r598627;
        double r598640 = r598637 - r598639;
        double r598641 = r598635 * r598640;
        double r598642 = r598631 - r598641;
        double r598643 = y2;
        double r598644 = r598614 * r598643;
        double r598645 = y3;
        double r598646 = r598617 * r598645;
        double r598647 = r598644 - r598646;
        double r598648 = r598636 * r598626;
        double r598649 = r598638 * r598623;
        double r598650 = r598648 - r598649;
        double r598651 = r598647 * r598650;
        double r598652 = r598642 + r598651;
        double r598653 = r598618 * r598607;
        double r598654 = r598615 * r598633;
        double r598655 = r598653 - r598654;
        double r598656 = y4;
        double r598657 = r598656 * r598624;
        double r598658 = y5;
        double r598659 = r598658 * r598627;
        double r598660 = r598657 - r598659;
        double r598661 = r598655 * r598660;
        double r598662 = r598652 + r598661;
        double r598663 = r598618 * r598643;
        double r598664 = r598615 * r598645;
        double r598665 = r598663 - r598664;
        double r598666 = r598656 * r598626;
        double r598667 = r598658 * r598623;
        double r598668 = r598666 - r598667;
        double r598669 = r598665 * r598668;
        double r598670 = r598662 - r598669;
        double r598671 = r598656 * r598638;
        double r598672 = r598633 * r598643;
        double r598673 = r598607 * r598645;
        double r598674 = r598672 - r598673;
        double r598675 = r598671 * r598674;
        double r598676 = -r598658;
        double r598677 = r598636 * r598674;
        double r598678 = r598676 * r598677;
        double r598679 = r598675 + r598678;
        double r598680 = r598670 + r598679;
        double r598681 = r598620 * r598629;
        double r598682 = r598681 + r598651;
        double r598683 = r598682 + r598661;
        double r598684 = r598683 - r598669;
        double r598685 = r598684 + r598679;
        double r598686 = r598613 ? r598680 : r598685;
        return r598686;
}

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

Target

Original	27.0
Target	30.8
Herbie	28.1

\[\begin{array}{l} \mathbf{if}\;y4 \lt -7.206256231996481342319540724063498925423 \cdot 10^{60}:\\ \;\;\;\;\left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right)\right) - \left(\frac{y2 \cdot t - y3 \cdot y}{\frac{1}{y4 \cdot c - y5 \cdot a}} - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\\ \mathbf{elif}\;y4 \lt -3.364603505246316896676998939327711644754 \cdot 10^{-66}:\\ \;\;\;\;\left(\left(\left(\left(t \cdot c\right) \cdot \left(i \cdot z\right) - \left(a \cdot t\right) \cdot \left(b \cdot z\right)\right) - \left(y \cdot c\right) \cdot \left(i \cdot x\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right)\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) - \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - a \cdot y5\right) - \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\\ \mathbf{elif}\;y4 \lt -1.200006505568611600888263862102883004513 \cdot 10^{-105}:\\ \;\;\;\;\left(\left(\left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) - \left(y3 \cdot y\right) \cdot \left(y5 \cdot a - y4 \cdot c\right)\right) + \left(\left(y5 \cdot a\right) \cdot \left(t \cdot y2\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) - \left(\left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right) - \left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 6.718963124057494636349617318198742025856 \cdot 10^{-279}:\\ \;\;\;\;\left(\left(\left(\left(k \cdot y\right) \cdot \left(y5 \cdot i\right) - \left(y \cdot b\right) \cdot \left(y4 \cdot k\right)\right) - \left(y5 \cdot t\right) \cdot \left(i \cdot j\right)\right) - \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right) - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(y2 \cdot x - y3 \cdot z\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 4.779626814037919873410686589412258835104 \cdot 10^{-222}:\\ \;\;\;\;\left(\left(\left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) - \left(y3 \cdot y\right) \cdot \left(y5 \cdot a - y4 \cdot c\right)\right) + \left(\left(y5 \cdot a\right) \cdot \left(t \cdot y2\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) - \left(\left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right) - \left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 2.285224154126683459205023499639872822811 \cdot 10^{-175}:\\ \;\;\;\;\left(\left(\left(\left(k \cdot y\right) \cdot \left(y5 \cdot i\right) - \left(y \cdot b\right) \cdot \left(y4 \cdot k\right)\right) - \left(y5 \cdot t\right) \cdot \left(i \cdot j\right)\right) - \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right) - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(y2 \cdot x - y3 \cdot z\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(k \cdot \left(i \cdot \left(z \cdot y1\right)\right) - \left(j \cdot \left(i \cdot \left(x \cdot y1\right)\right) + y0 \cdot \left(k \cdot \left(z \cdot b\right)\right)\right)\right)\right) + \left(z \cdot \left(y3 \cdot \left(a \cdot y1\right)\right) - \left(y2 \cdot \left(x \cdot \left(a \cdot y1\right)\right) + y0 \cdot \left(z \cdot \left(c \cdot y3\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)\\ \end{array}\]

Derivation

1. Split input into 2 regimes

2. if j < -5.423307827391988e-206 or 6.591415557374127e-241 < j

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

   3. Applied sub-neg 26.9

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

   4. Applied distribute-lft-in 26.9

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

   5. Simplified 26.9

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

   6. Simplified 26.9

      \[\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) + \left(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \color{blue}{\left(-y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right)}\right)\]
   7. Using strategy rm

   8. Applied distribute-lft-neg-in 26.9

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

   9. Applied associate-*l* 27.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 \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(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \color{blue}{\left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)}\right)\]
   10. Using strategy rm

   11. Applied add-cube-cbrt 27.7

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

   12. Applied associate-*l* 27.7

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

   if -5.423307827391988e-206 < j < 6.591415557374127e-241

   1. Initial program 27.3

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

   3. Applied sub-neg 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(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 \color{blue}{\left(y4 \cdot y1 + \left(-y5 \cdot y0\right)\right)}\]

   4. Applied distribute-lft-in 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(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(\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)}\]

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

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

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

   9. Applied associate-*l* 27.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 \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(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \color{blue}{\left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)}\right)\]

   10. 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) - \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(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\]
3. Recombined 2 regimes into one program.

4. Final simplification 28.1

   \[\leadsto \begin{array}{l} \mathbf{if}\;j \le -5.423307827391987656847104322360977276686 \cdot 10^{-206} \lor \neg \left(j \le 6.591415557374126792319668655786595642762 \cdot 10^{-241}\right):\\ \;\;\;\;\left(\left(\left(\left(\left(\sqrt[3]{x \cdot y - z \cdot t} \cdot \sqrt[3]{x \cdot y - z \cdot t}\right) \cdot \left(\sqrt[3]{x \cdot y - z \cdot t} \cdot \left(a \cdot b - c \cdot i\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(\left(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\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(y4 \cdot y1\right) \cdot \left(k \cdot y2 - j \cdot y3\right) + \left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019323 +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"
  :precision binary64

  :herbie-target
  (if (< y4 -7.206256231996481e+60) (- (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))))) (- (/ (- (* y2 t) (* y3 y)) (/ 1 (- (* y4 c) (* y5 a)))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (if (< y4 -3.364603505246317e-66) (+ (- (- (- (* (* t c) (* i z)) (* (* a t) (* b z))) (* (* y c) (* i x))) (* (- (* b y0) (* i y1)) (- (* j x) (* k z)))) (- (* (- (* y0 c) (* a y1)) (- (* x y2) (* z y3))) (- (* (- (* t y2) (* y y3)) (- (* y4 c) (* a y5))) (* (- (* y1 y4) (* y5 y0)) (- (* k y2) (* j y3)))))) (if (< y4 -1.2000065055686116e-105) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 6.718963124057495e-279) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (if (< y4 4.77962681403792e-222) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 2.2852241541266835e-175) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (- (* k (* i (* z y1))) (+ (* j (* i (* x y1))) (* y0 (* k (* z b)))))) (- (* z (* y3 (* a y1))) (+ (* y2 (* x (* a y1))) (* y0 (* z (* c y3)))))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))))))))

  (+ (- (+ (+ (- (* (- (* 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)))))