realgeom benchmark

https://github.com/kovzol/realgeom/blob/master/src/test/resources/benchmark.csv
上記の各 LHS，RHS の s に (a+b+c)/2 を代入し，LHS-m*RHS を通分した有理式の分子 P に対する

tst12([ex,ex], [m,b,c], andx, "P|_{a=1}=0, 1<b+c, b<c+1, c<1+b, 0<m"); Ans();

の Core i7-7700K (4.20/4.50GHz) による実行結果です．

                         GP/PARI CALCULATOR Version 2.14.0 (development git-b0a4238356)
                          amd64 running linux (x86-64/GMP-6.2.1 kernel) 64-bit version
                    compiled: Feb 21 2021, gcc version 9.3.0 (Ubuntu 9.3.0-17ubuntu1~20.04)
                                            threading engine: single
                                 (readline v8.0 enabled, extended help enabled)

                                     Copyright (C) 2000-2021 The PARI Group

PARI/GP is free software, covered by the GNU General Public License, and comes WITHOUT ANY WARRANTY WHATSOEVER.

Type ? for help, \q to quit.
Type ?17 for how to get moral (and possibly technical) support.

parisizemax = 20000002048, primelimit = 500000
? bmgg()
1. Test 1
 *** using Lazard's method (MPP17).
[c,4]
[b,5]
[m,3]
time = 63 ms.
3 29(0,2) 1(0,33) 
 *** combined adjacent 0 cells.
1[[m-1,1] < m,true,true]
proj+cad = 79 ms.

2. Test 2
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,3]
time = 44 ms.
5 43(4,5) 3(0,41) 
 *** combined adjacent 2 cells.
1[[2*m-1,1] < m,true,true]
proj+cad = 74 ms.

3. Bottema 1.1
 *** using Lazard's method (MPP17).
[c,4]
[b,6]
[m,7]
time = 54 ms.
11 127(8,15) 6(18,48) 
 *** combined adjacent 5 cells.
1[[4*m-1,1] < m <= [3*m-1,1],true,true]
proj+cad = 98 ms.

4. Bottema 1.2
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,14]
time = 94 ms.
17 327(16,27) 8(64,212) 
 *** combined adjacent 7 cells.
1[[35*m-36,1] <= m < [m-2,1],true,true]
proj+cad = 378 ms.

5. Bottema 1.3
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,5]
time = 47 ms.
5 39(2,2) 2(14,47) 
 *** combined adjacent 1 cells.
1[[m,1] < m <= [8*m-1,1],true,true]
proj+cad = 99 ms.

6. Bottema 1.4
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,7]
time = 51 ms.
13 223(12,24) 6(52,134) 
 *** combined adjacent 5 cells.
1[[m,1] < m <= [8*m-1,1],true,true]
proj+cad = 174 ms.

7. Bottema 1.5
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[m,11]
time = 71 ms.
13 183(10,16) 10(65,100) 
 *** combined adjacent 9 cells.
1[[m-1,1] < m <= [3*m-8,1],true,true]
proj+cad = 201 ms.

8. Bottema 1.6
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,13]
time = 79 ms.
27 473(18,39) 10(69,306) 
 *** combined adjacent 9 cells.
1[[2*m-3,1] <= m < [m-2,1],true,true]
proj+cad = 504 ms.

9. Bottema 1.7
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,6]
time = 53 ms.
7 57(4,6) 2(24,97) 
 *** combined adjacent 1 cells.
1[[3*m-2,1] <= m < [m-1,1],true,true]
proj+cad = 132 ms.

10. Bottema 1.8
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,6]
time = 65 ms.
13 123(6,6) 2(38,102) 
 *** combined adjacent 1 cells.
1[[m-48,1] <= m,true,true]
proj+cad = 268 ms.

11. Bottema 1.9
 *** using Lazard's method (MPP17).
[c,4]
[b,6]
[m,15]
time = 101 ms.
29 613(22,42) 10(198,375) 
 *** combined adjacent 9 cells.
1[[2*m-1,1] < m <= [m-1,1],true,true]
proj+cad = 927 ms.

12. Bottema 1.11
 *** using Lazard's method (MPP17).
[c,4]
[b,6]
[m,16]
time = 116 ms.
27 519(10,18) 27(74,118) 
 *** combined adjacent 26 cells.
1[[m,1] < m,true,true]
proj+cad = 552 ms.

13. Bottema 1.12
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,6]
time = 65 ms.
9 87(6,8) 6(96,75) 
 *** combined adjacent 5 cells.
1[[m,1] < m <= [64*m-27,1],true,true]
proj+cad = 225 ms.

14. Bottema 1.14
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,12]
time = 65 ms.
17 237(10,20) 12(62,62) 
 *** combined adjacent 11 cells.
1[[m,1] < m <= [2*m-1,1],true,true]
proj+cad = 168 ms.

15. Bottema 1.15
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[m,5]
time = 51 ms.
7 53(4,4) 2(16,64) 
 *** combined adjacent 1 cells.
1[[m-9,1] <= m,true,true]
proj+cad = 128 ms.

16. Bottema 1.16
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,14]
time = 91 ms.
17 267(8,15) 8(90,136) 
 *** combined adjacent 7 cells.
1[[2*m-3,1] <= m < [m-2,1],true,true]
proj+cad = 375 ms.

17. Bottema 1.17
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,13]
time = 85 ms.
17 267(8,15) 8(90,136) 
 *** combined adjacent 7 cells.
1[[4*m-15,1] <= m < [2*m-9,1],true,true]
proj+cad = 359 ms.

18. Bottema 1.18
 *** using Lazard's method (MPP17).
[c,4]
[b,3]
[m,3]
time = 42 ms.
3 19(0,0) 1(2,31) 
 *** combined adjacent 0 cells.
1[[m-1,1] < m,true,true]
proj+cad = 53 ms.

19. Bottema 1.19
 *** using Lazard's method (MPP17).
[c,4]
[b,6]
[m,7]
time = 56 ms.
15 215(10,21) 6(18,136) 
 *** combined adjacent 5 cells.
1[[3*m-1,1] <= m < [2*m-1,1],true,true]
proj+cad = 165 ms.

20. Bottema 1.23
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[m,12]
time = 74 ms.
27 477(14,35) 10(70,306) 
 *** combined adjacent 9 cells.
1[[5*m-4,1] < m <= [m-1,1],true,true]
proj+cad = 510 ms.

21. Bottema 1.24
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[m,12]
time = 74 ms.
17 287(0,21) 13(32,222) 
 *** combined adjacent 12 cells.
1[[5*m-1,1] < m < [m-1,1],true,true]
proj+cad = 216 ms.

total = 5,685 ms.

同じく

tst12([ex,ex,ex], [m,a,b,c], andx, "P=0, a<b+c, b<c+a, c<a+b, 0<m"); Ans();

の実行結果です．

1. Test 1
 *** using Lazard's method (MPP17).
[c,4]
[b,5]
[a,1]
[m,3]
time = 72 ms.
3 9(0,0) 67(0,18) 1(0,96) 
 *** combined adjacent 0 cells.
1[[m-1,1] < m,true,true,true]
proj+cad = 117 ms.

2. Test 2
 *** using Lazard's method (MPP17).
[c,4]
[b,5]
[a,1]
[m,3]
time = 43 ms.
5 15(0,0) 101(34,35) 3(10,140) 
 *** combined adjacent 2 cells.
1[[2*m-1,1] < m,true,true,true]
proj+cad = 115 ms.

3. Bottema 1.1
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,8]
time = 56 ms.
11 33(0,0) 295(124,109) 6(72,238) 
 *** combined adjacent 5 cells.
1[[4*m-1,1] < m <= [3*m-1,1],true,true,true]
proj+cad = 208 ms.

4. Bottema 1.2
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[a,1]
[m,18]
time = 100 ms.
25 75(0,0) 1201(379,284) 8(362,1073) 
 *** combined adjacent 7 cells.
1[[35*m-36,1] <= m < [m-2,1],true,true,true]
proj+cad = 1,341 ms.

5. Bottema 1.3
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[a,1]
[m,5]
time = 47 ms.
5 15(0,0) 93(24,24) 2(65,167) 
 *** combined adjacent 1 cells.
1[[m,1] < m <= [8*m-1,1],true,true,true]
proj+cad = 169 ms.

6. Bottema 1.4
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,7]
time = 53 ms.
13 39(0,0) 485(152,138) 6(126,459) 
 *** combined adjacent 5 cells.
1[[m,1] < m <= [8*m-1,1],true,true,true]
proj+cad = 365 ms.

7. Bottema 1.5
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[a,1]
[m,11]
time = 79 ms.
13 39(0,0) 405(171,136) 10(191,418) 
 *** combined adjacent 9 cells.
