本日のC.A.D.

a, b, c がある 3 角形の 3 辺の長さ，s=(a+b+c)/2，d=(a^2+b^2+c^2-ab-bc-ca)^(1/2) ならば

$25abc<2(s-d)(2s+d)^2\le27abc\le2(s+d)(2s-d)^2$

1.13 Bottema, et. al. "GEOMETRIC INEQUALITIES" （原著に 25abc はありません）

今回も 0＜a, 0＜b を制約に加え，不要な cell の生成を抑制します．

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,a<b+c,b<c+a,c<a+b,0<d,2*d^2==(a-b)^2+(b-c)^2+(c-a)^2,0<x,x*a*b*c==(a+b+c-2*d)*(a+b+c+d)^2");Ans()
 *** using Lazard's method (MPP17).
[d,3]
[c,7]
[b,15]
[a,1]
[x,33]
time = 283 ms.
67 67(0,0) 1437(34,91) 4479(328,1394) 4(2162,2980) 
 *** combined adjacent 3 cells.
1[[x-25,1] < x <= [x-27,1],true,true,true,true]
time = 10,229 ms.

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,a<b+c,b<c+a,c<a+b,0<d,2*d^2==(a-b)^2+(b-c)^2+(c-a)^2,0<x,x*a*b*c==(a+b+c+2*d)*(a+b+c-d)^2");Ans()
 *** using Lazard's method (MPP17).
[d,3]
[c,7]
[b,15]
[a,1]
[x,33]
time = 299 ms.
67 67(0,0) 1437(34,91) 4479(328,1394) 42(50,184) 
 *** combined adjacent 41 cells.
1[[x-27,1] <= x,true,true,true,true]
time = 4,652 ms.

WLOG 版．

? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,0<x,x*b*c==(1+b+c-2*d)*(1+b+c+d)^2",7);Ans()
 *** using the sum of squares projection.
[d,3]
[c,6]
[b,10]
[x,26]
time = 293 ms.
31 204(27,31) 490(98,246) 4(134,195) 
 *** combined adjacent 3 cells.
1[[x-25,1] < x <= [x-27,1],true,true,true]
time = 1,191 ms.

? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,0<x,x*b*c==(1+b+c+2*d)*(1+b+c-d)^2",7);Ans()
 *** using the sum of squares projection.
[d,3]
[c,6]
[b,10]
[x,26]
time = 290 ms.
31 204(27,31) 490(98,246) 14(134,173) 
 *** combined adjacent 13 cells.
1[[x-27,1] <= x,true,true,true]
time = 1,141 ms.

なお，s-d＞0，つまり，a^2+b^2+c^2＜2(ab+bc+ca) は，例えば，|a-b|^2＜c^2 などの辺々の和から得られますが，これを既知としない，つまり，0＜x を付さない場合は次のようになります．

? tst12([ex,ex,ex,ex],[x,a,b,c,d],andx,"0<a,0<b,a<b+c,b<c+a,c<a+b,0<d,2*d^2==(a-b)^2+(b-c)^2+(c-a)^2,x*a*b*c==(a+b+c-2*d)*(a+b+c+d)^2");Ans()
 *** using Lazard's method (MPP17).
[d,3]
[c,7]
[b,15]
[a,1]
[x,33]
time = 261 ms.
125 125(0,0) 2427(64,208) 5585(479,2450) 4(2296,3096) 
 *** combined adjacent 3 cells.
1[[x-25,1] < x <= [x-27,1],true,true,true,true]
time = 13,427 ms.

WLOG 版．

? tst12([ex,ex,ex],[x,b,c,d],andx,"1<=b,b<=c,c<1+b,0<d,2*d^2==(1-b)^2+(b-c)^2+(c-1)^2,x*b*c==(1+b+c-2*d)*(1+b+c+d)^2",7);Ans()
 *** using the sum of squares projection.
[d,3]
[c,6]
[b,10]
[x,26]
time = 296 ms.
79 366(52,95) 814(204,506) 4(238,291) 
 *** combined adjacent 3 cells.
1[[x-25,1] < x <= [x-27,1],true,true,true]
time = 1,956 ms.