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