How to efficiently specify a MILP constraint with nested AND and ORs
It can be done with two auxiliary variables, y1,y2:

x1 &gt;= y1
x1 &gt;= y2
x1 &lt;= y1 + y2

x2 + x3 + x4 &gt;= 3*(y2 - y1)
x2 + x3 + x4 &lt;= 2 + y1 + y2

x5 + x6 &gt;= 2*(y1 - y2)
x5 + x6 &lt;= 1 + y1 + y2

x7 &gt;= y1 + y2 - 1
x7 &lt;= y1 + y2


The idea here is that if (y1,y2) = (0,1), then the first and-clause is forced to be true; if (y1,y2) = (1,0), then the second and-clause is forced to be true; if (y1,y2) = (1,1), then the third and-clause is forced to be true; and if (y1,y2) = 0, then all three and-clauses are forced to be false.

In other words, (y1,y2) represents the index (in binary) of which of the three and-clauses is true; or (0,0) if none of them are true.

I would be surprised if it is possible to encode your constraint using only a single auxiliary variable.

This trick can be generalized: if you have an OR of $2^k-1$ AND-clauses, then you can find an encoding that uses $k$ auxiliary variables.