1[[m-1,1] < m <= [3*m-8,1],true,true,true]
proj+cad = 463 ms.

8. Bottema 1.6
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[a,1]
[m,16]
time = 96 ms.
37 111(0,0) 1573(553,424) 16(364,1399) 
 *** combined adjacent 15 cells.
1[[2*m-3,1] <= m < [m-2,1],true,true,true]
proj+cad = 1,661 ms.

9. Bottema 1.7
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[a,1]
[m,6]
time = 47 ms.
7 21(0,0) 135(35,40) 2(99,295) 
 *** combined adjacent 1 cells.
1[[3*m-2,1] <= m < [m-1,1],true,true,true]
proj+cad = 233 ms.

10. Bottema 1.8
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[a,1]
[m,11]
time = 79 ms.
27 81(0,0) 635(392,240) 2(245,754) 
 *** combined adjacent 1 cells.
1[[m-48,1] <= m,true,true,true]
proj+cad = 947 ms.

11. Bottema 1.9
 *** using Lazard's method (MPP17).
[c,4]
[b,6]
[a,1]
[m,15]
time = 111 ms.
29 87(0,0) 1313(503,258) 10(680,1157) 
 *** combined adjacent 9 cells.
1[[2*m-1,1] < m <= [m-1,1],true,true,true]
proj+cad = 2,188 ms.

12. Bottema 1.11
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,21]
[m,1]
time = 69 ms.
1 63(0,0) 1345(30,47) 1(302,323) 
 *** combined adjacent 0 cells.
1[[m,1] < m,true,true,true]
proj+cad = 1,301 ms.

13. Bottema 1.12
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[a,1]
[m,6]
time = 63 ms.
9 27(0,0) 201(83,52) 6(379,291) 
 *** combined adjacent 5 cells.
1[[m,1] < m <= [64*m-27,1],true,true,true]
proj+cad = 579 ms.

14. Bottema 1.14
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,12]
time = 67 ms.
17 51(0,0) 525(290,159) 12(206,363) 
 *** combined adjacent 11 cells.
1[[m,1] < m <= [2*m-1,1],true,true,true]
proj+cad = 395 ms.

15. Bottema 1.15
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[a,1]
[m,5]
time = 43 ms.
7 21(0,0) 127(34,36) 2(76,222) 
 *** combined adjacent 1 cells.
1[[m-9,1] <= m,true,true,true]
proj+cad = 216 ms.

16. Bottema 1.16
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,14]
time = 74 ms.
17 51(0,0) 585(215,149) 8(249,534) 
 *** combined adjacent 7 cells.
1[[2*m-3,1] <= m < [m-2,1],true,true,true]
proj+cad = 743 ms.

17. Bottema 1.17
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,13]
time = 73 ms.
17 51(0,0) 585(215,149) 8(249,534) 
 *** combined adjacent 7 cells.
1[[4*m-15,1] <= m < [2*m-9,1],true,true,true]
proj+cad = 751 ms.

18. Bottema 1.18
 *** using Lazard's method (MPP17).
[c,4]
[b,4]
[a,1]
[m,4]
time = 39 ms.
5 15(0,0) 105(8,23) 3(32,141) 
 *** combined adjacent 2 cells.
1[[m-1,1] < m,true,true,true]
proj+cad = 101 ms.

19. Bottema 1.19
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,8]
time = 56 ms.
17 51(0,0) 605(186,175) 6(82,525) 
 *** combined adjacent 5 cells.
1[[3*m-1,1] <= m < [2*m-1,1],true,true,true]
proj+cad = 456 ms.

20. Bottema 1.23
 *** using Lazard's method (MPP17).
[c,4]
[b,7]
[a,1]
[m,12]
time = 64 ms.
27 81(0,0) 1035(347,259) 10(277,1048) 
 *** combined adjacent 9 cells.
1[[5*m-4,1] < m <= [m-1,1],true,true,true]
proj+cad = 1,198 ms.

21. Bottema 1.24
 *** using Lazard's method (MPP17).
[c,4]
[b,8]
[a,1]
[m,12]
time = 62 ms.
17 51(0,0) 625(30,175) 13(132,640) 
 *** combined adjacent 12 cells.
1[[5*m-1,1] < m < [m-1,1],true,true,true]
proj+cad = 432 ms.

total = 13,979 ms.

なお，Mathematica が利用できる環境で realgeom を

realgeom -b -c mathematica,qepcad -i ./benchmark.csv -o ./timing.html -l log.log -t 60

のように実行すると，benchmark.csv で指定した問題が処理され，処理時間（ms）の一覧と QE ツールの入出力ログが生成されます．


Automatic substitution（ a = 1 ）
Name mathematicaqepcad
Test 10.0443.618
Test 20.053.577
Bottema 1.10.1283.562
Bottema 1.20.5924.527
Bottema 1.30.0373.556
Bottema 1.40.1863.637
Bottema 1.50.0763.573
Bottema 1.60.4863.655
Bottema 1.70.0643.565
Bottema 1.80.1333.63
Bottema 1.90.5469.769
Bottema 1.110.1186.381
Bottema 1.120.1113.668
Bottema 1.140.2073.61
Bottema 1.150.0933.566
Bottema 1.160.193.751
Bottema 1.170.1933.701
Bottema 1.180.073.599
Bottema 1.190.1523.602
Bottema 1.230.3033.619
Bottema 1.240.1583.594
Summary (of 21)2121

No substitution
Name mathematicaqepcad
Test 10.0033.594
Test 20.1163.589
Bottema 1.10.1213.624
Bottema 1.21.56.887
Bottema 1.30.0853.62
Bottema 1.40.5133.626
Bottema 1.50.2183.608
Bottema 1.61.3344.038
Bottema 1.70.1273.639
Bottema 1.80.2843.763
Bottema 1.91.19618.151
Bottema 1.110.572t/o
Bottema 1.120.2664.491
Bottema 1.140.3633.668
Bottema 1.150.1773.619
Bottema 1.160.5043.831
Bottema 1.170.4923.843
Bottema 1.180.0393.571
Bottema 1.190.3463.65
Bottema 1.230.7963.849
Bottema 1.240.1963.644
Summary (of 21)2120

2021-05-18 20:08:49.695 LOG: subst() => lhs=1+b,rhs=c
2021-05-18 20:08:49.696 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b == m * (c))
2021-05-18 20:08:49.696 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b == m * (c))],Reals],Reals]
2021-05-18 20:08:49.737 m > 1
2021-05-18 20:08:49.738 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a+b == m * (c))
2021-05-18 20:08:49.738 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a+b == m * (c))],Reals],Reals]
2021-05-18 20:08:49.741 m > 1
2021-05-18 20:08:49.741 LOG: subst() => lhs=1+b,rhs=c
2021-05-18 20:08:49.742 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b+1=(c m)
2021-05-18 20:08:49.742 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b+1=(c m)].
assume[m>0].
finish

2021-05-18 20:08:53.357 LOG: result=m - 1 > 0
2021-05-18 20:08:53.358 LOG: mathcode=Reduce[m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:08:53.359 m > 1
2021-05-18 20:08:53.359 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a+b=(c m)
2021-05-18 20:08:53.359 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a+b=(c m)].
assume[m>0].
finish

2021-05-18 20:08:56.952 LOG: result=m - 1 > 0
2021-05-18 20:08:56.953 LOG: mathcode=Reduce[m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:08:56.953 m > 1
2021-05-18 20:08:56.954 LOG: subst() => lhs=1+b*b,rhs=c*c
2021-05-18 20:08:56.954 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b*b == m * (c*c))
2021-05-18 20:08:56.954 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b*b == m * (c*c))],Reals],Reals]
2021-05-18 20:08:57.003 m > 1/2
2021-05-18 20:08:57.005 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*a+b*b == m * (c*c))
2021-05-18 20:08:57.005 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*a+b*b == m * (c*c))],Reals],Reals]
2021-05-18 20:08:57.12 m > 1/2
2021-05-18 20:08:57.121 LOG: subst() => lhs=1+b*b,rhs=c*c
2021-05-18 20:08:57.121 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^2+1=(c^2 m)
2021-05-18 20:08:57.121 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^2+1=(c^2 m)].
assume[m>0].
finish

2021-05-18 20:09:00.695 LOG: result=2 m - 1 > 0
2021-05-18 20:09:00.696 LOG: mathcode=Reduce[2 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:09:00.697 m > 1/2
2021-05-18 20:09:00.697 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^2+b^2=(c^2 m)
2021-05-18 20:09:00.697 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^2+b^2=(c^2 m)].
assume[m>0].
finish

