if y3 < -2.418844690205582e-102

1. Started with
   \[\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)\]
   25.7
2. Applied simplify to get
   \[\color{red}{\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)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
   25.7
3. Using strategy rm
   25.7
4. Applied add-cube-cbrt to get
   \[\color{red}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)} \leadsto \color{blue}{{\left(\sqrt[3]{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\right)}^3}\]
   26.3

if -2.418844690205582e-102 < y3 < 6.018594943091541e-236

1. Started with
   \[\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)\]
   24.2
2. Applied simplify to get
   \[\color{red}{\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)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
   24.2
3. Using strategy rm
   24.2
4. Applied sub-neg to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{red}{\left(y0 \cdot c - a \cdot y1\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{blue}{\left(y0 \cdot c + \left(-a \cdot y1\right)\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   24.2
5. Applied distribute-lft-in to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{red}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c + \left(-a \cdot y1\right)\right)\right)})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right)})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   24.2
6. Using strategy rm
   24.2
7. Applied associate-*r* to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\color{red}{\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right)} + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c} + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   23.8
8. Applied taylor to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(y1 \cdot \left(y3 \cdot \left(a \cdot z\right)\right) - y1 \cdot \left(a \cdot \left(x \cdot y2\right)\right)\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   24.4
9. Taylor expanded around inf to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{red}{\left(y1 \cdot \left(y3 \cdot \left(a \cdot z\right)\right) - y1 \cdot \left(a \cdot \left(x \cdot y2\right)\right)\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \color{blue}{\left(y1 \cdot \left(y3 \cdot \left(a \cdot z\right)\right) - y1 \cdot \left(a \cdot \left(x \cdot y2\right)\right)\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   24.4
10. Applied simplify to get
    \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(\left(x \cdot y2 - z \cdot y3\right) \cdot y0\right) \cdot c + \left(y1 \cdot \left(y3 \cdot \left(a \cdot z\right)\right) - y1 \cdot \left(a \cdot \left(x \cdot y2\right)\right)\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + \left((y1 * \left(\left(y3 \cdot a\right) \cdot z - \left(x \cdot a\right) \cdot y2\right) + \left(\left(y0 \cdot c\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right))_*\right))_*\right))_* + \left(\left(b \cdot a - c \cdot i\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - a \cdot y5\right)\right))_*\right)\]
    24.5

---

11. Applied final simplification
12. Applied simplify to get
    \[\color{red}{(\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + \left((y1 * \left(\left(y3 \cdot a\right) \cdot z - \left(x \cdot a\right) \cdot y2\right) + \left(\left(y0 \cdot c\right) \cdot \left(x \cdot y2 - z \cdot y3\right)\right))_*\right))_*\right))_* + \left(\left(b \cdot a - c \cdot i\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - a \cdot y5\right)\right))_*\right)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + \left((y1 * \left(a \cdot \left(y3 \cdot z - y2 \cdot x\right)\right) + \left(\left(y2 \cdot x - y3 \cdot z\right) \cdot \left(c \cdot y0\right)\right))_*\right))_*\right))_* + \left(\left(a \cdot b - c \cdot i\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(x \cdot j - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y3 \cdot y\right) \cdot \left(c \cdot y4 - y5 \cdot a\right)\right))_*\right)}\]
    23.9

if 6.018594943091541e-236 < y3 < 1.472261549911078e-183

1. Started with
   \[\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)\]
   23.1
2. Applied simplify to get
   \[\color{red}{\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)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
   23.1
3. Using strategy rm
   23.1
4. Applied add-cube-cbrt to get
   \[\color{red}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)} \leadsto \color{blue}{{\left(\sqrt[3]{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\right)}^3}\]
   23.7
5. Applied taylor to get
   \[{\left(\sqrt[3]{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\right)}^3 \leadsto {\left(\sqrt[3]{\left(y \cdot \left(b \cdot \left(a \cdot x\right)\right) + \left((\left(y4 \cdot y1 - y5 \cdot y0\right) * \left(k \cdot y2 - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right))_*\right))_* + c \cdot \left(t \cdot \left(i \cdot z\right)\right)\right)\right) - \left(y \cdot \left(c \cdot \left(x \cdot i\right)\right) + \left(b \cdot \left(t \cdot \left(a \cdot z\right)\right) + (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - y1 \cdot i\right) + \left(\left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right))_*\right)\right)}\right)}^3\]
   26.1
