ForAll[v5, Exists[v4, ForAll[v3, Exists[v2, ForAll[v1, Exists[v0, And[And[And[And[Or[((2*v5)+(1*v2)+(5*v2)+(2*v5)+(-3*v0)+(-7*v0))<=7, ((-5*v4)+(-2*v1)+(10*v3)+(-4*v1)+(8*v1)+(0*v0))<=5], And[((6*v3)+(-1*v1)+(-8*v0)+(9*v3)+(3*v4)+(-7*v3))<=10, ((-7*v5)+(4*v1)+(-5*v1)+(8*v1)+(-2*v1)+(7*v4))<=-6]], Or[And[((-10*v4)+(6*v3)+(9*v2)+(-5*v5)+(-2*v1)+(10*v5))<=7, ((-8*v0)+(7*v4)+(-3*v1)+(-5*v1)+(-9*v2)+(5*v5))<=-2], And[((-1*v5)+(-8*v2)+(-6*v0)+(9*v2)+(5*v5)+(1*v1))<=-8, ((7*v1)+(9*v2)+(4*v0)+(4*v3)+(8*v5)+(-2*v1))<=10]]], And[And[((-9*v2)+(4*v4)+(5*v4)+(5*v0)+(-3*v2)+(-6*v3))<=5, Or[((-3*v0)+(4*v0)+(-10*v0)+(2*v0)+(3*v1)+(4*v5))<=-10, ((-1*v0)+(-3*v3)+(0*v2)+(2*v3)+(-1*v0)+(-2*v4))<=-8]], Or[((-2*v1)+(-1*v5)+(0*v5)+(-6*v0)+(5*v5)+(1*v0))<=-3, And[((0*v3)+(4*v2)+(1*v2)+(5*v4)+(4*v3)+(-2*v0))<=10, ((-1*v5)+(-10*v4)+(1*v0)+(8*v3)+(8*v4)+(9*v3))<=0]]]], ((-3*v5)+(-7*v0)+(7*v2)+(-8*v3)+(-2*v1)+(-2*v0))<=2]]]]]]]
