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