(* These are the 56 virtual substitution examples. First 16 come from *) (* applications, the last 40 are randomly generated. The code for generating *) (* the examples and running the test comes after the examples. The examples *) (* are in the format {{{{quantifier, variables}, ...}, formula}, ...}, with *) (* the innermost quantifiers coming first in the list. *) (* There is no documented Mathematica function running virtual substitution *) (* directly. Functions like Reduce, Resolve or FindInstance use virtual *) (* substitution as one of their methods. Here we call an internal function *) (* which is a part of Reduce/Resolve code. *) examples = {{{{Exists, {x}}}, 1 + v*x + u*x^2 == 0 && u + w*x + v*x^3 == 0 && u + v*x + w*x^2 <= 0}, {{{Exists, {r}}}, -a^2 - b^2 - 2*a*r + 3*b^2*r + 3*a*r^2 < 0 && 2*a - 2*a^2 - 2*b^2 + r - 4*a*r + 3*a^2*r + 3*b^2*r > 0 && a >= 1/2 && b > 0 && r > 0 && r < 1}, {{{ForAll, {a, b}}, {Exists, {c}}}, Implies[(a == d && b == c) || (a == c && b == 1), a^2 == b]}, {{{ForAll, {x, y}}}, Implies[-(a^2*b^2) + b^2*(-c + x)^2 + a^2*y^2 == 0, x^2 + y^2 <= 1]}, {{{Exists, {x}}}, cc1 + bb1*x + aa1*x^2 == 0 && cc2 + bb2*x + aa2*x^2 == 0 && cc3 + bb3*x + aa3*x^2 < 0 && cc4 + bb4*x + aa4*x^2 < 0 && cc5 + bb5*x + aa5*x^2 < 0}, {{{ForAll, {x, y}}}, 1 + x^2*y^2*(-3 + x^2 + y^2) >= 0}, {{{ForAll, {x, y}}, {Exists, {r}}}, Implies[x > r && y > r, x^2*(1 + 2*y)^2 > (1 + 2*x^2)*y^2]}, {{{Exists, {x, y}}}, x^2 + y^2 + z^2 == 1 && y + x*z + z^3 == 0}, {{{Exists, {r}}}, (16 - 24*r + r^2 < 0 || (r > 1 && 16 - 24*r + r^2 >= 0)) && -1 < u < v < 1 && -1 + a - b*u - a*u^2 + r*u^3 + u^4 == -b + r && -1 + a - b*v - a*v^2 + r*v^3 + v^4 == b - r && -b - 2*a*u + 3*r*u^2 + 4*u^3 == 0 && -b - 2*a*v + 3*r*v^2 + 4*v^3 == 0 && -b + r > 0}, {{{Exists, {x, y}}}, 1 - x - 12*y - 3*x*y + 9*z - 14*x*z + 6*y*z - 7*x*y*z == 0 && -15*x + 14*y + 15*x*y + 14*z - y*z + 2*x*y*z == 0 && -14 + 10*x + 2*y + 15*x*y - 5*z - 12*x*z + 11*y*z - 8*x*y*z == 0}, {{{Exists, {x, y}}}, 1 <= 4*a <= 7 && -3 <= 4*b <= 3 && -1 <= x <= 0 && 0 <= y <= 1 && -a - 2*x + 3*x^2 == 0 && -(a*x) - x^2 + x^3 == 2 - a + 2*b && -a - 2*y + 3*y^2 == 0 && -(a*y) - y^2 + y^3 == -2 + a}, {{{ForAll, {p1, p2, w1, w2}}}, Implies[16 <= 20*p1 <= 25 && 16 <= 20*p2 <= 25 && 0 <= w1 <= 2, p2*(1 + p1*q1) < 0 && p2^2*(-25 + (1 + p1*q1)^2) - 24*w1^2 > 0 && p2^2*(-q1^2 + 400*(1 + p1*q1)^2) + (400 - q1^2)*w2^2 > 0]}, {{{ForAll, {w}}, {Exists, {q1, q2}}}, q1 > 1 && q2 > 0 && Implies[nbyd >= 0, (-1 + nbyd)*q2^2 + (-q1^2 + nbyd*((1 + q1)^2 - 2*q2) - q2^2)*w^2 + (nbyd - q1^2)*w^4 >= 0 && (-1 + nbyd)*q2^2 + (-q1^2 + nbyd*((-1 + q1)^2 - 2*q2) - q2^2)*w^2 + (nbyd - q1^2)*w^4 >= 0]}, {{{ForAll, {x}}, {Exists, {d}}, {ForAll, {e}}}, Implies[e > 0, d > 0 && Implies[-d < -1 + x < d, (1 + x > 0 && -(e*(1 + x)) < -2 + x - l*(1 + x) < e*(1 + x)) || (1 + x < 0 && -(e*(1 + x)) > -2 + x - l*(1 + x) > e*(1 + x))]]}, {{{ForAll, {a, b, c, d, e, f}}}, a < 0 || b < 0 || c < 0 || d < 0 || e < 0 || f < 0 || a^2 + b^2 > e^2 || c^2 + d^2 > f^2 || a*c + b*d <= e*f}, {{{ForAll, {a, b, c, l}}}, Implies[a + c >= b && c >= 0 && b + c >= a && b >= 0 && a + b >= c && a >= 0 && l > 0, ((a + b + c)/2 + a*l)*((a + b + c)/2 + b*l)* ((a + b + c)/2 + c*l) >= (-a + (a + b + c)/2)*(-b + (a + b + c)/2)* (-c + (a + b + c)/2)*(3 + 2*l)^3]}, {{{Exists, {x[2]}}}, -704 - 279*x[1] - 188*x[1]^2 - 689*x[2] - 179*x[1]*x[2] + 5*x[2]^2 == 0 && 1000 + 427*x[1] + 879*x[1]^2 + 422*x[2] - 222*x[1]*x[2] - 685*x[2]^2 < 0 && -191 + 815*x[1] + 528*x[1]^2 - 152*x[2] - 410*x[1]*x[2] - 602*x[2]^2 >= 0 && -749 - 558*x[1] + 147*x[1]^2 + 323*x[2] + 400*x[1]*x[2] - 536*x[2]^2 >= 0}, {{{Exists, {x[2]}}}, -723 - 380*x[1] - 9*x[1]^2 - 964*x[2] + 497*x[1]*x[2] + 935*x[2]^2 == 0 && 32 + 3*x[1] + 302*x[1]^2 - 550*x[2] + 610*x[1]*x[2] + 764*x[2]^2 == 0 && -309 - 407*x[1] + 606*x[1]^2 - 111*x[2] - 982*x[1]*x[2] + 773*x[2]^2 == 0 && 453 + 758*x[1] + 377*x[1]^2 - 659*x[2] + 451*x[1]*x[2] - 865*x[2]^2 == 0 && -250 - 481*x[1] - 96*x[1]^2 + 194*x[2] - 78*x[1]*x[2] - 540*x[2]^2 == 0 && -937 + 734*x[1] + 515*x[1]^2 - 825*x[2] + 760*x[1]*x[2] + 545*x[2]^2 == 0 && 516 - 553*x[1] + 514*x[1]^2 - 927*x[2] - 68*x[1]*x[2] + 197*x[2]^2 == 0 && 798 - 175*x[1] - 354*x[1]^2 + 119*x[2] - 820*x[1]*x[2] + 824*x[2]^2 == 0 && 532 + 650*x[1] + 587*x[1]^2 + 780*x[2] - 432*x[1]*x[2] - 401*x[2]^2 == 0 && -229 - 360*x[1] + 1024*x[1]^2 - 306*x[2] - 543*x[1]*x[2] - 250*x[2]^2 == 0 && -923 + 45*x[1] - 602*x[1]^2 - 297*x[2] + 777*x[1]*x[2] + 105*x[2]^2 < 0 && -677 - 95*x[1] + 985*x[1]^2 - 470*x[2] - 693*x[1]*x[2] + 987*x[2]^2 < 0 && -81 + 44*x[1] + 609*x[1]^2 - 792*x[2] + 982*x[1]*x[2] - 41*x[2]^2 < 0 && -631 - 307*x[1] - 567*x[1]^2 - 503*x[2] + 161*x[1]*x[2] - 806*x[2]^2 < 0 && -500 - 5*x[1] + 269*x[1]^2 - 230*x[2] + 716*x[1]*x[2] - 163*x[2]^2 < 0 && -132 + 374*x[1] + 414*x[1]^2 + 995*x[2] - 194*x[1]*x[2] + 112*x[2]^2 >= 0 && -776 - 395*x[1] - 855*x[1]^2 + 96*x[2] - 788*x[1]*x[2] - 131*x[2]^2 >= 0 && 942 - 561*x[1] - 198*x[1]^2 - 580*x[2] - 970*x[1]*x[2] + 220*x[2]^2 >= 0 && -270 - 868*x[1] + 125*x[1]^2 - 76*x[2] - 687*x[1]*x[2] + 713*x[2]^2 >= 0 && 227 + 950*x[1] + 150*x[1]^2 - 700*x[2] + 885*x[1]*x[2] - 232*x[2]^2 >= 0}, {{{Exists, {x[2]}}}, -111 - 376*x[1] + 584*x[1]^2 + 120*x[2] + 968*x[1]*x[2] + 184*x[2]^2 < 0 && -59 + 254*x[1] - 102*x[1]^2 - 218*x[2] - 495*x[1]*x[2] - 888*x[2]^2 < 0 && 497 + 395*x[1] - 208*x[1]^2 - 1006*x[2] + 280*x[1]*x[2] - 862*x[2]^2 >= 0 && 826 + 275*x[1] - 443*x[1]^2 - 117*x[2] + 413*x[1]*x[2] + 753*x[2]^2 >= 0 && 427 - 545*x[1] - 266*x[1]^2 - 562*x[2] - 810*x[1]*x[2] + 120*x[2]^2 >= 0}, {{{Exists, {x[3]}}}, 941 - 160*x[1] + 123*x[1]^2 + 1003*x[2] + 625*x[1]*x[2] + 442*x[2]^2 - 691*x[3] - 877*x[1]*x[3] + 43*x[2]*x[3] - 320*x[3]^2 == 0 && 131 + 379*x[1] + 206*x[1]^2 - 740*x[2] + 516*x[1]*x[2] - 516*x[2]^2 + 495*x[3] + 805*x[1]*x[3] + 142*x[2]*x[3] + 750*x[3]^2 < 0 && 962 + 294*x[1] + 384*x[1]^2 - 627*x[2] - 816*x[1]*x[2] + 417*x[2]^2 - 854*x[3] - 974*x[1]*x[3] - 158*x[2]*x[3] + 391*x[3]^2 >= 0}, {{{Exists, {x[3]}}}, 824 - 350*x[1] + 753*x[1]^2 + 520*x[2] - 707*x[1]*x[2] - 125*x[2]^2 - 627*x[3] + 546*x[1]*x[3] - x[2]*x[3] - 311*x[3]^2 == 0 && 430 + 543*x[1] + 470*x[1]^2 + 631*x[2] + 236*x[1]*x[2] + 919*x[2]^2 - 848*x[3] + 348*x[1]*x[3] - 462*x[2]*x[3] + 182*x[3]^2 < 0 && -158 - 961*x[1] + 811*x[1]^2 + 649*x[2] + 713*x[1]*x[2] - 189*x[2]^2 + 912*x[3] - 262*x[1]*x[3] + 319*x[2]*x[3] + 39*x[3]^2 < 0 && -662 + 742*x[1] - 84*x[1]^2 + 565*x[2] - 371*x[1]*x[2] + 853*x[2]^2 - 721*x[3] + 866*x[1]*x[3] - 586*x[2]*x[3] - 131*x[3]^2 >= 0 && 30 + 870*x[1] + 813*x[1]^2 - 350*x[2] - 175*x[1]*x[2] - 886*x[2]^2 + 846*x[3] + 920*x[1]*x[3] - 461*x[2]*x[3] - 792*x[3]^2 >= 0}, {{{Exists, {x[3]}}}, 397 + 548*x[1] - 162*x[1]^2 - 945*x[2] - 488*x[1]*x[2] - 423*x[2]^2 - 423*x[3] + 751*x[1]*x[3] + 55*x[2]*x[3] + 579*x[3]^2 < 0 && 525 + 397*x[1] + 919*x[1]^2 + 30*x[2] + 744*x[1]*x[2] + 459*x[2]^2 + 889*x[3] + 167*x[1]*x[3] + 638*x[2]*x[3] - 248*x[3]^2 >= 0}, {{{Exists, {x[3]}}}, 909 - 54*x[1] + 206*x[1]^2 + 112*x[2] - 24*x[1]*x[2] - 852*x[2]^2 + 938*x[3] + 915*x[1]*x[3] + 401*x[2]*x[3] + 207*x[3]^2 < 0 && 355 + 959*x[1] - 42*x[1]^2 - 450*x[2] + 484*x[1]*x[2] - 878*x[2]^2 + 13*x[3] + 667*x[1]*x[3] - 734*x[2]*x[3] + 207*x[3]^2 >= 0 && -343 - 961*x[1] + 437*x[1]^2 + 348*x[2] + 859*x[1]*x[2] - 749*x[2]^2 - 509*x[3] - 201*x[1]*x[3] - 239*x[2]*x[3] - 77*x[3]^2 >= 0}, {{{Exists, {x[3]}}}, 985 + 641*x[1] + 559*x[1]^2 + 69*x[2] + 71*x[1]*x[2] - 600*x[2]^2 + 424*x[3] + 818*x[1]*x[3] + 13*x[2]*x[3] - 126*x[3]^2 < 0 && 992 + 216*x[1] + 313*x[1]^2 + 292*x[2] - 980*x[1]*x[2] - 803*x[2]^2 - 246*x[3] - 109*x[1]*x[3] + 862*x[2]*x[3] - 64*x[3]^2 < 0 && -940 - 791*x[1] - 765*x[1]^2 - 73*x[2] - 120*x[1]*x[2] - 333*x[2]^2 + 168*x[3] + 582*x[1]*x[3] - 905*x[2]*x[3] - 144*x[3]^2 >= 0 && -487 + 412*x[1] + 312*x[1]^2 - 295*x[2] - 501*x[1]*x[2] + 201*x[2]^2 + 665*x[3] - 148*x[1]*x[3] + 9*x[2]*x[3] + 805*x[3]^2 >= 0}, {{{Exists, {x[2], x[1]}}}, 36 - 41*x[1] + 398*x[1]^2 - 494*x[2] + 306*x[1]*x[2] + 72*x[2]^2 == 0 && 154 - 366*x[1] + 594*x[1]^2 + 312*x[2] + 521*x[1]*x[2] + 701*x[2]^2 < 0 && -665 + 146*x[1] + 618*x[1]^2 - 344*x[2] + 771*x[1]*x[2] - 420*x[2]^2 < 0 && 564 - 334*x[1] - 702*x[1]^2 - 47*x[2] + 151*x[1]*x[2] - 48*x[2]^2 >= 0 && 366 - 34*x[1] - 541*x[1]^2 - 301*x[2] - 482*x[1]*x[2] + 645*x[2]^2 >= 0 && 274 - 25*x[1] + 727*x[1]^2 + 903*x[2] - 201*x[1]*x[2] - 178*x[2]^2 >= 0}, {{{Exists, {x[3], x[2]}}}, 898 - 853*x[1] + 800*x[1]^2 + 852*x[2] - 724*x[1]*x[2] + 663*x[2]^2 + 1024*x[3] + 911*x[1]*x[3] - 615*x[2]*x[3] + 931*x[3]^2 == 0 && 667 - 370*x[1] - 252*x[1]^2 + 225*x[2] + 277*x[1]*x[2] - 482*x[2]^2 - 747*x[3] - 615*x[1]*x[3] + 759*x[2]*x[3] + 146*x[3]^2 < 0 && 749 - 704*x[1] - 543*x[1]^2 - 588*x[2] + 899*x[1]*x[2] - 910*x[2]^2 - 294*x[3] + 815*x[1]*x[3] - 407*x[2]*x[3] - 618*x[3]^2 >= 0}, {{{Exists, {x[3], x[2]}}}, 847 + 711*x[1] + 299*x[1]^2 + 844*x[2] - 838*x[1]*x[2] - 283*x[2]^2 - 293*x[3] - 279*x[1]*x[3] - 760*x[2]*x[3] + 640*x[3]^2 == 0 && -948 - 101*x[1] - 421*x[1]^2 + 919*x[2] - 300*x[1]*x[2] - 869*x[2]^2 - 769*x[3] + 547*x[1]*x[3] - 477*x[2]*x[3] - 211*x[3]^2 < 0 && -172 - 820*x[1] + 721*x[1]^2 + 929*x[2] - 958*x[1]*x[2] + 103*x[2]^2 - 805*x[3] + 147*x[1]*x[3] + 824*x[2]*x[3] - 879*x[3]^2 >= 0 && 792 + 61*x[1] + 114*x[1]^2 + 491*x[2] + 34*x[1]*x[2] + 354*x[2]^2 - 138*x[3] + 731*x[1]*x[3] + 341*x[2]*x[3] + 59*x[3]^2 >= 0}, {{{Exists, {x[3], x[2]}}}, 12 + 584*x[1] + 689*x[1]^2 + 969*x[2] + 242*x[1]*x[2] - 292*x[2]^2 + 192*x[3] + 699*x[1]*x[3] + 492*x[2]*x[3] + 229*x[3]^2 < 0 && 456 - 221*x[1] + 835*x[1]^2 + 595*x[2] - 228*x[1]*x[2] - 488*x[2]^2 + 750*x[3] + 513*x[1]*x[3] - 698*x[2]*x[3] - 1016*x[3]^2 >= 0}, {{{Exists, {x[3], x[2]}}}, -565 + 850*x[1] + 851*x[1]^2 + 107*x[2] + 212*x[1]*x[2] + 629*x[2]^2 - 122*x[3] + 609*x[1]*x[3] - 155*x[2]*x[3] + 871*x[3]^2 < 0 && 853 - 829*x[1] + 68*x[1]^2 - 601*x[2] - 627*x[1]*x[2] - 515*x[2]^2 - 886*x[3] - 995*x[1]*x[3] - 531*x[2]*x[3] - 440*x[3]^2 >= 0 && 942 + 469*x[1] - 909*x[1]^2 - 368*x[2] + 277*x[1]*x[2] - 217*x[2]^2 - 849*x[3] + 418*x[1]*x[3] - 75*x[2]*x[3] + 101*x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3], x[4]}}}, 662 + 426*x[1] + 813*x[1]^2 - 806*x[2] - 748*x[1]*x[2] - 301*x[2]^2 - 774*x[3] + 360*x[1]*x[3] + 691*x[2]*x[3] - 892*x[3]^2 + 313*x[4] + 28*x[1]*x[4] - 922*x[2]*x[4] + 367*x[3]*x[4] + 679*x[4]^2 == 0 && 853 - 358*x[1] + 584*x[1]^2 + 614*x[2] + 146*x[1]*x[2] - 960*x[2]^2 - 120*x[3] + 158*x[1]*x[3] + 241*x[2]*x[3] + 254*x[3]^2 + 765*x[4] + 909*x[1]*x[4] + 380*x[2]*x[4] + 394*x[3]*x[4] - 891*x[4]^2 < 0 && 1008 - 13*x[1] + 707*x[1]^2 + 990*x[2] + 197*x[1]*x[2] - 574*x[2]^2 - 527*x[3] - 105*x[1]*x[3] - 645*x[2]*x[3] - 111*x[3]^2 + 85*x[4] - 423*x[1]*x[4] - 778*x[2]*x[4] - 694*x[3]*x[4] + 856*x[4]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -468 - 344*x[1] + 1023*x[1]^2 + 717*x[2] + 1011*x[1]*x[2] + 1002*x[2]^2 + 923*x[3] - 255*x[1]*x[3] + 998*x[2]*x[3] + 300*x[3]^2 < 0 && 904 - 222*x[1] - 556*x[1]^2 - 666*x[2] - 518*x[1]*x[2] - 140*x[2]^2 + 972*x[3] + 801*x[1]*x[3] - 527*x[2]*x[3] + 900*x[3]^2 >= 0 && 915 - 792*x[1] + 596*x[1]^2 + 100*x[2] + 602*x[1]*x[2] - 373*x[2]^2 - 353*x[3] - 713*x[1]*x[3] + 235*x[2]*x[3] - 695*x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 905 + 476*x[1] + 772*x[1]^2 - 961*x[2] + 152*x[1]*x[2] - 244*x[2]^2 + 758*x[3] + 340*x[1]*x[3] - 444*x[2]*x[3] + 566*x[3]^2 == 0 && 979 - 240*x[1] - 306*x[1]^2 - 797*x[2] - 626*x[1]*x[2] - 188*x[2]^2 + 394*x[3] + 282*x[1]*x[3] - 1019*x[2]*x[3] - 709*x[3]^2 < 0 && 407 - 288*x[1] - 128*x[1]^2 - 414*x[2] - 681*x[1]*x[2] - 353*x[2]^2 - 963*x[3] - 658*x[1]*x[3] - 680*x[2]*x[3] - 950*x[3]^2 >= 0 && -780 + 985*x[1] + 126*x[1]^2 + 830*x[2] + 1008*x[1]*x[2] - 428*x[2]^2 - 859*x[3] - 353*x[1]*x[3] + 37*x[2]*x[3] - 912*x[3]^2 >= 0}, {{{Exists, {x[2]}}}, 1274 + 1727*x[1]^2 + 361*x[1]^3 + 172*x[2] + (262 - 411*x[1]^2)*x[2]^2 == 0 && -866 + 335*x[1] - 1670*x[1]^3 + (719 + 174*x[1]^2 + 791*x[1]^3)*x[2] + (738 - 600*x[1] + 261*x[1]^2 - 788*x[1]^3)*x[2]^2 < 0 && 862 - 471*x[1] + 1023*x[1]^2 + (629 - 39*x[1])*x[2] + (-542 + 857*x[1] - 712*x[1]^3)*x[2]^2 >= 0 && 1718 - 404*x[1] - 493*x[1]^2 + 193*x[1]^3 + (651 - 412*x[1])*x[2] + (-250 + 700*x[1] + 624*x[1]^3)*x[2]^2 >= 0}, {{{Exists, {x[2]}}}, 293 + 657*x[1]^3 - 392*x[1]^5 + (382 - 1259*x[1]^4)*x[2] + (-795 - 120*x[1] + 242*x[1]^2 - 996*x[1]^4)*x[2]^2 == 0 && -519 + 582*x[1] + 658*x[1]^2 - 944*x[1]^3 - 231*x[1]^5 + (-2431 - 404*x[1]^3 + 802*x[1]^5)*x[2] + (-336 + 954*x[1] + 389*x[1]^2 + 935*x[1]^4 + 988*x[1]^5)*x[2]^2 < 0 && 373 - 650*x[1]^2 - 896*x[1]^3 - 547*x[1]^4 + 229*x[1]^5 + (-2000 + 71*x[1]^2 + 857*x[1]^5)*x[2] + (700 - 838*x[1] + 557*x[1]^3 - 1038*x[1]^4)*x[2]^2 >= 0 && -16 + 232*x[1]^3 - 766*x[1]^5 + (376 + 396*x[1] - 321*x[1]^4)*x[2] + (994 + 953*x[1] + 103*x[1]^3 - 178*x[1]^5)*x[2]^2 >= 0}, {{{Exists, {x[2]}}}, -1056 + 634*x[1]^2 - 57*x[1]^3 + (170 + 76*x[1] + 741*x[1]^3 + 666*x[1]^5)*x[2] + (555 + 311*x[1] + 956*x[1]^2 + 831*x[1]^5)*x[2]^2 < 0 && 212 - 423*x[1]^3 - 671*x[1]^4 - 462*x[1]^5 + (-123 - 602*x[1] - 732*x[1]^2)*x[2] + (1558 + 380*x[1]^2 + 58*x[1]^3 - 938*x[1]^5)*x[2]^2 < 0 && 277 + 991*x[1] - 207*x[1]^3 + (1417 - 750*x[1]^2 - 953*x[1]^3 + 556*x[1]^5)*x[2] + (-185 - 44*x[1] + 1344*x[1]^4)*x[2]^2 >= 0 && 1620 - 537*x[1] - 318*x[1]^2 - 960*x[1]^3 + (252 + 999*x[1] + 845*x[1]^2 - 279*x[1]^5)*x[2] + (-784 + 1425*x[1]^2 - 559*x[1]^5)*x[2]^2 >= 0}, {{{Exists, {x[3]}}}, -773 + 278*x[2] - 740*x[1]^2*x[2] - 298*x[1]*x[2]^2 - 207*x[2]^4 + (831 + 257*x[1]^4 - 604*x[2] + 376*x[1]^2*x[2] - 217*x[2]^2)*x[3] + (-943 + 111*x[1]^3 - 570*x[2] - 690*x[1]*x[2]^3 - 735*x[2]^4)* x[3]^2 == 0 && -146 - 587*x[1]*x[2] - 683*x[2]^2 - 1897*x[2]^4 + (582 - 538*x[1] - 455*x[1]^4 + 233*x[1]^2*x[2] + 50*x[1]^3*x[2])* x[3] + (238 + 703*x[2] - 202*x[1]*x[2] + 198*x[1]^3*x[2] + 936*x[2]^3)*x[3]^2 >= 0}, {{{Exists, {x[3]}}}, 605 + 718*x[1]*x[2] + 177*x[1]^2*x[2]^2 - 398*x[2]^5 + (674 - 14*x[1]^5 + 425*x[1]^2*x[2] - 4*x[1]^2*x[2]^2 - 376*x[1]^3*x[2]^2)*x[3] + (779 - 782*x[1]^2*x[2] + 458*x[1]^3*x[2] - 150*x[1]^3*x[2]^2 - 839*x[2]^4)*x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -822 - 659*x[1]*x[2]^3 + 135*x[1]^2*x[2]^3 - 348*x[2]^5 + (-666 + 280*x[1]^4 - 105*x[1]*x[2]^3 - 776*x[1]*x[2]^4 + 889*x[2]^5)* x[3] + (-488 + 152*x[1]^4*x[2] - 437*x[1]^2*x[2]^2 - 926*x[1]*x[2]^3 + 519*x[1]*x[2]^4)*x[3]^2 < 0 && 419 + 395*x[1]^4 - 540*x[1]^2*x[2]^2 - 137*x[1]^2*x[2]^3 + (-926 + 126*x[1]^2 + 1098*x[1]^3*x[2] + 616*x[2]^5)*x[3] + (-294 - 655*x[2]^2 + 763*x[1]^2*x[2]^2 + 1588*x[1]*x[2]^4)*x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3], x[4]}}}, 502 + 603*x[2]^3 - 70*x[1]^2*x[3] + 1002*x[1]*x[2]*x[3] - 418*x[2]*x[3]^2 + (246 - 319*x[2] + 240*x[3]^2 + 940*x[2]*x[3]^2)* x[4] + (845 - 358*x[3] + 579*x[2]*x[3] - 1024*x[2]^2*x[3])* x[4]^2 == 0 && -49 - 306*x[1]*x[2] - 760*x[3] + 896*x[1]^2*x[3] - 432*x[1]*x[2]*x[3] + (-552 + 684*x[2]*x[3] - 102*x[3]^2 - 710*x[2]*x[3]^2 + 374*x[3]^3)*x[4] + (-512 - 569*x[2]^2 + 863*x[1]*x[2]^2 - 1272*x[2]^3)*x[4]^2 >= 0}, {{{Exists, {x[2]}}}, 288 + 183*x[1] + 391*x[1]^3 + (-1043 - 61*x[1] + 843*x[1]^6)*x[2] + x[2]^2 < 0 && 530 + 913*x[1]^2 - 993*x[1]^5 - 474*x[1]^6 + (-677 + 864*x[1] - 989*x[1]^2 - 263*x[1]^3 + 255*x[1]^4)*x[2] + x[2]^2 >= 0 && -168 + 217*x[1] + 350*x[1]^2 - 532*x[1]^5 + (-646 - 313*x[1]^2 - 685*x[1]^3 - 264*x[1]^6 + 674*x[1]^7)*x[2] + x[2]^2 >= 0}, {{{Exists, {x[2]}}}, 314 - 811*x[1]^2 - 19*x[1]^3 + (316 - 226*x[1]^2 + 392*x[1]^5 - 35*x[1]^6)*x[2] + x[2]^2 == 0 && 316 - 158*x[1] - 427*x[1]^5 + 56*x[1]^6 + (-829 - 481*x[1]^4 - 531*x[1]^5 - 405*x[1]^7)*x[2] + x[2]^2 < 0 && 947 - 976*x[1] + 429*x[1]^6 + (-919 + 54*x[1] + 906*x[1]^4 + 506*x[1]^5)*x[2] + x[2]^2 >= 0 && -633 - 651*x[1] - 344*x[1]^3 - 6*x[1]^7 + (-277 + 82*x[1] - 286*x[1]^4 - 22*x[1]^7)*x[2] + x[2]^2 >= 0}, {{{Exists, {x[2]}}}, -752 + 855*x[1]^3 + 242*x[1]^4 - 837*x[1]^6 + (1469 - 388*x[1] + 713*x[1]^6)*x[2] + x[2]^2 == 0 && -36 - 148*x[1]^3 - 1776*x[1]^4 - 951*x[1]^5 + (-644 - 879*x[1] + 646*x[1]^6)*x[2] + x[2]^2 < 0 && -967 + 599*x[1] - 126*x[1]^2 - 891*x[1]^3 - 78*x[1]^6 + (-492 + 218*x[1]^4 + 889*x[1]^5 + 837*x[1]^6)*x[2] + x[2]^2 < 0 && -238 + 243*x[1]^2 - 193*x[1]^3 + 775*x[1]^5 - 545*x[1]^6 + (-176 - 624*x[1]^2 - 770*x[1]^7)*x[2] + x[2]^2 >= 0 && -289 - 408*x[1]^2 + 206*x[1]^4 + 210*x[1]^6 + (917 - 699*x[1] + 932*x[1]^3 - 958*x[1]^4)*x[2] + x[2]^2 >= 0 && 322 + 518*x[1] - 186*x[1]^2 + 640*x[1]^3 - 916*x[1]^7 + (-308 - 1802*x[1] - 1023*x[1]^2 - 469*x[1]^7)*x[2] + x[2]^2 >= 0}, {{{Exists, {x[1], x[2], x[3], x[4]}}}, 876 + 861*x[1]^2*x[3] - 34*x[2]*x[3] + 733*x[2]*x[3]^2 + 216*x[3]^3 + (238 + 1005*x[1]*x[2] + 670*x[2]^3 + 348*x[2]*x[3] + 747*x[2]^2*x[3])*x[4] + x[4]^2 == 0 && 700 - 180*x[1]^3 - 282*x[1]^2*x[3] + 418*x[2]*x[3] - 1019*x[2]^2*x[3] + (705 - 595*x[2]^2 - 650*x[2]^3 + 535*x[1]*x[2]*x[3] - 670*x[2]*x[3]^2)*x[4] + x[4]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -426 - 44*x[1]^3 - 869*x[1]^2*x[2] - 271*x[2]^2 - 312*x[1]*x[2]^2 + (-686 + 942*x[1]^3 + 558*x[1]^2*x[2] - 41*x[2]^2 + 296*x[2]^3)* x[3] + x[3]^2 < 0 && 811 + 298*x[2] + 759*x[1]^2*x[2] - 1187*x[1]*x[2]^2 + (92 - 785*x[2] + 372*x[1]^2*x[2] + 348*x[2]^2)* x[3] + x[3]^2 >= 0 && 44 + 724*x[1]*x[2] - 721*x[1]^2*x[2] + 1038*x[2]^2 + (354 - 194*x[2] - 5*x[2]^2 + 397*x[1]*x[2]^2)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 809 + 327*x[1] - 370*x[2]^3 + (-552 + 128*x[2] - 936*x[2]^2 + 692*x[2]^3)*x[3] + x[3]^2 < 0 && -1071 + 34*x[1] + 925*x[2] + 283*x[1]*x[2] + (-435 - 701*x[1]^2 + 346*x[1]^3 - 182*x[1]*x[2])* x[3] + x[3]^2 < 0 && 626 + 131*x[1]^2 - 344*x[1]^2*x[2] - 115*x[2]^3 + (1443 - 731*x[1]^3 + 930*x[1]^2*x[2] + 75*x[1]*x[2]^2)* x[3] + x[3]^2 >= 0 && -933 + 48*x[2] + 370*x[1]*x[2] - 613*x[2]^2 - 1007*x[2]^3 + (734 + 164*x[1]^3 - 501*x[2] + 487*x[2]^3)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -618 - 212*x[1]*x[2] + 103*x[1]^2*x[2] - 882*x[2]^2 + (-939 + 719*x[1] + 1003*x[2] + 908*x[1]^2*x[2] + 100*x[2]^3)*x[3] + x[3]^2 == 0 && 291 + 216*x[1]^2 - 181*x[1]^3 + 247*x[2] + 537*x[2]^2 + (-187 + 112*x[1]*x[2] + 1481*x[1]^2*x[2] - 291*x[2]^3)* x[3] + x[3]^2 < 0 && -235 - 124*x[2] - 575*x[1]*x[2] - 681*x[1]*x[2]^2 - 909*x[2]^3 + (-942 - 910*x[1] + 580*x[2] - 406*x[1]^2*x[2] + 81*x[2]^3)*x[3] + x[3]^2 >= 0 && 883 - 552*x[1]^3 + 920*x[2] + 1621*x[1]^2*x[2] + (-821 + 945*x[2] - 555*x[1]^2*x[2] - 1213*x[2]^2)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 607 + 871*x[1]^3 - 73*x[2] - 1015*x[1]*x[2] + 469*x[2]^3 + (-593 - 398*x[1]^2 + 645*x[2] + 705*x[1]*x[2]^2 - 143*x[2]^3)*x[3] + x[3]^2 == 0 && 532 - 640*x[1]^2*x[2] + 1242*x[1]*x[2]^2 + (-295 - 316*x[1]^2 + 936*x[1]*x[2]^2 + 777*x[2]^3)*x[3] + x[3]^2 < 0 && 1257 - 236*x[1]^3 + 909*x[2] + (718 - 81*x[1] + 165*x[1]^3 - 1148*x[1]^2*x[2])*x[3] + x[3]^2 < 0 && -17 - 160*x[1]^2 + 790*x[1]^2*x[2] - 685*x[1]*x[2]^2 + (457 - 246*x[1]^3 - 497*x[1]*x[2] + 418*x[1]*x[2]^2 + 201*x[2]^3)* x[3] + x[3]^2 >= 0 && 958 - 175*x[1]*x[2] + 61*x[1]^2*x[2] + 844*x[1]*x[2]^2 - 313*x[2]^3 + (448 - 273*x[1] - 310*x[2]^2 + 249*x[1]*x[2]^2)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -637 + 839*x[1]^2*x[2] - 24*x[1]^2*x[2]^2 - 472*x[2]^3 - 811*x[1]*x[2]^3 + (569 + 1136*x[1]^2*x[2] + 10*x[1]*x[2]^2 - 304*x[1]*x[2]^3)*x[3] + x[3]^2 == 0 && 1345 + 271*x[1]^3 + 301*x[1]^3*x[2] + 990*x[1]*x[2]^3 + (-205 + 1017*x[1]^2 + 763*x[1]^3 + 1319*x[1]*x[2]^3)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 962 + 408*x[1]^2 + 387*x[2] + 126*x[1]*x[2]^2 + 244*x[2]^4 + (-610 + 134*x[1] - 541*x[1]^4 - 768*x[1]^2*x[2]^2)*x[3] + x[3]^2 == 0 && 884 - 470*x[1]^2 - 805*x[1]*x[2] + 473*x[1]^3*x[2] - 317*x[1]^2*x[2]^2 + (990 + 99*x[1] - 708*x[1]^2*x[2] + 115*x[1]^3*x[2] + 830*x[2]^3)*x[3] + x[3]^2 < 0 && 619 - 564*x[1]^2 + 398*x[1]^2*x[2]^2 - 337*x[2]^3 - 468*x[1]*x[2]^3 + (-10 + 11*x[2] - 537*x[2]^2 - 191*x[1]^2*x[2]^2 + 691*x[2]^3)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 764 + 597*x[1]^2*x[2] + 725*x[2]^2 - 713*x[2]^3 - 756*x[2]^4 + (-867 + 397*x[1]^3 + 832*x[1]*x[2]^2 - 148*x[1]*x[2]^3)*x[3] + x[3]^2 == 0 && 446 - 20*x[1]*x[2]^2 - 929*x[2]^3 - 447*x[2]^4 + (-546 + 335*x[1] - 728*x[1]^3*x[2] - 410*x[1]*x[2]^2 - 683*x[1]*x[2]^3)*x[3] + x[3]^2 < 0 && 982 - 920*x[1]^3 + 25*x[1]^2*x[2] - 138*x[2]^3 + 397*x[1]*x[2]^3 + (980 - 903*x[1]^2 - 245*x[1]*x[2]^2 + 925*x[1]^2*x[2]^2 - 765*x[1]*x[2]^3)*x[3] + x[3]^2 >= 0 && -383 + 187*x[1]^2 - 201*x[1]*x[2]^2 + 1326*x[2]^3 + (-202 - 694*x[1]*x[2] + 696*x[1]*x[2]^2 + 710*x[2]^3)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, -956 - 21*x[1]*x[2]^2 + 1437*x[1]^2*x[2]^3 + 294*x[1]*x[2]^4 + (-1007 - 451*x[1]^3 + 161*x[1]^4*x[2] - 176*x[1]*x[2]^2 + 590*x[2]^4)*x[3] + x[3]^2 == 0 && -314 - 131*x[1]^3 + 784*x[1]*x[2] + 669*x[2]^2 - 355*x[2]^3 + (1581 - 843*x[1] - 643*x[1]*x[2] - 371*x[1]*x[2]^3)*x[3] + x[3]^2 >= 0}, {{{Exists, {x[1], x[2], x[3]}}}, 469 + 121*x[2] + 647*x[1]^2*x[2] - 484*x[1]^2*x[2]^2 - 971*x[2]^3 + (412 - 324*x[1]^5 + 989*x[2]^2 + 622*x[1]*x[2]^3 - 943*x[1]*x[2]^4)* x[3] + x[3]^2 == 0 && 290 - 307*x[1]*x[2] - 203*x[1]^4*x[2] - 741*x[2]^3 + (980 - 346*x[1]^2*x[2] - 404*x[1]^2*x[2]^3 - 641*x[1]*x[2]^4 + 50*x[2]^5)*x[3] + x[3]^2 < 0 && -362 - 231*x[1]^2 - 554*x[1]^3*x[2]^2 + 449*x[1]*x[2]^3 - 464*x[1]^2*x[2]^3 + (-525 + 178*x[1] - 797*x[1]^2*x[2] + 624*x[1]^2*x[2]^3 + 947*x[2]^4)*x[3] + x[3]^2 >= 0}, {{{ForAll, {x[2]}}}, 694 - 739*x[1] + 212*x[1]^2 + 333*x[2] - 322*x[1]*x[2] - 88*x[2]^2 == 0 && 472 + 296*x[1] + 747*x[1]^2 + 889*x[2] - 844*x[1]*x[2] + 438*x[2]^2 == 0 && 194 - 728*x[1] - 983*x[1]^2 + 418*x[2] - 249*x[1]*x[2] - 195*x[2]^2 < 0 && -427 - 977*x[1] - 527*x[1]^2 - 683*x[2] - 963*x[1]*x[2] - 240*x[2]^2 >= 0}, {{{ForAll, {x[3]}}}, -335 + 627*x[1] + 947*x[1]^2 - 508*x[2] + 622*x[1]*x[2] - 411*x[2]^2 - 503*x[3] - 626*x[1]*x[3] - 457*x[2]*x[3] + 729*x[3]^2 == 0 && 854 + 853*x[1] + 390*x[1]^2 - 969*x[2] + 891*x[1]*x[2] - 803*x[2]^2 - 1013*x[3] - 598*x[1]*x[3] + 128*x[2]*x[3] - 435*x[3]^2 == 0 && 648 - 366*x[1] - 811*x[1]^2 - 457*x[2] + 510*x[1]*x[2] + 739*x[2]^2 + 586*x[3] - 223*x[1]*x[3] + 141*x[2]*x[3] + 110*x[3]^2 >= 0}, {{{ForAll, {x[3]}}, {Exists, {x[2]}}}, 846 + 928*x[1] + 92*x[1]^2 - 227*x[2] + 466*x[1]*x[2] + 846*x[2]^2 - 942*x[3] - 358*x[1]*x[3] + 42*x[2]*x[3] - 15*x[3]^2 < 0 && 221 + 791*x[1] + 51*x[1]^2 + 276*x[2] + 79*x[1]*x[2] + 609*x[2]^2 + 859*x[3] - 968*x[1]*x[3] - 589*x[2]*x[3] + 785*x[3]^2 >= 0}, {{{ForAll, {x[3]}}, {Exists, {x[2]}}}, 559 + 386*x[1] + 994*x[1]^2 - 365*x[2] - 323*x[1]*x[2] - 546*x[2]^2 - 498*x[3] + 36*x[1]*x[3] - 691*x[2]*x[3] - 744*x[3]^2 < 0 && -1005 + 744*x[1] + 449*x[1]^2 + 6*x[2] + 574*x[1]*x[2] - 55*x[2]^2 - 737*x[3] + 615*x[1]*x[3] + 920*x[2]*x[3] + 131*x[3]^2 >= 0 && 969 - 425*x[1] + 157*x[1]^2 + 478*x[2] + 561*x[1]*x[2] - 972*x[2]^2 - 851*x[3] - 759*x[1]*x[3] + 1009*x[2]*x[3] + 604*x[3]^2 >= 0}}; (************************************************************************* Code used to run the examples: *************************************************************************) factorcount[a:(_And|_Or)] := Plus@@(factorcount/@(List@@a)) factorcount[(Less|LessEqual|Greater|GreaterEqual|Equal|Unequal)[a_, b_]] := Plus@@(#[[2]]&/@Select[FactorList[a-b], !NumericQ[#[[1]]]&]) factorcount[other_] := 0 testvs[quants_, form_] := Module[{a, b}, Print["*** ", i++, " ***"]; a=Timing[Reduce`VirtSubstQE[quants, form, True]]; b={Chop[a[[1]]], factorcount[a[[2, 2]]], Length[a[[2, 3]]], a[[2, 4]]}; Print[b]; b] (************************************************************************* Code used to run the random examples: *************************************************************************) SeedRandom[1234]; rint[l_]:=Random[Integer, {-2^l, 2^l}] (* n variables, degree d, l bit coeeficients *) rterm[n_, d_, l_] := With[{t=Sort[Table[Random[Integer, {0, d}], {n}]]}, rint[l]*x[1]^t[[1]]*Times@@Table[x[i]^(t[[i]]-t[[i-1]]), {i, 2, n}]] (* n variables, degree d, l bit coeeficients, k terms *) rpoly[n_, d_, l_, k_] := Sum[rterm[n, d, l], {k-1}]+rint[l] (* Random polynomial of total degree 2 in n variables *) rqtot[n_, l_] := Sum[rint[l] x[i] x[j], {i, n}, {j, i, n}]+ Sum[rint[l] x[i], {i, n}]+rint[l] (* Random polynomial of degree 2 in x[n+1], with rpoly[n, d, l, k] coeffs. *) rquad[n_, d_, l_, k_] := rpoly[n, d, l, k] x[n+1]^2+rpoly[n, d, l, k] x[n+1]+rpoly[n, d, l, k] (* Monic rquad. *) rmquad[n_, d_, l_, k_] := x[n+1]^2+rpoly[n, d, l, k] x[n+1]+rpoly[n, d, l, k] test1[n_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rqtot[n, 10]==0, {neq}] && And@@Table[rqtot[n, 10]<0, {m}] && And@@Table[rqtot[n, 10]>=0, {nin-m}]; {{{Exists, {x[n]}}}, form}] test2[n_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rqtot[n, 10]==0, {neq}] && And@@Table[rqtot[n, 10]<0, {m}] && And@@Table[rqtot[n, 10]>=0, {nin-m}]; {{{Exists, {x[n], x[n-1]}}}, form}] test3[n_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rqtot[n, 10]==0, {neq}] && And@@Table[rqtot[n, 10]<0, {m}] && And@@Table[rqtot[n, 10]>=0, {nin-m}]; {{{Exists, x/@Range[n]}}, form}] test4[n_, d_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rquad[n-1, d, 10, 5]==0, {neq}] && And@@Table[rquad[n-1, d, 10, 5]<0, {m}] && And@@Table[rquad[n-1, d, 10, 5]>=0, {nin-m}]; {{{Exists, {x[n]}}}, form}] test5[n_, d_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rquad[n-1, d, 10, 5]==0, {neq}] && And@@Table[rquad[n-1, d, 10, 5]<0, {m}] && And@@Table[rquad[n-1, d, 10, 5]>=0, {nin-m}]; {{{Exists, x/@Range[n]}}, form}] test6[n_, d_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rmquad[n-1, d, 10, 5]==0, {neq}] && And@@Table[rmquad[n-1, d, 10, 5]<0, {m}] && And@@Table[rmquad[n-1, d, 10, 5]>=0, {nin-m}]; {{{Exists, {x[n]}}}, form}] test7[n_, d_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rmquad[n-1, d, 10, 5]==0, {neq}] && And@@Table[rmquad[n-1, d, 10, 5]<0, {m}] && And@@Table[rmquad[n-1, d, 10, 5]>=0, {nin-m}]; {{{Exists, x/@Range[n]}}, form}] test8[n_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rqtot[n, 10]==0, {neq}] && And@@Table[rqtot[n, 10]<0, {m}] && And@@Table[rqtot[n, 10]>=0, {nin-m}]; {{{ForAll, {x[n]}}}, form}] test9[n_, neq_, nin_] := Module[{form, m=Floor[nin/2]}, form=And@@Table[rqtot[n, 10]==0, {neq}] && And@@Table[rqtot[n, 10]<0, {m}] && And@@Table[rqtot[n, 10]>=0, {nin-m}]; {{{ForAll, {x[n]}}, {Exists, {x[n-1]}}}, form}] examples={ {{{Exists, {x}}}, u x^2+v x+1==0 && v x^3+w x+u==0 && w x^2+v x+u<=0}, {{{Exists, {r}}}, 3a r^2-a^2-2a r+3b^2 r-b^2<0 && 3a^2 r-2a^2-4a r+2a+3b^2 r-2 b^2+r>0 && a>=1/2 && b>0 && r>0 && r<1}, {{{ForAll, {a, b}}, {Exists, {c}}}, Implies[a==d && b==c || a==c && b==1, a^2==b]}, {{{ForAll, {x, y}}}, Implies[b^2 (x-c)^2+a^2 y^2-a^2 b^2==0, x^2+y^2<=1]}, {{{Exists, {x}}}, aa1 x^2+bb1 x+cc1==0 && aa2 x^2+bb2 x+cc2==0 && aa3 x^2+bb3 x+cc3<0 && aa4 x^2+bb4 x+cc4<0 && aa5 x^2+bb5 x+cc5<0}, {{{ForAll, {x, y}}}, 1+x^2 y^2(x^2+y^2-3)>=0}, {{{ForAll, {x, y}}, {Exists, {r}}}, (Implies[x>r && y>r, x^2(1+2y)^2>y^2(1+2x^2)])}, {{{Exists, {x, y}}}, (x^2+y^2+z^2==1 && z^3+x z+y==0)}, {{{Exists, {r}}}, (r^2-24r+16<0 || r>1 && r^2-24r+16>=0) && -10}, {{{Exists, {x, y}}}, (-7x y z+6y z-14x z+9 z-3x y-12 y-x+1==0 && 2 x y z-y z+14 z+15x y+14 y-15x==0 && -8x y z+11y z-12x z-5 z+15x y+2y+10x-14==0)}, {{{Exists, {x, y}}}, 1<=4a<=7 && -3<=4b<=3 && -1<=x<=0 && 0<=y<=1 && 3x^2-2x-a==0 && x^3-x^2-a x==2b-a+2 && 3y^2-2y-a==0 && y^3-y^2-a y==a-2}, {{{ForAll, {p1, p2, w1, w2}}}, Implies[16<=20p1<=25 && 16<=20p2<=25 && 0<=w1<=2, p2(1+p1 q1)<0 && -24w1^2+p2^2((1+p1 q1)^2-25)>0 && (400-q1^2) w2^2+p2^2(400(1+p1 q1)^2-q1^2)>0]}, {{{ForAll, {w}}, {Exists, {q1, q2}}}, q1>1 && q2>0 && Implies[nbyd>=0, (nbyd-q1^2)w^4+(nbyd((1+q1)^2-2 q2)-(q2^2+q1^2))w^2+(nbyd-1)q2^2>=0 && (nbyd-q1^2)w^4+(nbyd((-1+q1)^2-2 q2)-(q2^2+q1^2))w^2+(nbyd-1)q2^2>=0]}, {{{ForAll, {x}}, {Exists, {d}}, {ForAll, {e}}}, Implies[e > 0, d > 0 && Implies[-d < -1 + x < d, (1+x)>0 && -e(1+x) < -l(1+x) + x-2 < e(1+x) || (1+x)<0 && -e(1+x) > -l(1+x) + x-2 > e(1+x)]]}, {{{ForAll, {a, b, c, d, e, f}}}, a < 0 || b < 0 || c < 0 || d < 0 || e < 0 || f < 0 || a^2 + b^2 > e^2 || c^2 + d^2 > f^2 || a*c + b*d <= e*f}, {{{ForAll, {a, b, c, l}}}, Implies[a + c >= b && c >= 0 && b + c >= a && b >= 0 && a + b >= c && a >= 0 && l > 0, (((a + b + c)/2 + a*l)*((a + b + c)/2 + b*l)*((a + b + c)/2 + c*l)) >= (3 + 2*l)^3*((-a + (a + b + c)/2)*(-b + (a + b + c)/2)*(-c + (a + b + c)/2))]}, test1[2, 1, 3], test1[2, 10, 10], test1[2, 0, 5], test1[3, 1, 2], test1[3, 1, 4], test1[3, 0, 2], test1[3, 0, 3], test1[3, 0, 4], test2[2, 1, 5], test2[3, 1, 2], test2[3, 1, 3], test2[3, 0, 2], test2[3, 0, 3], test3[4, 1, 2], test3[3, 0, 3], test3[3, 1, 3], test4[2, 3, 1, 3], test4[2, 5, 1, 3], test4[2, 5, 0, 4], test4[3, 4, 1, 1], test4[3, 5, 0, 1], test5[3, 5, 0, 2], test5[4, 3, 1, 1], test6[2, 7, 0, 3], test6[2, 7, 1, 3], test6[2, 7, 1, 5], test7[4, 3, 1, 1], test7[3, 3, 0, 3], test7[3, 3, 0, 4], test7[3, 3, 1, 3], test7[3, 3, 1, 4], test7[3, 4, 1, 1], test7[3, 4, 1, 2], test7[3, 4, 1, 3], test7[3, 5, 1, 1], test7[3, 5, 1, 2], test8[2, 2, 2], test8[3, 2, 1], test9[3, 0, 2], test9[3, 0, 3]}; (* This tells whether the new inequality simplifications should be used. *) SetSystemOption["InequalitySolvingOptions"->{"SimplifyInequalities"->False}] (* SetSystemOption["InequalitySolvingOptions"->{"SimplifyInequalities"->True}] *) (* This removes restrictions on disjunctive normal form computations. *) System`Private`SetInternalVariable["VSTermBound", 0] System`Private`SetInternalVariable["VSPrimeImplicantsBound", 1000] i=1; ans=testvs@@@examples;