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