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

↓

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

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

↓

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

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

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

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

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

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

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

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
        double r558566 = x;
        double r558567 = y;
        double r558568 = r558566 * r558567;
        double r558569 = z;
        double r558570 = t;
        double r558571 = r558569 * r558570;
        double r558572 = r558568 - r558571;
        double r558573 = a;
        double r558574 = b;
        double r558575 = r558573 * r558574;
        double r558576 = c;
        double r558577 = i;
        double r558578 = r558576 * r558577;
        double r558579 = r558575 - r558578;
        double r558580 = r558572 * r558579;
        double r558581 = j;
        double r558582 = r558566 * r558581;
        double r558583 = k;
        double r558584 = r558569 * r558583;
        double r558585 = r558582 - r558584;
        double r558586 = y0;
        double r558587 = r558586 * r558574;
        double r558588 = y1;
        double r558589 = r558588 * r558577;
        double r558590 = r558587 - r558589;
        double r558591 = r558585 * r558590;
        double r558592 = r558580 - r558591;
        double r558593 = y2;
        double r558594 = r558566 * r558593;
        double r558595 = y3;
        double r558596 = r558569 * r558595;
        double r558597 = r558594 - r558596;
        double r558598 = r558586 * r558576;
        double r558599 = r558588 * r558573;
        double r558600 = r558598 - r558599;
        double r558601 = r558597 * r558600;
        double r558602 = r558592 + r558601;
        double r558603 = r558570 * r558581;
        double r558604 = r558567 * r558583;
        double r558605 = r558603 - r558604;
        double r558606 = y4;
        double r558607 = r558606 * r558574;
        double r558608 = y5;
        double r558609 = r558608 * r558577;
        double r558610 = r558607 - r558609;
        double r558611 = r558605 * r558610;
        double r558612 = r558602 + r558611;
        double r558613 = r558570 * r558593;
        double r558614 = r558567 * r558595;
        double r558615 = r558613 - r558614;
        double r558616 = r558606 * r558576;
        double r558617 = r558608 * r558573;
        double r558618 = r558616 - r558617;
        double r558619 = r558615 * r558618;
        double r558620 = r558612 - r558619;
        double r558621 = r558583 * r558593;
        double r558622 = r558581 * r558595;
        double r558623 = r558621 - r558622;
        double r558624 = r558606 * r558588;
        double r558625 = r558608 * r558586;
        double r558626 = r558624 - r558625;
        double r558627 = r558623 * r558626;
        double r558628 = r558620 + r558627;
        return r558628;
}

