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