\[\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}\;y5 \le -2.645872884294979270972396519223668320819 \cdot 10^{-7}:\\ \;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\right)\right)\\ \mathbf{elif}\;y5 \le -7.030729012634303785773879484609313612868 \cdot 10^{-117}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\left(\left(k \cdot \left(z \cdot y1\right)\right) \cdot i - \left(x \cdot y1\right) \cdot \left(i \cdot j\right)\right) - \left(b \cdot z\right) \cdot \left(y0 \cdot k\right)\right)\right) + \left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -2.973178669568692220900414141880610015231 \cdot 10^{-136}:\\ \;\;\;\;\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -3.545560197893551018782475666749631787843 \cdot 10^{-212}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(\left(i \cdot t\right) \cdot \left(c \cdot z\right) - \left(\left(y \cdot c\right) \cdot \left(i \cdot x\right) + \left(a \cdot \left(b \cdot t\right)\right) \cdot z\right)\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -2.134673394508608503697255936436163807406 \cdot 10^{-282}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\left(\left(k \cdot \left(z \cdot y1\right)\right) \cdot i - \left(x \cdot y1\right) \cdot \left(i \cdot j\right)\right) - \left(b \cdot z\right) \cdot \left(y0 \cdot k\right)\right)\right) + \left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le 4.458463361947369366431691027484730583643 \cdot 10^{-176}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(\left(\left(y3 \cdot \left(y5 \cdot j\right)\right) \cdot y0 - k \cdot \left(y2 \cdot \left(y0 \cdot y5\right)\right)\right) - y1 \cdot \left(j \cdot \left(y3 \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\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}\;y5 \le -2.645872884294979270972396519223668320819 \cdot 10^{-7}:\\
\;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\right)\right)\\

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

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

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

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

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

\mathbf{else}:\\
\;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\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 r517091 = x;
        double r517092 = y;
        double r517093 = r517091 * r517092;
        double r517094 = z;
        double r517095 = t;
        double r517096 = r517094 * r517095;
        double r517097 = r517093 - r517096;
        double r517098 = a;
        double r517099 = b;
        double r517100 = r517098 * r517099;
        double r517101 = c;
        double r517102 = i;
        double r517103 = r517101 * r517102;
        double r517104 = r517100 - r517103;
        double r517105 = r517097 * r517104;
        double r517106 = j;
        double r517107 = r517091 * r517106;
        double r517108 = k;
        double r517109 = r517094 * r517108;
        double r517110 = r517107 - r517109;
        double r517111 = y0;
        double r517112 = r517111 * r517099;
        double r517113 = y1;
        double r517114 = r517113 * r517102;
        double r517115 = r517112 - r517114;
        double r517116 = r517110 * r517115;
        double r517117 = r517105 - r517116;
        double r517118 = y2;
        double r517119 = r517091 * r517118;
        double r517120 = y3;
        double r517121 = r517094 * r517120;
        double r517122 = r517119 - r517121;
        double r517123 = r517111 * r517101;
        double r517124 = r517113 * r517098;
        double r517125 = r517123 - r517124;
        double r517126 = r517122 * r517125;
        double r517127 = r517117 + r517126;
        double r517128 = r517095 * r517106;
        double r517129 = r517092 * r517108;
        double r517130 = r517128 - r517129;
        double r517131 = y4;
        double r517132 = r517131 * r517099;
        double r517133 = y5;
        double r517134 = r517133 * r517102;
        double r517135 = r517132 - r517134;
        double r517136 = r517130 * r517135;
        double r517137 = r517127 + r517136;
        double r517138 = r517095 * r517118;
        double r517139 = r517092 * r517120;
        double r517140 = r517138 - r517139;
        double r517141 = r517131 * r517101;
        double r517142 = r517133 * r517098;
        double r517143 = r517141 - r517142;
        double r517144 = r517140 * r517143;
        double r517145 = r517137 - r517144;
        double r517146 = r517108 * r517118;
        double r517147 = r517106 * r517120;
        double r517148 = r517146 - r517147;
        double r517149 = r517131 * r517113;
        double r517150 = r517133 * r517111;
        double r517151 = r517149 - r517150;
        double r517152 = r517148 * r517151;
        double r517153 = r517145 + r517152;
        return r517153;
}