2021-05-18 20:09:04.284 LOG: result=2 m - 1 > 0
2021-05-18 20:09:04.285 LOG: mathcode=Reduce[2 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:09:04.286 m > 1/2
2021-05-18 20:09:04.286 LOG: subst() => lhs=b*c+c+b,rhs=(1+b+c)^2
2021-05-18 20:09:04.286 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c+c+b == m * ((1+b+c)^2))
2021-05-18 20:09:04.286 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c+c+b == m * ((1+b+c)^2))],Reals],Reals]
2021-05-18 20:09:04.414 Inequality[1/4, Less, m, LessEqual, 1/3]
2021-05-18 20:09:04.415 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (b*c+c*a+a*b == m * ((a+b+c)^2))
2021-05-18 20:09:04.415 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (b*c+c*a+a*b == m * ((a+b+c)^2))],Reals],Reals]
2021-05-18 20:09:04.535 Inequality[1/4, Less, m, LessEqual, 1/3]
2021-05-18 20:09:04.536 LOG: subst() => lhs=b*c+c+b,rhs=(1+b+c)^2
2021-05-18 20:09:04.537 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b c+b+c=(b^2 m+2 b c m+2 b m+c^2 m+2 c m+m)
2021-05-18 20:09:04.537 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b c+b+c=(b^2 m+2 b c m+2 b m+c^2 m+2 c m+m)].
assume[m>0].
finish

2021-05-18 20:09:08.096 LOG: result=4 m - 1 > 0 /\ 3 m - 1 <= 0
2021-05-18 20:09:08.097 LOG: mathcode=Reduce[4 m - 1 > 0 && 3 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:08.098 Inequality[1/4, Less, m, LessEqual, 1/3]
2021-05-18 20:09:08.099 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a b+a c+b c=(a^2 m+2 a b m+2 a c m+b^2 m+2 b c m+c^2 m)
2021-05-18 20:09:08.099 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a b+a c+b c=(a^2 m+2 a b m+2 a c m+b^2 m+2 b c m+c^2 m)].
assume[m>0].
finish

2021-05-18 20:09:11.718 LOG: result=4 m - 1 > 0 /\ 3 m - 1 <= 0
2021-05-18 20:09:11.718 LOG: mathcode=Reduce[4 m - 1 > 0 && 3 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:11.722 Inequality[1/4, Less, m, LessEqual, 1/3]
2021-05-18 20:09:11.723 LOG: subst() => lhs=1+b^2+c^2,rhs=((1+b+c)/2)^2+b*c/(1+b+c)*2
2021-05-18 20:09:11.723 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b^2+c^2 == m * (((1+b+c)/2)^2+b*c/(1+b+c)*2))
2021-05-18 20:09:11.723 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b^2+c^2 == m * (((1+b+c)/2)^2+b*c/(1+b+c)*2))],Reals],Reals]
2021-05-18 20:09:12.313 Inequality[36/35, LessEqual, m, Less, 2]
2021-05-18 20:09:12.314 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2+b^2+c^2 == m * (((a+b+c)/2)^2+a*b*c/(a+b+c)*2))
2021-05-18 20:09:12.314 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2+b^2+c^2 == m * (((a+b+c)/2)^2+a*b*c/(a+b+c)*2))],Reals],Reals]
2021-05-18 20:09:13.814 Inequality[36/35, LessEqual, m, Less, 2]
2021-05-18 20:09:13.814 LOG: subst() => lhs=1+b^2+c^2,rhs=((1+b+c)/2)^2+b*c/(1+b+c)*2
2021-05-18 20:09:13.816 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 4 b^3+4 b^2 c+4 b^2+4 b c^2+4 b+4 c^3+4 c^2+4 c+4=(b^3 m+3 b^2 c m+3 b^2 m+3 b c^2 m+14 b c m+3 b m+c^3 m+3 c^2 m+3 c m+m)
2021-05-18 20:09:13.816 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 4 b^3+4 b^2 c+4 b^2+4 b c^2+4 b+4 c^3+4 c^2+4 c+4=(b^3 m+3 b^2 c m+3 b^2 m+3 b c^2 m+14 b c m+3 b m+c^3 m+3 c^2 m+3 c m+m)].
assume[m>0].
finish

2021-05-18 20:09:18.339 LOG: result=m - 2 < 0 /\ 35 m - 36 >= 0
2021-05-18 20:09:18.34 LOG: mathcode=Reduce[m - 2 < 0 && 35 m - 36 >= 0 && m>0,m,Reals]
2021-05-18 20:09:18.341 Inequality[36/35, LessEqual, m, Less, 2]
2021-05-18 20:09:18.343 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ 4 a^3+4 a^2 b+4 a^2 c+4 a b^2+4 a c^2+4 b^3+4 b^2 c+4 b c^2+4 c^3=(a^3 m+3 a^2 b m+3 a^2 c m+3 a b^2 m+14 a b c m+3 a c^2 m+b^3 m+3 b^2 c m+3 b c^2 m+c^3 m)
2021-05-18 20:09:18.343 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ 4 a^3+4 a^2 b+4 a^2 c+4 a b^2+4 a c^2+4 b^3+4 b^2 c+4 b c^2+4 c^3=(a^3 m+3 a^2 b m+3 a^2 c m+3 a b^2 m+14 a b c m+3 a c^2 m+b^3 m+3 b^2 c m+3 b c^2 m+c^3 m)].
assume[m>0].
finish

2021-05-18 20:09:25.226 LOG: result=m - 2 < 0 /\ 35 m - 36 >= 0
2021-05-18 20:09:25.227 LOG: mathcode=Reduce[m - 2 < 0 && 35 m - 36 >= 0 && m>0,m,Reals]
2021-05-18 20:09:25.228 Inequality[36/35, LessEqual, m, Less, 2]
2021-05-18 20:09:25.228 LOG: subst() => lhs=((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c),rhs=b*c
2021-05-18 20:09:25.229 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c) == m * (b*c))
2021-05-18 20:09:25.229 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c) == m * (b*c))],Reals],Reals]
2021-05-18 20:09:25.265 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:25.265 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c) == m * (a*b*c))
2021-05-18 20:09:25.265 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c) == m * (a*b*c))],Reals],Reals]
2021-05-18 20:09:25.35 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:25.351 LOG: subst() => lhs=((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c),rhs=b*c
2021-05-18 20:09:25.352 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ -b^3+b^2 c+b^2+b c^2-2 b c+b-c^3+c^2+c-1=(8 b c m)
2021-05-18 20:09:25.352 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ -b^3+b^2 c+b^2+b c^2-2 b c+b-c^3+c^2+c-1=(8 b c m)].
assume[m>0].
finish

2021-05-18 20:09:28.905 LOG: result=8 m - 1 <= 0
2021-05-18 20:09:28.905 LOG: mathcode=Reduce[8 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:28.906 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:28.908 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ -a^3+a^2 b+a^2 c+a b^2-2 a b c+a c^2-b^3+b^2 c+b c^2-c^3=(8 a b c m)
2021-05-18 20:09:28.908 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ -a^3+a^2 b+a^2 c+a b^2-2 a b c+a c^2-b^3+b^2 c+b c^2-c^3=(8 a b c m)].
assume[m>0].
finish

2021-05-18 20:09:32.523 LOG: result=8 m - 1 <= 0
2021-05-18 20:09:32.525 LOG: mathcode=Reduce[8 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:32.526 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:32.526 LOG: subst() => lhs=b*c,rhs=(1+b)*(b+c)*(c+1)
2021-05-18 20:09:32.526 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c == m * ((1+b)*(b+c)*(c+1)))
2021-05-18 20:09:32.526 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c == m * ((1+b)*(b+c)*(c+1)))],Reals],Reals]
2021-05-18 20:09:32.712 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:32.713 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*b*c == m * ((a+b)*(b+c)*(c+a)))
2021-05-18 20:09:32.713 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*b*c == m * ((a+b)*(b+c)*(c+a)))],Reals],Reals]
2021-05-18 20:09:33.225 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:33.226 LOG: subst() => lhs=b*c,rhs=(1+b)*(b+c)*(c+1)
2021-05-18 20:09:33.226 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b c=(b^2 c m+b^2 m+b c^2 m+2 b c m+b m+c^2 m+c m)
2021-05-18 20:09:33.226 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b c=(b^2 c m+b^2 m+b c^2 m+2 b c m+b m+c^2 m+c m)].
assume[m>0].
finish

