@acer Thanks. I find the identical error when Maple calls certain external routines: 

(* omitted *)
trace(SMTLIB:-Satisfiable, statements = false):
coulditbe(m, 0);
{--> enter SMTLIB:-Satisfiable, args = {Or(1 <= n_2, n_2 < 0), m_1 = 0, 0 < m_1-(1/2)*n_2^2+(1/2)*n_2}, timelimit = .25
<-- ERROR in SMTLIB:-Satisfiable (now in \`is/internal/SMTLIB\`) = external linking: error loading external library %1: %2, mplsmtlib.dll, �Ҳ���ָ����ģ�顣\r\n}
{--> enter SMTLIB:-Satisfiable, args = {Or(1 <= n_2, n_2 < 0), m_1 = 0, 0 < m_1-(1/2)*n_2^2+(1/2)*n_2}, timelimit = .25
<-- ERROR in SMTLIB:-Satisfiable (now in \`is/internal/SMTLIB\`) = external linking: error loading external library %1: %2, mplsmtlib.dll, �Ҳ���ָ����ģ�顣\r\n}
                              FAIL

I also believe that the problem lies in the compatibility between SMTLIB:-smtlib_execute and vcredist_x64.exe.

@Thomas Richard Thanks. That is strange indeed. https://www.maplesoft.com/support/help/Maple/view.aspx?path=updates/Maple2020/AdvancedMath#section155 says: 

So I guess that the problem is due to some compatibility issue of the SMTLIB package. 
Besides, I find a related compatibility issue of SMTLIB:-Satisfy before. Can you reproduce the same bug in that example? Actually, if I install the Microsoft Visual C++ 2013 x64 Additional Runtime (not "2015-2022"), those errors will disappear immediately, while if I uninstall the Microsoft Visual C++ 2013 Redistributable (x64) (not "2015-2022"), I'll get those errors again.

@Thomas Richard Thanks for your reply. The documentation of coulditbe says that:

Besides, have you installed the Microsoft Visual C++ 2013 x64 Additional Runtime? I find that if I install or reinstall it, such computations will no longer fail immediately, while if I uninstall it, I'll get FAIL again. The problem is: Maple 2023.0, by default, don't install Microsoft Visual C++ 2013 Redistributable (x64), as the directory "<Maple>\redist\" (where <Maple> is the Maple installation directory, i.e., kernelopts(mapledir);) only contains two (rather than six) redistributable files.
But why is there a (hidden) compatibility issue? I cannot find it here.

@vv That's a pity; I don't know why Maple^® cannot handle real algebraic functions directly and then give a more readable (but still correct) solution.
Let us see what Symbolic Math Toolbox™ returns: 

@vv Thanks.

But how about the poster's question (instead of generalized cases)? 

@vv Thanks. But how do I force Maple to eliminate the dummy variable t3 from the output automatically (instead of by hand later)? Actually, the desired result should resemble .

@Kitonum 

Download inequalities_are_not_supported.mw

@vs140580 Sorry, I just want to reply to CL's "fast or slow" statement. I don't answer your question.

@Carl Love Thanks.

Incidentally, it appears that the seq version is somewhat faster: (Another comparison.) 

Download iRandomPointVector1.mw
 

Download iRandomPointVector2.mw

@vs140580 How large is your n? However, I think that the most convenient way is using seq(seq(seq(…, k in list), j in list), i in list); (or seq(…, l in combinat:-choose(list, 3));).
(By the way, it seems to me that using for loops in Maple is generally not the most efficient way to iterate over some index variable(s).)

@acer Thanks for your observation.
Can anyone reproduce that bug in Maple 2018?

@mmcdara Thanks. If I understand right, for this purpose, I have to replace the problem variables manually first. So, is it impossible to find the exact supermun directly?
Actually, I have some more complex expressions, but Maple's maximize (or minimize) often gives incorrect results without any exception messages (although the Student[MultivariateCalculus][LagrangeMultipliers] function sometimes works). 

@Carl Love Well, you may consider 

k*x*y - (x - y)^2/2; # which is equal to (1 + k)*x*y - (x^2 + y^2)/2

 for some real parameter k. When k = 0, its supremum is just 0, while when k > 0, its supremum is no longer 0 (but it appears that Maple don't know this fact). (As the arithmetic mean-geometric mean inequality says, we have x²＋y²≥2xy, where the coefficient "2" cannot be replaced with a larger number in general.)

@QM I agree you. This example is simple enough, so it's not hard to find (and then fix) such a bug; nonetheless, ensuring the correctness would never be users' responsibility!

@C_R Thanks. That's really strange. I don't know what happened in Maple 2023: sqrt(A^2) doesn't work, but sqrt(A)^2, sqrt(A*A), and sqrt(A)*sqrt(A) all works.