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