本日のC.A.D.

? tst12([],[c,a,d,b],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2<=a,b^2<=b,c^2<=c,d^2<=d,(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0",17);Ans();
 *** using Lazard's method (BM20).
1
[b,3]
0,0,-5
[d,7]
[a,16]
[c,3]
[[[c-1],[a-1],[],[]],[[c-1],[a+1],[],[]],[[c],[a],[],[]],[[c+1],[a-1],[],[]],[[c+1],[a+1],[],[]]]
time = 2165 ms.
7 145(90,46) 1967(158,205) 16733(2500,1450) 
 *** combined adjacent 16732 cells.
1[true,true,true,true]
time = 3,933 ms.

? tst12([],[a,b,c,d],(f1,f2,f3,f4,f5)->imp(f1*f2*f3*f4,f5),"a^2<=a,b^2<=b,c^2<=c,d^2<=d,(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0",17);Ans();
 *** using Lazard's method (BM20).
1
[d,3]
0,0,0
[c,8]
-5,-5,-5,-5,-5,-5,-5,-5,-5,-5,-5,-5
[b,18]
[a,30]
[[[a-1],[b-1],[],[]],[[a],[b],[],[]],[[a+1],[b+1],[],[]]]
time = 2306 ms.
103 5601(74,121) 92535(3000,5402) 794143(64444,37904) 
 *** combined adjacent 794142 cells.
1[true,true,true,true]
time = 3min, 19,428 ms.

Wolfram Language 12.2.0 Engine for Linux x86 (64-bit)
Copyright 1988-2021 Wolfram Research, Inc.

In[1]:= CylindricalDecomposition[Implies[And[a^2<=a,b^2<=b,c^2<=c,d^2<=d],(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(
c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0],{c,a,d,b},"Function"]//Timing                     

Out[1]= {6.577429, True}

In[2]:= CylindricalDecomposition[Implies[And[a^2<=a,b^2<=b,c^2<=c,d^2<=d],(1-a^2*b^2)*(1-c*d)*(a*d-b*c)^2+2*a*b*(
c*d-a*b)*(1-a*b)*(c-d)^2+(a^2*b^2-c^2*d^2)*(1-c*d)*(a-b)^2>=0],{a,b,c,d},"Function"]//Timing                     

Out[2]= {98.025059, True}

G.O.Passmore "Combined Decision Procedures for Nonlinear Arithmetics, Real and Complex"