2021-05-18 20:09:36.861 LOG: result=8 m - 1 <= 0
2021-05-18 20:09:36.861 LOG: mathcode=Reduce[8 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:36.861 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:36.862 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a b c=(a^2 b m+a^2 c m+a b^2 m+2 a b c m+a c^2 m+b^2 c m+b c^2 m)
2021-05-18 20:09:36.863 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a b c=(a^2 b m+a^2 c m+a b^2 m+2 a b c m+a c^2 m+b^2 c m+b c^2 m)].
assume[m>0].
finish

2021-05-18 20:09:40.487 LOG: result=8 m - 1 <= 0
2021-05-18 20:09:40.487 LOG: mathcode=Reduce[8 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:09:40.488 Inequality[0, Less, m, LessEqual, 1/8]
2021-05-18 20:09:40.489 LOG: subst() => lhs=(1+b)*(b+c)*(c+1),rhs=1+b^3+c^3
2021-05-18 20:09:40.489 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b)*(b+c)*(c+1) == m * (1+b^3+c^3))
2021-05-18 20:09:40.489 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b)*(b+c)*(c+1) == m * (1+b^3+c^3))],Reals],Reals]
2021-05-18 20:09:40.564 Inequality[1, Less, m, LessEqual, 8/3]
2021-05-18 20:09:40.565 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b)*(b+c)*(c+a) == m * (a^3+b^3+c^3))
2021-05-18 20:09:40.565 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b)*(b+c)*(c+a) == m * (a^3+b^3+c^3))],Reals],Reals]
2021-05-18 20:09:40.782 Inequality[1, Less, m, LessEqual, 8/3]
2021-05-18 20:09:40.783 LOG: subst() => lhs=(1+b)*(b+c)*(c+1),rhs=1+b^3+c^3
2021-05-18 20:09:40.783 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^2 c+b^2+b c^2+2 b c+b+c^2+c=(b^3 m+c^3 m+m)
2021-05-18 20:09:40.783 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^2 c+b^2+b c^2+2 b c+b+c^2+c=(b^3 m+c^3 m+m)].
assume[m>0].
finish

2021-05-18 20:09:44.353 LOG: result=m - 1 > 0 /\ 3 m - 8 <= 0
2021-05-18 20:09:44.354 LOG: mathcode=Reduce[m - 1 > 0 && 3 m - 8 <= 0 && m>0,m,Reals]
2021-05-18 20:09:44.354 Inequality[1, Less, m, LessEqual, 8/3]
2021-05-18 20:09:44.356 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^2 b+a^2 c+a b^2+2 a b c+a c^2+b^2 c+b c^2=(a^3 m+b^3 m+c^3 m)
2021-05-18 20:09:44.356 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^2 b+a^2 c+a b^2+2 a b c+a c^2+b^2 c+b c^2=(a^3 m+b^3 m+c^3 m)].
assume[m>0].
finish

2021-05-18 20:09:47.961 LOG: result=m - 1 > 0 /\ 3 m - 8 <= 0
2021-05-18 20:09:47.962 LOG: mathcode=Reduce[m - 1 > 0 && 3 m - 8 <= 0 && m>0,m,Reals]
2021-05-18 20:09:47.963 Inequality[1, Less, m, LessEqual, 8/3]
2021-05-18 20:09:47.963 LOG: subst() => lhs=(1+b+c)*(1+b^2+c^2),rhs=1+b^3+c^3+3*b*c
2021-05-18 20:09:47.964 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)*(1+b^2+c^2) == m * (1+b^3+c^3+3*b*c))
2021-05-18 20:09:47.964 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)*(1+b^2+c^2) == m * (1+b^3+c^3+3*b*c))],Reals],Reals]
2021-05-18 20:09:48.449 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:09:48.45 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)*(a^2+b^2+c^2) == m * (a^3+b^3+c^3+3*a*b*c))
2021-05-18 20:09:48.45 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)*(a^2+b^2+c^2) == m * (a^3+b^3+c^3+3*a*b*c))],Reals],Reals]
2021-05-18 20:09:49.784 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:09:49.785 LOG: subst() => lhs=(1+b+c)*(1+b^2+c^2),rhs=1+b^3+c^3+3*b*c
2021-05-18 20:09:49.786 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^3+b^2 c+b^2+b c^2+b+c^3+c^2+c+1=(b^3 m+3 b c m+c^3 m+m)
2021-05-18 20:09:49.786 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^3+b^2 c+b^2+b c^2+b+c^3+c^2+c+1=(b^3 m+3 b c m+c^3 m+m)].
assume[m>0].
finish

2021-05-18 20:09:53.438 LOG: result=m - 2 < 0 /\ 2 m - 3 >= 0
2021-05-18 20:09:53.438 LOG: mathcode=Reduce[m - 2 < 0 && 2 m - 3 >= 0 && m>0,m,Reals]
2021-05-18 20:09:53.439 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:09:53.44 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^3+a^2 b+a^2 c+a b^2+a c^2+b^3+b^2 c+b c^2+c^3=(a^3 m+3 a b c m+b^3 m+c^3 m)
2021-05-18 20:09:53.44 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^3+a^2 b+a^2 c+a b^2+a c^2+b^3+b^2 c+b c^2+c^3=(a^3 m+3 a b c m+b^3 m+c^3 m)].
assume[m>0].
finish

2021-05-18 20:09:57.475 LOG: result=m - 2 < 0 /\ 2 m - 3 >= 0
2021-05-18 20:09:57.476 LOG: mathcode=Reduce[m - 2 < 0 && 2 m - 3 >= 0 && m>0,m,Reals]
2021-05-18 20:09:57.477 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:09:57.478 LOG: subst() => lhs=b*c,rhs=(1+b+c)/2-1+b^2*((1+b+c)/2-b)+c^2*((1+b+c)/2-c)
2021-05-18 20:09:57.48 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c == m * ((1+b+c)/2-1+b^2*((1+b+c)/2-b)+c^2*((1+b+c)/2-c)))
2021-05-18 20:09:57.48 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c == m * ((1+b+c)/2-1+b^2*((1+b+c)/2-b)+c^2*((1+b+c)/2-c)))],Reals],Reals]
2021-05-18 20:09:57.541 Inequality[2/3, LessEqual, m, Less, 1]
2021-05-18 20:09:57.541 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*b*c == m * (a^2*((a+b+c)/2-a)+b^2*((a+b+c)/2-b)+c^2*((a+b+c)/2-c)))
2021-05-18 20:09:57.541 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a*b*c == m * (a^2*((a+b+c)/2-a)+b^2*((a+b+c)/2-b)+c^2*((a+b+c)/2-c)))],Reals],Reals]
2021-05-18 20:09:57.668 Inequality[2/3, LessEqual, m, Less, 1]
2021-05-18 20:09:57.669 LOG: subst() => lhs=b*c,rhs=(1+b+c)/2-1+b^2*((1+b+c)/2-b)+c^2*((1+b+c)/2-c)
2021-05-18 20:09:57.671 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 2 b c=(-b^3 m+b^2 c m+b^2 m+b c^2 m+b m-c^3 m+c^2 m+c m-m)
2021-05-18 20:09:57.671 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 2 b c=(-b^3 m+b^2 c m+b^2 m+b c^2 m+b m-c^3 m+c^2 m+c m-m)].
assume[m>0].
finish

2021-05-18 20:10:01.233 LOG: result=m - 1 < 0 /\ 3 m - 2 >= 0
2021-05-18 20:10:01.233 LOG: mathcode=Reduce[m - 1 < 0 && 3 m - 2 >= 0 && m>0,m,Reals]
2021-05-18 20:10:01.234 Inequality[2/3, LessEqual, m, Less, 1]
2021-05-18 20:10:01.236 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ 2 a b c=(-a^3 m+a^2 b m+a^2 c m+a b^2 m+a c^2 m-b^3 m+b^2 c m+b c^2 m-c^3 m)
2021-05-18 20:10:01.236 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ 2 a b c=(-a^3 m+a^2 b m+a^2 c m+a b^2 m+a c^2 m-b^3 m+b^2 c m+b c^2 m-c^3 m)].
assume[m>0].
finish