↓

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 r517154 = y5;
        double r517155 = -2.6458728842949793e-07;
        bool r517156 = r517154 <= r517155;
        double r517157 = i;
        double r517158 = r517154 * r517157;
        double r517159 = t;
        double r517160 = j;
        double r517161 = r517159 * r517160;
        double r517162 = y;
        double r517163 = k;
        double r517164 = r517162 * r517163;
        double r517165 = r517161 - r517164;
        double r517166 = r517158 * r517165;
        double r517167 = -r517166;
        double r517168 = y4;
        double r517169 = b;
        double r517170 = r517169 * r517165;
        double r517171 = r517168 * r517170;
        double r517172 = r517167 + r517171;
        double r517173 = y0;
        double r517174 = c;
        double r517175 = r517173 * r517174;
        double r517176 = y1;
        double r517177 = a;
        double r517178 = r517176 * r517177;
        double r517179 = r517175 - r517178;
        double r517180 = y2;
        double r517181 = x;
        double r517182 = r517180 * r517181;
        double r517183 = y3;
        double r517184 = z;
        double r517185 = r517183 * r517184;
        double r517186 = r517182 - r517185;
        double r517187 = r517179 * r517186;
        double r517188 = r517181 * r517162;
        double r517189 = r517159 * r517184;
        double r517190 = r517188 - r517189;
        double r517191 = r517177 * r517169;
        double r517192 = r517157 * r517174;
        double r517193 = r517191 - r517192;
        double r517194 = r517190 * r517193;
        double r517195 = r517173 * r517169;
        double r517196 = r517157 * r517176;
        double r517197 = r517195 - r517196;
        double r517198 = r517181 * r517160;
        double r517199 = r517184 * r517163;
        double r517200 = r517198 - r517199;
        double r517201 = r517197 * r517200;
        double r517202 = r517194 - r517201;
        double r517203 = r517187 + r517202;
        double r517204 = r517172 + r517203;
        double r517205 = r517168 * r517174;
        double r517206 = r517154 * r517177;
        double r517207 = r517205 - r517206;
        double r517208 = r517180 * r517159;
        double r517209 = r517183 * r517162;
        double r517210 = r517208 - r517209;
        double r517211 = r517207 * r517210;
        double r517212 = r517204 - r517211;
        double r517213 = r517180 * r517163;
        double r517214 = r517160 * r517183;
        double r517215 = r517213 - r517214;
        double r517216 = r517168 * r517215;
        double r517217 = r517176 * r517216;
        double r517218 = r517173 * r517215;
        double r517219 = -r517154;
        double r517220 = r517218 * r517219;
        double r517221 = r517217 + r517220;
        double r517222 = r517212 + r517221;
        double r517223 = -7.030729012634304e-117;
        bool r517224 = r517154 <= r517223;
        double r517225 = r517184 * r517176;
        double r517226 = r517163 * r517225;
        double r517227 = r517226 * r517157;
        double r517228 = r517181 * r517176;
        double r517229 = r517157 * r517160;
        double r517230 = r517228 * r517229;
        double r517231 = r517227 - r517230;
        double r517232 = r517169 * r517184;
        double r517233 = r517173 * r517163;
        double r517234 = r517232 * r517233;
        double r517235 = r517231 - r517234;
        double r517236 = r517194 - r517235;
        double r517237 = r517236 + r517187;
        double r517238 = r517237 + r517172;
        double r517239 = r517238 - r517211;
        double r517240 = r517168 * r517176;
        double r517241 = r517173 * r517154;
        double r517242 = r517240 - r517241;
        double r517243 = r517215 * r517242;
        double r517244 = r517239 + r517243;
        double r517245 = -2.9731786695686922e-136;
        bool r517246 = r517154 <= r517245;
        double r517247 = r517203 - r517211;
        double r517248 = r517247 + r517243;
        double r517249 = -3.545560197893551e-212;
        bool r517250 = r517154 <= r517249;
        double r517251 = r517157 * r517159;
        double r517252 = r517174 * r517184;
        double r517253 = r517251 * r517252;
        double r517254 = r517162 * r517174;
        double r517255 = r517157 * r517181;
        double r517256 = r517254 * r517255;
        double r517257 = r517169 * r517159;
        double r517258 = r517177 * r517257;
        double r517259 = r517258 * r517184;
        double r517260 = r517256 + r517259;
        double r517261 = r517253 - r517260;
        double r517262 = r517261 - r517201;
        double r517263 = r517187 + r517262;
        double r517264 = r517263 + r517172;
        double r517265 = r517264 - r517211;
        double r517266 = r517265 + r517243;
        double r517267 = -2.1346733945086085e-282;
        bool r517268 = r517154 <= r517267;
        double r517269 = 4.4584633619473694e-176;
        bool r517270 = r517154 <= r517269;
        double r517271 = r517168 * r517169;
        double r517272 = r517271 - r517158;
        double r517273 = r517165 * r517272;
        double r517274 = r517203 + r517273;
        double r517275 = r517274 - r517211;
        double r517276 = r517154 * r517160;
        double r517277 = r517183 * r517276;
        double r517278 = r517277 * r517173;
        double r517279 = r517180 * r517241;
        double r517280 = r517163 * r517279;
        double r517281 = r517278 - r517280;
        double r517282 = r517183 * r517168;
        double r517283 = r517160 * r517282;
        double r517284 = r517176 * r517283;
        double r517285 = r517281 - r517284;
        double r517286 = r517275 + r517285;
        double r517287 = r517270 ? r517286 : r517222;
        double r517288 = r517268 ? r517244 : r517287;
        double r517289 = r517250 ? r517266 : r517288;
        double r517290 = r517246 ? r517248 : r517289;
        double r517291 = r517224 ? r517244 : r517290;
        double r517292 = r517156 ? r517222 : r517291;
        return r517292;
}

