本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2 ならば

$\sqrt{s}<\sqrt{s-a}+\sqrt{s-b}+\sqrt{s-c}\le\sqrt{3s}$

1.20 Bottema, et. al. "GEOMETRIC INEQUALITIES"

まず，a，b，c に対する不等式制約は 0＜a，0＜b，a＜b+c，b＜c+a，c＜a+b とし，s＞0 により，s=1（つまり，a/s，b/s，c/s を改めて a，b，c）としても値域は不変，また，tst12 の入力に根号は使えないので，s>a，s>b，s>c により，x=sqrt(s-a)，y=sqrt(s-b)，z=sqrt(s-c)（つまり，0＜x，0＜y，0＜z，a=s-x^2，b=s-y^2，c=s-z^2）とおき，実行すると

? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,0<y,0<z,0<1-x^2,0<1-y^2,1-x^2<1-y^2+1-z^2,1-y^2<1-z^2+1-x^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d,x+y+z=d",7);Ans()
 *** using the sum of squares projection.
[z,6]
[y,13]
[x,32]
[d,94]
time = 2,928 ms.
261 7203(50,436) 71001(574,9217) 64(21460,61970) 
 *** combined adjacent 63 cells.
1[[d-1,1] < d <= [d^2-3,2],true,true,true]
time = 1min, 59,976 ms.

? pp[4]
%1 = [z,-x^2+(y^2+(z^2-1)),x^2+(-y^2+(z^2-1)),-x^2+(-y^2+(z^2+1)),x^2+(y^2+(z^2-1)),x+(y+(z-d))]

のように最上位の 2 次の射影因子が 4 個生じますが，WLOG で 2 個に減らし，0＜a，a≦b，b≦c，c＜a+b とすると

? tst12([ex,ex,ex],[d,x,y,z],andx,"0<x,0<y,0<z,0<1-x^2,1-x^2<=1-y^2,1-y^2<=1-z^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d,x+y+z=d",7);Ans()
 *** using the sum of squares projection.
[z,6]
[y,9]
[x,19]
[d,37]
time = 554 ms.
73 1529(16,110) 9830(128,2273) 26(2296,8713) 
 *** combined adjacent 25 cells.
1[[d-1,1] < d <= [d^2-3,2],true,true,true]
time = 14,005 ms.

? pp[4]
%2 = [z,-y+z,y+z,-x^2+(-y^2+(z^2+1)),x^2+(y^2+(z^2-1)),x+(y+(z-d))]

或いは，z=d-x-y により z を消去すると

? "0<x,0<y,0<z,0<1-x^2,0<1-y^2,1-x^2<1-y^2+1-z^2,1-y^2<1-z^2+1-x^2,1-z^2<1-x^2+1-y^2,1-x^2+1-y^2+1-z^2=2,0<d";
? strrep(%,["z"],["(d-x-y)"]);
? tst12([ex,ex],[d,x,y],andx,%);Ans()
 *** using Lazard's method (MPP17).
[y,8]
[x,17]
[d,18]
time = 156 ms.
27 251(12,56) 8(56,230) 
 *** combined adjacent 7 cells.
1[[d-1,1] < d <= [d^2-3,2],true,true]
time = 411 ms.

のように大幅に高速化します．

tarski による実行例．

time echo "(display (normalize(qepcad-qe(qfr[ex a,b,c,s1,s2,s3,s0[a<b+c /\ b<c+a /\ c<a+b /\ 2s0^2=a+b+c /\ 0<s0 /\ 2s1^2=-a+b+c /\ 0<s1 /\ 2s2^2=a-b+c /\ 0<s2 /\ 2s3^2=a+b-c /\ 0<s3 /\ s1+s2+s3=x s0 /\ 0<x]]))) ) \n" | tarski -q
[x - 1 > 0 /\ x^2 - 3 <= 0]
real	0m0.300s
user	0m0.263s
sys	0m0.030s