Average Error: 27.0 → 28.9
Time: 1.6m
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}\;y0 \le 5.749763712456293113407547722630045171857 \cdot 10^{-291}:\\ \;\;\;\;\left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(-\left(b \cdot a - i \cdot c\right)\right) \cdot t\right) \cdot z + \left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right) + \left(\left(y2 \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot k + \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(j \cdot \left(-y3\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 6.775599914751334075033450717146304319597 \cdot 10^{-133}:\\ \;\;\;\;\left(\left(b \cdot y4 - y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(\left(i \cdot z\right) \cdot \left(y1 \cdot k\right) - x \cdot \left(\left(i \cdot y1\right) \cdot j\right)\right) - z \cdot \left(y0 \cdot \left(k \cdot b\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 3.752462145591352509949230881744242858799 \cdot 10^{-114}:\\ \;\;\;\;\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right) + \left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(j \cdot \left(-y3\right)\right)\right)\right)\right) + \left(\left(b \cdot y4 - y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le 1.754288039130151086263759757107990974195 \cdot 10^{-20}:\\ \;\;\;\;\left(\left(\left(-\left(t \cdot \left(y5 \cdot \left(i \cdot j\right)\right) - \left(y \cdot y5\right) \cdot \left(i \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x + \left(z \cdot t\right) \cdot \left(-\left(b \cdot a - i \cdot c\right)\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right)\\ \mathbf{elif}\;y0 \le 230996834181259362304:\\ \;\;\;\;\left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(\left(b \cdot y0 - i \cdot y1\right) \cdot x\right) \cdot j + k \cdot \left(z \cdot \left(-\left(b \cdot y0 - i \cdot y1\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 4.937292836495024929351098438929698850087 \cdot 10^{123}:\\ \;\;\;\;\left(\left(\left(\left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x + \left(z \cdot t\right) \cdot \left(-\left(b \cdot a - i \cdot c\right)\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(\left(y2 \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot k + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot j\right) \cdot \left(-y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \end{array}\]
\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)
↓
\begin{array}{l}
\mathbf{if}\;y0 \le 5.749763712456293113407547722630045171857 \cdot 10^{-291}:\\
\;\;\;\;\left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(-\left(b \cdot a - i \cdot c\right)\right) \cdot t\right) \cdot z + \left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right) + \left(\left(y2 \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot k + \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(j \cdot \left(-y3\right)\right)\right)\right)\right)\\

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

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

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

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

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

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

\end{array}
double f(double x, double y, double z, double t, double a, double b, double c, double i, double j, double k, double y0, double y1, double y2, double y3, double y4, double y5) {
        double r138016 = x;
        double r138017 = y;
        double r138018 = r138016 * r138017;
        double r138019 = z;
        double r138020 = t;
        double r138021 = r138019 * r138020;
        double r138022 = r138018 - r138021;
        double r138023 = a;
        double r138024 = b;
        double r138025 = r138023 * r138024;
        double r138026 = c;
        double r138027 = i;
        double r138028 = r138026 * r138027;
        double r138029 = r138025 - r138028;
        double r138030 = r138022 * r138029;
        double r138031 = j;
        double r138032 = r138016 * r138031;
        double r138033 = k;
        double r138034 = r138019 * r138033;
        double r138035 = r138032 - r138034;
        double r138036 = y0;
        double r138037 = r138036 * r138024;
        double r138038 = y1;
        double r138039 = r138038 * r138027;
        double r138040 = r138037 - r138039;
        double r138041 = r138035 * r138040;
        double r138042 = r138030 - r138041;
        double r138043 = y2;
        double r138044 = r138016 * r138043;
        double r138045 = y3;
        double r138046 = r138019 * r138045;
        double r138047 = r138044 - r138046;
        double r138048 = r138036 * r138026;
        double r138049 = r138038 * r138023;
        double r138050 = r138048 - r138049;
        double r138051 = r138047 * r138050;
        double r138052 = r138042 + r138051;
        double r138053 = r138020 * r138031;
        double r138054 = r138017 * r138033;
        double r138055 = r138053 - r138054;
        double r138056 = y4;
        double r138057 = r138056 * r138024;
        double r138058 = y5;
        double r138059 = r138058 * r138027;
        double r138060 = r138057 - r138059;
        double r138061 = r138055 * r138060;
        double r138062 = r138052 + r138061;
        double r138063 = r138020 * r138043;
        double r138064 = r138017 * r138045;
        double r138065 = r138063 - r138064;
        double r138066 = r138056 * r138026;
        double r138067 = r138058 * r138023;
        double r138068 = r138066 - r138067;
        double r138069 = r138065 * r138068;
        double r138070 = r138062 - r138069;
        double r138071 = r138033 * r138043;
        double r138072 = r138031 * r138045;
        double r138073 = r138071 - r138072;
        double r138074 = r138056 * r138038;
        double r138075 = r138058 * r138036;
        double r138076 = r138074 - r138075;
        double r138077 = r138073 * r138076;
        double r138078 = r138070 + r138077;
        return r138078;
}
↓
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 r138079 = y0;
        double r138080 = 5.749763712456293e-291;
        bool r138081 = r138079 <= r138080;
        double r138082 = t;
        double r138083 = j;
        double r138084 = r138082 * r138083;
        double r138085 = y;
        double r138086 = k;
        double r138087 = r138085 * r138086;
        double r138088 = r138084 - r138087;
        double r138089 = y5;
        double r138090 = -r138089;
        double r138091 = i;
        double r138092 = r138090 * r138091;
        double r138093 = r138088 * r138092;
        double r138094 = y4;
        double r138095 = r138088 * r138094;
        double r138096 = b;
        double r138097 = r138095 * r138096;
        double r138098 = r138093 + r138097;
        double r138099 = c;
        double r138100 = r138094 * r138099;
        double r138101 = a;
        double r138102 = r138089 * r138101;
        double r138103 = r138100 - r138102;
        double r138104 = y2;
        double r138105 = r138082 * r138104;
        double r138106 = y3;
        double r138107 = r138106 * r138085;
        double r138108 = r138105 - r138107;
        double r138109 = r138103 * r138108;
        double r138110 = r138098 - r138109;
        double r138111 = r138096 * r138101;
        double r138112 = r138091 * r138099;
        double r138113 = r138111 - r138112;
        double r138114 = -r138113;
        double r138115 = r138114 * r138082;
        double r138116 = z;
        double r138117 = r138115 * r138116;
        double r138118 = r138085 * r138113;
        double r138119 = x;
        double r138120 = r138118 * r138119;
        double r138121 = r138117 + r138120;
        double r138122 = r138096 * r138079;
        double r138123 = y1;
        double r138124 = r138091 * r138123;
        double r138125 = r138122 - r138124;
        double r138126 = r138119 * r138083;
        double r138127 = r138086 * r138116;
        double r138128 = r138126 - r138127;
        double r138129 = r138125 * r138128;
        double r138130 = r138121 - r138129;
        double r138131 = r138104 * r138119;
        double r138132 = r138116 * r138106;
        double r138133 = r138131 - r138132;
        double r138134 = r138079 * r138099;
        double r138135 = r138101 * r138123;
        double r138136 = r138134 - r138135;
        double r138137 = r138133 * r138136;
        double r138138 = r138123 * r138094;
        double r138139 = r138089 * r138079;
        double r138140 = r138138 - r138139;
        double r138141 = r138104 * r138140;
        double r138142 = r138141 * r138086;
        double r138143 = -r138106;
        double r138144 = r138083 * r138143;
        double r138145 = r138140 * r138144;
        double r138146 = r138142 + r138145;
        double r138147 = r138137 + r138146;
        double r138148 = r138130 + r138147;
        double r138149 = r138110 + r138148;
        double r138150 = 6.775599914751334e-133;
        bool r138151 = r138079 <= r138150;
        double r138152 = r138096 * r138094;
        double r138153 = r138089 * r138091;
        double r138154 = r138152 - r138153;
        double r138155 = r138154 * r138088;
        double r138156 = r138155 - r138109;
        double r138157 = r138104 * r138086;
        double r138158 = r138083 * r138106;
        double r138159 = r138157 - r138158;
        double r138160 = r138140 * r138159;
        double r138161 = r138160 + r138137;
        double r138162 = r138085 * r138119;
        double r138163 = r138116 * r138082;
        double r138164 = r138162 - r138163;
        double r138165 = r138164 * r138113;
        double r138166 = r138091 * r138116;
        double r138167 = r138123 * r138086;
        double r138168 = r138166 * r138167;
        double r138169 = r138124 * r138083;
        double r138170 = r138119 * r138169;
        double r138171 = r138168 - r138170;
        double r138172 = r138086 * r138096;
        double r138173 = r138079 * r138172;
        double r138174 = r138116 * r138173;
        double r138175 = r138171 - r138174;
        double r138176 = r138165 - r138175;
        double r138177 = r138161 + r138176;
        double r138178 = r138156 + r138177;
        double r138179 = 3.7524621455913525e-114;
        bool r138180 = r138079 <= r138179;
        double r138181 = r138165 - r138129;
        double r138182 = r138140 * r138086;
        double r138183 = r138104 * r138182;
        double r138184 = r138183 + r138145;
        double r138185 = r138137 + r138184;
        double r138186 = r138181 + r138185;
        double r138187 = r138186 + r138156;
        double r138188 = 1.754288039130151e-20;
        bool r138189 = r138079 <= r138188;
        double r138190 = r138091 * r138083;
        double r138191 = r138089 * r138190;
        double r138192 = r138082 * r138191;
        double r138193 = r138085 * r138089;
        double r138194 = r138091 * r138086;
        double r138195 = r138193 * r138194;
        double r138196 = r138192 - r138195;
        double r138197 = -r138196;
        double r138198 = r138197 + r138097;
        double r138199 = r138198 - r138109;
        double r138200 = r138163 * r138114;
        double r138201 = r138120 + r138200;
        double r138202 = r138201 - r138129;
        double r138203 = r138202 + r138161;
        double r138204 = r138199 + r138203;
        double r138205 = 2.3099683418125936e+20;
        bool r138206 = r138079 <= r138205;
        double r138207 = r138125 * r138119;
        double r138208 = r138207 * r138083;
        double r138209 = -r138125;
        double r138210 = r138116 * r138209;
        double r138211 = r138086 * r138210;
        double r138212 = r138208 + r138211;
        double r138213 = r138165 - r138212;
        double r138214 = r138161 + r138213;
        double r138215 = r138110 + r138214;
        double r138216 = 4.937292836495025e+123;
        bool r138217 = r138079 <= r138216;
        double r138218 = r138140 * r138083;
        double r138219 = r138218 * r138143;
        double r138220 = r138142 + r138219;
        double r138221 = r138220 + r138137;
        double r138222 = r138202 + r138221;
        double r138223 = r138222 + r138110;
        double r138224 = -r138129;
        double r138225 = r138224 + r138161;
        double r138226 = r138225 + r138110;
        double r138227 = r138217 ? r138223 : r138226;
        double r138228 = r138206 ? r138215 : r138227;
        double r138229 = r138189 ? r138204 : r138228;
        double r138230 = r138180 ? r138187 : r138229;
        double r138231 = r138151 ? r138178 : r138230;
        double r138232 = r138081 ? r138149 : r138231;
        return r138232;
}

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 7 regimes

  2. if y0 < 5.749763712456293e-291

    1. Initial program 27.2

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

    2. Simplified27.2

      \[\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.2

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in27.2

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified27.4

      \[\leadsto \left(\left(\color{blue}{b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified27.4

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \color{blue}{\left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Using strategy rm

    9. Applied sub-neg27.4

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

    10. Applied distribute-lft-in27.4

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

    11. Simplified28.2

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

    12. Simplified28.2

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(x \cdot \left(y \cdot \left(b \cdot a - c \cdot i\right)\right) + \color{blue}{\left(\left(-z\right) \cdot t\right) \cdot \left(b \cdot a - c \cdot i\right)}\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    13. Using strategy rm

    14. Applied sub-neg28.2

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

    15. Applied distribute-lft-in28.2

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

    16. Simplified28.5

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

    17. Simplified28.5

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

    19. Applied associate-*l*28.7

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

    20. Simplified28.7

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

    if 5.749763712456293e-291 < y0 < 6.775599914751334e-133

    1. Initial program 27.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. Simplified27.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. Taylor expanded around inf 30.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) - \color{blue}{\left(i \cdot \left(z \cdot \left(y1 \cdot k\right)\right) - \left(x \cdot \left(y1 \cdot \left(j \cdot i\right)\right) + y0 \cdot \left(z \cdot \left(b \cdot k\right)\right)\right)\right)}\right)\right)\]

    4. Simplified29.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(\left(i \cdot z\right) \cdot \left(k \cdot y1\right) - \left(j \cdot \left(y1 \cdot i\right)\right) \cdot x\right) - \left(y0 \cdot \left(k \cdot b\right)\right) \cdot z\right)}\right)\right)\]

    if 6.775599914751334e-133 < y0 < 3.7524621455913525e-114

    1. Initial program 28.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. Simplified28.8

      \[\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.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 \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in28.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(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified28.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(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot k\right) \cdot y2} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified28.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(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot k\right) \cdot y2 + \color{blue}{\left(\left(-y3\right) \cdot j\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)}\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    if 3.7524621455913525e-114 < y0 < 1.754288039130151e-20

    1. Initial program 22.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. Simplified22.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-neg22.1

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in22.1

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified22.3

      \[\leadsto \left(\left(\color{blue}{b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified22.3

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \color{blue}{\left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Using strategy rm

    9. Applied sub-neg22.3

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

    10. Applied distribute-lft-in22.3

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

    11. Simplified23.1

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

    12. Simplified23.1

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

    13. Taylor expanded around inf 25.5

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

    14. Simplified25.8

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

    if 1.754288039130151e-20 < y0 < 2.3099683418125936e+20

    1. Initial program 22.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. Simplified22.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-neg22.4

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in22.4

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified22.9

      \[\leadsto \left(\left(\color{blue}{b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified22.9

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \color{blue}{\left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Using strategy rm

    9. Applied sub-neg22.9

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

    10. Applied distribute-lft-in22.9

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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) - \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)\]

    11. Simplified23.9

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

    12. Simplified24.4

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

    if 2.3099683418125936e+20 < y0 < 4.937292836495025e+123

    1. Initial program 26.4

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

    2. Simplified26.4

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

    4. Applied sub-neg26.4

      \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in26.4

      \[\leadsto \left(\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified26.9

      \[\leadsto \left(\left(\color{blue}{b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified26.9

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \color{blue}{\left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    8. Using strategy rm

    9. Applied sub-neg26.9

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

    10. Applied distribute-lft-in26.9

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

    11. Simplified27.5

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

    12. Simplified27.5

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(x \cdot \left(y \cdot \left(b \cdot a - c \cdot i\right)\right) + \color{blue}{\left(\left(-z\right) \cdot t\right) \cdot \left(b \cdot a - c \cdot i\right)}\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
    13. Using strategy rm

    14. Applied sub-neg27.5

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

    15. Applied distribute-lft-in27.5

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

    16. Simplified29.0

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

    17. Simplified29.0

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

    19. Applied associate-*l*29.7

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

    20. Simplified29.7

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

    if 4.937292836495025e+123 < y0

    1. Initial program 32.2

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

    2. Simplified32.2

      \[\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-neg32.2

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    5. Applied distribute-lft-in32.2

      \[\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    6. Simplified33.0

      \[\leadsto \left(\left(\color{blue}{b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\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(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]

    7. Simplified33.0

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

    8. Taylor expanded around 0 34.6

      \[\leadsto \left(\left(b \cdot \left(y4 \cdot \left(t \cdot j - k \cdot y\right)\right) + \left(-\left(i \cdot y5\right) \cdot \left(t \cdot j - k \cdot y\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(\color{blue}{0} - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
  3. Recombined 7 regimes into one program.

  4. Final simplification28.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;y0 \le 5.749763712456293113407547722630045171857 \cdot 10^{-291}:\\ \;\;\;\;\left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(\left(-\left(b \cdot a - i \cdot c\right)\right) \cdot t\right) \cdot z + \left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right) + \left(\left(y2 \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot k + \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(j \cdot \left(-y3\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 6.775599914751334075033450717146304319597 \cdot 10^{-133}:\\ \;\;\;\;\left(\left(b \cdot y4 - y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(\left(i \cdot z\right) \cdot \left(y1 \cdot k\right) - x \cdot \left(\left(i \cdot y1\right) \cdot j\right)\right) - z \cdot \left(y0 \cdot \left(k \cdot b\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 3.752462145591352509949230881744242858799 \cdot 10^{-114}:\\ \;\;\;\;\left(\left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right) + \left(y2 \cdot \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot k\right) + \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(j \cdot \left(-y3\right)\right)\right)\right)\right) + \left(\left(b \cdot y4 - y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{elif}\;y0 \le 1.754288039130151086263759757107990974195 \cdot 10^{-20}:\\ \;\;\;\;\left(\left(\left(-\left(t \cdot \left(y5 \cdot \left(i \cdot j\right)\right) - \left(y \cdot y5\right) \cdot \left(i \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(\left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x + \left(z \cdot t\right) \cdot \left(-\left(b \cdot a - i \cdot c\right)\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right)\\ \mathbf{elif}\;y0 \le 230996834181259362304:\\ \;\;\;\;\left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right) + \left(\left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right) - \left(\left(\left(b \cdot y0 - i \cdot y1\right) \cdot x\right) \cdot j + k \cdot \left(z \cdot \left(-\left(b \cdot y0 - i \cdot y1\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;y0 \le 4.937292836495024929351098438929698850087 \cdot 10^{123}:\\ \;\;\;\;\left(\left(\left(\left(y \cdot \left(b \cdot a - i \cdot c\right)\right) \cdot x + \left(z \cdot t\right) \cdot \left(-\left(b \cdot a - i \cdot c\right)\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(\left(y2 \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot k + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot j\right) \cdot \left(-y3\right)\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right)\right) + \left(\left(\left(t \cdot j - y \cdot k\right) \cdot \left(\left(-y5\right) \cdot i\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot y4\right) \cdot b\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019195 
(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)))))