Original	27.0
Target	31.2
Herbie	28.3

Derivation

Split input into 5 regimes
if y5 < -2.6458728842949793e-07 or 4.4584633619473694e-176 < y5
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 \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 \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(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) - \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) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. 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(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(\color{blue}{y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. 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(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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \color{blue}{\left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)}\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.4
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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.4
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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.5
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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 y4\right) \cdot y1} + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(-y5 \cdot y0\right)\right)\]
11. Simplified27.5
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\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 y4\right) \cdot y1 + \color{blue}{\left(\left(-y5\right) \cdot y0\right) \cdot \left(k \cdot y2 - j \cdot y3\right)}\right)\]
12. Using strategy rm
13. Applied associate-*l*26.3
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\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 y4\right) \cdot y1 + \color{blue}{\left(-y5\right) \cdot \left(y0 \cdot \left(k \cdot y2 - j \cdot y3\right)\right)}\right)\]
14. Simplified26.3
  \[\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\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 y4\right) \cdot y1 + \left(-y5\right) \cdot \color{blue}{\left(\left(k \cdot y2 - j \cdot y3\right) \cdot y0\right)}\right)\]
if -2.6458728842949793e-07 < y5 < -7.030729012634304e-117 or -3.545560197893551e-212 < y5 < -2.1346733945086085e-282
1. Initial program 25.5
  \[\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.5
  \[\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 \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in25.5
  \[\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) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified26.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) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\color{blue}{y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified26.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) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \color{blue}{\left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)}\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.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(i \cdot \left(z \cdot \left(y1 \cdot k\right)\right) - \left(k \cdot \left(z \cdot \left(b \cdot y0\right)\right) + i \cdot \left(j \cdot \left(x \cdot y1\right)\right)\right)\right)}\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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)\]
8. Simplified30.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(i \cdot \left(k \cdot \left(z \cdot y1\right)\right) - \left(j \cdot i\right) \cdot \left(y1 \cdot x\right)\right) - \left(b \cdot z\right) \cdot \left(y0 \cdot k\right)\right)}\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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 -7.030729012634304e-117 < y5 < -2.9731786695686922e-136
1. Initial program 25.5
  \[\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 0 32.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) + \color{blue}{0}\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 -2.9731786695686922e-136 < y5 < -3.545560197893551e-212
