Average Error: 26.6 → 28.9
Time: 1.9m
Precision: 64
\[\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}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le -5.212201362120861737639528461196706285071 \cdot 10^{-300}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(\left(i \cdot \left(y \cdot y5\right)\right) \cdot k - y5 \cdot \left(t \cdot \left(i \cdot j\right)\right)\right) - \left(y \cdot \left(b \cdot y4\right)\right) \cdot k\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.631852305333888237634247798553947975175 \cdot 10^{-100}:\\ \;\;\;\;\left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right) + \left(\left(a \cdot y1\right) \cdot \left(-\left(x \cdot y2 - y3 \cdot z\right)\right) + \left(c \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.579949190118836318625873998095204368512 \cdot 10^{-46}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(y5 \cdot \left(-\left(t \cdot y2 - y \cdot y3\right) \cdot a\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot y4\right) \cdot c\right)\right) + \left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right)\\ \mathbf{elif}\;y3 \le 9.090613409892616259914995320157486017171 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(k \cdot \left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) + j \cdot \left(\left(-x\right) \cdot \left(y0 \cdot b - i \cdot y1\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right) \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(i \cdot y5\right) \cdot \left(-\left(t \cdot j - y \cdot k\right)\right) + \left(y4 \cdot \left(t \cdot j - y \cdot k\right)\right) \cdot b\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \end{array}\]
\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)
↓
\begin{array}{l}
\mathbf{if}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\
\;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\

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

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

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

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

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

