Average Error: 27.3 → 28.7
Time: 1.7m
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 -5786491170666683947777798438912:\\ \;\;\;\;\left(\left(\left(\left(b \cdot y4\right) \cdot \left(j \cdot t - y \cdot k\right) + \left(i \cdot \left(j \cdot t - y \cdot k\right)\right) \cdot \left(-y5\right)\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(\left(-c\right) \cdot \left(\left(x \cdot y - z \cdot t\right) \cdot i\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right)\\ \mathbf{elif}\;y0 \le -8.786125919528224793905083657034450831039 \cdot 10^{-224}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y5 \cdot \left(y0 \cdot j\right)\right) \cdot y3 - \left(j \cdot \left(y4 \cdot y3\right)\right) \cdot y1\right) - \left(y0 \cdot \left(y5 \cdot y2\right)\right) \cdot k\right)\\ \mathbf{elif}\;y0 \le -1.387344368902326401165044648447173965079 \cdot 10^{-285}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(\left(-c\right) \cdot \left(\left(x \cdot y - z \cdot t\right) \cdot i\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right) + \left(i \cdot \left(\left(y \cdot k\right) \cdot y5\right) - \left(\left(y \cdot b\right) \cdot \left(y4 \cdot k\right) + \left(t \cdot i\right) \cdot \left(j \cdot y5\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right)\\ \mathbf{elif}\;y0 \le 3.154737685128260050578032978426267444435 \cdot 10^{-259}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(a \cdot \left(\left(y1 \cdot z\right) \cdot y3 - y2 \cdot \left(y1 \cdot x\right)\right) - y3 \cdot \left(\left(c \cdot z\right) \cdot y0\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right) + \left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(\left(\left(t \cdot y2 - y3 \cdot y\right) \cdot c\right) \cdot y4 + a \cdot \left(\left(t \cdot y2 - y3 \cdot y\right) \cdot \left(-y5\right)\right)\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 -5786491170666683947777798438912:\\
\;\;\;\;\left(\left(\left(\left(b \cdot y4\right) \cdot \left(j \cdot t - y \cdot k\right) + \left(i \cdot \left(j \cdot t - y \cdot k\right)\right) \cdot \left(-y5\right)\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(\left(-c\right) \cdot \left(\left(x \cdot y - z \cdot t\right) \cdot i\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right)\\

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

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

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

\mathbf{else}:\\
\;\;\;\;\left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right) + \left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(\left(\left(t \cdot y2 - y3 \cdot y\right) \cdot c\right) \cdot y4 + a \cdot \left(\left(t \cdot y2 - y3 \cdot y\right) \cdot \left(-y5\right)\right)\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 r137111 = x;
        double r137112 = y;
        double r137113 = r137111 * r137112;
        double r137114 = z;
        double r137115 = t;
        double r137116 = r137114 * r137115;
        double r137117 = r137113 - r137116;
        double r137118 = a;
        double r137119 = b;
        double r137120 = r137118 * r137119;
        double r137121 = c;
        double r137122 = i;
        double r137123 = r137121 * r137122;
        double r137124 = r137120 - r137123;
        double r137125 = r137117 * r137124;
        double r137126 = j;
        double r137127 = r137111 * r137126;
        double r137128 = k;
        double r137129 = r137114 * r137128;
        double r137130 = r137127 - r137129;
        double r137131 = y0;
        double r137132 = r137131 * r137119;
        double r137133 = y1;
        double r137134 = r137133 * r137122;
        double r137135 = r137132 - r137134;
        double r137136 = r137130 * r137135;
        double r137137 = r137125 - r137136;
        double r137138 = y2;
        double r137139 = r137111 * r137138;
        double r137140 = y3;
        double r137141 = r137114 * r137140;
        double r137142 = r137139 - r137141;
        double r137143 = r137131 * r137121;
        double r137144 = r137133 * r137118;
        double r137145 = r137143 - r137144;
        double r137146 = r137142 * r137145;
        double r137147 = r137137 + r137146;
        double r137148 = r137115 * r137126;
        double r137149 = r137112 * r137128;
        double r137150 = r137148 - r137149;
        double r137151 = y4;
        double r137152 = r137151 * r137119;
        double r137153 = y5;
        double r137154 = r137153 * r137122;
        double r137155 = r137152 - r137154;
        double r137156 = r137150 * r137155;
        double r137157 = r137147 + r137156;
        double r137158 = r137115 * r137138;
        double r137159 = r137112 * r137140;
        double r137160 = r137158 - r137159;
        double r137161 = r137151 * r137121;
        double r137162 = r137153 * r137118;
        double r137163 = r137161 - r137162;
        double r137164 = r137160 * r137163;
        double r137165 = r137157 - r137164;
        double r137166 = r137128 * r137138;
        double r137167 = r137126 * r137140;
        double r137168 = r137166 - r137167;
        double r137169 = r137151 * r137133;
        double r137170 = r137153 * r137131;
        double r137171 = r137169 - r137170;
        double r137172 = r137168 * r137171;
        double r137173 = r137165 + r137172;
        return r137173;
}
↓
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 r137174 = y0;
        double r137175 = -5.786491170666684e+30;
        bool r137176 = r137174 <= r137175;
        double r137177 = b;
        double r137178 = y4;
        double r137179 = r137177 * r137178;
        double r137180 = j;
        double r137181 = t;
        double r137182 = r137180 * r137181;
        double r137183 = y;
        double r137184 = k;
        double r137185 = r137183 * r137184;
        double r137186 = r137182 - r137185;
        double r137187 = r137179 * r137186;
        double r137188 = i;
        double r137189 = r137188 * r137186;
        double r137190 = y5;
        double r137191 = -r137190;
        double r137192 = r137189 * r137191;
        double r137193 = r137187 + r137192;
        double r137194 = c;
        double r137195 = r137174 * r137194;
        double r137196 = a;
        double r137197 = y1;
        double r137198 = r137196 * r137197;
        double r137199 = r137195 - r137198;
        double r137200 = y2;
        double r137201 = x;
        double r137202 = r137200 * r137201;
        double r137203 = z;
        double r137204 = y3;
        double r137205 = r137203 * r137204;
        double r137206 = r137202 - r137205;
        double r137207 = r137199 * r137206;
        double r137208 = -r137194;
        double r137209 = r137201 * r137183;
        double r137210 = r137203 * r137181;
        double r137211 = r137209 - r137210;
        double r137212 = r137211 * r137188;
        double r137213 = r137208 * r137212;
        double r137214 = r137211 * r137177;
        double r137215 = r137214 * r137196;
        double r137216 = r137213 + r137215;
        double r137217 = r137201 * r137180;
        double r137218 = r137184 * r137203;
        double r137219 = r137217 - r137218;
        double r137220 = r137177 * r137219;
        double r137221 = r137174 * r137220;
        double r137222 = -r137188;
        double r137223 = r137197 * r137219;
        double r137224 = r137222 * r137223;
        double r137225 = r137221 + r137224;
        double r137226 = r137216 - r137225;
        double r137227 = r137207 + r137226;
        double r137228 = r137193 + r137227;
        double r137229 = r137178 * r137194;
        double r137230 = r137190 * r137196;
        double r137231 = r137229 - r137230;
        double r137232 = r137181 * r137200;
        double r137233 = r137204 * r137183;
        double r137234 = r137232 - r137233;
        double r137235 = r137231 * r137234;
        double r137236 = r137228 - r137235;
        double r137237 = r137200 * r137184;
        double r137238 = r137180 * r137204;
        double r137239 = r137237 - r137238;
        double r137240 = -r137239;
        double r137241 = r137190 * r137174;
        double r137242 = r137240 * r137241;
        double r137243 = r137239 * r137197;
        double r137244 = r137243 * r137178;
        double r137245 = r137242 + r137244;
        double r137246 = r137236 + r137245;
        double r137247 = -8.786125919528225e-224;
        bool r137248 = r137174 <= r137247;
        double r137249 = r137188 * r137190;
        double r137250 = r137179 - r137249;
        double r137251 = r137186 * r137250;
        double r137252 = r137196 * r137177;
        double r137253 = r137194 * r137188;
        double r137254 = r137252 - r137253;
        double r137255 = r137211 * r137254;
        double r137256 = r137255 - r137225;
        double r137257 = r137207 + r137256;
        double r137258 = r137251 + r137257;
        double r137259 = r137258 - r137235;
        double r137260 = r137174 * r137180;
        double r137261 = r137190 * r137260;
        double r137262 = r137261 * r137204;
        double r137263 = r137178 * r137204;
        double r137264 = r137180 * r137263;
        double r137265 = r137264 * r137197;
        double r137266 = r137262 - r137265;
        double r137267 = r137190 * r137200;
        double r137268 = r137174 * r137267;
        double r137269 = r137268 * r137184;
        double r137270 = r137266 - r137269;
        double r137271 = r137259 + r137270;
        double r137272 = -1.3873443689023264e-285;
        bool r137273 = r137174 <= r137272;
        double r137274 = r137185 * r137190;
        double r137275 = r137188 * r137274;
        double r137276 = r137183 * r137177;
        double r137277 = r137178 * r137184;
        double r137278 = r137276 * r137277;
        double r137279 = r137181 * r137188;
        double r137280 = r137180 * r137190;
        double r137281 = r137279 * r137280;
        double r137282 = r137278 + r137281;
        double r137283 = r137275 - r137282;
        double r137284 = r137227 + r137283;
        double r137285 = r137284 - r137235;
        double r137286 = r137285 + r137245;
        double r137287 = 3.15473768512826e-259;
        bool r137288 = r137174 <= r137287;
        double r137289 = r137177 * r137174;
        double r137290 = r137188 * r137197;
        double r137291 = r137289 - r137290;
        double r137292 = r137291 * r137219;
        double r137293 = r137255 - r137292;
        double r137294 = r137197 * r137203;
        double r137295 = r137294 * r137204;
        double r137296 = r137197 * r137201;
        double r137297 = r137200 * r137296;
        double r137298 = r137295 - r137297;
        double r137299 = r137196 * r137298;
        double r137300 = r137194 * r137203;
        double r137301 = r137300 * r137174;
        double r137302 = r137204 * r137301;
        double r137303 = r137299 - r137302;
        double r137304 = r137293 + r137303;
        double r137305 = r137251 + r137304;
        double r137306 = r137305 - r137235;
        double r137307 = r137197 * r137178;
        double r137308 = r137307 - r137241;
        double r137309 = r137239 * r137308;
        double r137310 = r137306 + r137309;
        double r137311 = r137234 * r137194;
        double r137312 = r137311 * r137178;
        double r137313 = r137234 * r137191;
        double r137314 = r137196 * r137313;
        double r137315 = r137312 + r137314;
        double r137316 = r137258 - r137315;
        double r137317 = r137245 + r137316;
        double r137318 = r137288 ? r137310 : r137317;
        double r137319 = r137273 ? r137286 : r137318;
        double r137320 = r137248 ? r137271 : r137319;
        double r137321 = r137176 ? r137246 : r137320;
        return r137321;
}

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

  2. if y0 < -5.786491170666684e+30

    1. Initial program 30.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. Using strategy rm

    3. Applied sub-neg30.6

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

    4. Applied distribute-lft-in30.6

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

    5. Simplified27.8

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

    6. Simplified27.8

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

    8. Applied sub-neg27.8

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

    9. Applied distribute-lft-in27.8

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

    10. Simplified27.4

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

    11. Simplified27.4

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

    13. Applied sub-neg27.4

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

    14. Applied distribute-lft-in27.4

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

    15. Simplified27.2

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

    16. Simplified27.4

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

    18. Applied sub-neg27.4

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

    19. Applied distribute-lft-in27.4

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

    20. Simplified27.4

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

    21. Simplified27.8

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

    if -5.786491170666684e+30 < y0 < -8.786125919528225e-224

    1. Initial program 25.7

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

    3. Applied sub-neg25.7

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

    4. Applied distribute-lft-in25.7

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

    5. Simplified26.6

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

    6. Simplified26.9

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

    7. Taylor expanded around inf 29.0

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

    8. Simplified29.9

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

    if -8.786125919528225e-224 < y0 < -1.3873443689023264e-285

    1. Initial program 27.0

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

    3. Applied sub-neg27.0

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

    4. Applied distribute-lft-in27.0

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

    5. Simplified29.1

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

    6. Simplified29.5

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

    8. Applied sub-neg29.5

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

    9. Applied distribute-lft-in29.5

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

    10. Simplified29.2

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

    11. Simplified29.2

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

    13. Applied sub-neg29.2

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

    14. Applied distribute-lft-in29.2

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

    15. Simplified29.5

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

    16. Simplified29.1

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

    17. Taylor expanded around inf 32.8

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

    18. Simplified31.9

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

    if -1.3873443689023264e-285 < y0 < 3.15473768512826e-259

    1. Initial program 26.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. Taylor expanded around inf 27.0

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

    3. Simplified29.0

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

    if 3.15473768512826e-259 < y0

    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. Using strategy rm

    3. Applied sub-neg27.1

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

    4. Applied distribute-lft-in27.1

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

    5. Simplified27.3

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

    6. Simplified27.3

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

    8. Applied sub-neg27.3

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

    9. Applied distribute-lft-in27.3

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

    10. Simplified27.2

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

    11. Simplified27.2

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

    13. Applied sub-neg27.2

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

    14. Applied distribute-lft-in27.2

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

    15. Simplified27.4

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

    16. Simplified27.7

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

  4. Final simplification28.7

    \[\leadsto \begin{array}{l} \mathbf{if}\;y0 \le -5786491170666683947777798438912:\\ \;\;\;\;\left(\left(\left(\left(b \cdot y4\right) \cdot \left(j \cdot t - y \cdot k\right) + \left(i \cdot \left(j \cdot t - y \cdot k\right)\right) \cdot \left(-y5\right)\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(\left(-c\right) \cdot \left(\left(x \cdot y - z \cdot t\right) \cdot i\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right)\\ \mathbf{elif}\;y0 \le -8.786125919528224793905083657034450831039 \cdot 10^{-224}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(\left(y5 \cdot \left(y0 \cdot j\right)\right) \cdot y3 - \left(j \cdot \left(y4 \cdot y3\right)\right) \cdot y1\right) - \left(y0 \cdot \left(y5 \cdot y2\right)\right) \cdot k\right)\\ \mathbf{elif}\;y0 \le -1.387344368902326401165044648447173965079 \cdot 10^{-285}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(\left(-c\right) \cdot \left(\left(x \cdot y - z \cdot t\right) \cdot i\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot b\right) \cdot a\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right) + \left(i \cdot \left(\left(y \cdot k\right) \cdot y5\right) - \left(\left(y \cdot b\right) \cdot \left(y4 \cdot k\right) + \left(t \cdot i\right) \cdot \left(j \cdot y5\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right)\\ \mathbf{elif}\;y0 \le 3.154737685128260050578032978426267444435 \cdot 10^{-259}:\\ \;\;\;\;\left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(a \cdot \left(\left(y1 \cdot z\right) \cdot y3 - y2 \cdot \left(y1 \cdot x\right)\right) - y3 \cdot \left(\left(c \cdot z\right) \cdot y0\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(-\left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(y5 \cdot y0\right) + \left(\left(y2 \cdot k - j \cdot y3\right) \cdot y1\right) \cdot y4\right) + \left(\left(\left(j \cdot t - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(y2 \cdot x - z \cdot y3\right) + \left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(y0 \cdot \left(b \cdot \left(x \cdot j - k \cdot z\right)\right) + \left(-i\right) \cdot \left(y1 \cdot \left(x \cdot j - k \cdot z\right)\right)\right)\right)\right)\right) - \left(\left(\left(t \cdot y2 - y3 \cdot y\right) \cdot c\right) \cdot y4 + a \cdot \left(\left(t \cdot y2 - y3 \cdot y\right) \cdot \left(-y5\right)\right)\right)\right)\\ \end{array}\]

Reproduce

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