\[\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 r501185 = x;
        double r501186 = y;
        double r501187 = r501185 * r501186;
        double r501188 = z;
        double r501189 = t;
        double r501190 = r501188 * r501189;
        double r501191 = r501187 - r501190;
        double r501192 = a;
        double r501193 = b;
        double r501194 = r501192 * r501193;
        double r501195 = c;
        double r501196 = i;
        double r501197 = r501195 * r501196;
        double r501198 = r501194 - r501197;
        double r501199 = r501191 * r501198;
        double r501200 = j;
        double r501201 = r501185 * r501200;
        double r501202 = k;
        double r501203 = r501188 * r501202;
        double r501204 = r501201 - r501203;
        double r501205 = y0;
        double r501206 = r501205 * r501193;
        double r501207 = y1;
        double r501208 = r501207 * r501196;
        double r501209 = r501206 - r501208;
        double r501210 = r501204 * r501209;
        double r501211 = r501199 - r501210;
        double r501212 = y2;
        double r501213 = r501185 * r501212;
        double r501214 = y3;
        double r501215 = r501188 * r501214;
        double r501216 = r501213 - r501215;
        double r501217 = r501205 * r501195;
        double r501218 = r501207 * r501192;
        double r501219 = r501217 - r501218;
        double r501220 = r501216 * r501219;
        double r501221 = r501211 + r501220;
        double r501222 = r501189 * r501200;
        double r501223 = r501186 * r501202;
        double r501224 = r501222 - r501223;
        double r501225 = y4;
        double r501226 = r501225 * r501193;
        double r501227 = y5;
        double r501228 = r501227 * r501196;
        double r501229 = r501226 - r501228;
        double r501230 = r501224 * r501229;
        double r501231 = r501221 + r501230;
        double r501232 = r501189 * r501212;
        double r501233 = r501186 * r501214;
        double r501234 = r501232 - r501233;
        double r501235 = r501225 * r501195;
        double r501236 = r501227 * r501192;
        double r501237 = r501235 - r501236;
        double r501238 = r501234 * r501237;
        double r501239 = r501231 - r501238;
        double r501240 = r501202 * r501212;
        double r501241 = r501200 * r501214;
        double r501242 = r501240 - r501241;
        double r501243 = r501225 * r501207;
        double r501244 = r501227 * r501205;
        double r501245 = r501243 - r501244;
        double r501246 = r501242 * r501245;
        double r501247 = r501239 + r501246;
        return r501247;
}

