sol=Reduce[(x^2)+(y^2)≤ (z^2)&&(Subscript[∃, t])((Subscript[∀, u])t x>u y z+7||(x^2) t==2 z+1),{x,y,z},Reals]

lexp[e_Or]:=lexp/@e
lexp[And[a___,b_Or,c___]]:=lexp[And[a,#,c]]&/@b
lexp[other_]:=other

lexp[sol]

Resolve[(x^2)+(y^2)≤ (z^2)&&(Subscript[∃, t])((Subscript[∀, u])t x>u y z+7||(x^2) t==2 z+1),Reals]

FindInstance[(x^2)+(y^2)≤ (z^2)&&(Subscript[∃, t])((Subscript[∀, u])t x>u y z+7||(x^2) t==2 z+1),{x,y,z},Reals]

CylindricalDecomposition[1≤ x^2+y^2<2, {x, y}]

SemialgebraicComponentInstances[1≤ x^2+y^2<2, {x, y}]

Reduce[(Subscript[∃, {x,y}])((x^2)+(y^2)≤(16/25)&&(x^4)+(y^4)-2 x y>1),Reals]

FindInstance[(x^2)+(y^2)≤1&&(x^4)+(y^4)-2 x y>1, {x, y},Reals]

Reduce[(Subscript[∀, {x,y},r>0&&(x^2)+(y^2)≤(r^2)])(x^4)+(y^4)-2 x y≤1,r,Reals]

Reduce[(Subscript[∃, z])(x^2)+(y^2)+(z^2)-x y z≤1,{x,y}]

Reduce[(Subscript[∃, x])(x^2)-(y^2) z==0,{y,z},Reals]

Reduce[(Subscript[∃, d,d>0])((Subscript[∀, {v,w},(((v-y))^2)+(((w-z))^2)≤d])((Subscript[∃, u])(u^2)-(v^2) w==0)),{y,z},Reals]

Resolve[(Subscript[∃, x])(a x≥(b^3)-3 a (c^2)-5 (a^3) b c+9&&b (c^2) x-3 x≤11 (a^2) b-3 (c^3)+4 a (b^2) c+9)]

(RefLink[Reduce, paclet:ref/Reduce]), (RefLink[Resolve, paclet:ref/Resolve]), and (RefLink[FindInstance, paclet:ref/FindInstance]) options affecting the behavior for real polynomial systems.

Reduce[(x^3)-3 x+7==0, x,Reals]

Reduce[(x^3)-3 x+7==0, x, Reals,Cubics->True]

Reduce[(x^3)==a,x,Reals,Cubics->True]

sol=Reduce[(x^3)==a,x,Cubics->True]

sol/.{{a->-1},{a->1}}

Reduce[(Subscript[∃, {y,z}])((x^4)+2 (y^4)+3 (z^4)≤1&&(x^3)-9 (y^3)+7 (z^3)≥2),x,Reals,WorkingPrecision->30]//Timing

Reduce[(Subscript[∃, {y,z}])((x^4)+2 (y^4)+3 (z^4)≤1&&(x^3)-9 (y^3)+7 (z^3)≥2),x,Reals]//Timing

(RefLink[SetSystemOptions, paclet:ref/SetSystemOptions])["ReduceOptions"->{"option name"->value}].

ReduceOptions group options affecting the behavior of (RefLink[Reduce, paclet:ref/Reduce]), (RefLink[Resolve, paclet:ref/Resolve]), and (RefLink[FindInstance, paclet:ref/FindInstance]) for real polynomial systems.

AlgebraicNumberOutput

Reduce[(y^5)-3 (y^2)+(x^5)+4==0&&(y^2)+y-(x^5)-3 x-11==0,{x,y},Reals,Backsubstitution->True]

SetSystemOptions["ReduceOptions"->"AlgebraicNumberOutput"->False];
Reduce[(y^5)-3 (y^2)+(x^5)+4==0&&(y^2)+y-(x^5)-3 x-11==0,{x,y},Reals,Backsubstitution->True]

SetSystemOptions["ReduceOptions"->"AlgebraicNumberOutput"->True];

FactorEquations

SetSystemOptions["ReduceOptions"->"FactorEquations"->False];
t1=Timing[Reduce[((x^2)-2 y z) ((x^3)-y+z)==0&&(x^3)-2 x y+3 y z+(z^4)==0&&(x^4)-y (z^3)==2,{x,y,z}]][[1]];
t2=Timing[Reduce[((x^2)-2 y z) ((x^3)-y+z)==0&&(x^3)-2 x y+3 y z+(z^4)<0&&(x^4)-y (z^3)≥2,{x,y,z},Reals]][[1]];
{t1,t2}

SetSystemOptions["ReduceOptions"->"FactorEquations"->True];
t1=Timing[Reduce[((x^2)-2 y z) ((x^3)-y+z)==0&&(x^3)-2 x y+3 y z+(z^4)==0&&(x^4)-y (z^3)==2,{x,y,z}]][[1]];
t2=Timing[Reduce[((x^2)-2 y z) ((x^3)-y+z)==0&&(x^3)-2 x y+3 y z+(z^4)<0&&(x^4)-y (z^3)≥2,{x,y,z},Reals]][[1]];
{t1,t2}

SetSystemOptions["ReduceOptions"->"FactorEquations"->Automatic];

FactorInequalities

t1=Timing[Reduce[((x^3)-5 x (y^2)-3 (y^2)+7 (z^2)-1) ((x^2)-3 x y+5 (y^2)+3 y z-2) ((x^2)-2 z+y-3)≤0&&((x^3)-5 x (y^2)-3 (y^2)+7 (z^2)-1) ((x^2)-3 x y+5 (y^2)+3 y z-2)≥0&&(x^2)-2 z+y-3>0,{x,y,z},Reals]][[1]];
t2=Timing[Reduce[(∏_(i=1)^10)(x-y i)≤0,{x,y},Reals]][[1]];
{t1,t2}

SetSystemOptions["ReduceOptions"->"FactorInequalities"->True];
t1=Timing[Reduce[((x^3)-5 x (y^2)-3 (y^2)+7 (z^2)-1) ((x^2)-3 x y+5 (y^2)+3 y z-2) ((x^2)-2 z+y-3)≤0&&((x^3)-5 x (y^2)-3 (y^2)+7 (z^2)-1) ((x^2)-3 x y+5 (y^2)+3 y z-2)≥0&&(x^2)-2 z+y-3>0,{x,y,z},Reals]][[1]];
t2=Timing[Reduce[(∏_(i=1)^10)(x-y i)≤0,{x,y},Reals]][[1]];
{t1,t2}

SetSystemOptions["ReduceOptions"->"FactorInequalities"->False];

ReorderVariables

Reduce[x>(y^3)+7 y-1,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"ReorderVariables"->True];
Reduce[x>(y^3)+7 y-1,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"ReorderVariables"->Automatic];

Solve[x==(y^3)+7 y-1&&(y^5)-y==2,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"ReorderVariables"->False];
Solve[x==(y^3)+7 y-1&&(y^5)-y==2,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"ReorderVariables"->Automatic];

UseNestedRoots

Reduce[(x^3)+x+1==0&&(y^3)+3 (x^2) y+1==0,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->False];
Reduce[(x^3)+x+1==0&&(y^3)+3 (x^2) y+1==0,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->Automatic];
Reduce[(x^7)+x+1==0&&(y^7)+3 (x^2) y+1==0&&(z^7)+3 (y^2) z+1==0,{x,y,z},Reals]//Timing

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->False];
Reduce[(x^7)+x+1==0&&(y^7)+3 (x^2) y+1==0&&(z^7)+3 (y^2) z+1==0,{x,y,z},Reals]//Timing

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->True];
Reduce[(x^3)+x (y^2)-x-1==0&&(y^3)+3 (x^2) y+1==0,{x,y},Reals]

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->Automatic];
Reduce[(x^3)+x (y^2)-x-1==0&&(y^3)+3 (x^2) y+1==0,{x,y},Reals]

