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