Boolean characterization of minimally invariant car lengths with four cars

Let $\mathbf{y}=(y_1,y_2,y_3,y_4)\in\mathbb{N}^4$. A car-length vector is minimally invariant when it has the minimal invariance property defined in the paper. Four-car minimal-invariance conjecture. Then, $\mathbf{y}$ is minimally invariant if and only if

$$\begin{aligned} & (y_1 < y_2) \land (y_1 < y_3) \land (y_1 < y_4) \land (y_2 \neq y_1 + y_3) \land (y_2 \neq y_1 + y_3 + y_4) \\ & \quad \land ((y_2 < y_1 + y_3) \lor (y_3 \neq y_1 + y_4)) \\ & \quad \land ((y_2 > y_1 + y_3) \lor ((y_2 \neq y_1 + y_4) \land ((y_2 < y_3) \lor (y_3 \neq y_1 + y_4)))). \end{aligned}$$

This would extend the Boolean characterizations established in the paper for minimally invariant car lengths with two and three cars; the source presents the formula as suggested by computational experiments, and no proof or resolution is given.