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