(RefLink[SetSystemOptions, paclet:ref/SetSystemOptions])["InequalitySolvingOptions"->{"option name"->value}].

InequalitySolvingOptions group options affecting the behavior of (RefLink[Reduce, paclet:ref/Reduce]), (RefLink[Resolve, paclet:ref/Resolve]), and (RefLink[FindInstance, paclet:ref/FindInstance]) for real polynomial systems.

ARSDecision

SetSystemOptions["InequalitySolvingOptions"->"ARSDecision"->True];FindInstance[-a-b+(Subscript[b, 1])+(Subscript[b, 2])+(Subscript[b, 3])==0&&-(1/2)-(b/2)+a b-(b^2)+(Subscript[b, 2]) (Subscript[c, 2])+(Subscript[b, 3]) (Subscript[c, 3])==0&&((4 b)/3)+(b^2)+(b^3)-a ((1/3)+(b^2))+(Subscript[b, 2]) (Subscript[c, 2]^2)+(Subscript[b, 3]) (Subscript[c, 3]^2)==0&&((2 b)/3)+(b^2)+(b^3)-a ((1/6)+(b/2)+(b^2))+(Subscript[b, 3]) (Subscript[c, 2]) (Subscript[a, 3,2])==0&&-(1/4)-(b/4)-((5 (b^2))/2)-((3 (b^3))/2)-(b^4)+a (b+(b^3))+(Subscript[b, 2]) (Subscript[c, 2]^3)+(Subscript[b, 3]) (Subscript[c, 3]^3)==0&&-(1/8)-((3 b)/8)-((7 (b^2))/4)-((3 (b^3))/2)-(b^4)+a ((b/2)+((b^2)/2)+(b^3))+(Subscript[b, 3]) (Subscript[c, 2]) (Subscript[c, 3]) (Subscript[a, 3,2])==0&&-(1/12)-(b/12)-((7 (b^2))/6)-((3 (b^3))/2)-(b^4)+a (((2 b)/3)+(b^2)+(b^3))+(Subscript[b, 3]) (Subscript[c, 2]^2) (Subscript[a, 3,2])==0&&(1/24)+((7 b)/24)+((13 (b^2))/12)+((3 (b^3))/2)+(b^4)-a ((b/3)+(b^2)+(b^3))==0,{a,b,(Subscript[a, 3,2]),(Subscript[b, 1]),(Subscript[b, 2]),(Subscript[b, 3]),(Subscript[c, 2]),(Subscript[c, 3])},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ARSDecision"->False];

BrownProjection

t1=Timing[Reduce[(Subscript[∃, {q1,q2},q1>1&&q2>0])((Subscript[∀, w,w∈Reals])((4-(q1^2)) (w^4)+(4 ((((1+q1))^2)-2 q2)-((q2^2)+(q1^2))) (w^2)+3 (q2^2)≥0&&(4-(q1^2)) (w^4)+(4 ((((-1+q1))^2)-2 q2)-((q2^2)+(q1^2))) (w^2)+3 (q2^2)≥0))]][[1]];
f=(x^3)-5 x y-3 (y^2)+7;
g=(x^4)-4 (x^2) y-(y^3)-1;
t2=Timing[Reduce[f (z^2)<f+g,{x,y,z},Reals]][[1]];
{t1,t2}

SetSystemOptions["InequalitySolvingOptions"->"BrownProjection"->False];

t1=Timing[Reduce[(Subscript[∃, {q1,q2},q1>1&&q2>0])((Subscript[∀, w,w∈Reals])((4-(q1^2)) (w^4)+(4 ((((1+q1))^2)-2 q2)-((q2^2)+(q1^2))) (w^2)+3 (q2^2)≥0&&(4-(q1^2)) (w^4)+(4 ((((-1+q1))^2)-2 q2)-((q2^2)+(q1^2))) (w^2)+3 (q2^2)≥0))]][[1]];
t2=Timing[Reduce[f (z^2)<f+g,{x,y,z},Reals]][[1]];
{t1,t2}

SetSystemOptions["InequalitySolvingOptions"->"BrownProjection"->True];

CAD

SetSystemOptions["InequalitySolvingOptions"->"CAD"->False];
Reduce[(x^12)+2 (x^7) (y^5) (z^3)-21 (z^4) (t^2) (y^7)+19≤0&&(t^7)-24 (x^5) (y^4) z-32 (z^11)==0,{x,y,z,t},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"CAD"->True];

CADBacksubstitution

CylindricalDecomposition[(x^2)==4&&(y^2)<x,{x,y}]

CylindricalDecomposition[(x^2)==2&&(y^2)<x,{x,y}]

SetSystemOptions["InequalitySolvingOptions"->"CADBacksubstitution"->True];
CylindricalDecomposition[(x^2)==4&&(y^2)<x,{x,y}]

CylindricalDecomposition[(x^2)==2&&(y^2)<x,{x,y}]

SetSystemOptions["InequalitySolvingOptions"->"CADBacksubstitution"->False];
CylindricalDecomposition[(x^2)==4&&(y^2)<x,{x,y}]

CylindricalDecomposition[(x^2)==2&&(y^2)<x,{x,y}]

SetSystemOptions["InequalitySolvingOptions"->"CADBacksubstitution"->Automatic];

CADCombineCells

CylindricalDecomposition[(y^3)-x y-1==0&&-3 (y^2)+x≤0&&(y^3)-4<0,{x,y}]

Plot[Root[-1-x #1+((#1)^3)&,1],{x,-5,5},Exclusions->{Discriminant[(y^3)-x y-1,y]==0}]

SetSystemOptions["InequalitySolvingOptions"->"CADCombineCells"->Automatic];
CylindricalDecomposition[(y^3)-x y-1==0&&-3 (y^2)+x≤0&&(y^3)-4<0,{x,y}]

CylindricalDecomposition[(x^2)+(y^2)==1&&y≤1,{x,y}]

SetSystemOptions["InequalitySolvingOptions"->"CADCombineCells"->False];
CylindricalDecomposition[(x^2)+(y^2)==1&&y≤1,{x,y}]

SetSystemOptions["InequalitySolvingOptions"->"CADCombineCells"->True];

CADConstruction

SetSystemOptions["InequalitySolvingOptions"->"CADConstruction"->"GlobalProjection"];
syst=-21+28*x[1]*x[4]+68*x[3]*x[4]+64*x[2]*x[5]+46*x[5]^2-66*x[3]*x[6]+42*x[4]*x[6]≤0;
vars={x[1],x[2],x[3],x[4],x[5],x[6]};
CylindricalDecomposition[syst,vars];//AbsoluteTiming

SetSystemOptions["InequalitySolvingOptions"->"CADConstruction"->"LocalProjection"];
CylindricalDecomposition[syst,vars];//AbsoluteTiming

SetSystemOptions["InequalitySolvingOptions"->"CADConstruction"->Automatic];
CylindricalDecomposition[syst,vars];//AbsoluteTiming

LaunchKernels[2];
CylindricalDecomposition[syst,vars];//AbsoluteTiming

CloseKernels[];

CADDefaultPrecision and CADExtraPrecision

Reduce[(Subscript[∃, {x,y}])(931+576 (y^3)+626 (x^2) y-564 y z-750 (z^2)<0&&-535+961 y+578 z≤0&&-410+528 (y^2)-905 x≤0&&(z^2)-71 x y+4 (y^2)-81≤0),z,Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADDefaultPrecision"->16];
Reduce[(Subscript[∃, {x,y}])(931+576 (y^3)+626 (x^2) y-564 y z-750 (z^2)<0&&-535+961 y+578 z≤0&&-410+528 (y^2)-905 x≤0&&(z^2)-71 x y+4 (y^2)-81≤0),z,Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADDefaultPrecision"->30.103];

CADMethod

SetSystemOptions["InequalitySolvingOptions"->"CADMethod"->"Direct"];
CylindricalDecomposition[Or@@Table[(((x-a))^2)+(((y-a))^2)+(((z-a))^2)≤1,{a,0,20}],{x,y,z}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADMethod"->"Recursive"];
CylindricalDecomposition[Or@@Table[(((x-a))^2)+(((y-a))^2)+(((z-a))^2)≤1,{a,0,20}],{x,y,z}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADMethod"->"Direct"];
CylindricalDecomposition[(((-(1/2)+x))^2)+(((-(989/1142)+y))^2)+(z^2)≤2&&((((1/2)+x))^2)+(((-(989/1142)+y))^2)+(z^2)≤2&&(((1+x))^2)+(y^2)+(z^2)≤2&&((((1/2)+x))^2)+((((989/1142)+y))^2)+(z^2)≤2&&(((-(1/2)+x))^2)+((((989/1142)+y))^2)+(z^2)≤2&&(((-1+x))^2)+(y^2)+(z^2)≤2,{x,y,z}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADMethod"->"Iterative"];
CylindricalDecomposition[(((-(1/2)+x))^2)+(((-(989/1142)+y))^2)+(z^2)≤2&&((((1/2)+x))^2)+(((-(989/1142)+y))^2)+(z^2)≤2&&(((1+x))^2)+(y^2)+(z^2)≤2&&((((1/2)+x))^2)+((((989/1142)+y))^2)+(z^2)≤2&&(((-(1/2)+x))^2)+((((989/1142)+y))^2)+(z^2)≤2&&(((-1+x))^2)+(y^2)+(z^2)≤2,{x,y,z}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADMethod"->Automatic];

CADSortVariables

Reduce[(Subscript[∀, {(Subscript[p, 1]),(Subscript[p, 2]),(Subscript[w, 1]),(Subscript[w, 2])},16≤20 (Subscript[p, 1])≤25&&16≤20 (Subscript[p, 2])≤25&&0≤(Subscript[w, 1])≤2])((Subscript[p, 2]) (1+(Subscript[p, 1]) (Subscript[q, 1]))<0&&-24 (Subscript[w, 1]^2)+(Subscript[p, 2]^2) ((((1+(Subscript[p, 1]) (Subscript[q, 1])))^2)-25)>0&&(400-(Subscript[q, 1]^2)) (Subscript[w, 2]^2)+(Subscript[p, 2]^2) (400 (((1+(Subscript[p, 1]) (Subscript[q, 1])))^2)-(Subscript[q, 1]^2))>0),(Subscript[q, 1]),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADSortVariables"->False];

Reduce[(Subscript[∀, {(Subscript[w, 1]),(Subscript[w, 2]),(Subscript[p, 2]),(Subscript[p, 1])},16≤20 (Subscript[p, 1])≤25&&16≤20 (Subscript[p, 2])≤25&&0≤(Subscript[w, 1])≤2])((Subscript[p, 2]) (1+(Subscript[p, 1]) (Subscript[q, 1]))<0&&-24 (Subscript[w, 1]^2)+(Subscript[p, 2]^2) ((((1+(Subscript[p, 1]) (Subscript[q, 1])))^2)-25)>0&&(400-(Subscript[q, 1]^2)) (Subscript[w, 2]^2)+(Subscript[p, 2]^2) (400 (((1+(Subscript[p, 1]) (Subscript[q, 1])))^2)-(Subscript[q, 1]^2))>0),(Subscript[q, 1]),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"CADSortVariables"->True];

CADZeroTest

SetSystemOptions["InequalitySolvingOptions"->"CADDefaultPrecision"->Infinity];
Timing[Reduce[(Subscript[∃, z])((z^3)-(a^2) z+b==0&&(z^3)-(b^2) z+a==0),{a,b},Reals]][[1]]

SetSystemOptions["InequalitySolvingOptions"->"CADZeroTest"->{2,30}];
Timing[Reduce[(Subscript[∃, z])((z^3)-(a^2) z+b==0&&(z^3)-(b^2) z+a==0),{a,b},Reals]][[1]]

SetSystemOptions["InequalitySolvingOptions"->"CADZeroTest"->{0,Infinity}];
SetSystemOptions["InequalitySolvingOptions"->"CADDefaultPrecision"->30.103];
Timing[Reduce[(Subscript[∃, z])((z^3)-(a^2) z+b==0&&(z^3)-(b^2) z+a==0),{a,b},Reals]][[1]]

EquationalConstraintsCAD

SetSystemOptions["InequalitySolvingOptions"->"EquationalConstraintsCAD"->True];
FindInstance[(x^2)+(y^2)+(z^2)+(t^2)==1&&(x^2) (y^2)==(z^2)-2 t z&&x y-z t==3 (u^2)&&x+y+z+t+u≤3,{x,y,z,t,u},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"EquationalConstraintsCAD"->Automatic];
FindInstance[(x^2)+(y^2)+(z^2)+(t^2)==1&&(x^2) (y^2)==(z^2)-2 t z&&x y-z t==3 (u^2)&&x+y+z+t+u≤3,{x,y,z,t,u},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"EquationalConstraintsCAD"->False];
FindInstance[(x^2)+(y^2)+(z^2)+(t^2)==1&&(x^2) (y^2)==(z^2)-2 t z&&x y-z t==3 (u^2)&&x+y+z+t+u≤3,{x,y,z,t,u},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"EquationalConstraintsCAD"->True];
FindInstance[(x^2)+(y^2)+(z^2)+(t^2)==1&&(x^2) (y^2)==(z^2)-2 t z&&x y-z t==3 (u^2)&&(t z-1) (t z-2)<1,{x,y,z,t,u},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"EquationalConstraintsCAD"->Automatic];
FindInstance[(x^2)+(y^2)+(z^2)+(t^2)==1&&(x^2) (y^2)==(z^2)-2 t z&&x y-z t==3 (u^2)&&(t z-1) (t z-2)<1,{x,y,z,t,u},Reals]//Timing

FGLMBasisConversion

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->False];
t1=Timing[Reduce[(x^10)+3 (x^4)-5 (x^3)+7 (x^2)-9 x==11&&(y^7)-(y^2)+x==1&&(z^5)+2 z-3 x==4,{x,y,z},Reals]];
SetSystemOptions["InequalitySolvingOptions"->"FGLMBasisConversion"->True];
t2=Timing[Reduce[(x^10)+3 (x^4)-5 (x^3)+7 (x^2)-9 x==11&&(y^7)-(y^2)+x==1&&(z^5)+2 z-3 x==4,{x,y,z},Reals]];
{t1[[1]],t2[[1]],t1[[2]]===t2[[2]]}

SetSystemOptions["ReduceOptions"->"UseNestedRoots"->Automatic];
SetSystemOptions["InequalitySolvingOptions"->"FGLMBasisConversion"->False];

FGLMElimination

Resolve[(Subscript[∃, z])((x^2)+2 (y^3)-3 x y+4 x z+2 (z^3)==1&&(y^3)-2 (x^2) z+5 x-7 (z^3)==2&&3 x y+4 (z^3)-5 (y^3)==0),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"FGLMElimination"->False];
Resolve[(Subscript[∃, z])((x^2)+2 (y^3)-3 x y+4 x z+2 (z^3)==1&&(y^3)-2 (x^2) z+5 x-7 (z^3)==2&&3 x y+4 (z^3)-5 (y^3)==0),Reals]//Timing//N

SetSystemOptions["InequalitySolvingOptions"->"FGLMElimination"->Automatic];
Resolve[(Subscript[∃, {y,z}])((x^2)+2 (y^3)-3 x y+4 x z+2 (z^3)==1&&(y^3)-2 (x^2) z+5 x-7 (z^3)==2&&3 x y+4 (z^3)-5 (y^3)==0),Reals]//Timing//N

SetSystemOptions["InequalitySolvingOptions"->"FGLMElimination"->True];
Resolve[(Subscript[∃, {y,z}])((x^2)+2 (y^3)-3 x y+4 x z+2 (z^3)==1&&(y^3)-2 (x^2) z+5 x-7 (z^3)==2&&3 x y+4 (z^3)-5 (y^3)==0),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"FGLMElimination"->Automatic];

GenericCAD

FindInstance[(x^4)+(y^4)+(z^4)≤12&&(x^2) (y^2)-3 (x^2) (z^2)≥1&&x y≤3 (z^3)+4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->False];
FindInstance[(x^4)+(y^4)+(z^4)≤12&&(x^2) (y^2)-3 (x^2) (z^2)≥1&&x y≤3 (z^3)+4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->True];

FindInstance[(x^4)+(y^4)+(z^4)≤12&&(x^3)+(y^3)-(z^3)≥9,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->False];
FindInstance[(x^4)+(y^4)+(z^4)≤12&&(x^3)+(y^3)-(z^3)≥9,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->True];

FindInstance[(x^4)+(y^4)+(z^4)<12&&(x^2) (y^2)-3 (x^2) (z^2)>7&&x y<3 (z^3)+4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->False];
FindInstance[(x^4)+(y^4)+(z^4)<12&&(x^2) (y^2)-3 (x^2) (z^2)>7&&x y<3 (z^3)+4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"GenericCAD"->True];

GroebnerCAD

a1=Reduce[(x^3)+(y^3)+(z^3)==12&&(x^2) (y^2)-3 (x^2) (z^2)==1&&x y==3 (z^5)+4,{x,y,z},Reals];//Timing

SetSystemOptions["InequalitySolvingOptions"->"GroebnerCAD"->False];

a2=Reduce[(x^3)+(y^3)+(z^3)==12&&(x^2) (y^2)-3 (x^2) (z^2)==1&&x y==3 (z^5)+4,{x,y,z},Reals];//Timing

N[{x,y,z}//.{ToRules[a1]},20]-N[{x,y,z}//.{ToRules[a2]},20]

SetSystemOptions["InequalitySolvingOptions"->"GroebnerCAD"->True];

LinearDecisionMethodCrossovers, LWDecision, and Simplex

FindInstance[x+2y+3z==4&&5x+6y-7z≤8&&9x-10y+11z>12,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearDecisionMethodCrossovers"->{0,0,20,Automatic}];
FindInstance[x+2y+3z==4&&5x+6y-7z≤8&&9x-10y+11z>12,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearDecisionMethodCrossovers"->{10,0,20,Automatic}];
FindInstance[x+2y+3z==4&&5x+6y-7z≤8&&9x-10y+11z>12,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearDecisionMethodCrossovers"->{0,30,20,Automatic}];

FindInstance[x+π y+E z>Sin[1]&&Log[2] x+(π^E) y-(7^π) z==(8/E),{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWDecision"->False];
FindInstance[x+π y+E z>Sin[1]&&Log[2] x+(π^E) y-(7^π) z==(8/E),{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWDecision"->True];

LinearEquations

FindInstance[x+2 (y^2)+(z^3)==7&&2 (x^2) (y^3)-3 x (z^3)+5 x y z-(x^3)+x+y-z≥3&&4 x (y^3)+5 (y^4) (z^2)+11 y (z^2)≤3 (z^3)+7&&(x^2)+(y^2)+(z^2)≤4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearEquations"->False];
FindInstance[x+2 (y^2)+(z^3)==7&&2 (x^2) (y^3)-3 x (z^3)+5 x y z-(x^3)+x+y-z≥3&&4 x (y^3)+5 (y^4) (z^2)+11 y (z^2)≤3 (z^3)+7&&(x^2)+(y^2)+(z^2)≤4,{x,y,z},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearEquations"->True];

LinearQE

a1=Reduce[(Subscript[∃, {x,y}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)-x≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^3)+(z^3)≤(z^2) y-3 y+5 x),{z,t}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->Automatic];
a2=Reduce[(Subscript[∃, {x,y}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)-x≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^3)+(z^3)≤(z^2) y-3 y+5 x),{z,t}];//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->False];
a3=Reduce[(Subscript[∃, {x,y}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)-x≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^3)+(z^3)≤(z^2) y-3 y+5 x),{z,t}];//Timing

a1===a2===a3

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->True];
Reduce[(Subscript[∃, {x,y,z}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y),t]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->Automatic];
Reduce[(Subscript[∃, {x,y,z}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y),t]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->False];
Reduce[(Subscript[∃, {x,y,z}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y),t]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LinearQE"->True];
Resolve[(Subscript[∃, {x,y}])(2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)u+v^7-6w^4t≤3&&3 x-5 t (z^2)-3 (t^2)-y z t-5y w z≥2),Reals]//Timing

LWPreprocessor

FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->True];
FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->False];
FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)≤z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->Automatic];
FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)==z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->True];
FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)==z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->False];
FindInstance[2 x+3 y z+4 (z^2) t≤1&&5 (t^3) y+7 (z^4)-4 (t^3)+4 (z^2) (t^2)≤3&&3 x-5 t (z^2)-3 (t^2)-y z t≥2&&(t^2)+(z^2)==z y,{x,y,z,t}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"LWPreprocessor"->Automatic];

ProjectAlgebraic

(Subscript[r, 1])=Root[((#1)^210)-11 #1+7&,1];
(Subscript[r, 2])=Root[((#1)^75)-5 #1+3&,1];
SetSystemOptions["InequalitySolvingOptions"->"ProjectAlgebraic"->True];
FindInstance[(Subscript[r, 1]) (x^2)-(Subscript[r, 2])(y^2)-x y==1 &&x≠0,{x,y},Reals]//Timing//N

SetSystemOptions["InequalitySolvingOptions"->"ProjectAlgebraic"->False];
FindInstance[(Subscript[r, 1]) (x^2)-(Subscript[r, 2])(y^2)-x y==1 &&x≠0,{x,y},Reals]//Timing//N

SetSystemOptions["InequalitySolvingOptions"->"ProjectAlgebraic"->True];
FindInstance[(x^2)+(y^2)-(Sqrt[2])x-(Sqrt[3])y-(Sqrt[5])<0 &&x<(Sqrt[7]) y^2,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ProjectAlgebraic"->False];
FindInstance[(x^2)+(y^2)-(Sqrt[2])x-(Sqrt[3])y-(Sqrt[5])<0 &&x<(Sqrt[7]) y^2,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ProjectAlgebraic"->Automatic];

ProveMultiplicities

SetSystemOptions["InequalitySolvingOptions"->"ProveMultiplicities"->True];
Reduce[(Subscript[∃, {y,z}])((x^4)+(y^4)+(z^4)==1&&2+x y+z≤(x^2)+(y^2)+(z^2)),x,Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ProveMultiplicities"->Automatic];
Reduce[(Subscript[∃, {y,z}])((x^4)+(y^4)+(z^4)==1&&2+x y+z≤(x^2)+(y^2)+(z^2)),x,Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ProveMultiplicities"->False];
TimeConstrained[Reduce[(Subscript[∃, {y,z}])((x^4)+(y^4)+(z^4)==1&&2+x y+z≤(x^2)+(y^2)+(z^2)),x,Reals],60]

SetSystemOptions["InequalitySolvingOptions"->"ProveMultiplicities"->True];

QuadraticQE

Resolve[(Subscript[∃, x])(a (x^2)+b x+c) (c (x^2)+b x+a)<=0,Reals]//Timing

Reduce[(Subscript[∃, x])(a (x^2)+b x+c) (c (x^2)+b x+a)<=0,{a,b,c},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QuadraticQE"->True];
Reduce[(Subscript[∃, x])(a (x^2)+b x+c) (c (x^2)+b x+a)<=0,{a,b,c},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QuadraticQE"->Automatic];
Resolve[(Subscript[∃, t])(-602+528 z-222 (z^2)-410 t-685 z t+427 (t^2)+422 x+5 z x-279 t x-188 (x^2)+1000 y-704 z y+879 t y-179 x y-689 (y^2)==0&&-723-380 z+323 (z^2)-964 t-749 z t-9 (t^2)+497 x-191 z x+147 t x+815 (x^2)+935 y-536 z y-558 t y-152 x y+400 (y^2)≥0),Reals]//LeafCount//Timing

SetSystemOptions["InequalitySolvingOptions"->"QuadraticQE"->False];
Resolve[(Subscript[∃, t])(-602+528 z-222 (z^2)-410 t-685 z t+427 (t^2)+422 x+5 z x-279 t x-188 (x^2)+1000 y-704 z y+879 t y-179 x y-689 (y^2)==0&&-723-380 z+323 (z^2)-964 t-749 z t-9 (t^2)+497 x-191 z x+147 t x+815 (x^2)+935 y-536 z y-558 t y-152 x y+400 (y^2)≥0),Reals]//Short[#,10]&//LeafCount//Timing

Resolve[(Subscript[∀, {x,y}])Implies[x>r&&y>r,(x^2) (((1+2 y))^2)>(y^2) (1+2 (x^2))],Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QuadraticQE"->True];
Resolve[(Subscript[∀, {x,y}])Implies[x>r&&y>r,(x^2) (((1+2 y))^2)>(y^2) (1+2 (x^2))],Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QuadraticQE"->Automatic];

QVSPreprocessor

SetSystemOptions["InequalitySolvingOptions"->"QVSPreprocessor"->True];
FindInstance[-11-909 y z-462 (y^2) z+(657-471 (y^3)+501 z-48 x z) t+(t^2)==0&&258+223 (x^2) y-544 (y^3)+571 (z^2)+38 y (z^2)+(-798+79 (x^2) y+214 (y^2)-828 (x^2) z-392 (z^2)) t+(t^2)≥0,{x,y,z,t},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QVSPreprocessor"->False];
FindInstance[-11-909 y z-462 (y^2) z+(657-471 (y^3)+501 z-48 x z) t+(t^2)==0&&258+223 (x^2) y-544 (y^3)+571 (z^2)+38 y (z^2)+(-798+79 (x^2) y+214 (y^2)-828 (x^2) z-392 (z^2)) t+(t^2)≥0,{x,y,z,t},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QVSPreprocessor"->True]; 
f=.;FindInstance[!(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),{a,b,c,d,e,f},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"QVSPreprocessor"->False]; 
FindInstance[!(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),{a,b,c,d,e,f},Reals]//Timing

ReducePowers

Reduce[(x^42)+3 (x^21) (y^25)-5 (y^50)==1,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ReducePowers"->False];
Reduce[(x^42)+3 (x^21) (y^25)-5 (y^50)==1,{x,y},Reals]//Timing

RootReduced

Reduce[(y^5)-3 (y^2)+2 y+(x^5)+7 x+4==0&&(y^2)+y-(x^5)-3 x-11==0,{x,y},Reals]//Timing

Reduce[(y^5)-3 (y^2)+2 y+(x^5)+7 x+4==0&&(y^2)+y-(x^5)-3 x-11==0,{x,y},Reals,Backsubstitution->True]//Timing

SetSystemOptions["InequalitySolvingOptions"->"RootReduced"->True];
Reduce[(y^5)-3 (y^2)+2 y+(x^5)+7 x+4==0&&(y^2)+y-(x^5)-3 x-11==0,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"RootReduced"->False];

Reduce[(x^11)+x+1==0&&(y^11)+3 (x^2) y+1==0,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"RootReduced"->True];
Reduce[(x^11)+x+1==0&&(y^11)+3 (x^2) y+1==0,{x,y},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"RootReduced"->False];

SimplifyInequalities

Reduce[c (x^3)+b (x^2)+a x+1≥0&&a-(b^2)-b-c>1&&b-(a^2)-c≥2&&c-(b^2)>3,{a,b,c,x}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"SimplifyInequalities"->False];
Reduce[c (x^3)+b (x^2)+a x+1≥0&&a-(b^2)-b-c>1&&b-(a^2)-c≥2&&c-(b^2)>3,{a,b,c,x}]//Timing

SetSystemOptions["InequalitySolvingOptions"->"SimplifyInequalities"->True];
f=3 (x^2)-4 (y^3)+6 x y z+9 (z^3)-7;
g=7 (x^2)+6 (y^2)-4 x y z+5 y z-3;
h=x^2+y^2-x y z+1;
{Timing[CylindricalDecomposition[f≤0&&g≤0&&h≥0&&f g h==0,{x,y,z}]][[1]],Timing[CylindricalDecomposition[-x≤0&&x-(Sqrt[(y^2)+(z^2)])<0&&-3+(y^2)-2 z-(z^2)==0&&y+y z==0&&-(y^2)-(z^2)≤0,{x,y,z}]][[1]]}

SetSystemOptions["InequalitySolvingOptions"->"SimplifyInequalities"->Automatic];
{Timing[CylindricalDecomposition[f≤0&&g≤0&&h≥0&&f g h==0,{x,y,z}]][[1]],Timing[CylindricalDecomposition[-x≤0&&x-(Sqrt[(y^2)+(z^2)])<0&&-3+(y^2)-2 z-(z^2)==0&&y+y z==0&&-(y^2)-(z^2)≤0,{x,y,z}]][[1]]}

ThreadOr

Reduce[(Subscript[∃, {x,y,z}])(x+y+z≥0||((x^5)-3 x (y^4) z+17 (x^3) (z^2)-11 y==0&&(x^2)+(y^2)+(z^2)≤1)),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ThreadOr"->False];
Reduce[(Subscript[∃, {x,y,z}])(x+y+z≥0||((x^5)-3 x (y^4) z+17 (x^3) (z^2)-11 y==0&&(x^2)+(y^2)+(z^2)≤1)),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ThreadOr"->True];
Reduce[(Subscript[∃, {x,y,z}])(((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)<1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)<1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)<1)),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ThreadOr"->False];
Reduce[(Subscript[∃, {x,y,z}])(((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)≥1)||((x^4)+(y^4)+(z^4)<1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)<1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)<1&&(x^2)+(((y-2))^2)+(z^2)≥1&&(x^2)+(y^2)+(((z-2))^2)<1)||((x^4)+(y^4)+(z^4)≥1&&(((x-2))^2)+(y^2)+(z^2)≥1&&(x^2)+(((y-2))^2)+(z^2)<1&&(x^2)+(y^2)+(((z-2))^2)<1)),Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ThreadOr"->True];

ZengDecision

FindInstance[(x^4)+(y^4)+(z^4)+(w^4)-5 x y z w+(x^2)+(y^2)+(z^2)+(w^2)+1<0,{x,y,z,w},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ZengDecision"->True];
FindInstance[(x^4)+(y^4)+(z^4)+(w^4)-5 x y z w+(x^2)+(y^2)+(z^2)+(w^2)+1<0,{x,y,z,w},Reals]//Timing

SetSystemOptions["InequalitySolvingOptions"->"ZengDecision"->False];