2021-05-18 20:10:04.871 LOG: result=m - 1 < 0 /\ 3 m - 2 >= 0
2021-05-18 20:10:04.872 LOG: mathcode=Reduce[m - 1 < 0 && 3 m - 2 >= 0 && m>0,m,Reals]
2021-05-18 20:10:04.873 Inequality[2/3, LessEqual, m, Less, 1]
2021-05-18 20:10:04.873 LOG: subst() => lhs=b*c*(b+c)+c*(c+1)+b*(1+b),rhs=((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c)
2021-05-18 20:10:04.874 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c*(b+c)+c*(c+1)+b*(1+b) == m * (((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c)))
2021-05-18 20:10:04.874 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*c*(b+c)+c*(c+1)+b*(1+b) == m * (((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c)))],Reals],Reals]
2021-05-18 20:10:05.006 m >= 48
2021-05-18 20:10:05.007 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (b*c*(b+c)+c*a*(c+a)+a*b*(a+b) == m * (((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c)))
2021-05-18 20:10:05.007 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (b*c*(b+c)+c*a*(c+a)+a*b*(a+b) == m * (((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c)))],Reals],Reals]
2021-05-18 20:10:05.29 m >= 48
2021-05-18 20:10:05.291 LOG: subst() => lhs=b*c*(b+c)+c*(c+1)+b*(1+b),rhs=((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c)
2021-05-18 20:10:05.292 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 8 b^2 c+8 b^2+8 b c^2+8 b+8 c^2+8 c=(-b^3 m+b^2 c m+b^2 m+b c^2 m-2 b c m+b m-c^3 m+c^2 m+c m-m)
2021-05-18 20:10:05.293 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 8 b^2 c+8 b^2+8 b c^2+8 b+8 c^2+8 c=(-b^3 m+b^2 c m+b^2 m+b c^2 m-2 b c m+b m-c^3 m+c^2 m+c m-m)].
assume[m>0].
finish

2021-05-18 20:10:08.918 LOG: result=m - 48 >= 0
2021-05-18 20:10:08.92 LOG: mathcode=Reduce[m - 48 >= 0 && m>0,m,Reals]
2021-05-18 20:10:08.92 m >= 48
2021-05-18 20:10:08.922 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ 8 a^2 b+8 a^2 c+8 a b^2+8 a c^2+8 b^2 c+8 b c^2=(-a^3 m+a^2 b m+a^2 c m+a b^2 m-2 a b c m+a c^2 m-b^3 m+b^2 c m+b c^2 m-c^3 m)
2021-05-18 20:10:08.922 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ 8 a^2 b+8 a^2 c+8 a b^2+8 a c^2+8 b^2 c+8 b c^2=(-a^3 m+a^2 b m+a^2 c m+a b^2 m-2 a b c m+a c^2 m-b^3 m+b^2 c m+b c^2 m-c^3 m)].
assume[m>0].
finish

2021-05-18 20:10:12.683 LOG: result=m - 48 >= 0
2021-05-18 20:10:12.683 LOG: mathcode=Reduce[m - 48 >= 0 && m>0,m,Reals]
2021-05-18 20:10:12.684 m >= 48
2021-05-18 20:10:12.685 LOG: subst() => lhs=(1+b+c)/2-1+b^3*((1+b+c)/2-b)+c^3*((1+b+c)/2-c),rhs=b*c*(1+b+c)/2
2021-05-18 20:10:12.685 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)/2-1+b^3*((1+b+c)/2-b)+c^3*((1+b+c)/2-c) == m * (b*c*(1+b+c)/2))
2021-05-18 20:10:12.685 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)/2-1+b^3*((1+b+c)/2-b)+c^3*((1+b+c)/2-c) == m * (b*c*(1+b+c)/2))],Reals],Reals]
2021-05-18 20:10:13.23 Inequality[1/2, Less, m, LessEqual, 1]
2021-05-18 20:10:13.231 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^3*((a+b+c)/2-a)+b^3*((a+b+c)/2-b)+c^3*((a+b+c)/2-c) == m * (a*b*c*(a+b+c)/2))
2021-05-18 20:10:13.231 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^3*((a+b+c)/2-a)+b^3*((a+b+c)/2-b)+c^3*((a+b+c)/2-c) == m * (a*b*c*(a+b+c)/2))],Reals],Reals]
2021-05-18 20:10:14.426 Inequality[1/2, Less, m, LessEqual, 1]
2021-05-18 20:10:14.427 LOG: subst() => lhs=(1+b+c)/2-1+b^3*((1+b+c)/2-b)+c^3*((1+b+c)/2-c),rhs=b*c*(1+b+c)/2
2021-05-18 20:10:14.428 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ -2 b^4+2 b^3 c+2 b^3+2 b c^3+2 b-2 c^4+2 c^3+2 c-2=(2 b^2 c m+2 b c^2 m+2 b c m)
2021-05-18 20:10:14.428 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ -2 b^4+2 b^3 c+2 b^3+2 b c^3+2 b-2 c^4+2 c^3+2 c-2=(2 b^2 c m+2 b c^2 m+2 b c m)].
assume[m>0].
finish

2021-05-18 20:10:24.194 LOG: result=m - 1 <= 0 /\ 2 m - 1 > 0
2021-05-18 20:10:24.194 LOG: mathcode=Reduce[m - 1 <= 0 && 2 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:10:24.195 Inequality[1/2, Less, m, LessEqual, 1]
2021-05-18 20:10:24.197 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ -2 a^4+2 a^3 b+2 a^3 c+2 a b^3+2 a c^3-2 b^4+2 b^3 c+2 b c^3-2 c^4=(2 a^2 b c m+2 a b^2 c m+2 a b c^2 m)
2021-05-18 20:10:24.197 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ -2 a^4+2 a^3 b+2 a^3 c+2 a b^3+2 a c^3-2 b^4+2 b^3 c+2 b c^3-2 c^4=(2 a^2 b c m+2 a b^2 c m+2 a b c^2 m)].
assume[m>0].
finish

2021-05-18 20:10:42.345 LOG: result=m - 1 <= 0 /\ 2 m - 1 > 0
2021-05-18 20:10:42.345 LOG: mathcode=Reduce[m - 1 <= 0 && 2 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:10:42.346 Inequality[1/2, Less, m, LessEqual, 1]
2021-05-18 20:10:42.346 LOG: subst() => lhs=b*(1-b)+b^2*c*(b-c)+c^2*(c-1),rhs=1
2021-05-18 20:10:42.346 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*(1-b)+b^2*c*(b-c)+c^2*(c-1) == m * (1))
2021-05-18 20:10:42.347 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (b*(1-b)+b^2*c*(b-c)+c^2*(c-1) == m * (1))],Reals],Reals]
2021-05-18 20:10:42.464 m > 0
2021-05-18 20:10:42.464 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2*b*(a-b)+b^2*c*(b-c)+c^2*a*(c-a) == m * (1))
2021-05-18 20:10:42.464 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2*b*(a-b)+b^2*c*(b-c)+c^2*a*(c-a) == m * (1))],Reals],Reals]
2021-05-18 20:10:43.036 m > 0
2021-05-18 20:10:43.037 LOG: subst() => lhs=b*(1-b)+b^2*c*(b-c)+c^2*(c-1),rhs=1
2021-05-18 20:10:43.037 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^3 c-b^2 c^2-b^2+b+c^3-c^2=m
2021-05-18 20:10:43.038 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^3 c-b^2 c^2-b^2+b+c^3-c^2=m].
assume[m>0].
finish

2021-05-18 20:10:49.416 LOG: result=TRUE
2021-05-18 20:10:49.416 LOG: mathcode=Reduce[True && m>0,m,Reals]
2021-05-18 20:10:49.417 m > 0
2021-05-18 20:10:49.418 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^3 b-a^2 b^2-a^2 c^2+a c^3+b^3 c-b^2 c^2=m
2021-05-18 20:10:49.418 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^3 b-a^2 b^2-a^2 c^2+a c^3+b^3 c-b^2 c^2=m].
assume[m>0].
finish

2021-05-18 20:11:49.482 LOG: result=
2021-05-18 20:11:49.482 LOG: mathcode=Reduce[ && m>0,m,Reals]
2021-05-18 20:11:49.514 $Failed
2021-05-18 20:11:49.515 LOG: subst() => lhs=((1+b+c)/2)^3*((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c),rhs=b^2*c^2
2021-05-18 20:11:49.515 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2)^3*((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c) == m * (b^2*c^2))
2021-05-18 20:11:49.515 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2)^3*((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c) == m * (b^2*c^2))],Reals],Reals]
2021-05-18 20:11:49.625 Inequality[0, Less, m, LessEqual, 27/64]
2021-05-18 20:11:49.625 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2)^3*((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c) == m * (a^2*b^2*c^2))
2021-05-18 20:11:49.625 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2)^3*((a+b+c)/2-a)*((a+b+c)/2-b)*((a+b+c)/2-c) == m * (a^2*b^2*c^2))],Reals],Reals]
2021-05-18 20:11:49.891 Inequality[0, Less, m, LessEqual, 27/64]
2021-05-18 20:11:49.891 LOG: subst() => lhs=((1+b+c)/2)^3*((1+b+c)/2-1)*((1+b+c)/2-b)*((1+b+c)/2-c),rhs=b^2*c^2
2021-05-18 20:11:49.893 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ -b^6-2 b^5 c-2 b^5+b^4 c^2-2 b^4 c+b^4+4 b^3 c^3+4 b^3 c^2+4 b^3 c+4 b^3+b^2 c^4+4 b^2 c^3+6 b^2 c^2+4 b^2 c+b^2-2 b c^5-2 b c^4+4 b c^3+4 b c^2-2 b c-2 b-c^6-2 c^5+c^4+4 c^3+c^2-2 c-1=(64 b^2 c^2 m)
2021-05-18 20:11:49.893 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ -b^6-2 b^5 c-2 b^5+b^4 c^2-2 b^4 c+b^4+4 b^3 c^3+4 b^3 c^2+4 b^3 c+4 b^3+b^2 c^4+4 b^2 c^3+6 b^2 c^2+4 b^2 c+b^2-2 b c^5-2 b c^4+4 b c^3+4 b c^2-2 b c-2 b-c^6-2 c^5+c^4+4 c^3+c^2-2 c-1=(64 b^2 c^2 m)].
assume[m>0].
finish