\end{array}
double f(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
        double r149890 = x;
        double r149891 = y;
        double r149892 = r149890 * r149891;
        double r149893 = z;
        double r149894 = t;
        double r149895 = r149893 * r149894;
        double r149896 = r149892 - r149895;
        double r149897 = a;
        double r149898 = b;
        double r149899 = r149897 * r149898;
        double r149900 = c;
        double r149901 = i;
        double r149902 = r149900 * r149901;
        double r149903 = r149899 - r149902;
        double r149904 = r149896 * r149903;
        double r149905 = j;
        double r149906 = r149890 * r149905;
        double r149907 = k;
        double r149908 = r149893 * r149907;
        double r149909 = r149906 - r149908;
        double r149910 = y0;
        double r149911 = r149910 * r149898;
        double r149912 = y1;
        double r149913 = r149912 * r149901;
        double r149914 = r149911 - r149913;
        double r149915 = r149909 * r149914;
        double r149916 = r149904 - r149915;
        double r149917 = y2;
        double r149918 = r149890 * r149917;
        double r149919 = y3;
        double r149920 = r149893 * r149919;
        double r149921 = r149918 - r149920;
        double r149922 = r149910 * r149900;
        double r149923 = r149912 * r149897;
        double r149924 = r149922 - r149923;
        double r149925 = r149921 * r149924;
        double r149926 = r149916 + r149925;
        double r149927 = r149894 * r149905;
        double r149928 = r149891 * r149907;
        double r149929 = r149927 - r149928;
        double r149930 = y4;
        double r149931 = r149930 * r149898;
        double r149932 = y5;
        double r149933 = r149932 * r149901;
        double r149934 = r149931 - r149933;
        double r149935 = r149929 * r149934;
        double r149936 = r149926 + r149935;
        double r149937 = r149894 * r149917;
        double r149938 = r149891 * r149919;
        double r149939 = r149937 - r149938;
        double r149940 = r149930 * r149900;
        double r149941 = r149932 * r149897;
        double r149942 = r149940 - r149941;
        double r149943 = r149939 * r149942;
        double r149944 = r149936 - r149943;
        double r149945 = r149907 * r149917;
        double r149946 = r149905 * r149919;
        double r149947 = r149945 - r149946;
        double r149948 = r149930 * r149912;
        double r149949 = r149932 * r149910;
        double r149950 = r149948 - r149949;
        double r149951 = r149947 * r149950;
        double r149952 = r149944 + r149951;
        return r149952;
}
↓
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 r149953 = y3;
        double r149954 = -7.037329032246424e-139;
        bool r149955 = r149953 <= r149954;
        double r149956 = c;
        double r149957 = y0;
        double r149958 = r149956 * r149957;
        double r149959 = a;
        double r149960 = y1;
        double r149961 = r149959 * r149960;
        double r149962 = r149958 - r149961;
        double r149963 = x;
        double r149964 = y2;
        double r149965 = r149963 * r149964;
        double r149966 = z;
        double r149967 = r149953 * r149966;
        double r149968 = r149965 - r149967;
        double r149969 = r149962 * r149968;
        double r149970 = k;
        double r149971 = r149970 * r149964;
        double r149972 = j;
        double r149973 = r149972 * r149953;
        double r149974 = r149971 - r149973;
        double r149975 = y4;
        double r149976 = r149960 * r149975;
        double r149977 = y5;
        double r149978 = r149977 * r149957;
        double r149979 = r149976 - r149978;
        double r149980 = r149974 * r149979;
        double r149981 = r149969 + r149980;
        double r149982 = b;
        double r149983 = r149959 * r149982;
        double r149984 = i;
        double r149985 = r149984 * r149956;
        double r149986 = r149983 - r149985;
        double r149987 = y;
        double r149988 = r149987 * r149963;
        double r149989 = t;
        double r149990 = r149989 * r149966;
        double r149991 = r149988 - r149990;
        double r149992 = r149986 * r149991;
        double r149993 = r149957 * r149982;
        double r149994 = r149984 * r149960;
        double r149995 = r149993 - r149994;
        double r149996 = r149963 * r149995;
        double r149997 = r149996 * r149972;
        double r149998 = r149995 * r149966;
        double r149999 = r149998 * r149970;
        double r150000 = -r149999;
        double r150001 = r149997 + r150000;
        double r150002 = r149992 - r150001;
        double r150003 = r149981 + r150002;
        double r150004 = r149989 * r149972;
        double r150005 = r149987 * r149970;
        double r150006 = r150004 - r150005;
        double r150007 = r149982 * r149975;
        double r150008 = r149984 * r149977;
        double r150009 = r150007 - r150008;
        double r150010 = r150006 * r150009;
        double r150011 = r149987 * r149977;
        double r150012 = r149953 * r150011;
        double r150013 = r150012 * r149959;
        double r150014 = r149964 * r149959;
        double r150015 = r149989 * r149977;
        double r150016 = r150014 * r150015;
        double r150017 = r150013 - r150016;
        double r150018 = r149956 * r149975;
        double r150019 = r150018 * r149987;
        double r150020 = r150019 * r149953;
        double r150021 = r150017 - r150020;
        double r150022 = r150010 - r150021;
        double r150023 = r150003 + r150022;
        double r150024 = -5.212201362120862e-300;
        bool r150025 = r149953 <= r150024;
        double r150026 = r149984 * r150011;
        double r150027 = r150026 * r149970;
        double r150028 = r149984 * r149972;
        double r150029 = r149989 * r150028;
        double r150030 = r149977 * r150029;
        double r150031 = r150027 - r150030;
        double r150032 = r149987 * r150007;
        double r150033 = r150032 * r149970;
        double r150034 = r150031 - r150033;
        double r150035 = r149977 * r149959;
        double r150036 = r150018 - r150035;
        double r150037 = r149989 * r149964;
        double r150038 = r149987 * r149953;
        double r150039 = r150037 - r150038;
        double r150040 = r150036 * r150039;
        double r150041 = r150034 - r150040;
        double r150042 = r150003 + r150041;
        double r150043 = 1.6318523053338882e-100;
        bool r150044 = r149953 <= r150043;
        double r150045 = -r149968;
        double r150046 = r149961 * r150045;
        double r150047 = r149956 * r149968;
        double r150048 = r150047 * r149957;
        double r150049 = r150046 + r150048;
        double r150050 = r149980 + r150049;
        double r150051 = r149963 * r149972;
        double r150052 = r149970 * r149966;
        double r150053 = r150051 - r150052;
        double r150054 = r149995 * r150053;
        double r150055 = r149992 - r150054;
        double r150056 = r150050 + r150055;
        double r150057 = r150010 - r150040;
        double r150058 = r150056 + r150057;
        double r150059 = 1.5799491901188363e-46;
        bool r150060 = r149953 <= r150059;
        double r150061 = r150039 * r149959;
        double r150062 = -r150061;
        double r150063 = r149977 * r150062;
        double r150064 = r150039 * r149975;
        double r150065 = r150064 * r149956;
        double r150066 = r150063 + r150065;
        double r150067 = r150010 - r150066;
        double r150068 = r150067 + r150003;
        double r150069 = 9.090613409892616e-26;
        bool r150070 = r149953 <= r150069;
        double r150071 = r149970 * r149998;
        double r150072 = -r149963;
        double r150073 = r150072 * r149995;
        double r150074 = r149972 * r150073;
        double r150075 = r150071 + r150074;
        double r150076 = r149981 + r150075;
        double r150077 = cbrt(r150040);
        double r150078 = r150077 * r150077;
        double r150079 = r150078 * r150077;
        double r150080 = r150010 - r150079;
        double r150081 = r150076 + r150080;
        double r150082 = -r150006;
        double r150083 = r150008 * r150082;
        double r150084 = r149975 * r150006;
        double r150085 = r150084 * r149982;
        double r150086 = r150083 + r150085;
        double r150087 = r150086 - r150040;
        double r150088 = r150003 + r150087;
        double r150089 = r150070 ? r150081 : r150088;
        double r150090 = r150060 ? r150068 : r150089;
        double r150091 = r150044 ? r150058 : r150090;
        double r150092 = r150025 ? r150042 : r150091;
        double r150093 = r149955 ? r150023 : r150092;
        return r150093;
}