↓

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 r501248 = y0;
        double r501249 = -5.786491170666684e+30;
        bool r501250 = r501248 <= r501249;
        double r501251 = b;
        double r501252 = y4;
        double r501253 = r501251 * r501252;
        double r501254 = j;
        double r501255 = t;
        double r501256 = r501254 * r501255;
        double r501257 = y;
        double r501258 = k;
        double r501259 = r501257 * r501258;
        double r501260 = r501256 - r501259;
        double r501261 = r501253 * r501260;
        double r501262 = i;
        double r501263 = r501262 * r501260;
        double r501264 = y5;
        double r501265 = -r501264;
        double r501266 = r501263 * r501265;
        double r501267 = r501261 + r501266;
        double r501268 = c;
        double r501269 = r501248 * r501268;
        double r501270 = a;
        double r501271 = y1;
        double r501272 = r501270 * r501271;
        double r501273 = r501269 - r501272;
        double r501274 = y2;
        double r501275 = x;
        double r501276 = r501274 * r501275;
        double r501277 = z;
        double r501278 = y3;
        double r501279 = r501277 * r501278;
        double r501280 = r501276 - r501279;
        double r501281 = r501273 * r501280;
        double r501282 = -r501268;
        double r501283 = r501275 * r501257;
        double r501284 = r501277 * r501255;
        double r501285 = r501283 - r501284;
        double r501286 = r501285 * r501262;
        double r501287 = r501282 * r501286;
        double r501288 = r501285 * r501251;
        double r501289 = r501288 * r501270;
        double r501290 = r501287 + r501289;
        double r501291 = r501275 * r501254;
        double r501292 = r501258 * r501277;
        double r501293 = r501291 - r501292;
        double r501294 = r501251 * r501293;
        double r501295 = r501248 * r501294;
        double r501296 = -r501262;
        double r501297 = r501271 * r501293;
        double r501298 = r501296 * r501297;
        double r501299 = r501295 + r501298;
        double r501300 = r501290 - r501299;
        double r501301 = r501281 + r501300;
        double r501302 = r501267 + r501301;
        double r501303 = r501252 * r501268;
        double r501304 = r501264 * r501270;
        double r501305 = r501303 - r501304;
        double r501306 = r501255 * r501274;
        double r501307 = r501278 * r501257;
        double r501308 = r501306 - r501307;
        double r501309 = r501305 * r501308;
        double r501310 = r501302 - r501309;
        double r501311 = r501274 * r501258;
        double r501312 = r501254 * r501278;
        double r501313 = r501311 - r501312;
        double r501314 = -r501313;
        double r501315 = r501264 * r501248;
        double r501316 = r501314 * r501315;
        double r501317 = r501313 * r501271;
        double r501318 = r501317 * r501252;
        double r501319 = r501316 + r501318;
        double r501320 = r501310 + r501319;
        double r501321 = -8.786125919528225e-224;
        bool r501322 = r501248 <= r501321;
        double r501323 = r501262 * r501264;
        double r501324 = r501253 - r501323;
        double r501325 = r501260 * r501324;
        double r501326 = r501270 * r501251;
        double r501327 = r501268 * r501262;
        double r501328 = r501326 - r501327;
        double r501329 = r501285 * r501328;
        double r501330 = r501329 - r501299;
        double r501331 = r501281 + r501330;
        double r501332 = r501325 + r501331;
        double r501333 = r501332 - r501309;
        double r501334 = r501248 * r501254;
        double r501335 = r501264 * r501334;
        double r501336 = r501335 * r501278;
        double r501337 = r501252 * r501278;
        double r501338 = r501254 * r501337;
        double r501339 = r501338 * r501271;
        double r501340 = r501336 - r501339;
        double r501341 = r501264 * r501274;
        double r501342 = r501248 * r501341;
        double r501343 = r501342 * r501258;
        double r501344 = r501340 - r501343;
        double r501345 = r501333 + r501344;
        double r501346 = -1.3873443689023264e-285;
        bool r501347 = r501248 <= r501346;
        double r501348 = r501259 * r501264;
        double r501349 = r501262 * r501348;
        double r501350 = r501257 * r501251;
        double r501351 = r501252 * r501258;
        double r501352 = r501350 * r501351;
        double r501353 = r501255 * r501262;
        double r501354 = r501254 * r501264;
        double r501355 = r501353 * r501354;
        double r501356 = r501352 + r501355;
        double r501357 = r501349 - r501356;
        double r501358 = r501301 + r501357;
        double r501359 = r501358 - r501309;
        double r501360 = r501359 + r501319;
        double r501361 = 3.15473768512826e-259;
        bool r501362 = r501248 <= r501361;
        double r501363 = r501251 * r501248;
        double r501364 = r501262 * r501271;
        double r501365 = r501363 - r501364;
        double r501366 = r501365 * r501293;
        double r501367 = r501329 - r501366;
        double r501368 = r501271 * r501277;
        double r501369 = r501368 * r501278;
        double r501370 = r501271 * r501275;
        double r501371 = r501274 * r501370;
        double r501372 = r501369 - r501371;
        double r501373 = r501270 * r501372;
        double r501374 = r501268 * r501277;
        double r501375 = r501374 * r501248;
        double r501376 = r501278 * r501375;
        double r501377 = r501373 - r501376;
        double r501378 = r501367 + r501377;
        double r501379 = r501325 + r501378;
        double r501380 = r501379 - r501309;
        double r501381 = r501271 * r501252;
        double r501382 = r501381 - r501315;
        double r501383 = r501313 * r501382;
        double r501384 = r501380 + r501383;
        double r501385 = r501308 * r501268;
        double r501386 = r501385 * r501252;
        double r501387 = r501308 * r501265;
        double r501388 = r501270 * r501387;
        double r501389 = r501386 + r501388;
        double r501390 = r501332 - r501389;
        double r501391 = r501319 + r501390;
        double r501392 = r501362 ? r501384 : r501391;
        double r501393 = r501347 ? r501360 : r501392;
        double r501394 = r501322 ? r501345 : r501393;
        double r501395 = r501250 ? r501320 : r501394;
        return r501395;
}

Original	27.3
Target	30.7
Herbie	28.7

Derivation

Split input into 5 regimes
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)\]
Recombined 5 regimes into one program.
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}\]

Error

Try it out

Target

Derivation

`if y0 < -5.786491170666684e+30`

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

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

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

`if 3.15473768512826e-259 < y0`

Reproduce

In
Out