2021-05-18 20:11:53.558 LOG: result=64 m - 27 <= 0
2021-05-18 20:11:53.558 LOG: mathcode=Reduce[64 m - 27 <= 0 && m>0,m,Reals]
2021-05-18 20:11:53.559 Inequality[0, Less, m, LessEqual, 27/64]
2021-05-18 20:11:53.561 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ -a^6-2 a^5 b-2 a^5 c+a^4 b^2-2 a^4 b c+a^4 c^2+4 a^3 b^3+4 a^3 b^2 c+4 a^3 b c^2+4 a^3 c^3+a^2 b^4+4 a^2 b^3 c+6 a^2 b^2 c^2+4 a^2 b c^3+a^2 c^4-2 a b^5-2 a b^4 c+4 a b^3 c^2+4 a b^2 c^3-2 a b c^4-2 a c^5-b^6-2 b^5 c+b^4 c^2+4 b^3 c^3+b^2 c^4-2 b c^5-c^6=(64 a^2 b^2 c^2 m)
2021-05-18 20:11:53.561 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ -a^6-2 a^5 b-2 a^5 c+a^4 b^2-2 a^4 b c+a^4 c^2+4 a^3 b^3+4 a^3 b^2 c+4 a^3 b c^2+4 a^3 c^3+a^2 b^4+4 a^2 b^3 c+6 a^2 b^2 c^2+4 a^2 b c^3+a^2 c^4-2 a b^5-2 a b^4 c+4 a b^3 c^2+4 a b^2 c^3-2 a b c^4-2 a c^5-b^6-2 b^5 c+b^4 c^2+4 b^3 c^3+b^2 c^4-2 b c^5-c^6=(64 a^2 b^2 c^2 m)].
assume[m>0].
finish

2021-05-18 20:11:58.048 LOG: result=64 m - 27 <= 0
2021-05-18 20:11:58.049 LOG: mathcode=Reduce[64 m - 27 <= 0 && m>0,m,Reals]
2021-05-18 20:11:58.05 Inequality[0, Less, m, LessEqual, 27/64]
2021-05-18 20:11:58.05 LOG: subst() => lhs=(1+b+c)/2/b/c,rhs=1+1/(b*b)+1/(c*c)
2021-05-18 20:11:58.05 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)/2/b/c == m * (1+1/(b*b)+1/(c*c)))
2021-05-18 20:11:58.05 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)/2/b/c == m * (1+1/(b*b)+1/(c*c)))],Reals],Reals]
2021-05-18 20:11:58.257 Inequality[0, Less, m, LessEqual, 1/2]
2021-05-18 20:11:58.257 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)/2/(a*b*c) == m * (1/(a*a)+1/(b*b)+1/(c*c)))
2021-05-18 20:11:58.257 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)/2/(a*b*c) == m * (1/(a*a)+1/(b*b)+1/(c*c)))],Reals],Reals]
2021-05-18 20:11:58.62 Inequality[0, Less, m, LessEqual, 1/2]
2021-05-18 20:11:58.621 LOG: subst() => lhs=(1+b+c)/2/b/c,rhs=1+1/(b*b)+1/(c*c)
2021-05-18 20:11:58.622 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^3 c^2+b^2 c^3+b^2 c^2=(2 b^3 c^3 m+2 b^3 c m+2 b c^3 m)
2021-05-18 20:11:58.622 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^3 c^2+b^2 c^3+b^2 c^2=(2 b^3 c^3 m+2 b^3 c m+2 b c^3 m)].
assume[m>0].
finish

2021-05-18 20:12:02.228 LOG: result=2 m - 1 <= 0
2021-05-18 20:12:02.228 LOG: mathcode=Reduce[2 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:12:02.229 Inequality[0, Less, m, LessEqual, 1/2]
2021-05-18 20:12:02.231 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^3 b^2 c^2+a^2 b^3 c^2+a^2 b^2 c^3=(2 a^3 b^3 c m+2 a^3 b c^3 m+2 a b^3 c^3 m)
2021-05-18 20:12:02.231 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^3 b^2 c^2+a^2 b^3 c^2+a^2 b^2 c^3=(2 a^3 b^3 c m+2 a^3 b c^3 m+2 a b^3 c^3 m)].
assume[m>0].
finish

2021-05-18 20:12:05.896 LOG: result=2 m - 1 <= 0
2021-05-18 20:12:05.897 LOG: mathcode=Reduce[2 m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:12:05.898 Inequality[0, Less, m, LessEqual, 1/2]
2021-05-18 20:12:05.899 LOG: subst() => lhs=1/((1+b+c)/2-1)+1/((1+b+c)/2-b)+1/((1+b+c)/2-c),rhs=2/(1+b+c)
2021-05-18 20:12:05.899 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1/((1+b+c)/2-1)+1/((1+b+c)/2-b)+1/((1+b+c)/2-c) == m * (2/(1+b+c)))
2021-05-18 20:12:05.899 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1/((1+b+c)/2-1)+1/((1+b+c)/2-b)+1/((1+b+c)/2-c) == m * (2/(1+b+c)))],Reals],Reals]
2021-05-18 20:12:05.991 m >= 9
2021-05-18 20:12:05.991 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (1/((a+b+c)/2-a)+1/((a+b+c)/2-b)+1/((a+b+c)/2-c) == m * (1/(a+b+c)*2))
2021-05-18 20:12:05.992 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (1/((a+b+c)/2-a)+1/((a+b+c)/2-b)+1/((a+b+c)/2-c) == m * (1/(a+b+c)*2))],Reals],Reals]
2021-05-18 20:12:06.168 m >= 9
2021-05-18 20:12:06.168 LOG: subst() => lhs=1/((1+b+c)/2-1)+1/((1+b+c)/2-b)+1/((1+b+c)/2-c),rhs=2/(1+b+c)
2021-05-18 20:12:06.171 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 2 b^3-2 b^2 c-2 b^2-2 b c^2-12 b c-2 b+2 c^3-2 c^2-2 c+2=(2 b^3 m-2 b^2 c m-2 b^2 m-2 b c^2 m+4 b c m-2 b m+2 c^3 m-2 c^2 m-2 c m+2 m)
2021-05-18 20:12:06.171 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 2 b^3-2 b^2 c-2 b^2-2 b c^2-12 b c-2 b+2 c^3-2 c^2-2 c+2=(2 b^3 m-2 b^2 c m-2 b^2 m-2 b c^2 m+4 b c m-2 b m+2 c^3 m-2 c^2 m-2 c m+2 m)].
assume[m>0].
finish

2021-05-18 20:12:09.733 LOG: result=m - 9 >= 0
2021-05-18 20:12:09.733 LOG: mathcode=Reduce[m - 9 >= 0 && m>0,m,Reals]
2021-05-18 20:12:09.734 m >= 9
2021-05-18 20:12:09.737 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ 2 a^3-2 a^2 b-2 a^2 c-2 a b^2-12 a b c-2 a c^2+2 b^3-2 b^2 c-2 b c^2+2 c^3=(2 a^3 m-2 a^2 b m-2 a^2 c m-2 a b^2 m+4 a b c m-2 a c^2 m+2 b^3 m-2 b^2 c m-2 b c^2 m+2 c^3 m)
2021-05-18 20:12:09.737 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ 2 a^3-2 a^2 b-2 a^2 c-2 a b^2-12 a b c-2 a c^2+2 b^3-2 b^2 c-2 b c^2+2 c^3=(2 a^3 m-2 a^2 b m-2 a^2 c m-2 a b^2 m+4 a b c m-2 a c^2 m+2 b^3 m-2 b^2 c m-2 b c^2 m+2 c^3 m)].
assume[m>0].
finish

