\[\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}\;a \le -3288986673738299426122743563600321839104:\\ \;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \left(y5 \cdot \left(\left(y3 \cdot a\right) \cdot y\right) - \mathsf{fma}\left(a, \left(y5 \cdot t\right) \cdot y2, \left(y3 \cdot \left(y \cdot c\right)\right) \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \left(\sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \left(\left(\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \sqrt[3]{y4 \cdot c - a \cdot y5}\right) \cdot \left(t \cdot y2 - y \cdot y3\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}\;a \le -3288986673738299426122743563600321839104:\\
\;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \left(y5 \cdot \left(\left(y3 \cdot a\right) \cdot y\right) - \mathsf{fma}\left(a, \left(y5 \cdot t\right) \cdot y2, \left(y3 \cdot \left(y \cdot c\right)\right) \cdot y4\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \left(\sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \left(\left(\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \sqrt[3]{y4 \cdot c - a \cdot y5}\right) \cdot \left(t \cdot y2 - y \cdot y3\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 r25184391 = x;
        double r25184392 = y;
        double r25184393 = r25184391 * r25184392;
        double r25184394 = z;
        double r25184395 = t;
        double r25184396 = r25184394 * r25184395;
        double r25184397 = r25184393 - r25184396;
        double r25184398 = a;
        double r25184399 = b;
        double r25184400 = r25184398 * r25184399;
        double r25184401 = c;
        double r25184402 = i;
        double r25184403 = r25184401 * r25184402;
        double r25184404 = r25184400 - r25184403;
        double r25184405 = r25184397 * r25184404;
        double r25184406 = j;
        double r25184407 = r25184391 * r25184406;
        double r25184408 = k;
        double r25184409 = r25184394 * r25184408;
        double r25184410 = r25184407 - r25184409;
        double r25184411 = y0;
        double r25184412 = r25184411 * r25184399;
        double r25184413 = y1;
        double r25184414 = r25184413 * r25184402;
        double r25184415 = r25184412 - r25184414;
        double r25184416 = r25184410 * r25184415;
        double r25184417 = r25184405 - r25184416;
        double r25184418 = y2;
        double r25184419 = r25184391 * r25184418;
        double r25184420 = y3;
        double r25184421 = r25184394 * r25184420;
        double r25184422 = r25184419 - r25184421;
        double r25184423 = r25184411 * r25184401;
        double r25184424 = r25184413 * r25184398;
        double r25184425 = r25184423 - r25184424;
        double r25184426 = r25184422 * r25184425;
        double r25184427 = r25184417 + r25184426;
        double r25184428 = r25184395 * r25184406;
        double r25184429 = r25184392 * r25184408;
        double r25184430 = r25184428 - r25184429;
        double r25184431 = y4;
        double r25184432 = r25184431 * r25184399;
        double r25184433 = y5;
        double r25184434 = r25184433 * r25184402;
        double r25184435 = r25184432 - r25184434;
        double r25184436 = r25184430 * r25184435;
        double r25184437 = r25184427 + r25184436;
        double r25184438 = r25184395 * r25184418;
        double r25184439 = r25184392 * r25184420;
        double r25184440 = r25184438 - r25184439;
        double r25184441 = r25184431 * r25184401;
        double r25184442 = r25184433 * r25184398;
        double r25184443 = r25184441 - r25184442;
        double r25184444 = r25184440 * r25184443;
        double r25184445 = r25184437 - r25184444;
        double r25184446 = r25184408 * r25184418;
        double r25184447 = r25184406 * r25184420;
        double r25184448 = r25184446 - r25184447;
        double r25184449 = r25184431 * r25184413;
        double r25184450 = r25184433 * r25184411;
        double r25184451 = r25184449 - r25184450;
        double r25184452 = r25184448 * r25184451;
        double r25184453 = r25184445 + r25184452;
        return r25184453;
}

↓

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 r25184454 = a;
        double r25184455 = -3.2889866737382994e+39;
        bool r25184456 = r25184454 <= r25184455;
        double r25184457 = y2;
        double r25184458 = k;
        double r25184459 = r25184457 * r25184458;
        double r25184460 = j;
        double r25184461 = y3;
        double r25184462 = r25184460 * r25184461;
        double r25184463 = r25184459 - r25184462;
        double r25184464 = y4;
        double r25184465 = y1;
        double r25184466 = r25184464 * r25184465;
        double r25184467 = y5;
        double r25184468 = y0;
        double r25184469 = r25184467 * r25184468;
        double r25184470 = r25184466 - r25184469;
        double r25184471 = r25184463 * r25184470;
        double r25184472 = c;
        double r25184473 = r25184472 * r25184468;
        double r25184474 = r25184454 * r25184465;
        double r25184475 = r25184473 - r25184474;
        double r25184476 = x;
        double r25184477 = r25184476 * r25184457;
        double r25184478 = z;
        double r25184479 = r25184478 * r25184461;
        double r25184480 = r25184477 - r25184479;
        double r25184481 = r25184475 * r25184480;
        double r25184482 = y;
        double r25184483 = r25184476 * r25184482;
        double r25184484 = t;
        double r25184485 = r25184484 * r25184478;
        double r25184486 = r25184483 - r25184485;
        double r25184487 = b;
        double r25184488 = r25184454 * r25184487;
        double r25184489 = i;
        double r25184490 = r25184489 * r25184472;
        double r25184491 = r25184488 - r25184490;
        double r25184492 = r25184486 * r25184491;
        double r25184493 = r25184476 * r25184460;
        double r25184494 = r25184478 * r25184458;
        double r25184495 = r25184493 - r25184494;
        double r25184496 = r25184487 * r25184468;
        double r25184497 = r25184489 * r25184465;
        double r25184498 = r25184496 - r25184497;
        double r25184499 = r25184495 * r25184498;
        double r25184500 = r25184492 - r25184499;
        double r25184501 = r25184481 + r25184500;
        double r25184502 = r25184460 * r25184484;
        double r25184503 = r25184482 * r25184458;
        double r25184504 = r25184502 - r25184503;
        double r25184505 = r25184464 * r25184487;
        double r25184506 = r25184489 * r25184467;
        double r25184507 = r25184505 - r25184506;
        double r25184508 = r25184504 * r25184507;
        double r25184509 = r25184501 + r25184508;
        double r25184510 = r25184461 * r25184454;
        double r25184511 = r25184510 * r25184482;
        double r25184512 = r25184467 * r25184511;
        double r25184513 = r25184467 * r25184484;
        double r25184514 = r25184513 * r25184457;
        double r25184515 = r25184482 * r25184472;
        double r25184516 = r25184461 * r25184515;
        double r25184517 = r25184516 * r25184464;
        double r25184518 = fma(r25184454, r25184514, r25184517);
        double r25184519 = r25184512 - r25184518;
        double r25184520 = r25184509 - r25184519;
        double r25184521 = r25184471 + r25184520;
        double r25184522 = r25184464 * r25184472;
        double r25184523 = r25184454 * r25184467;
        double r25184524 = r25184522 - r25184523;
        double r25184525 = r25184484 * r25184457;
        double r25184526 = r25184482 * r25184461;
        double r25184527 = r25184525 - r25184526;
        double r25184528 = r25184524 * r25184527;
        double r25184529 = cbrt(r25184528);
        double r25184530 = cbrt(r25184524);
        double r25184531 = r25184530 * r25184530;
        double r25184532 = r25184531 * r25184527;
        double r25184533 = r25184530 * r25184532;
        double r25184534 = cbrt(r25184533);
        double r25184535 = r25184529 * r25184534;
        double r25184536 = r25184529 * r25184535;
        double r25184537 = r25184509 - r25184536;
        double r25184538 = r25184471 + r25184537;
        double r25184539 = r25184456 ? r25184521 : r25184538;
        return r25184539;
}

Target

Original	26.4
Target	30.1
Herbie	26.8

\[\begin{array}{l} \mathbf{if}\;y4 \lt -7.206256231996481342319540724063498925423 \cdot 10^{60}:\\ \;\;\;\;\left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right)\right) - \left(\frac{y2 \cdot t - y3 \cdot y}{\frac{1}{y4 \cdot c - y5 \cdot a}} - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\\ \mathbf{elif}\;y4 \lt -3.364603505246316896676998939327711644754 \cdot 10^{-66}:\\ \;\;\;\;\left(\left(\left(\left(t \cdot c\right) \cdot \left(i \cdot z\right) - \left(a \cdot t\right) \cdot \left(b \cdot z\right)\right) - \left(y \cdot c\right) \cdot \left(i \cdot x\right)\right) - \left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right)\right) + \left(\left(y0 \cdot c - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) - \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - a \cdot y5\right) - \left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right)\right)\right)\\ \mathbf{elif}\;y4 \lt -1.200006505568611600888263862102883004513 \cdot 10^{-105}:\\ \;\;\;\;\left(\left(\left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) - \left(y3 \cdot y\right) \cdot \left(y5 \cdot a - y4 \cdot c\right)\right) + \left(\left(y5 \cdot a\right) \cdot \left(t \cdot y2\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) - \left(\left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right) - \left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 6.718963124057494636349617318198742025856 \cdot 10^{-279}:\\ \;\;\;\;\left(\left(\left(\left(k \cdot y\right) \cdot \left(y5 \cdot i\right) - \left(y \cdot b\right) \cdot \left(y4 \cdot k\right)\right) - \left(y5 \cdot t\right) \cdot \left(i \cdot j\right)\right) - \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right) - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(y2 \cdot x - y3 \cdot z\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 4.779626814037919873410686589412258835104 \cdot 10^{-222}:\\ \;\;\;\;\left(\left(\left(j \cdot t - k \cdot y\right) \cdot \left(y4 \cdot b - y5 \cdot i\right) - \left(y3 \cdot y\right) \cdot \left(y5 \cdot a - y4 \cdot c\right)\right) + \left(\left(y5 \cdot a\right) \cdot \left(t \cdot y2\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - a \cdot y1\right) - \left(\left(b \cdot y0 - i \cdot y1\right) \cdot \left(j \cdot x - k \cdot z\right) - \left(y \cdot x - z \cdot t\right) \cdot \left(b \cdot a - i \cdot c\right)\right)\right)\\ \mathbf{elif}\;y4 \lt 2.285224154126683459205023499639872822811 \cdot 10^{-175}:\\ \;\;\;\;\left(\left(\left(\left(k \cdot y\right) \cdot \left(y5 \cdot i\right) - \left(y \cdot b\right) \cdot \left(y4 \cdot k\right)\right) - \left(y5 \cdot t\right) \cdot \left(i \cdot j\right)\right) - \left(\left(y2 \cdot t - y3 \cdot y\right) \cdot \left(y4 \cdot c - y5 \cdot a\right) - \left(y2 \cdot k - y3 \cdot j\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\right)\right) + \left(\left(b \cdot a - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(j \cdot x - k \cdot z\right) \cdot \left(y0 \cdot b - i \cdot y1\right) - \left(y2 \cdot x - y3 \cdot z\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(k \cdot \left(i \cdot \left(z \cdot y1\right)\right) - \left(j \cdot \left(i \cdot \left(x \cdot y1\right)\right) + y0 \cdot \left(k \cdot \left(z \cdot b\right)\right)\right)\right)\right) + \left(z \cdot \left(y3 \cdot \left(a \cdot y1\right)\right) - \left(y2 \cdot \left(x \cdot \left(a \cdot y1\right)\right) + y0 \cdot \left(z \cdot \left(c \cdot y3\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)\\ \end{array}\]

Derivation

Split input into 2 regimes
if a < -3.2889866737382994e+39
1. Initial program 28.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. Taylor expanded around inf 27.7
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \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(a \cdot \left(y3 \cdot \left(y \cdot y5\right)\right) - \left(y3 \cdot \left(y4 \cdot \left(c \cdot y\right)\right) + a \cdot \left(y2 \cdot \left(t \cdot y5\right)\right)\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
3. Simplified30.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 \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) - \color{blue}{\left(\left(\left(a \cdot y3\right) \cdot y\right) \cdot y5 - \mathsf{fma}\left(a, y2 \cdot \left(y5 \cdot t\right), \left(y3 \cdot \left(c \cdot y\right)\right) \cdot y4\right)\right)}\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
if -3.2889866737382994e+39 < a
1. Initial program 26.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 add-cube-cbrt26.2
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \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(\sqrt[3]{\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)} \cdot \sqrt[3]{\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)}\right) \cdot \sqrt[3]{\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. Using strategy rm
5. Applied add-cube-cbrt26.2
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \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(\sqrt[3]{\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)} \cdot \sqrt[3]{\left(t \cdot y2 - y \cdot y3\right) \cdot \color{blue}{\left(\left(\sqrt[3]{y4 \cdot c - y5 \cdot a} \cdot \sqrt[3]{y4 \cdot c - y5 \cdot a}\right) \cdot \sqrt[3]{y4 \cdot c - y5 \cdot a}\right)}}\right) \cdot \sqrt[3]{\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. Applied associate-*r*26.2
  \[\leadsto \left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \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(\sqrt[3]{\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)} \cdot \sqrt[3]{\color{blue}{\left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(\sqrt[3]{y4 \cdot c - y5 \cdot a} \cdot \sqrt[3]{y4 \cdot c - y5 \cdot a}\right)\right) \cdot \sqrt[3]{y4 \cdot c - y5 \cdot a}}}\right) \cdot \sqrt[3]{\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)\]
Recombined 2 regimes into one program.
Final simplification26.8
\[\leadsto \begin{array}{l} \mathbf{if}\;a \le -3288986673738299426122743563600321839104:\\ \;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \left(y5 \cdot \left(\left(y3 \cdot a\right) \cdot y\right) - \mathsf{fma}\left(a, \left(y5 \cdot t\right) \cdot y2, \left(y3 \cdot \left(y \cdot c\right)\right) \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right) + \left(\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - z \cdot y3\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(b \cdot y0 - i \cdot y1\right)\right)\right) + \left(j \cdot t - y \cdot k\right) \cdot \left(y4 \cdot b - i \cdot y5\right)\right) - \sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \left(\sqrt[3]{\left(y4 \cdot c - a \cdot y5\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \left(\left(\sqrt[3]{y4 \cdot c - a \cdot y5} \cdot \sqrt[3]{y4 \cdot c - a \cdot y5}\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)}\right)\right)\\ \end{array}\]

Reproduce

herbie shell --seed 2019170 +o rules:numerics
(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"

  :herbie-target
  (if (< y4 -7.206256231996481e+60) (- (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))))) (- (/ (- (* y2 t) (* y3 y)) (/ 1.0 (- (* y4 c) (* y5 a)))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (if (< y4 -3.364603505246317e-66) (+ (- (- (- (* (* t c) (* i z)) (* (* a t) (* b z))) (* (* y c) (* i x))) (* (- (* b y0) (* i y1)) (- (* j x) (* k z)))) (- (* (- (* y0 c) (* a y1)) (- (* x y2) (* z y3))) (- (* (- (* t y2) (* y y3)) (- (* y4 c) (* a y5))) (* (- (* y1 y4) (* y5 y0)) (- (* k y2) (* j y3)))))) (if (< y4 -1.2000065055686116e-105) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 6.718963124057495e-279) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (if (< y4 4.77962681403792e-222) (+ (+ (- (* (- (* j t) (* k y)) (- (* y4 b) (* y5 i))) (* (* y3 y) (- (* y5 a) (* y4 c)))) (+ (* (* y5 a) (* t y2)) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* x y2) (* z y3)) (- (* c y0) (* a y1))) (- (* (- (* b y0) (* i y1)) (- (* j x) (* k z))) (* (- (* y x) (* z t)) (- (* b a) (* i c)))))) (if (< y4 2.2852241541266835e-175) (+ (- (- (- (* (* k y) (* y5 i)) (* (* y b) (* y4 k))) (* (* y5 t) (* i j))) (- (* (- (* y2 t) (* y3 y)) (- (* y4 c) (* y5 a))) (* (- (* y2 k) (* y3 j)) (- (* y4 y1) (* y5 y0))))) (- (* (- (* b a) (* i c)) (- (* y x) (* t z))) (- (* (- (* j x) (* k z)) (- (* y0 b) (* i y1))) (* (- (* y2 x) (* y3 z)) (- (* c y0) (* y1 a)))))) (+ (- (+ (+ (- (* (- (* x y) (* z t)) (- (* a b) (* c i))) (- (* k (* i (* z y1))) (+ (* j (* i (* x y1))) (* y0 (* k (* z b)))))) (- (* z (* y3 (* a y1))) (+ (* y2 (* x (* a y1))) (* y0 (* z (* c y3)))))) (* (- (* t j) (* y k)) (- (* y4 b) (* y5 i)))) (* (- (* t y2) (* y y3)) (- (* y4 c) (* y5 a)))) (* (- (* k y2) (* j y3)) (- (* y4 y1) (* y5 y0))))))))))

  (+ (- (+ (+ (- (* (- (* 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)))))

Error

Target

Derivation

`if a < -3.2889866737382994e+39`

`if -3.2889866737382994e+39 < a`

Reproduce