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