2021-05-18 20:12:13.352 LOG: result=m - 9 >= 0
2021-05-18 20:12:13.353 LOG: mathcode=Reduce[m - 9 >= 0 && m>0,m,Reals]
2021-05-18 20:12:13.353 m >= 9
2021-05-18 20:12:13.354 LOG: subst() => lhs=1/(b+c)+b/(c+1)+c/(1+b),rhs=1
2021-05-18 20:12:13.354 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1/(b+c)+b/(c+1)+c/(1+b) == m * (1))
2021-05-18 20:12:13.354 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1/(b+c)+b/(c+1)+c/(1+b) == m * (1))],Reals],Reals]
2021-05-18 20:12:13.544 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:12:13.544 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a/(b+c)+b/(c+a)+c/(a+b) == m * (1))
2021-05-18 20:12:13.544 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a/(b+c)+b/(c+a)+c/(a+b) == m * (1))],Reals],Reals]
2021-05-18 20:12:14.048 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:12:14.049 LOG: subst() => lhs=1/(b+c)+b/(c+1)+c/(1+b),rhs=1
2021-05-18 20:12:14.05 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^3+b^2 c+b^2+b c^2+3 b c+b+c^3+c^2+c+1=(b^2 c m+b^2 m+b c^2 m+2 b c m+b m+c^2 m+c m)
2021-05-18 20:12:14.05 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^3+b^2 c+b^2+b c^2+3 b c+b+c^3+c^2+c+1=(b^2 c m+b^2 m+b c^2 m+2 b c m+b m+c^2 m+c m)].
assume[m>0].
finish

2021-05-18 20:12:17.797 LOG: result=m - 2 < 0 /\ 2 m - 3 >= 0
2021-05-18 20:12:17.798 LOG: mathcode=Reduce[m - 2 < 0 && 2 m - 3 >= 0 && m>0,m,Reals]
2021-05-18 20:12:17.799 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:12:17.801 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^3+a^2 b+a^2 c+a b^2+3 a b c+a c^2+b^3+b^2 c+b c^2+c^3=(a^2 b m+a^2 c m+a b^2 m+2 a b c m+a c^2 m+b^2 c m+b c^2 m)
2021-05-18 20:12:17.801 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^3+a^2 b+a^2 c+a b^2+3 a b c+a c^2+b^3+b^2 c+b c^2+c^3=(a^2 b m+a^2 c m+a b^2 m+2 a b c m+a c^2 m+b^2 c m+b c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:21.627 LOG: result=m - 2 < 0 /\ 2 m - 3 >= 0
2021-05-18 20:12:21.629 LOG: mathcode=Reduce[m - 2 < 0 && 2 m - 3 >= 0 && m>0,m,Reals]
2021-05-18 20:12:21.63 Inequality[3/2, LessEqual, m, Less, 2]
2021-05-18 20:12:21.63 LOG: subst() => lhs=((1+b+c)/2+1)/(b+c)+((1+b+c)/2+b)/(c+1)+((1+b+c)/2+c)/(1+b),rhs=1
2021-05-18 20:12:21.631 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2+1)/(b+c)+((1+b+c)/2+b)/(c+1)+((1+b+c)/2+c)/(1+b) == m * (1))
2021-05-18 20:12:21.631 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (((1+b+c)/2+1)/(b+c)+((1+b+c)/2+b)/(c+1)+((1+b+c)/2+c)/(1+b) == m * (1))],Reals],Reals]
2021-05-18 20:12:21.823 Inequality[15/4, LessEqual, m, Less, 9/2]
2021-05-18 20:12:21.823 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2+a)/(b+c)+((a+b+c)/2+b)/(c+a)+((a+b+c)/2+c)/(a+b) == m * (1))
2021-05-18 20:12:21.824 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (((a+b+c)/2+a)/(b+c)+((a+b+c)/2+b)/(c+a)+((a+b+c)/2+c)/(a+b) == m * (1))],Reals],Reals]
2021-05-18 20:12:22.315 Inequality[15/4, LessEqual, m, Less, 9/2]
2021-05-18 20:12:22.316 LOG: subst() => lhs=((1+b+c)/2+1)/(b+c)+((1+b+c)/2+b)/(c+1)+((1+b+c)/2+c)/(1+b),rhs=1
2021-05-18 20:12:22.318 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 3 b^3+6 b^2 c+6 b^2+6 b c^2+15 b c+6 b+3 c^3+6 c^2+6 c+3=(2 b^2 c m+2 b^2 m+2 b c^2 m+4 b c m+2 b m+2 c^2 m+2 c m)
2021-05-18 20:12:22.318 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 3 b^3+6 b^2 c+6 b^2+6 b c^2+15 b c+6 b+3 c^3+6 c^2+6 c+3=(2 b^2 c m+2 b^2 m+2 b c^2 m+4 b c m+2 b m+2 c^2 m+2 c m)].
assume[m>0].
finish

2021-05-18 20:12:26.014 LOG: result=2 m - 9 < 0 /\ 4 m - 15 >= 0
2021-05-18 20:12:26.015 LOG: mathcode=Reduce[2 m - 9 < 0 && 4 m - 15 >= 0 && m>0,m,Reals]
2021-05-18 20:12:26.017 Inequality[15/4, LessEqual, m, Less, 9/2]
2021-05-18 20:12:26.019 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ 3 a^3+6 a^2 b+6 a^2 c+6 a b^2+15 a b c+6 a c^2+3 b^3+6 b^2 c+6 b c^2+3 c^3=(2 a^2 b m+2 a^2 c m+2 a b^2 m+4 a b c m+2 a c^2 m+2 b^2 c m+2 b c^2 m)
2021-05-18 20:12:26.019 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ 3 a^3+6 a^2 b+6 a^2 c+6 a b^2+15 a b c+6 a c^2+3 b^3+6 b^2 c+6 b c^2+3 c^3=(2 a^2 b m+2 a^2 c m+2 a b^2 m+4 a b c m+2 a c^2 m+2 b^2 c m+2 b c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:29.859 LOG: result=2 m - 9 < 0 /\ 4 m - 15 >= 0
2021-05-18 20:12:29.859 LOG: mathcode=Reduce[2 m - 9 < 0 && 4 m - 15 >= 0 && m>0,m,Reals]
2021-05-18 20:12:29.86 Inequality[15/4, LessEqual, m, Less, 9/2]
2021-05-18 20:12:29.861 LOG: subst() => lhs=(1-1/b)*(1-1/c)+1,rhs=(c-1)/b+(b-1)/c
2021-05-18 20:12:29.861 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1-1/b)*(1-1/c)+1 == m * ((c-1)/b+(b-1)/c))
2021-05-18 20:12:29.861 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1-1/b)*(1-1/c)+1 == m * ((c-1)/b+(b-1)/c))],Reals],Reals]
2021-05-18 20:12:29.93 m > 1
2021-05-18 20:12:29.93 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((1-a/b)*(1-a/c)+1 == m * ((c-a)/b+(b-a)/c))
2021-05-18 20:12:29.93 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((1-a/b)*(1-a/c)+1 == m * ((c-a)/b+(b-a)/c))],Reals],Reals]
2021-05-18 20:12:29.969 m > 1
2021-05-18 20:12:29.969 LOG: subst() => lhs=(1-1/b)*(1-1/c)+1,rhs=(c-1)/b+(b-1)/c
2021-05-18 20:12:29.97 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ 2 b^2 c^2-b^2 c-b c^2+b c=(b^3 c m-b^2 c m+b c^3 m-b c^2 m)
2021-05-18 20:12:29.97 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ 2 b^2 c^2-b^2 c-b c^2+b c=(b^3 c m-b^2 c m+b c^3 m-b c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:33.566 LOG: result=m - 1 > 0
2021-05-18 20:12:33.567 LOG: mathcode=Reduce[m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:12:33.568 m > 1
2021-05-18 20:12:33.569 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^2 b c-a b^2 c-a b c^2+2 b^2 c^2=(-a b^2 c m-a b c^2 m+b^3 c m+b c^3 m)
2021-05-18 20:12:33.569 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^2 b c-a b^2 c-a b c^2+2 b^2 c^2=(-a b^2 c m-a b c^2 m+b^3 c m+b c^3 m)].
assume[m>0].
finish

2021-05-18 20:12:37.137 LOG: result=m - 1 > 0
2021-05-18 20:12:37.138 LOG: mathcode=Reduce[m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:12:37.139 m > 1
2021-05-18 20:12:37.139 LOG: subst() => lhs=1+b^2+c^2,rhs=(1+b+c)^2
2021-05-18 20:12:37.14 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b^2+c^2 == m * ((1+b+c)^2))
2021-05-18 20:12:37.14 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] (1+b^2+c^2 == m * ((1+b+c)^2))],Reals],Reals]
2021-05-18 20:12:37.291 Inequality[1/3, LessEqual, m, Less, 1/2]
2021-05-18 20:12:37.292 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2+b^2+c^2 == m * ((a+b+c)^2))
2021-05-18 20:12:37.292 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] (a^2+b^2+c^2 == m * ((a+b+c)^2))],Reals],Reals]
2021-05-18 20:12:37.637 Inequality[1/3, LessEqual, m, Less, 1/2]
2021-05-18 20:12:37.638 LOG: subst() => lhs=1+b^2+c^2,rhs=(1+b+c)^2
2021-05-18 20:12:37.638 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^2+c^2+1=(b^2 m+2 b c m+2 b m+c^2 m+2 c m+m)
2021-05-18 20:12:37.638 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^2+c^2+1=(b^2 m+2 b c m+2 b m+c^2 m+2 c m+m)].
assume[m>0].
finish

