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

↓

\[\begin{array}{l} \mathbf{if}\;y4 \le -5.251989081102843998303817495533040824814 \cdot 10^{-102}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right) + \left(\left(y5 \cdot \left(j \cdot t - k \cdot y\right)\right) \cdot \left(-i\right) + y4 \cdot \left(b \cdot \left(j \cdot t - k \cdot y\right)\right)\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le -1.928340879078260545478042674485809270234 \cdot 10^{-260}:\\ \;\;\;\;\left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right) + \left(\left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - k \cdot y\right)\right)\\ \mathbf{elif}\;y4 \le 1.006085650983031288358764710016604798395 \cdot 10^{-180}:\\ \;\;\;\;\left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right) + \left(\left(\left(\left(\left(y5 \cdot k\right) \cdot i\right) \cdot y - \left(\left(b \cdot y4\right) \cdot \left(k \cdot y\right) + \left(i \cdot j\right) \cdot \left(y5 \cdot t\right)\right)\right) + \left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right)\right) - \left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right) + \left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(-i\right)\right) \cdot c + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - k \cdot y\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\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}\;y4 \le -5.251989081102843998303817495533040824814 \cdot 10^{-102}:\\
\;\;\;\;\left(\left(\left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right) + \left(\left(y5 \cdot \left(j \cdot t - k \cdot y\right)\right) \cdot \left(-i\right) + y4 \cdot \left(b \cdot \left(j \cdot t - k \cdot y\right)\right)\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right)\\

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

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

\mathbf{else}:\\
\;\;\;\;\left(\left(\left(\left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right) + \left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(-i\right)\right) \cdot c + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - k \cdot y\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\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 r434742 = x;
        double r434743 = y;
        double r434744 = r434742 * r434743;
        double r434745 = z;
        double r434746 = t;
        double r434747 = r434745 * r434746;
        double r434748 = r434744 - r434747;
        double r434749 = a;
        double r434750 = b;
        double r434751 = r434749 * r434750;
        double r434752 = c;
        double r434753 = i;
        double r434754 = r434752 * r434753;
        double r434755 = r434751 - r434754;
        double r434756 = r434748 * r434755;
        double r434757 = j;
        double r434758 = r434742 * r434757;
        double r434759 = k;
        double r434760 = r434745 * r434759;
        double r434761 = r434758 - r434760;
        double r434762 = y0;
        double r434763 = r434762 * r434750;
        double r434764 = y1;
        double r434765 = r434764 * r434753;
        double r434766 = r434763 - r434765;
        double r434767 = r434761 * r434766;
        double r434768 = r434756 - r434767;
        double r434769 = y2;
        double r434770 = r434742 * r434769;
        double r434771 = y3;
        double r434772 = r434745 * r434771;
        double r434773 = r434770 - r434772;
        double r434774 = r434762 * r434752;
        double r434775 = r434764 * r434749;
        double r434776 = r434774 - r434775;
        double r434777 = r434773 * r434776;
        double r434778 = r434768 + r434777;
        double r434779 = r434746 * r434757;
        double r434780 = r434743 * r434759;
        double r434781 = r434779 - r434780;
        double r434782 = y4;
        double r434783 = r434782 * r434750;
        double r434784 = y5;
        double r434785 = r434784 * r434753;
        double r434786 = r434783 - r434785;
        double r434787 = r434781 * r434786;
        double r434788 = r434778 + r434787;
        double r434789 = r434746 * r434769;
        double r434790 = r434743 * r434771;
        double r434791 = r434789 - r434790;
        double r434792 = r434782 * r434752;
        double r434793 = r434784 * r434749;
        double r434794 = r434792 - r434793;
        double r434795 = r434791 * r434794;
        double r434796 = r434788 - r434795;
        double r434797 = r434759 * r434769;
        double r434798 = r434757 * r434771;
        double r434799 = r434797 - r434798;
        double r434800 = r434782 * r434764;
        double r434801 = r434784 * r434762;
        double r434802 = r434800 - r434801;
        double r434803 = r434799 * r434802;
        double r434804 = r434796 + r434803;
        return r434804;
}

↓

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 r434805 = y4;
        double r434806 = -5.251989081102844e-102;
        bool r434807 = r434805 <= r434806;
        double r434808 = y;
        double r434809 = x;
        double r434810 = r434808 * r434809;
        double r434811 = z;
        double r434812 = t;
        double r434813 = r434811 * r434812;
        double r434814 = r434810 - r434813;
        double r434815 = c;
        double r434816 = i;
        double r434817 = -r434816;
        double r434818 = r434815 * r434817;
        double r434819 = r434814 * r434818;
        double r434820 = b;
        double r434821 = r434814 * r434820;
        double r434822 = a;
        double r434823 = r434821 * r434822;
        double r434824 = r434819 + r434823;
        double r434825 = y0;
        double r434826 = r434820 * r434825;
        double r434827 = y1;
        double r434828 = r434816 * r434827;
        double r434829 = r434826 - r434828;
        double r434830 = j;
        double r434831 = r434809 * r434830;
        double r434832 = k;
        double r434833 = r434832 * r434811;
        double r434834 = r434831 - r434833;
        double r434835 = r434829 * r434834;
        double r434836 = r434824 - r434835;
        double r434837 = r434822 * r434827;
        double r434838 = y2;
        double r434839 = r434838 * r434809;
        double r434840 = y3;
        double r434841 = r434840 * r434811;
        double r434842 = r434839 - r434841;
        double r434843 = r434837 * r434842;
        double r434844 = -r434843;
        double r434845 = r434842 * r434825;
        double r434846 = r434815 * r434845;
        double r434847 = r434844 + r434846;
        double r434848 = r434836 + r434847;
        double r434849 = y5;
        double r434850 = r434830 * r434812;
        double r434851 = r434832 * r434808;
        double r434852 = r434850 - r434851;
        double r434853 = r434849 * r434852;
        double r434854 = r434853 * r434817;
        double r434855 = r434820 * r434852;
        double r434856 = r434805 * r434855;
        double r434857 = r434854 + r434856;
        double r434858 = r434848 + r434857;
        double r434859 = r434838 * r434812;
        double r434860 = r434840 * r434808;
        double r434861 = r434859 - r434860;
        double r434862 = r434861 * r434815;
        double r434863 = r434805 * r434862;
        double r434864 = -r434849;
        double r434865 = r434864 * r434822;
        double r434866 = r434865 * r434861;
        double r434867 = r434863 + r434866;
        double r434868 = r434858 - r434867;
        double r434869 = r434827 * r434805;
        double r434870 = r434825 * r434849;
        double r434871 = r434869 - r434870;
        double r434872 = r434832 * r434838;
        double r434873 = r434840 * r434830;
        double r434874 = r434872 - r434873;
        double r434875 = r434871 * r434874;
        double r434876 = r434868 + r434875;
        double r434877 = -1.9283408790782605e-260;
        bool r434878 = r434805 <= r434877;
        double r434879 = r434820 * r434805;
        double r434880 = r434816 * r434849;
        double r434881 = r434879 - r434880;
        double r434882 = r434881 * r434852;
        double r434883 = r434848 + r434882;
        double r434884 = r434875 + r434883;
        double r434885 = 1.0060856509830313e-180;
        bool r434886 = r434805 <= r434885;
        double r434887 = r434849 * r434832;
        double r434888 = r434887 * r434816;
        double r434889 = r434888 * r434808;
        double r434890 = r434879 * r434851;
        double r434891 = r434816 * r434830;
        double r434892 = r434849 * r434812;
        double r434893 = r434891 * r434892;
        double r434894 = r434890 + r434893;
        double r434895 = r434889 - r434894;
        double r434896 = r434895 + r434848;
        double r434897 = r434805 * r434815;
        double r434898 = r434849 * r434822;
        double r434899 = r434897 - r434898;
        double r434900 = r434861 * r434899;
        double r434901 = r434896 - r434900;
        double r434902 = r434875 + r434901;
        double r434903 = r434814 * r434817;
        double r434904 = r434903 * r434815;
        double r434905 = r434904 + r434823;
        double r434906 = r434905 - r434835;
        double r434907 = r434847 + r434906;
        double r434908 = r434907 + r434882;
        double r434909 = r434908 - r434867;
        double r434910 = r434909 + r434875;
        double r434911 = r434886 ? r434902 : r434910;
        double r434912 = r434878 ? r434884 : r434911;
        double r434913 = r434807 ? r434876 : r434912;
        return r434913;
}

