本日のC.A.D.

? tst12([all,ex],[a,b,x,y],(f1,f2)->f1*f2,"x^6+x*y+a>0,x+b*y^6+a<0",17);Ans()
 *** using Lazard's method (BM20).
1,0
[y,2]
-5
[x,3]
-5
[b,2]
[a,2]
[[[a],[],[x],[]]]
time = 1718 ms.
5 25(0,2) 180(55,29) 113(108,74) 
 *** combined adjacent 88 cells.
1[[a,1] < a,b < [b,1],true,true]
time = 1,264 ms.
Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[ForAll[x,Exists[y,x^6+x*y+a>0,x+b*y^6+a<0]],{a,b},"Function"]//Timing           

Out[1]= 
{23.867581, CylindricalDecompositionFunction[{CylindricalDecompositionFunction["Variable"][1] > 0 && 
     CylindricalDecompositionFunction["Variable"][2] < 0, {2, 2, 1}, 2657360598}][a, b]}

Thomas Sturm "A Survey of Some Methods for Real Quantifier Elimination, Decision, and Satisfiability and Their Applications" において "This instructive example has been used by Hoon Hong in a colloquium talk at the University of Passau in 2005." と紹介されている例の次数を上げたもの.