\[\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}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le -5.212201362120861737639528461196706285071 \cdot 10^{-300}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(\left(i \cdot \left(y \cdot y5\right)\right) \cdot k - y5 \cdot \left(t \cdot \left(i \cdot j\right)\right)\right) - \left(y \cdot \left(b \cdot y4\right)\right) \cdot k\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.631852305333888237634247798553947975175 \cdot 10^{-100}:\\ \;\;\;\;\left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right) + \left(\left(x \cdot y2 - y3 \cdot z\right) \cdot \left(-a \cdot y1\right) + \left(c \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.579949190118836318625873998095204368512 \cdot 10^{-46}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(-\left(\left(t \cdot y2 - y \cdot y3\right) \cdot a\right) \cdot y5\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot y4\right) \cdot c\right)\right) + \left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right)\\ \mathbf{elif}\;y3 \le 9.090613409892616259914995320157486017171 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(k \cdot \left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) + \left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(-x\right)\right) \cdot j\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right) \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right)\\ \mathbf{elif}\;y3 \le 7.724966512262014443012178268225335252016 \cdot 10^{87}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(i \cdot y5\right) \cdot \left(-\left(t \cdot j - y \cdot k\right)\right) + \left(y4 \cdot \left(t \cdot j - y \cdot k\right)\right) \cdot b\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right) + \left(\left(\sqrt[3]{x \cdot y2 - y3 \cdot z} \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) \cdot \left(\left(c \cdot y0 - a \cdot y1\right) \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) + \left(\left(j \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot \left(-y3\right) + \left(k \cdot y2\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\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}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\
\;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\

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

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

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

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

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

\mathbf{else}:\\
\;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right) + \left(\left(\sqrt[3]{x \cdot y2 - y3 \cdot z} \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) \cdot \left(\left(c \cdot y0 - a \cdot y1\right) \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) + \left(\left(j \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot \left(-y3\right) + \left(k \cdot y2\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\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 r1146073 = x;
        double r1146074 = y;
        double r1146075 = r1146073 * r1146074;
        double r1146076 = z;
        double r1146077 = t;
        double r1146078 = r1146076 * r1146077;
        double r1146079 = r1146075 - r1146078;
        double r1146080 = a;
        double r1146081 = b;
        double r1146082 = r1146080 * r1146081;
        double r1146083 = c;
        double r1146084 = i;
        double r1146085 = r1146083 * r1146084;
        double r1146086 = r1146082 - r1146085;
        double r1146087 = r1146079 * r1146086;
        double r1146088 = j;
        double r1146089 = r1146073 * r1146088;
        double r1146090 = k;
        double r1146091 = r1146076 * r1146090;
        double r1146092 = r1146089 - r1146091;
        double r1146093 = y0;
        double r1146094 = r1146093 * r1146081;
        double r1146095 = y1;
        double r1146096 = r1146095 * r1146084;
        double r1146097 = r1146094 - r1146096;
        double r1146098 = r1146092 * r1146097;
        double r1146099 = r1146087 - r1146098;
        double r1146100 = y2;
        double r1146101 = r1146073 * r1146100;
        double r1146102 = y3;
        double r1146103 = r1146076 * r1146102;
        double r1146104 = r1146101 - r1146103;
        double r1146105 = r1146093 * r1146083;
        double r1146106 = r1146095 * r1146080;
        double r1146107 = r1146105 - r1146106;
        double r1146108 = r1146104 * r1146107;
        double r1146109 = r1146099 + r1146108;
        double r1146110 = r1146077 * r1146088;
        double r1146111 = r1146074 * r1146090;
        double r1146112 = r1146110 - r1146111;
        double r1146113 = y4;
        double r1146114 = r1146113 * r1146081;
        double r1146115 = y5;
        double r1146116 = r1146115 * r1146084;
        double r1146117 = r1146114 - r1146116;
        double r1146118 = r1146112 * r1146117;
        double r1146119 = r1146109 + r1146118;
        double r1146120 = r1146077 * r1146100;
        double r1146121 = r1146074 * r1146102;
        double r1146122 = r1146120 - r1146121;
        double r1146123 = r1146113 * r1146083;
        double r1146124 = r1146115 * r1146080;
        double r1146125 = r1146123 - r1146124;
        double r1146126 = r1146122 * r1146125;
        double r1146127 = r1146119 - r1146126;
        double r1146128 = r1146090 * r1146100;
        double r1146129 = r1146088 * r1146102;
        double r1146130 = r1146128 - r1146129;
        double r1146131 = r1146113 * r1146095;
        double r1146132 = r1146115 * r1146093;
        double r1146133 = r1146131 - r1146132;
        double r1146134 = r1146130 * r1146133;
        double r1146135 = r1146127 + r1146134;
        return r1146135;
}

↓

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 r1146136 = y3;
        double r1146137 = -7.037329032246424e-139;
        bool r1146138 = r1146136 <= r1146137;
        double r1146139 = c;
        double r1146140 = y0;
        double r1146141 = r1146139 * r1146140;
        double r1146142 = a;
        double r1146143 = y1;
        double r1146144 = r1146142 * r1146143;
        double r1146145 = r1146141 - r1146144;
        double r1146146 = x;
        double r1146147 = y2;
        double r1146148 = r1146146 * r1146147;
        double r1146149 = z;
        double r1146150 = r1146136 * r1146149;
        double r1146151 = r1146148 - r1146150;
        double r1146152 = r1146145 * r1146151;
        double r1146153 = k;
        double r1146154 = r1146153 * r1146147;
        double r1146155 = j;
        double r1146156 = r1146155 * r1146136;
        double r1146157 = r1146154 - r1146156;
        double r1146158 = y4;
        double r1146159 = r1146143 * r1146158;
        double r1146160 = y5;
        double r1146161 = r1146160 * r1146140;
        double r1146162 = r1146159 - r1146161;
        double r1146163 = r1146157 * r1146162;
        double r1146164 = r1146152 + r1146163;
        double r1146165 = b;
        double r1146166 = r1146142 * r1146165;
        double r1146167 = i;
        double r1146168 = r1146167 * r1146139;
        double r1146169 = r1146166 - r1146168;
        double r1146170 = y;
        double r1146171 = r1146170 * r1146146;
        double r1146172 = t;
        double r1146173 = r1146172 * r1146149;
        double r1146174 = r1146171 - r1146173;
        double r1146175 = r1146169 * r1146174;
        double r1146176 = r1146140 * r1146165;
        double r1146177 = r1146167 * r1146143;
        double r1146178 = r1146176 - r1146177;
        double r1146179 = r1146146 * r1146178;
        double r1146180 = r1146179 * r1146155;
        double r1146181 = r1146149 * r1146178;
        double r1146182 = r1146181 * r1146153;
        double r1146183 = -r1146182;
        double r1146184 = r1146180 + r1146183;
        double r1146185 = r1146175 - r1146184;
        double r1146186 = r1146164 + r1146185;
        double r1146187 = r1146172 * r1146155;
        double r1146188 = r1146170 * r1146153;
        double r1146189 = r1146187 - r1146188;
        double r1146190 = r1146165 * r1146158;
        double r1146191 = r1146167 * r1146160;
        double r1146192 = r1146190 - r1146191;
        double r1146193 = r1146189 * r1146192;
        double r1146194 = r1146170 * r1146160;
        double r1146195 = r1146136 * r1146194;
        double r1146196 = r1146195 * r1146142;
        double r1146197 = r1146147 * r1146142;
        double r1146198 = r1146172 * r1146160;
        double r1146199 = r1146197 * r1146198;
        double r1146200 = r1146196 - r1146199;
        double r1146201 = r1146139 * r1146158;
        double r1146202 = r1146201 * r1146170;
        double r1146203 = r1146202 * r1146136;
        double r1146204 = r1146200 - r1146203;
        double r1146205 = r1146193 - r1146204;
        double r1146206 = r1146186 + r1146205;
        double r1146207 = -5.212201362120862e-300;
        bool r1146208 = r1146136 <= r1146207;
        double r1146209 = r1146167 * r1146194;
        double r1146210 = r1146209 * r1146153;
        double r1146211 = r1146167 * r1146155;
        double r1146212 = r1146172 * r1146211;
        double r1146213 = r1146160 * r1146212;
        double r1146214 = r1146210 - r1146213;
        double r1146215 = r1146170 * r1146190;
        double r1146216 = r1146215 * r1146153;
        double r1146217 = r1146214 - r1146216;
        double r1146218 = r1146160 * r1146142;
        double r1146219 = r1146201 - r1146218;
        double r1146220 = r1146172 * r1146147;
        double r1146221 = r1146170 * r1146136;
        double r1146222 = r1146220 - r1146221;
        double r1146223 = r1146219 * r1146222;
        double r1146224 = r1146217 - r1146223;
        double r1146225 = r1146186 + r1146224;
        double r1146226 = 1.6318523053338882e-100;
        bool r1146227 = r1146136 <= r1146226;
        double r1146228 = -r1146144;
        double r1146229 = r1146151 * r1146228;
        double r1146230 = r1146139 * r1146151;
        double r1146231 = r1146230 * r1146140;
        double r1146232 = r1146229 + r1146231;
        double r1146233 = r1146163 + r1146232;
        double r1146234 = r1146146 * r1146155;
        double r1146235 = r1146149 * r1146153;
        double r1146236 = r1146234 - r1146235;
        double r1146237 = r1146178 * r1146236;
        double r1146238 = r1146175 - r1146237;
        double r1146239 = r1146233 + r1146238;
        double r1146240 = r1146193 - r1146223;
        double r1146241 = r1146239 + r1146240;
        double r1146242 = 1.5799491901188363e-46;
        bool r1146243 = r1146136 <= r1146242;
        double r1146244 = r1146222 * r1146142;
        double r1146245 = r1146244 * r1146160;
        double r1146246 = -r1146245;
        double r1146247 = r1146222 * r1146158;
        double r1146248 = r1146247 * r1146139;
        double r1146249 = r1146246 + r1146248;
        double r1146250 = r1146193 - r1146249;
        double r1146251 = r1146250 + r1146186;
        double r1146252 = 9.090613409892616e-26;
        bool r1146253 = r1146136 <= r1146252;
        double r1146254 = r1146153 * r1146181;
        double r1146255 = -r1146146;
        double r1146256 = r1146178 * r1146255;
        double r1146257 = r1146256 * r1146155;
        double r1146258 = r1146254 + r1146257;
        double r1146259 = r1146164 + r1146258;
        double r1146260 = cbrt(r1146223);
        double r1146261 = r1146260 * r1146260;
        double r1146262 = r1146261 * r1146260;
        double r1146263 = r1146193 - r1146262;
        double r1146264 = r1146259 + r1146263;
        double r1146265 = 7.7249665122620144e+87;
        bool r1146266 = r1146136 <= r1146265;
        double r1146267 = -r1146189;
        double r1146268 = r1146191 * r1146267;
        double r1146269 = r1146158 * r1146189;
        double r1146270 = r1146269 * r1146165;
        double r1146271 = r1146268 + r1146270;
        double r1146272 = r1146271 - r1146223;
        double r1146273 = r1146186 + r1146272;
        double r1146274 = cbrt(r1146151);
        double r1146275 = r1146274 * r1146274;
        double r1146276 = r1146145 * r1146274;
        double r1146277 = r1146275 * r1146276;
        double r1146278 = r1146155 * r1146162;
        double r1146279 = -r1146136;
        double r1146280 = r1146278 * r1146279;
        double r1146281 = r1146154 * r1146162;
        double r1146282 = r1146280 + r1146281;
        double r1146283 = r1146277 + r1146282;
        double r1146284 = r1146185 + r1146283;
        double r1146285 = r1146240 + r1146284;
        double r1146286 = r1146266 ? r1146273 : r1146285;
        double r1146287 = r1146253 ? r1146264 : r1146286;
        double r1146288 = r1146243 ? r1146251 : r1146287;
        double r1146289 = r1146227 ? r1146241 : r1146288;
        double r1146290 = r1146208 ? r1146225 : r1146289;
        double r1146291 = r1146138 ? r1146206 : r1146290;
        return r1146291;
}

Original	26.6
Target	30.5
Herbie	28.5

Derivation

Split input into 7 regimes
if y3 < -7.037329032246424e-139
1. Initial program 25.4
  \[\left(\left(\left(\left(\left(x \cdot y - z \cdot t\right) \cdot \left(a \cdot b - c \cdot i\right) - \left(x \cdot j - z \cdot k\right) \cdot \left(y0 \cdot b - y1 \cdot i\right)\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(t \cdot j - y \cdot k\right) \cdot \left(y4 \cdot b - y5 \cdot i\right)\right) - \left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y4 \cdot y1 - y5 \cdot y0\right)\]
2. Simplified25.4
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg25.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in25.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified26.2
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified26.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Taylor expanded around inf 29.3
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\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(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
9. Simplified29.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \color{blue}{\left(\left(\left(y3 \cdot \left(y5 \cdot y\right)\right) \cdot a - \left(t \cdot y5\right) \cdot \left(y2 \cdot a\right)\right) - y3 \cdot \left(\left(c \cdot y4\right) \cdot y\right)\right)}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
if -7.037329032246424e-139 < y3 < -5.212201362120862e-300
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. Simplified27.1
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified27.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified28.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Taylor expanded around inf 32.2
  \[\leadsto \left(\color{blue}{\left(i \cdot \left(y \cdot \left(y5 \cdot k\right)\right) - \left(t \cdot \left(i \cdot \left(j \cdot y5\right)\right) + y \cdot \left(y4 \cdot \left(b \cdot k\right)\right)\right)\right)} - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
9. Simplified31.8
  \[\leadsto \left(\color{blue}{\left(\left(\left(i \cdot \left(y5 \cdot y\right)\right) \cdot k - \left(t \cdot \left(i \cdot j\right)\right) \cdot y5\right) - \left(y \cdot \left(y4 \cdot b\right)\right) \cdot k\right)} - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
if -5.212201362120862e-300 < y3 < 1.6318523053338882e-100
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. Simplified27.1
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \color{blue}{\left(y0 \cdot c + \left(-y1 \cdot a\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
5. Applied distribute-lft-in27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \color{blue}{\left(\left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(-y1 \cdot a\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
6. Simplified26.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(\color{blue}{\left(\left(x \cdot y2 - y3 \cdot z\right) \cdot c\right) \cdot y0} + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(-y1 \cdot a\right)\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
7. Simplified26.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(\left(\left(x \cdot y2 - y3 \cdot z\right) \cdot c\right) \cdot y0 + \color{blue}{\left(y1 \cdot a\right) \cdot \left(-\left(x \cdot y2 - y3 \cdot z\right)\right)}\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)\]
if 1.6318523053338882e-100 < y3 < 1.5799491901188363e-46
1. Initial program 22.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. Simplified22.6
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg22.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in22.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified23.4
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified23.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Using strategy rm
9. Applied sub-neg23.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \color{blue}{\left(c \cdot y4 + \left(-a \cdot y5\right)\right)}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
10. Applied distribute-lft-in23.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \color{blue}{\left(\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4\right) + \left(y2 \cdot t - y \cdot y3\right) \cdot \left(-a \cdot y5\right)\right)}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
11. Simplified24.2
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(\color{blue}{c \cdot \left(y4 \cdot \left(y2 \cdot t - y \cdot y3\right)\right)} + \left(y2 \cdot t - y \cdot y3\right) \cdot \left(-a \cdot y5\right)\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
12. Simplified24.0
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(c \cdot \left(y4 \cdot \left(y2 \cdot t - y \cdot y3\right)\right) + \color{blue}{\left(\left(y2 \cdot t - y \cdot y3\right) \cdot a\right) \cdot \left(-y5\right)}\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
if 1.5799491901188363e-46 < y3 < 9.090613409892616e-26
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. Simplified28.1
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg28.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in28.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified27.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified26.7
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Using strategy rm
9. Applied add-cube-cbrt26.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \color{blue}{\left(\sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)} \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)}\right) \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)}}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
10. Simplified26.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \color{blue}{\left(\sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)} \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)}\right)} \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
11. Simplified26.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(\sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)} \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)}\right) \cdot \color{blue}{\sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)}}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
12. Taylor expanded around 0 28.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(\sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)} \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)}\right) \cdot \sqrt[3]{\left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)}\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\color{blue}{0} - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
if 9.090613409892616e-26 < y3 < 7.7249665122620144e+87
1. Initial program 24.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. Simplified24.1
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg24.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in24.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified24.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified24.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Using strategy rm
9. Applied sub-neg24.5
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \color{blue}{\left(b \cdot y4 + \left(-y5 \cdot i\right)\right)} - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
10. Applied distribute-lft-in24.5
  \[\leadsto \left(\color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4\right) + \left(t \cdot j - k \cdot y\right) \cdot \left(-y5 \cdot i\right)\right)} - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