Original	27.2
Target	31.0
Herbie	27.9

Derivation

Split input into 4 regimes
if y4 < -5.251989081102844e-102
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. Using strategy rm
3. Applied sub-neg26.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 \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in26.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) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified27.3
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified27.3
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{blue}{\left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)}\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
7. Using strategy rm
8. Applied sub-neg27.3
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
9. Applied distribute-lft-in27.3
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
10. Simplified27.4
  \[\leadsto \left(\left(\left(\left(\left(\color{blue}{a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
11. Simplified27.4
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{\left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
12. Using strategy rm
13. Applied sub-neg27.4
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\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 \color{blue}{\left(y4 \cdot c + \left(-y5 \cdot a\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
14. Applied distribute-lft-in27.4
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \color{blue}{\left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-y5 \cdot a\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
15. Simplified26.5
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\color{blue}{\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4} + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-y5 \cdot a\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
16. Simplified26.5
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \color{blue}{\left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)}\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
17. Using strategy rm
18. Applied sub-neg26.5
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \color{blue}{\left(y4 \cdot b + \left(-y5 \cdot i\right)\right)}\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
19. Applied distribute-lft-in26.5
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \color{blue}{\left(\left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(-y5 \cdot i\right)\right)}\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
20. Simplified25.4
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(\color{blue}{\left(\left(j \cdot t - k \cdot y\right) \cdot b\right) \cdot y4} + \left(t \cdot j - y \cdot k\right) \cdot \left(-y5 \cdot i\right)\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
21. Simplified25.3
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(\left(\left(j \cdot t - k \cdot y\right) \cdot b\right) \cdot y4 + \color{blue}{\left(\left(j \cdot t - k \cdot y\right) \cdot y5\right) \cdot \left(-i\right)}\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if -5.251989081102844e-102 < y4 < -1.9283408790782605e-260
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 \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\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) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified26.9
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified26.9
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{blue}{\left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)}\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
7. Using strategy rm
8. Applied sub-neg26.9
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
9. Applied distribute-lft-in26.9
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
10. Simplified27.3
  \[\leadsto \left(\left(\left(\left(\left(\color{blue}{a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
11. Simplified27.3
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{\left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
12. Taylor expanded around 0 31.3
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \color{blue}{0}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if -1.9283408790782605e-260 < y4 < 1.0060856509830313e-180
1. Initial program 27.8
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Using strategy rm
3. Applied sub-neg27.8
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in27.8
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified27.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(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified27.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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{blue}{\left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)}\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
7. Using strategy rm
8. Applied sub-neg27.8
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
9. Applied distribute-lft-in27.8
  \[\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
10. Simplified28.7
  \[\leadsto \left(\left(\left(\left(\left(\color{blue}{a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
11. Simplified28.7
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{\left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
12. Taylor expanded around inf 29.2
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \color{blue}{\left(i \cdot \left(y \cdot \left(y5 \cdot k\right)\right) - \left(k \cdot \left(y \cdot \left(b \cdot y4\right)\right) + t \cdot \left(i \cdot \left(j \cdot y5\right)\right)\right)\right)}\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
13. Simplified30.2
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \color{blue}{\left(y \cdot \left(\left(k \cdot y5\right) \cdot i\right) - \left(\left(i \cdot j\right) \cdot \left(t \cdot y5\right) + \left(y \cdot k\right) \cdot \left(y4 \cdot b\right)\right)\right)}\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if 1.0060856509830313e-180 < y4
1. Initial program 27.3
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Using strategy rm
3. Applied sub-neg27.3
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in27.3
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified27.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(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified27.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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{blue}{\left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)}\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
7. Using strategy rm
8. 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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
9. 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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
10. Simplified28.1
  \[\leadsto \left(\left(\left(\left(\left(\color{blue}{a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\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(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
11. Simplified28.1
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{\left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
12. Using strategy rm
13. Applied sub-neg28.1
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\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 \color{blue}{\left(y4 \cdot c + \left(-y5 \cdot a\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
14. Applied distribute-lft-in28.1
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \color{blue}{\left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c\right) + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-y5 \cdot a\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
15. Simplified27.6
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\color{blue}{\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4} + \left(t \cdot y2 - y \cdot y3\right) \cdot \left(-y5 \cdot a\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
16. Simplified27.6
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \left(c \cdot \left(-i\right)\right) \cdot \left(y \cdot x - t \cdot z\right)\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \color{blue}{\left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)}\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
17. Using strategy rm
18. Applied associate-*l*27.0
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + \color{blue}{c \cdot \left(\left(-i\right) \cdot \left(y \cdot x - t \cdot z\right)\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
19. Simplified27.0
  \[\leadsto \left(\left(\left(\left(\left(a \cdot \left(b \cdot \left(y \cdot x - t \cdot z\right)\right) + c \cdot \color{blue}{\left(\left(y \cdot x - t \cdot z\right) \cdot \left(-i\right)\right)}\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(\left(-a\right) \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(\left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) \cdot y4 + \left(-\left(y2 \cdot t - y3 \cdot y\right)\right) \cdot \left(a \cdot y5\right)\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
Recombined 4 regimes into one program.
Final simplification27.9
\[\leadsto \begin{array}{l} \mathbf{if}\;y4 \le -5.251989081102843998303817495533040824814 \cdot 10^{-102}:\\ \;\;\;\;\left(\left(\left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right) + \left(\left(y5 \cdot \left(j \cdot t - k \cdot y\right)\right) \cdot \left(-i\right) + y4 \cdot \left(b \cdot \left(j \cdot t - k \cdot y\right)\right)\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right)\\ \mathbf{elif}\;y4 \le -1.928340879078260545478042674485809270234 \cdot 10^{-260}:\\ \;\;\;\;\left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right) + \left(\left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - k \cdot y\right)\right)\\ \mathbf{elif}\;y4 \le 1.006085650983031288358764710016604798395 \cdot 10^{-180}:\\ \;\;\;\;\left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right) + \left(\left(\left(\left(\left(y5 \cdot k\right) \cdot i\right) \cdot y - \left(\left(b \cdot y4\right) \cdot \left(k \cdot y\right) + \left(i \cdot j\right) \cdot \left(y5 \cdot t\right)\right)\right) + \left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(c \cdot \left(-i\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right)\right)\right) - \left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(-\left(a \cdot y1\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + c \cdot \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot y0\right)\right) + \left(\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(-i\right)\right) \cdot c + \left(\left(y \cdot x - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right)\right) + \left(b \cdot y4 - i \cdot y5\right) \cdot \left(j \cdot t - k \cdot y\right)\right) - \left(y4 \cdot \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot c\right) + \left(\left(-y5\right) \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right)\right) + \left(y1 \cdot y4 - y0 \cdot y5\right) \cdot \left(k \cdot y2 - y3 \cdot j\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y4 < -5.251989081102844e-102`

`if -5.251989081102844e-102 < y4 < -1.9283408790782605e-260`

`if -1.9283408790782605e-260 < y4 < 1.0060856509830313e-180`

`if 1.0060856509830313e-180 < y4`

Reproduce

In
Out