\[\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}\;c \le -1.520268482954330987110772716031092954836 \cdot 10^{-5}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(\left(a \cdot \left(-\mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right) \cdot y1 + c \cdot \left(y0 \cdot \mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\ \mathbf{elif}\;c \le -5.44363240207917693445236565463199493789 \cdot 10^{-107}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \mathbf{elif}\;c \le -1.658966746623872396328249367245659401154 \cdot 10^{-170}:\\ \;\;\;\;\left(\mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right) \cdot \left(\left(-y0\right) \cdot y5\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right) + \left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(\left(z \cdot \left(\left(t \cdot i\right) \cdot c\right) - \mathsf{fma}\left(t \cdot a, b \cdot z, x \cdot \left(i \cdot \left(y \cdot c\right)\right)\right)\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(x \cdot j - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;c \le 1.645164052734720604978390583791993656403 \cdot 10^{-93}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i}} \cdot \sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \sqrt[3]{b \cdot y0 - y1 \cdot i}}\right) \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(-i\right) \cdot \left(c \cdot \left(x \cdot y - t \cdot z\right)\right) + \left(b \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot a\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(x \cdot j - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;c \le -1.520268482954330987110772716031092954836 \cdot 10^{-5}:\\
\;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(\left(a \cdot \left(-\mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right) \cdot y1 + c \cdot \left(y0 \cdot \mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\

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

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

\mathbf{elif}\;c \le 1.645164052734720604978390583791993656403 \cdot 10^{-93}:\\
\;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i}} \cdot \sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \sqrt[3]{b \cdot y0 - y1 \cdot i}}\right) \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\

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

\end{array}

double f(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
        double r525613 = x;
        double r525614 = y;
        double r525615 = r525613 * r525614;
        double r525616 = z;
        double r525617 = t;
        double r525618 = r525616 * r525617;
        double r525619 = r525615 - r525618;
        double r525620 = a;
        double r525621 = b;
        double r525622 = r525620 * r525621;
        double r525623 = c;
        double r525624 = i;
        double r525625 = r525623 * r525624;
        double r525626 = r525622 - r525625;
        double r525627 = r525619 * r525626;
        double r525628 = j;
        double r525629 = r525613 * r525628;
        double r525630 = k;
        double r525631 = r525616 * r525630;
        double r525632 = r525629 - r525631;
        double r525633 = y0;
        double r525634 = r525633 * r525621;
        double r525635 = y1;
        double r525636 = r525635 * r525624;
        double r525637 = r525634 - r525636;
        double r525638 = r525632 * r525637;
        double r525639 = r525627 - r525638;
        double r525640 = y2;
        double r525641 = r525613 * r525640;
        double r525642 = y3;
        double r525643 = r525616 * r525642;
        double r525644 = r525641 - r525643;
        double r525645 = r525633 * r525623;
        double r525646 = r525635 * r525620;
        double r525647 = r525645 - r525646;
        double r525648 = r525644 * r525647;
        double r525649 = r525639 + r525648;
        double r525650 = r525617 * r525628;
        double r525651 = r525614 * r525630;
        double r525652 = r525650 - r525651;
        double r525653 = y4;
        double r525654 = r525653 * r525621;
        double r525655 = y5;
        double r525656 = r525655 * r525624;
        double r525657 = r525654 - r525656;
        double r525658 = r525652 * r525657;
        double r525659 = r525649 + r525658;
        double r525660 = r525617 * r525640;
        double r525661 = r525614 * r525642;
        double r525662 = r525660 - r525661;
        double r525663 = r525653 * r525623;
        double r525664 = r525655 * r525620;
        double r525665 = r525663 - r525664;
        double r525666 = r525662 * r525665;
        double r525667 = r525659 - r525666;
        double r525668 = r525630 * r525640;
        double r525669 = r525628 * r525642;
        double r525670 = r525668 - r525669;
        double r525671 = r525653 * r525635;
        double r525672 = r525655 * r525633;
        double r525673 = r525671 - r525672;
        double r525674 = r525670 * r525673;
        double r525675 = r525667 + r525674;
        return r525675;
}

↓

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 r525676 = c;
        double r525677 = -1.520268482954331e-05;
        bool r525678 = r525676 <= r525677;
        double r525679 = x;
        double r525680 = y;
        double r525681 = r525679 * r525680;
        double r525682 = t;
        double r525683 = z;
        double r525684 = r525682 * r525683;
        double r525685 = r525681 - r525684;
        double r525686 = a;
        double r525687 = b;
        double r525688 = r525686 * r525687;
        double r525689 = i;
        double r525690 = r525689 * r525676;
        double r525691 = r525688 - r525690;
        double r525692 = r525685 * r525691;
        double r525693 = y0;
        double r525694 = r525687 * r525693;
        double r525695 = y1;
        double r525696 = r525695 * r525689;
        double r525697 = r525694 - r525696;
        double r525698 = cbrt(r525697);
        double r525699 = j;
        double r525700 = -r525683;
        double r525701 = k;
        double r525702 = r525700 * r525701;
        double r525703 = fma(r525679, r525699, r525702);
        double r525704 = -r525695;
        double r525705 = r525689 * r525704;
        double r525706 = fma(r525687, r525693, r525705);
        double r525707 = cbrt(r525706);
        double r525708 = r525703 * r525707;
        double r525709 = r525708 * r525707;
        double r525710 = r525698 * r525709;
        double r525711 = r525692 - r525710;
        double r525712 = y3;
        double r525713 = y2;
        double r525714 = r525713 * r525679;
        double r525715 = fma(r525712, r525700, r525714);
        double r525716 = -r525715;
        double r525717 = r525686 * r525716;
        double r525718 = r525717 * r525695;
        double r525719 = r525693 * r525715;
        double r525720 = r525676 * r525719;
        double r525721 = r525718 + r525720;
        double r525722 = r525711 + r525721;
        double r525723 = r525699 * r525682;
        double r525724 = r525680 * r525701;
        double r525725 = r525723 - r525724;
        double r525726 = y4;
        double r525727 = r525726 * r525687;
        double r525728 = y5;
        double r525729 = r525728 * r525689;
        double r525730 = r525727 - r525729;
        double r525731 = r525725 * r525730;
        double r525732 = r525722 + r525731;
        double r525733 = r525676 * r525726;
        double r525734 = r525686 * r525728;
        double r525735 = r525733 - r525734;
        double r525736 = r525682 * r525713;
        double r525737 = r525680 * r525712;
        double r525738 = r525736 - r525737;
        double r525739 = r525735 * r525738;
        double r525740 = r525732 - r525739;
        double r525741 = -r525699;
        double r525742 = r525712 * r525741;
        double r525743 = fma(r525701, r525713, r525742);
        double r525744 = r525728 * r525743;
        double r525745 = r525744 * r525693;
        double r525746 = -r525745;
        double r525747 = r525695 * r525743;
        double r525748 = r525726 * r525747;
        double r525749 = r525746 + r525748;
        double r525750 = r525740 + r525749;
        double r525751 = -5.443632402079177e-107;
        bool r525752 = r525676 <= r525751;
        double r525753 = r525676 * r525693;
        double r525754 = r525695 * r525686;
        double r525755 = r525753 - r525754;
        double r525756 = r525712 * r525683;
        double r525757 = r525714 - r525756;
        double r525758 = r525755 * r525757;
        double r525759 = r525692 + r525758;
        double r525760 = r525759 + r525731;
        double r525761 = r525760 - r525739;
        double r525762 = r525713 * r525701;
        double r525763 = r525712 * r525699;
        double r525764 = r525762 - r525763;
        double r525765 = r525695 * r525726;
        double r525766 = r525728 * r525693;
        double r525767 = r525765 - r525766;
        double r525768 = r525764 * r525767;
        double r525769 = r525761 + r525768;
        double r525770 = -1.6589667466238724e-170;
        bool r525771 = r525676 <= r525770;
        double r525772 = -r525693;
        double r525773 = r525772 * r525728;
        double r525774 = r525743 * r525773;
        double r525775 = r525774 + r525748;
        double r525776 = r525682 * r525689;
        double r525777 = r525776 * r525676;
        double r525778 = r525683 * r525777;
        double r525779 = r525682 * r525686;
        double r525780 = r525687 * r525683;
        double r525781 = r525680 * r525676;
        double r525782 = r525689 * r525781;
        double r525783 = r525679 * r525782;
        double r525784 = fma(r525779, r525780, r525783);
        double r525785 = r525778 - r525784;
        double r525786 = r525679 * r525699;
        double r525787 = r525683 * r525701;
        double r525788 = r525786 - r525787;
        double r525789 = r525697 * r525788;
        double r525790 = r525785 - r525789;
        double r525791 = r525790 + r525758;
        double r525792 = r525731 + r525791;
        double r525793 = r525792 - r525739;
        double r525794 = r525775 + r525793;
        double r525795 = 1.6451640527347206e-93;
        bool r525796 = r525676 <= r525795;
        double r525797 = cbrt(r525698);
        double r525798 = r525698 * r525698;
        double r525799 = cbrt(r525798);
        double r525800 = r525797 * r525799;
        double r525801 = r525800 * r525709;
        double r525802 = r525692 - r525801;
        double r525803 = r525802 + r525758;
        double r525804 = r525731 + r525803;
        double r525805 = r525804 - r525739;
        double r525806 = r525805 + r525749;
        double r525807 = -r525689;
        double r525808 = r525676 * r525685;
        double r525809 = r525807 * r525808;
        double r525810 = r525687 * r525685;
        double r525811 = r525810 * r525686;
        double r525812 = r525809 + r525811;
        double r525813 = r525812 - r525789;
        double r525814 = r525813 + r525758;
        double r525815 = r525814 + r525731;
        double r525816 = r525815 - r525739;
        double r525817 = r525816 + r525768;
        double r525818 = r525796 ? r525806 : r525817;
        double r525819 = r525771 ? r525794 : r525818;
        double r525820 = r525752 ? r525769 : r525819;
        double r525821 = r525678 ? r525750 : r525820;
        return r525821;
}

Original	27.3
Target	30.7
Herbie	27.3

Derivation

Split input into 5 regimes
if c < -1.520268482954331e-05
1. Initial program 29.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-neg29.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 \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-in29.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 \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. Simplified29.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(\color{blue}{\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4} + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)\]
6. Simplified29.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \color{blue}{\left(-\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}\right)\]
7. Using strategy rm
8. Applied pow129.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot y0\right) \cdot \color{blue}{{\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}}\right)\right)\]
9. Applied pow129.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot \color{blue}{{y0}^{1}}\right) \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
10. Applied pow129.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(\color{blue}{{y5}^{1}} \cdot {y0}^{1}\right) \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
11. Applied pow-prod-down29.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\color{blue}{{\left(y5 \cdot y0\right)}^{1}} \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
12. Applied pow-prod-down29.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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\color{blue}{{\left(\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}}\right)\right)\]
13. Simplified30.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\color{blue}{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}}^{1}\right)\right)\]
14. Using strategy rm
15. Applied add-cube-cbrt30.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(\left(\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) \cdot \sqrt[3]{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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
16. Applied associate-*r*30.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(\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
17. Simplified30.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(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right)} \cdot \sqrt[3]{y0 \cdot b - y1 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
18. Using strategy rm
19. Applied sub-neg30.2
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \color{blue}{\left(y0 \cdot c + \left(-y1 \cdot a\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(\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
20. Applied distribute-lft-in30.2
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) + \color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-y1 \cdot a\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(\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
21. Simplified28.5
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) + \left(\color{blue}{\left(\mathsf{fma}\left(y3, -z, x \cdot y2\right) \cdot y0\right) \cdot c} + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-y1 \cdot a\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(\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
22. Simplified27.9
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) + \left(\left(\mathsf{fma}\left(y3, -z, x \cdot y2\right) \cdot y0\right) \cdot c + \color{blue}{y1 \cdot \left(\left(-a\right) \cdot \mathsf{fma}\left(y3, -z, x \cdot y2\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(\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
if -1.520268482954331e-05 < c < -5.443632402079177e-107
1. Initial program 25.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. Taylor expanded around 0 28.5
  \[\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 -5.443632402079177e-107 < c < -1.6589667466238724e-170
1. Initial program 25.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-neg25.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 \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-in25.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 \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. Simplified24.7
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4} + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)\]
6. Simplified24.7
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \color{blue}{\left(-\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}\right)\]
7. Taylor expanded around inf 26.3
  \[\leadsto \left(\left(\left(\left(\color{blue}{\left(t \cdot \left(i \cdot \left(z \cdot c\right)\right) - \left(a \cdot \left(t \cdot \left(b \cdot z\right)\right) + i \cdot \left(x \cdot \left(c \cdot y\right)\right)\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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)\right)\]
8. Simplified27.9
  \[\leadsto \left(\left(\left(\left(\color{blue}{\left(\left(\left(t \cdot i\right) \cdot c\right) \cdot z - \mathsf{fma}\left(a \cdot t, b \cdot z, \left(i \cdot \left(c \cdot y\right)\right) \cdot x\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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)\right)\]
if -1.6589667466238724e-170 < c < 1.6451640527347206e-93
1. Initial program 27.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-neg27.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(k \cdot y2 - j \cdot y3\right) \cdot \color{blue}{\left(y4 \cdot y1 + \left(-y5 \cdot y0\right)\right)}\]
4. Applied distribute-lft-in27.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) + \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. Simplified26.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4} + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)\]
6. Simplified26.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \color{blue}{\left(-\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}\right)\]
7. Using strategy rm
8. Applied pow126.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot y0\right) \cdot \color{blue}{{\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}}\right)\right)\]
9. Applied pow126.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(y5 \cdot \color{blue}{{y0}^{1}}\right) \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
10. Applied pow126.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\left(\color{blue}{{y5}^{1}} \cdot {y0}^{1}\right) \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
11. Applied pow-prod-down26.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\color{blue}{{\left(y5 \cdot y0\right)}^{1}} \cdot {\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}\right)\right)\]
12. Applied pow-prod-down26.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 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-\color{blue}{{\left(\left(y5 \cdot y0\right) \cdot \mathsf{fma}\left(k, y2, -j \cdot y3\right)\right)}^{1}}\right)\right)\]
13. Simplified26.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) + \left(\left(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\color{blue}{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}}^{1}\right)\right)\]
14. Using strategy rm
15. Applied add-cube-cbrt26.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 \color{blue}{\left(\left(\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) \cdot \sqrt[3]{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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
16. Applied associate-*r*26.5
  \[\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(\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right)\right) \cdot \sqrt[3]{y0 \cdot b - y1 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
17. Simplified26.5
  \[\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(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right)} \cdot \sqrt[3]{y0 \cdot b - y1 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
18. Using strategy rm
19. Applied add-cube-cbrt26.5
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \sqrt[3]{\color{blue}{\left(\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}\right) \cdot \sqrt[3]{y0 \cdot b - y1 \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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
20. Applied cbrt-prod26.5
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \color{blue}{\left(\sqrt[3]{\sqrt[3]{y0 \cdot b - y1 \cdot i} \cdot \sqrt[3]{y0 \cdot b - y1 \cdot i}} \cdot \sqrt[3]{\sqrt[3]{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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
21. Simplified26.5
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \left(\color{blue}{\sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \sqrt[3]{b \cdot y0 - y1 \cdot i}}} \cdot \sqrt[3]{\sqrt[3]{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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
22. Simplified26.5
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \left(\sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)} \cdot \mathsf{fma}\left(x, j, \left(-k\right) \cdot z\right)\right)\right) \cdot \left(\sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \sqrt[3]{b \cdot y0 - y1 \cdot i}} \cdot \color{blue}{\sqrt[3]{\sqrt[3]{b \cdot y0 - 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(\mathsf{fma}\left(k, y2, -j \cdot y3\right) \cdot y1\right) \cdot y4 + \left(-{\left(\left(\mathsf{fma}\left(k, y2, \left(-y3\right) \cdot j\right) \cdot y5\right) \cdot y0\right)}^{1}\right)\right)\]
if 1.6451640527347206e-93 < c
1. Initial program 27.7
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Using strategy rm
3. Applied sub-neg27.7
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \color{blue}{\left(a \cdot b + \left(-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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in27.7
  \[\leadsto \left(\left(\left(\left(\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(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)\]
5. Simplified27.6
  \[\leadsto \left(\left(\left(\left(\left(\color{blue}{\left(\left(y \cdot x - t \cdot z\right) \cdot b\right) \cdot a} + \left(x \cdot y - z \cdot t\right) \cdot \left(-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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified27.6
  \[\leadsto \left(\left(\left(\left(\left(\left(\left(y \cdot x - t \cdot z\right) \cdot b\right) \cdot a + \color{blue}{\left(\left(y \cdot x - t \cdot z\right) \cdot \left(-c\right)\right) \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)\]
Recombined 5 regimes into one program.
Final simplification27.3
\[\leadsto \begin{array}{l} \mathbf{if}\;c \le -1.520268482954330987110772716031092954836 \cdot 10^{-5}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(\left(a \cdot \left(-\mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right) \cdot y1 + c \cdot \left(y0 \cdot \mathsf{fma}\left(y3, -z, y2 \cdot x\right)\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\ \mathbf{elif}\;c \le -5.44363240207917693445236565463199493789 \cdot 10^{-107}:\\ \;\;\;\;\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \mathbf{elif}\;c \le -1.658966746623872396328249367245659401154 \cdot 10^{-170}:\\ \;\;\;\;\left(\mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right) \cdot \left(\left(-y0\right) \cdot y5\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right) + \left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(\left(z \cdot \left(\left(t \cdot i\right) \cdot c\right) - \mathsf{fma}\left(t \cdot a, b \cdot z, x \cdot \left(i \cdot \left(y \cdot c\right)\right)\right)\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(x \cdot j - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;c \le 1.645164052734720604978390583791993656403 \cdot 10^{-93}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i}} \cdot \sqrt[3]{\sqrt[3]{b \cdot y0 - y1 \cdot i} \cdot \sqrt[3]{b \cdot y0 - y1 \cdot i}}\right) \cdot \left(\left(\mathsf{fma}\left(x, j, \left(-z\right) \cdot k\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right) \cdot \sqrt[3]{\mathsf{fma}\left(b, y0, i \cdot \left(-y1\right)\right)}\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(-\left(y5 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right) \cdot y0\right) + y4 \cdot \left(y1 \cdot \mathsf{fma}\left(k, y2, y3 \cdot \left(-j\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(-i\right) \cdot \left(c \cdot \left(x \cdot y - t \cdot z\right)\right) + \left(b \cdot \left(x \cdot y - t \cdot z\right)\right) \cdot a\right) - \left(b \cdot y0 - y1 \cdot i\right) \cdot \left(x \cdot j - z \cdot k\right)\right) + \left(c \cdot y0 - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(c \cdot y4 - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \end{array}\]

Error

Target

Derivation

`if c < -1.520268482954331e-05`

`if -1.520268482954331e-05 < c < -5.443632402079177e-107`

`if -5.443632402079177e-107 < c < -1.6589667466238724e-170`

`if -1.6589667466238724e-170 < c < 1.6451640527347206e-93`

`if 1.6451640527347206e-93 < c`

Reproduce