11. Simplified24.6
  \[\leadsto \left(\left(\color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot y4\right) \cdot b} + \left(t \cdot j - k \cdot y\right) \cdot \left(-y5 \cdot i\right)\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
12. Simplified24.6
  \[\leadsto \left(\left(\left(\left(t \cdot j - k \cdot y\right) \cdot y4\right) \cdot b + \color{blue}{\left(-\left(t \cdot j - k \cdot y\right)\right) \cdot \left(y5 \cdot i\right)}\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
if 7.7249665122620144e+87 < y3
1. Initial program 31.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. Simplified31.6
  \[\leadsto \color{blue}{\left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x - z \cdot k\right)\right)\right)}\]
3. Using strategy rm
4. Applied sub-neg31.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \color{blue}{\left(j \cdot x + \left(-z \cdot k\right)\right)}\right)\right)\]
5. Applied distribute-lft-in31.6
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \color{blue}{\left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(j \cdot x\right) + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)}\right)\right)\]
6. Simplified33.0
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j} + \left(y0 \cdot b - i \cdot y1\right) \cdot \left(-z \cdot k\right)\right)\right)\right)\]
7. Simplified32.8
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(y2 \cdot x - z \cdot y3\right) \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \color{blue}{\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)}\right)\right)\right)\]
8. Using strategy rm
9. Applied add-cube-cbrt32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \color{blue}{\left(\left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right)} \cdot \left(y0 \cdot c - y1 \cdot a\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
10. Applied associate-*l*32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \color{blue}{\left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \left(y0 \cdot c - y1 \cdot a\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
11. Simplified32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k - j \cdot y3\right) + \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \color{blue}{\left(\sqrt[3]{x \cdot y2 - z \cdot y3} \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)}\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
12. Using strategy rm
13. Applied sub-neg32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \color{blue}{\left(y2 \cdot k + \left(-j \cdot y3\right)\right)} + \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \left(\sqrt[3]{x \cdot y2 - z \cdot y3} \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
14. Applied distribute-lft-in32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\color{blue}{\left(\left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(y2 \cdot k\right) + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right)} + \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \left(\sqrt[3]{x \cdot y2 - z \cdot y3} \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
15. Simplified32.9
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\color{blue}{\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k\right)} + \left(y4 \cdot y1 - y0 \cdot y5\right) \cdot \left(-j \cdot y3\right)\right) + \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \left(\sqrt[3]{x \cdot y2 - z \cdot y3} \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
16. Simplified29.1
  \[\leadsto \left(\left(t \cdot j - k \cdot y\right) \cdot \left(b \cdot y4 - y5 \cdot i\right) - \left(y2 \cdot t - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right) + \left(\left(\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot \left(y2 \cdot k\right) + \color{blue}{\left(\left(y1 \cdot y4 - y5 \cdot y0\right) \cdot j\right) \cdot \left(-y3\right)}\right) + \left(\sqrt[3]{y2 \cdot x - z \cdot y3} \cdot \sqrt[3]{y2 \cdot x - z \cdot y3}\right) \cdot \left(\sqrt[3]{x \cdot y2 - z \cdot y3} \cdot \left(c \cdot y0 - y1 \cdot a\right)\right)\right) + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(x \cdot y - z \cdot t\right) - \left(\left(\left(b \cdot y0 - y1 \cdot i\right) \cdot x\right) \cdot j + \left(\left(b \cdot y0 - y1 \cdot i\right) \cdot z\right) \cdot \left(-k\right)\right)\right)\right)\]
Recombined 7 regimes into one program.
Final simplification28.5
\[\leadsto \begin{array}{l} \mathbf{if}\;y3 \le -7.037329032246423528361422796149303081084 \cdot 10^{-139}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(\left(y3 \cdot \left(y \cdot y5\right)\right) \cdot a - \left(y2 \cdot a\right) \cdot \left(t \cdot y5\right)\right) - \left(\left(c \cdot y4\right) \cdot y\right) \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le -5.212201362120861737639528461196706285071 \cdot 10^{-300}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(\left(i \cdot \left(y \cdot y5\right)\right) \cdot k - y5 \cdot \left(t \cdot \left(i \cdot j\right)\right)\right) - \left(y \cdot \left(b \cdot y4\right)\right) \cdot k\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.631852305333888237634247798553947975175 \cdot 10^{-100}:\\ \;\;\;\;\left(\left(\left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right) + \left(\left(x \cdot y2 - y3 \cdot z\right) \cdot \left(-a \cdot y1\right) + \left(c \cdot \left(x \cdot y2 - y3 \cdot z\right)\right) \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(y0 \cdot b - i \cdot y1\right) \cdot \left(x \cdot j - z \cdot k\right)\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{elif}\;y3 \le 1.579949190118836318625873998095204368512 \cdot 10^{-46}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\left(-\left(\left(t \cdot y2 - y \cdot y3\right) \cdot a\right) \cdot y5\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot y4\right) \cdot c\right)\right) + \left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right)\\ \mathbf{elif}\;y3 \le 9.090613409892616259914995320157486017171 \cdot 10^{-26}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(k \cdot \left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) + \left(\left(y0 \cdot b - i \cdot y1\right) \cdot \left(-x\right)\right) \cdot j\right)\right) + \left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(\sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)} \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right) \cdot \sqrt[3]{\left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)}\right)\\ \mathbf{elif}\;y3 \le 7.724966512262014443012178268225335252016 \cdot 10^{87}:\\ \;\;\;\;\left(\left(\left(c \cdot y0 - a \cdot y1\right) \cdot \left(x \cdot y2 - y3 \cdot z\right) + \left(k \cdot y2 - j \cdot y3\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right)\right) + \left(\left(\left(i \cdot y5\right) \cdot \left(-\left(t \cdot j - y \cdot k\right)\right) + \left(y4 \cdot \left(t \cdot j - y \cdot k\right)\right) \cdot b\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\left(t \cdot j - y \cdot k\right) \cdot \left(b \cdot y4 - i \cdot y5\right) - \left(c \cdot y4 - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right) + \left(\left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - \left(\left(x \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot j + \left(-\left(z \cdot \left(y0 \cdot b - i \cdot y1\right)\right) \cdot k\right)\right)\right) + \left(\left(\sqrt[3]{x \cdot y2 - y3 \cdot z} \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) \cdot \left(\left(c \cdot y0 - a \cdot y1\right) \cdot \sqrt[3]{x \cdot y2 - y3 \cdot z}\right) + \left(\left(j \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right) \cdot \left(-y3\right) + \left(k \cdot y2\right) \cdot \left(y1 \cdot y4 - y5 \cdot y0\right)\right)\right)\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if y3 < -7.037329032246424e-139`

`if -7.037329032246424e-139 < y3 < -5.212201362120862e-300`

`if -5.212201362120862e-300 < y3 < 1.6318523053338882e-100`

`if 1.6318523053338882e-100 < y3 < 1.5799491901188363e-46`

`if 1.5799491901188363e-46 < y3 < 9.090613409892616e-26`

`if 9.090613409892616e-26 < y3 < 7.7249665122620144e+87`

`if 7.7249665122620144e+87 < y3`

Reproduce

In
Out