2021-05-18 20:12:41.238 LOG: result=2 m - 1 < 0 /\ 3 m - 1 >= 0
2021-05-18 20:12:41.238 LOG: mathcode=Reduce[2 m - 1 < 0 && 3 m - 1 >= 0 && m>0,m,Reals]
2021-05-18 20:12:41.239 Inequality[1/3, LessEqual, m, Less, 1/2]
2021-05-18 20:12:41.24 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^2+b^2+c^2=(a^2 m+2 a b m+2 a c m+b^2 m+2 b c m+c^2 m)
2021-05-18 20:12:41.24 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^2+b^2+c^2=(a^2 m+2 a b m+2 a c m+b^2 m+2 b c m+c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:44.886 LOG: result=2 m - 1 < 0 /\ 3 m - 1 >= 0
2021-05-18 20:12:44.888 LOG: mathcode=Reduce[2 m - 1 < 0 && 3 m - 1 >= 0 && m>0,m,Reals]
2021-05-18 20:12:44.889 Inequality[1/3, LessEqual, m, Less, 1/2]
2021-05-18 20:12:44.89 LOG: subst() => lhs=(1+b+c)^3,rhs=5*(b*c*(b+c)+c*(c+1)+b*(1+b))-3*b*c
2021-05-18 20:12:44.89 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)^3 == m * (5*(b*c*(b+c)+c*(c+1)+b*(1+b))-3*b*c))
2021-05-18 20:12:44.89 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+b+c)^3 == m * (5*(b*c*(b+c)+c*(c+1)+b*(1+b))-3*b*c))],Reals],Reals]
2021-05-18 20:12:45.192 Inequality[4/5, Less, m, LessEqual, 1]
2021-05-18 20:12:45.192 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)^3 == m * (5*(b*c*(b+c)+c*a*(c+a)+a*b*(a+b))-3*a*b*c))
2021-05-18 20:12:45.192 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((a+b+c)^3 == m * (5*(b*c*(b+c)+c*a*(c+a)+a*b*(a+b))-3*a*b*c))],Reals],Reals]
2021-05-18 20:12:45.988 Inequality[4/5, Less, m, LessEqual, 1]
2021-05-18 20:12:45.989 LOG: subst() => lhs=(1+b+c)^3,rhs=5*(b*c*(b+c)+c*(c+1)+b*(1+b))-3*b*c
2021-05-18 20:12:45.99 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^3+3 b^2 c+3 b^2+3 b c^2+6 b c+3 b+c^3+3 c^2+3 c+1=(5 b^2 c m+5 b^2 m+5 b c^2 m-3 b c m+5 b m+5 c^2 m+5 c m)
2021-05-18 20:12:45.99 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^3+3 b^2 c+3 b^2+3 b c^2+6 b c+3 b+c^3+3 c^2+3 c+1=(5 b^2 c m+5 b^2 m+5 b c^2 m-3 b c m+5 b m+5 c^2 m+5 c m)].
assume[m>0].
finish

2021-05-18 20:12:49.605 LOG: result=5 m - 4 > 0 /\ m - 1 <= 0
2021-05-18 20:12:49.606 LOG: mathcode=Reduce[5 m - 4 > 0 && m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:12:49.607 Inequality[4/5, Less, m, LessEqual, 1]
2021-05-18 20:12:49.609 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^3+3 a^2 b+3 a^2 c+3 a b^2+6 a b c+3 a c^2+b^3+3 b^2 c+3 b c^2+c^3=(5 a^2 b m+5 a^2 c m+5 a b^2 m-3 a b c m+5 a c^2 m+5 b^2 c m+5 b c^2 m)
2021-05-18 20:12:49.609 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^3+3 a^2 b+3 a^2 c+3 a b^2+6 a b c+3 a c^2+b^3+3 b^2 c+3 b c^2+c^3=(5 a^2 b m+5 a^2 c m+5 a b^2 m-3 a b c m+5 a c^2 m+5 b^2 c m+5 b c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:53.454 LOG: result=5 m - 4 > 0 /\ m - 1 <= 0
2021-05-18 20:12:53.455 LOG: mathcode=Reduce[5 m - 4 > 0 && m - 1 <= 0 && m>0,m,Reals]
2021-05-18 20:12:53.456 Inequality[4/5, Less, m, LessEqual, 1]
2021-05-18 20:12:53.456 LOG: subst() => lhs=(1+1/b)*(1+1/c),rhs=3+(1+b)/c+(1+c)/b
2021-05-18 20:12:53.456 LOG: ineqs=(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+1/b)*(1+1/c) == m * (3+(1+b)/c+(1+c)/b))
2021-05-18 20:12:53.456 LOG: code=Reduce[Resolve[Exists[{b,c},(m>0) \[And] (1+b>c) \[And] (b+c>1) \[And] (c+1>b) \[And] ((1+1/b)*(1+1/c) == m * (3+(1+b)/c+(1+c)/b))],Reals],Reals]
2021-05-18 20:12:53.614 Inequality[1/5, Less, m, Less, 1]
2021-05-18 20:12:53.615 LOG: ineqs=(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((1+a/b)*(1+a/c) == m * (3+(a+b)/c+(a+c)/b))
2021-05-18 20:12:53.615 LOG: code=Reduce[Resolve[Exists[{a,b,c},(m>0) \[And] (a+b>c) \[And] (b+c>a) \[And] (c+a>b) \[And] ((1+a/b)*(1+a/c) == m * (3+(a+b)/c+(a+c)/b))],Reals],Reals]
2021-05-18 20:12:53.81 Inequality[1/5, Less, m, Less, 1]
2021-05-18 20:12:53.81 LOG: subst() => lhs=(1+1/b)*(1+1/c),rhs=3+(1+b)/c+(1+c)/b
2021-05-18 20:12:53.811 LOG: ineqs=1+b>c /\ b+c>1 /\ c+1>b /\ b^2 c^2+b^2 c+b c^2+b c=(b^3 c m+3 b^2 c^2 m+b^2 c m+b c^3 m+b c^2 m)
2021-05-18 20:12:53.811 LOG: code=[]
(m,b,c)
1
(Eb)(Ec)[1+b>c /\ b+c>1 /\ c+1>b /\ b^2 c^2+b^2 c+b c^2+b c=(b^3 c m+3 b^2 c^2 m+b^2 c m+b c^3 m+b c^2 m)].
assume[m>0].
finish

2021-05-18 20:12:57.403 LOG: result=m - 1 < 0 /\ 5 m - 1 > 0
2021-05-18 20:12:57.404 LOG: mathcode=Reduce[m - 1 < 0 && 5 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:12:57.404 Inequality[1/5, Less, m, Less, 1]
2021-05-18 20:12:57.406 LOG: ineqs=a+b>c /\ b+c>a /\ c+a>b /\ a^2 b c+a b^2 c+a b c^2+b^2 c^2=(a b^2 c m+a b c^2 m+b^3 c m+3 b^2 c^2 m+b c^3 m)
2021-05-18 20:12:57.406 LOG: code=[]
(m,a,b,c)
1
(Ea)(Eb)(Ec)[a+b>c /\ b+c>a /\ c+a>b /\ a^2 b c+a b^2 c+a b c^2+b^2 c^2=(a b^2 c m+a b c^2 m+b^3 c m+3 b^2 c^2 m+b c^3 m)].
assume[m>0].
finish

2021-05-18 20:13:01.046 LOG: result=m - 1 < 0 /\ 5 m - 1 > 0
2021-05-18 20:13:01.047 LOG: mathcode=Reduce[m - 1 < 0 && 5 m - 1 > 0 && m>0,m,Reals]
2021-05-18 20:13:01.048 Inequality[1/5, Less, m, Less, 1]