6. Taylor expanded around 0 to get
   \[{\color{red}{\left(\sqrt[3]{\left(y \cdot \left(b \cdot \left(a \cdot x\right)\right) + \left((\left(y4 \cdot y1 - y5 \cdot y0\right) * \left(k \cdot y2 - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right))_*\right))_* + c \cdot \left(t \cdot \left(i \cdot z\right)\right)\right)\right) - \left(y \cdot \left(c \cdot \left(x \cdot i\right)\right) + \left(b \cdot \left(t \cdot \left(a \cdot z\right)\right) + (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - y1 \cdot i\right) + \left(\left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right))_*\right)\right)}\right)}}^3 \leadsto {\color{blue}{\left(\sqrt[3]{\left(y \cdot \left(b \cdot \left(a \cdot x\right)\right) + \left((\left(y4 \cdot y1 - y5 \cdot y0\right) * \left(k \cdot y2 - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right))_*\right))_* + c \cdot \left(t \cdot \left(i \cdot z\right)\right)\right)\right) - \left(y \cdot \left(c \cdot \left(x \cdot i\right)\right) + \left(b \cdot \left(t \cdot \left(a \cdot z\right)\right) + (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - y1 \cdot i\right) + \left(\left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right))_*\right)\right)}\right)}}^3\]
   26.1
7. Applied simplify to get
   \[{\left(\sqrt[3]{\left(y \cdot \left(b \cdot \left(a \cdot x\right)\right) + \left((\left(y4 \cdot y1 - y5 \cdot y0\right) * \left(k \cdot y2 - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - y5 \cdot i\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(c \cdot y0 - y1 \cdot a\right)\right))_*\right))_* + c \cdot \left(t \cdot \left(i \cdot z\right)\right)\right)\right) - \left(y \cdot \left(c \cdot \left(x \cdot i\right)\right) + \left(b \cdot \left(t \cdot \left(a \cdot z\right)\right) + (\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - y1 \cdot i\right) + \left(\left(y4 \cdot c - y5 \cdot a\right) \cdot \left(t \cdot y2 - y \cdot y3\right)\right))_*\right)\right)}\right)}^3 \leadsto (y * \left(x \cdot \left(b \cdot a\right)\right) + \left((\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(t \cdot j - y \cdot k\right) * \left(b \cdot y4 - y5 \cdot i\right) + \left(\left(y0 \cdot c - y1 \cdot a\right) \cdot \left(x \cdot y2 - y3 \cdot z\right)\right))_*\right))_*\right))_* + \left(\left(t \cdot c\right) \cdot \left(i \cdot z\right) - \left((\left(j \cdot x - k \cdot z\right) * \left(b \cdot y0 - y1 \cdot i\right) + \left(\left(y4 \cdot c - y5 \cdot a\right) \cdot \left(y2 \cdot t - y \cdot y3\right)\right))_* + (\left(\left(a \cdot t\right) \cdot z\right) * b + \left(\left(y \cdot c\right) \cdot \left(i \cdot x\right)\right))_*\right)\right)\]
   26.9

---

8. Applied final simplification

if 1.472261549911078e-183 < y3 < 2.1067913566185135e-101

1. Started with
   \[\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)\]
   37.6
2. Applied simplify to get
   \[\color{red}{\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)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
   37.6
3. Applied taylor to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + 0)_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   27.8
4. Taylor expanded around 0 to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{red}{0})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{blue}{0})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   27.8
5. Applied simplify to get
   \[\color{red}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + 0)_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)} \leadsto \color{blue}{(\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right))_*}\]
   27.8
6. Applied taylor to get
   \[(\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(y4 \cdot c - y5 \cdot a\right)\right))_* \leadsto (\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(y \cdot \left(y5 \cdot \left(a \cdot y3\right)\right) - \left(y5 \cdot \left(a \cdot \left(t \cdot y2\right)\right) + y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right)\right)\right))_*\]
   22.9
7. Taylor expanded around inf to get
   \[(\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \color{red}{\left(y \cdot \left(y5 \cdot \left(a \cdot y3\right)\right) - \left(y5 \cdot \left(a \cdot \left(t \cdot y2\right)\right) + y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right)\right)\right)})_* \leadsto (\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \color{blue}{\left(y \cdot \left(y5 \cdot \left(a \cdot y3\right)\right) - \left(y5 \cdot \left(a \cdot \left(t \cdot y2\right)\right) + y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right)\right)\right)})_*\]
   22.9