1. Initial program 28.5
  \[\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-neg28.5
  \[\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 \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
4. Applied distribute-lft-in28.5
  \[\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) + \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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
5. Simplified28.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(\color{blue}{y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\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(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
6. Simplified28.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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \color{blue}{\left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)}\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 32.3
  \[\leadsto \left(\left(\left(\left(\color{blue}{\left(t \cdot \left(i \cdot \left(z \cdot c\right)\right) - \left(a \cdot \left(t \cdot \left(b \cdot z\right)\right) + i \cdot \left(x \cdot \left(c \cdot y\right)\right)\right)\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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)\]
8. Simplified33.3
  \[\leadsto \left(\left(\left(\left(\color{blue}{\left(\left(c \cdot z\right) \cdot \left(i \cdot t\right) - \left(\left(y \cdot c\right) \cdot \left(x \cdot i\right) + \left(a \cdot \left(t \cdot b\right)\right) \cdot z\right)\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(y4 \cdot \left(b \cdot \left(j \cdot t - y \cdot k\right)\right) + \left(-\left(j \cdot t - y \cdot k\right) \cdot \left(y5 \cdot i\right)\right)\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 -2.1346733945086085e-282 < y5 < 4.4584633619473694e-176
1. Initial program 28.1
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Taylor expanded around inf 29.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(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)}\]
3. Simplified29.3
  \[\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(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \color{blue}{\left(\left(\left(y3 \cdot \left(y5 \cdot j\right)\right) \cdot y0 - k \cdot \left(y2 \cdot \left(y5 \cdot y0\right)\right)\right) - y1 \cdot \left(\left(y3 \cdot y4\right) \cdot j\right)\right)}\]
Recombined 5 regimes into one program.
Final simplification28.3
\[\leadsto \begin{array}{l} \mathbf{if}\;y5 \le -2.645872884294979270972396519223668320819 \cdot 10^{-7}:\\ \;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\right)\right)\\ \mathbf{elif}\;y5 \le -7.030729012634303785773879484609313612868 \cdot 10^{-117}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\left(\left(k \cdot \left(z \cdot y1\right)\right) \cdot i - \left(x \cdot y1\right) \cdot \left(i \cdot j\right)\right) - \left(b \cdot z\right) \cdot \left(y0 \cdot k\right)\right)\right) + \left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -2.973178669568692220900414141880610015231 \cdot 10^{-136}:\\ \;\;\;\;\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -3.545560197893551018782475666749631787843 \cdot 10^{-212}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(\left(i \cdot t\right) \cdot \left(c \cdot z\right) - \left(\left(y \cdot c\right) \cdot \left(i \cdot x\right) + \left(a \cdot \left(b \cdot t\right)\right) \cdot z\right)\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le -2.134673394508608503697255936436163807406 \cdot 10^{-282}:\\ \;\;\;\;\left(\left(\left(\left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(\left(\left(k \cdot \left(z \cdot y1\right)\right) \cdot i - \left(x \cdot y1\right) \cdot \left(i \cdot j\right)\right) - \left(b \cdot z\right) \cdot \left(y0 \cdot k\right)\right)\right) + \left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right)\right) + \left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y2 \cdot k - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y0 \cdot y5\right)\\ \mathbf{elif}\;y5 \le 4.458463361947369366431691027484730583643 \cdot 10^{-176}:\\ \;\;\;\;\left(\left(\left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(\left(\left(y3 \cdot \left(y5 \cdot j\right)\right) \cdot y0 - k \cdot \left(y2 \cdot \left(y0 \cdot y5\right)\right)\right) - y1 \cdot \left(j \cdot \left(y3 \cdot y4\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(\left(\left(-\left(y5 \cdot i\right) \cdot \left(t \cdot j - y \cdot k\right)\right) + y4 \cdot \left(b \cdot \left(t \cdot j - y \cdot k\right)\right)\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(y2 \cdot x - y3 \cdot z\right) + \left(\left(x \cdot y - t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right)\right) - \left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y3 \cdot y\right)\right) + \left(y1 \cdot \left(y4 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) + \left(y0 \cdot \left(y2 \cdot k - j \cdot y3\right)\right) \cdot \left(-y5\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y5 < -2.6458728842949793e-07 or 4.4584633619473694e-176 < y5`

`if -2.6458728842949793e-07 < y5 < -7.030729012634304e-117 or -3.545560197893551e-212 < y5 < -2.1346733945086085e-282`

`if -7.030729012634304e-117 < y5 < -2.9731786695686922e-136`

`if -2.9731786695686922e-136 < y5 < -3.545560197893551e-212`

`if -2.1346733945086085e-282 < y5 < 4.4584633619473694e-176`

Reproduce

In
Out