↓

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 r558629 = y0;
        double r558630 = -1.6677908776896365e+90;
        bool r558631 = r558629 <= r558630;
        double r558632 = a;
        double r558633 = b;
        double r558634 = r558632 * r558633;
        double r558635 = i;
        double r558636 = c;
        double r558637 = r558635 * r558636;
        double r558638 = r558634 - r558637;
        double r558639 = y;
        double r558640 = x;
        double r558641 = r558639 * r558640;
        double r558642 = t;
        double r558643 = z;
        double r558644 = r558642 * r558643;
        double r558645 = r558641 - r558644;
        double r558646 = r558638 * r558645;
        double r558647 = r558629 * r558633;
        double r558648 = y1;
        double r558649 = r558635 * r558648;
        double r558650 = r558647 - r558649;
        double r558651 = j;
        double r558652 = r558651 * r558640;
        double r558653 = k;
        double r558654 = r558643 * r558653;
        double r558655 = r558652 - r558654;
        double r558656 = r558650 * r558655;
        double r558657 = r558646 - r558656;
        double r558658 = r558636 * r558629;
        double r558659 = r558648 * r558632;
        double r558660 = r558658 - r558659;
        double r558661 = y2;
        double r558662 = r558640 * r558661;
        double r558663 = y3;
        double r558664 = r558663 * r558643;
        double r558665 = r558662 - r558664;
        double r558666 = r558660 * r558665;
        double r558667 = r558657 + r558666;
        double r558668 = r558642 * r558651;
        double r558669 = r558639 * r558653;
        double r558670 = r558668 - r558669;
        double r558671 = y4;
        double r558672 = r558633 * r558671;
        double r558673 = y5;
        double r558674 = r558635 * r558673;
        double r558675 = r558672 - r558674;
        double r558676 = r558670 * r558675;
        double r558677 = r558636 * r558671;
        double r558678 = r558673 * r558632;
        double r558679 = r558677 - r558678;
        double r558680 = r558642 * r558661;
        double r558681 = r558663 * r558639;
        double r558682 = r558680 - r558681;
        double r558683 = r558679 * r558682;
        double r558684 = r558676 - r558683;
        double r558685 = r558667 + r558684;
        double r558686 = -1.1987059924588957e-162;
        bool r558687 = r558629 <= r558686;
        double r558688 = r558648 * r558671;
        double r558689 = r558673 * r558629;
        double r558690 = r558688 - r558689;
        double r558691 = r558690 * r558653;
        double r558692 = r558661 * r558691;
        double r558693 = r558651 * r558663;
        double r558694 = -r558693;
        double r558695 = r558694 * r558690;
        double r558696 = r558692 + r558695;
        double r558697 = r558696 + r558666;
        double r558698 = r558635 * r558643;
        double r558699 = r558698 * r558648;
        double r558700 = r558699 * r558653;
        double r558701 = r558635 * r558651;
        double r558702 = r558701 * r558640;
        double r558703 = r558648 * r558702;
        double r558704 = r558700 - r558703;
        double r558705 = r558654 * r558633;
        double r558706 = r558705 * r558629;
        double r558707 = r558704 - r558706;
        double r558708 = r558646 - r558707;
        double r558709 = r558697 + r558708;
        double r558710 = r558709 + r558684;
        double r558711 = -1.869614940909926e-227;
        bool r558712 = r558629 <= r558711;
        double r558713 = r558646 + r558697;
        double r558714 = r558684 + r558713;
        double r558715 = 3.486128712704299e-82;
        bool r558716 = r558629 <= r558715;
        double r558717 = r558643 * r558648;
        double r558718 = r558717 * r558663;
        double r558719 = r558648 * r558661;
        double r558720 = r558719 * r558640;
        double r558721 = r558718 - r558720;
        double r558722 = r558721 * r558632;
        double r558723 = r558636 * r558643;
        double r558724 = r558629 * r558663;
        double r558725 = r558723 * r558724;
        double r558726 = r558722 - r558725;
        double r558727 = r558726 + r558696;
        double r558728 = r558727 + r558657;
        double r558729 = r558684 + r558728;
        double r558730 = 5.6900033333812694e+54;
        bool r558731 = r558629 <= r558730;
        double r558732 = r558661 * r558653;
        double r558733 = r558732 - r558693;
        double r558734 = r558690 * r558733;
        double r558735 = r558734 + r558666;
        double r558736 = r558650 * r558640;
        double r558737 = r558736 * r558651;
        double r558738 = r558650 * r558643;
        double r558739 = -r558738;
        double r558740 = r558739 * r558653;
        double r558741 = r558737 + r558740;
        double r558742 = r558646 - r558741;
        double r558743 = r558735 + r558742;
        double r558744 = r558743 + r558684;
        double r558745 = 6.20813424606636e+77;
        bool r558746 = r558629 <= r558745;
        double r558747 = r558637 * r558643;
        double r558748 = r558643 * r558633;
        double r558749 = r558748 * r558632;
        double r558750 = r558747 - r558749;
        double r558751 = r558642 * r558750;
        double r558752 = r558636 * r558639;
        double r558753 = r558640 * r558752;
        double r558754 = r558753 * r558635;
        double r558755 = r558751 - r558754;
        double r558756 = r558755 - r558656;
        double r558757 = r558697 + r558756;
        double r558758 = r558757 + r558684;
        double r558759 = r558746 ? r558714 : r558758;
        double r558760 = r558731 ? r558744 : r558759;
        double r558761 = r558716 ? r558729 : r558760;
        double r558762 = r558712 ? r558714 : r558761;
        double r558763 = r558687 ? r558710 : r558762;
        double r558764 = r558631 ? r558685 : r558763;
        return r558764;
}

Original	27.3
Target	30.7
Herbie	29.9

Derivation