8. Applied simplify to get
   \[(\left(x \cdot y - t \cdot z\right) * \left(a \cdot b - i \cdot c\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(j \cdot x - z \cdot k\right) * \left(b \cdot y0 - i \cdot y1\right) + \left(y \cdot \left(y5 \cdot \left(a \cdot y3\right)\right) - \left(y5 \cdot \left(a \cdot \left(t \cdot y2\right)\right) + y4 \cdot \left(y \cdot \left(c \cdot y3\right)\right)\right)\right))_* \leadsto (\left(y \cdot x - z \cdot t\right) * \left(a \cdot b - c \cdot i\right) + \left((\left(y4 \cdot y1 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(t \cdot j - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + 0)_*\right))_*\right))_* - (\left(x \cdot j - z \cdot k\right) * \left(y0 \cdot b - i \cdot y1\right) + \left(\left(y \cdot y5\right) \cdot \left(y3 \cdot a\right) - (y5 * \left(\left(t \cdot a\right) \cdot y2\right) + \left(\left(y \cdot y4\right) \cdot \left(c \cdot y3\right)\right))_*\right))_*\]
   23.8

---

9. Applied final simplification

if 2.1067913566185135e-101 < y3

1. Started with
   \[\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)\]
   25.2
2. Applied simplify to get
   \[\color{red}{\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)} \leadsto \color{blue}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c - a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
   25.2
3. Using strategy rm
   25.2
4. Applied sub-neg to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{red}{\left(y0 \cdot c - a \cdot y1\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \color{blue}{\left(y0 \cdot c + \left(-a \cdot y1\right)\right)}\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   25.2
5. Applied distribute-lft-in to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{red}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c + \left(-a \cdot y1\right)\right)\right)})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \color{blue}{\left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right)})_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x - t \cdot z\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   25.3
6. Using strategy rm
   25.3
7. Applied sub-neg to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \color{red}{\left(y \cdot x - t \cdot z\right)} - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(a \cdot b - i \cdot c\right) \cdot \color{blue}{\left(y \cdot x + \left(-t \cdot z\right)\right)} - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   25.3
8. Applied distribute-rgt-in to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\color{red}{\left(a \cdot b - i \cdot c\right) \cdot \left(y \cdot x + \left(-t \cdot z\right)\right)} - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\color{blue}{\left(\left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right)\right)} - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
   25.3
9. Applied associate--l+ to get
   \[(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \color{red}{\left(\left(\left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right)\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)} \leadsto (\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \color{blue}{\left(\left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(\left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\right)}\]
   25.3
10. Applied associate-+r+ to get
    \[\color{red}{(\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(\left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right) + \left(\left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\right)} \leadsto \color{blue}{\left((\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right)\right) + \left(\left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)}\]
    25.3
11. Applied simplify to get
    \[\color{red}{\left((\left(y4 \cdot y1 - y0 \cdot y5\right) * \left(y2 \cdot k - j \cdot y3\right) + \left((\left(j \cdot t - y \cdot k\right) * \left(y4 \cdot b - i \cdot y5\right) + \left(\left(x \cdot y2 - z \cdot y3\right) \cdot \left(y0 \cdot c\right) + \left(x \cdot y2 - z \cdot y3\right) \cdot \left(-a \cdot y1\right)\right))_*\right))_* + \left(y \cdot x\right) \cdot \left(a \cdot b - i \cdot c\right)\right)} + \left(\left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right) \leadsto \color{blue}{(y * \left(x \cdot \left(b \cdot a - i \cdot c\right)\right) + \left((\left(y1 \cdot y4 - y5 \cdot y0\right) * \left(y2 \cdot k - y3 \cdot j\right) + \left((\left(j \cdot t - k \cdot y\right) * \left(b \cdot y4 - y5 \cdot i\right) + \left((a * \left(-y1\right) + \left(y0 \cdot c\right))_* \cdot \left(x \cdot y2 - z \cdot y3\right)\right))_*\right))_*\right))_*} + \left(\left(-t \cdot z\right) \cdot \left(a \cdot b - i \cdot c\right) - (\left(j \cdot x - k \cdot z\right) * \left(y0 \cdot b - y1 \cdot i\right) + \left(\left(t \cdot y2 - y \cdot y3\right) \cdot \left(c \cdot y4 - a \cdot y5\right)\right))_*\right)\]
    25.4