Error

Bits error versus x

Bits error versus y

Bits error versus z

Bits error versus t

Bits error versus a

Bits error versus b

Bits error versus c

Bits error versus i

Bits error versus j

Bits error versus k

Bits error versus y0

Bits error versus y1

Bits error versus y2

Bits error versus y3

Bits error versus y4

Bits error versus y5

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Split input into 6 regimes

  2. if y3 < -7.037329032246424e-139

    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. Simplified25.4

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

    4. Applied sub-neg25.4

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

    5. Applied distribute-lft-in25.4

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

    6. Simplified26.2

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

    7. Simplified26.4

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

    8. Taylor expanded around inf 29.3

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

    9. Simplified29.6

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

    if -7.037329032246424e-139 < y3 < -5.212201362120862e-300

    1. Initial program 27.1

      \[\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. Simplified27.1

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

    4. Applied sub-neg27.1

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

    5. Applied distribute-lft-in27.1

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

    6. Simplified27.6

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

    7. Simplified28.4

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

    8. Taylor expanded around inf 32.2

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

    9. Simplified31.8

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

    if -5.212201362120862e-300 < y3 < 1.6318523053338882e-100

    1. Initial program 27.1

      \[\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. Simplified27.1

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

    4. Applied sub-neg27.1

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

    5. Applied distribute-lft-in27.1

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

    6. Simplified26.8

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

    7. Simplified26.8

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

    if 1.6318523053338882e-100 < y3 < 1.5799491901188363e-46

    1. Initial program 22.6

      \[\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. Simplified22.6

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

    4. Applied sub-neg22.6

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

    5. Applied distribute-lft-in22.6

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

    6. Simplified23.4

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

    7. Simplified23.7

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

    9. Applied sub-neg23.7

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

    10. Applied distribute-lft-in23.7

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

    11. Simplified24.2

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

    12. Simplified24.0

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

    if 1.5799491901188363e-46 < y3 < 9.090613409892616e-26

    1. Initial program 28.1

      \[\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. Simplified28.1

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

    4. Applied sub-neg28.1

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

    5. Applied distribute-lft-in28.1

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

    6. Simplified27.1

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

    7. Simplified26.7

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

    9. Applied add-cube-cbrt26.8

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

    10. Simplified26.8

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

    11. Simplified26.8

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

    12. Taylor expanded around 0 28.9

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

    if 9.090613409892616e-26 < y3

    1. Initial program 28.1

      \[\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. Simplified28.1

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

    4. Applied sub-neg28.1

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

    5. Applied distribute-lft-in28.1

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

    6. Simplified29.0

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

    7. Simplified29.0

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

    9. Applied sub-neg29.0

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

    10. Applied distribute-lft-in29.0

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

    11. Simplified28.8

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

    12. Simplified28.8

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

  4. Final simplification28.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le -5.212201362120861737639528461196706285071 \cdot 10^{-300}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(\left(i \cdot \left(y \cdot y5\right)\right) \cdot k - y5 \cdot \left(t \cdot \left(i \cdot j\right)\right)\right) - \left(y \cdot \left(b \cdot y4\right)\right) \cdot k\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.631852305333888237634247798553947975175 \cdot 10^{-100}:\\ \;\;\;\;\left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right) + \left(\left(a \cdot y1\right) \cdot \left(-\left(x \cdot y2 - y3 \cdot z\right)\right) + \left(c \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.579949190118836318625873998095204368512 \cdot 10^{-46}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(y5 \cdot \left(-\left(t \cdot y2 - y \cdot y3\right) \cdot a\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot y4\right) \cdot c\right)\right) + \left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right)\\ \mathbf{elif}\;y3 \le 9.090613409892616259914995320157486017171 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(k \cdot \left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) + j \cdot \left(\left(-x\right) \cdot \left(y0 \cdot b - i \cdot y1\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right) \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(\left(y0 \cdot b - i \cdot y1\right) \cdot z\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(i \cdot y5\right) \cdot \left(-\left(t \cdot j - y \cdot k\right)\right) + \left(y4 \cdot \left(t \cdot j - y \cdot k\right)\right) \cdot b\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019179 
(FPCore (x y z t a b c i j k y0 y1 y2 y3 y4 y5)
  :name "Linear.Matrix:det44 from linear-1.19.1.3"
  (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (* (- (* x j) (* z k)) (- (* y0 b) (* y1 i)))) (* (- (* x y2) (* z y3)) (- (* y0 c) (* y1 a)))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0)))))