Split input into 6 regimes
if y0 < -1.6677908776896365e+90
1. Initial program 32.5
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified32.5
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Taylor expanded around 0 38.2
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{0} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
if -1.6677908776896365e+90 < y0 < -1.1987059924588957e-162
1. Initial program 26.4
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified26.4
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg26.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
5. Applied distribute-lft-in26.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
6. Simplified27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
7. Simplified27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
8. Taylor expanded around inf 28.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(i \cdot \left(z \cdot \left(y1 \cdot k\right)\right) - \left(x \cdot \left(y1 \cdot \left(j \cdot i\right)\right) + y0 \cdot \left(z \cdot \left(b \cdot k\right)\right)\right)\right)}\right)\right)\]
9. Simplified29.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(\left(\left(i \cdot z\right) \cdot y1\right) \cdot k - \left(x \cdot \left(i \cdot j\right)\right) \cdot y1\right) - y0 \cdot \left(\left(k \cdot z\right) \cdot b\right)\right)}\right)\right)\]
if -1.1987059924588957e-162 < y0 < -1.869614940909926e-227 or 5.6900033333812694e+54 < y0 < 6.20813424606636e+77
1. Initial program 23.7
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified23.7
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg23.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
5. Applied distribute-lft-in23.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
6. Simplified23.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
7. Simplified23.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
8. Taylor expanded around 0 28.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{0}\right)\right)\]
if -1.869614940909926e-227 < y0 < 3.486128712704299e-82
1. Initial program 26.7
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified26.7
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg26.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
5. Applied distribute-lft-in26.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
6. Simplified26.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
7. Simplified26.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
8. Taylor expanded around inf 27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(a \cdot \left(y3 \cdot \left(y1 \cdot z\right)\right) - \left(a \cdot \left(x \cdot \left(y2 \cdot y1\right)\right) + c \cdot \left(z \cdot \left(y3 \cdot y0\right)\right)\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
9. Simplified28.2
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(a \cdot \left(\left(y1 \cdot z\right) \cdot y3 - x \cdot \left(y2 \cdot y1\right)\right) - \left(z \cdot c\right) \cdot \left(y0 \cdot y3\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
if 3.486128712704299e-82 < y0 < 5.6900033333812694e+54
1. Initial program 24.3
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified24.3
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg24.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in24.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified25.0
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{j \cdot \left(x \cdot \left(y0 \cdot b - y1 \cdot i\right)\right)} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified25.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(j \cdot \left(x \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \color{blue}{\left(\left(y0 \cdot b - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
if 6.20813424606636e+77 < y0
1. Initial program 31.5
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified31.5
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg31.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
5. Applied distribute-lft-in31.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
6. Simplified33.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
7. Simplified33.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
8. Taylor expanded around inf 33.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\color{blue}{\left(t \cdot \left(i \cdot \left(z \cdot c\right)\right) - \left(t \cdot \left(a \cdot \left(b \cdot z\right)\right) + x \cdot \left(i \cdot \left(c \cdot y\right)\right)\right)\right)} - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
9. Simplified33.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y2 \cdot \left(k \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\color{blue}{\left(t \cdot \left(z \cdot \left(i \cdot c\right) - a \cdot \left(z \cdot b\right)\right) - \left(x \cdot \left(c \cdot y\right)\right) \cdot i\right)} - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
Recombined 6 regimes into one program.
Final simplification29.9
\[\leadsto \begin{array}{l} \mathbf{if}\;y0 \le -1.667790877689636481505521901403068103115 \cdot 10^{90}:\\ \;\;\;\;\left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.198705992458895702428916734917044414201 \cdot 10^{-162}:\\ \;\;\;\;\left(\left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(\left(i \cdot z\right) \cdot y1\right) \cdot k - y1 \cdot \left(\left(i \cdot j\right) \cdot x\right)\right) - \left(\left(z \cdot k\right) \cdot b\right) \cdot y0\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le -1.869614940909926097226067307549077145402 \cdot 10^{-227}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{elif}\;y0 \le 3.486128712704299101676819382240846478502 \cdot 10^{-82}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(z \cdot y1\right) \cdot y3 - \left(y1 \cdot y2\right) \cdot x\right) \cdot a - \left(c \cdot z\right) \cdot \left(y0 \cdot y3\right)\right) + \left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\\ \mathbf{elif}\;y0 \le 5.69000333338126936863636307941908438558 \cdot 10^{54}:\\ \;\;\;\;\left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(\left(y0 \cdot b - i \cdot y1\right) \cdot x\right) \cdot j + \left(-\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le 6.208134246066359685262088422068626609998 \cdot 10^{77}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) + \left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(-j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) + \left(\left(t \cdot \left(\left(i \cdot c\right) \cdot z - \left(z \cdot b\right) \cdot a\right) - \left(x \cdot \left(c \cdot y\right)\right) \cdot i\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y0 < -1.6677908776896365e+90`

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

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

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

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

`if 6.20813424606636e+77 < y0`

Reproduce

In
Out