@vv I am in agreement with you.
The QuantifierElimination command (since Maple 2020) in the SemiAlgebraicSetTools subpackage of RegularChains appears to be not experimental now. Unfortunately, it seems that neither QuantifierElimination:-QuantifierEliminate nor RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination can effectively eliminate quantifiers (because of the high complexity?). 

Note. In modern Mathematica, the elimination is often much faster (Why??!): 

Mathematica 13.3.0 Kernel for Microsoft Windows (64-bit)
Copyright 1988-2023 Wolfram Research, Inc.

In[1]:= EchoTiming[Resolve[ForAll[{x,y,z},(x|y|z)\[Element]NonNegativeReals\[And]x+y+z\[GreaterEqual]x*y*z-2,12*K+(x+y+z-(-1))^2\[GreaterEqual]K*(y*z+z*x+x*y)+(6-(-1))^2],WorkingPrecision\[RuleDelayed]21+1],Method\[Rule]RepeatedTiming]
>> 10.458

Out[1]= K == 4

In[2]:= EchoTiming[Resolve[ForAll[{x,y,z},(x|y|z)\[Element]NonNegativeReals\[And]x+y+z\[GreaterEqual]x*y*z-2,12*K+(x+y+z-(+2))^2\[GreaterEqual]K*(y*z+z*x+x*y)+(6-(+2))^2],WorkingPrecision\[RuleDelayed]17+1],Method\[Rule]RepeatedTiming]
>> 5.56633

Out[2]= 2 <= K <= 3

I surmise that this is because certain core components call optimized and compiled 𝙲 code rather than execute shallow native 𝙼𝚖𝚊 code ... I suppose so.

Alas, every coin has two sides; this may also result in uncommon inefficiency (as one has seen here).

@tomleslie Well, I do not believe that this is just a “feature”, and yet Maple 2023 still cannot solve this more carefully.

@vv It is fortunate to see that solve solved those two systems at last (though one has to await them for enough long (!)). Nevertheless, the output of the first system is too complicated: 

Download half_an_hour.mw

As you have expected, the certified result is simply . I cannot know why Maple did not simplify the returned value in a long time, which only leads to an unreadable (and more or less worthless) solution!

@C_R Sorry for misunderstanding. I don't mean that "a = 2/(sqrt(5) + 1) should be treated as a separate solution"; I just want to stress that the output should be “a >= 2/(sqrt(5)+1)” instead of "a > 2/(sqrt(5)+1)". (Isn't this a bug?) 
Besides, I find that this bug can even be reproduced in an old version! 

# in Maple 1x
> solve({a > 0, ln(a)+ln(1+a) >= 0}, a);
 = 
           /      /  2                    \        \ 
          { RootOf\_Z  - _Z - 1, index = 1/ - 1 < a }
           \                                       / 

It seems that Maple's developers still don't know this ….

@mmcdara Thanks for your trick. However, it appears the output is still not very accurate when using larger Digits. (And in many cases, it is even nearly unexpected.) The documentation writes that this package "takes advantage of built-in library routines provided by NAG", but I don't know why it cannot return a result with high precision.

@Axel Vogt As for the "source", it comes from a difficult algebraic inequality. But this question is another thing (as I do not need an exact supremum here).

@acer Thanks for your kind reply. You mention the Optimization package. In my view, this toolbox is much less smart than solve/float, evalf/Int, dsolve/numeric, and evalf/Sum (for some unaccountable reason). One can often find (too) many warning messages and errors during a computation. Well, there is a reasonable prospect that it is no longer actively developed (though is still being maintained (just like the algsubs command)). What a pity.

@Carl Love Many thanks! 
You said that "Maple uses dynamic scoping", but recently, I noticed the following sentence in What Has Changed in Maple V Release 5: 

Does this mean that Maple uses a mixed version instead?

@nm You say: "It goes without saying that listing all the proc names in trace([foo,....],statements = false) is not a real solution.". But the following code does work: 

foo:=proc(n,m,k)   
   local r;  
   #if DO_TRACE then
   #   option trace=0:
   #fi;
   
   boo(1);
   r:=n:
   NULL;
 end proc:

boo:=proc(n)   
   local r;  
   r:=n:
   NULL;
 end proc:

trace~([foo, boo], statements = false):
foo(1, 2, 3);
{--> enter foo, args = 1, 2, 3
{--> enter boo, args = 1
<-- exit boo (now in foo) = }
<-- exit foo (now at top level) = }

Is there any misunderstanding?

@nm I think that what you need is just trace(…, statements = false) (as @ecterrab said before).

@acer Thanks. Yet I'm confused. You writes that

It's a hidden performance penalty.

When working with vectors and matrices for general purpose, in MATLAB^®, a multidimensional array is in the form of a concatenation of lists, while in the Wolfram Language, a generalized matrix (where Mma use the term "tensor", in name only) are simply represented with a nested list; the users are able to focus on dealing with their core tasks and do not need to change data types and formats at each stage. (In other words, the inefficient coercion is, in effect, unnecessary.)
I am curious about why Maple did not elect to use a uniform fundamental container. The documentation asserts:

Well, is this just for historical reasons? (Note that I do not mean that Maple's decision was void/devoid of foresight or elegance. Actually, if there is a consistent class to do so, I think that one can accomplish more work with less keystrokes.)

@Alejandro Jakubi However, there is (almost) no difference between `trig/reduce` and `convert/trig`, as

showstat(`convert/trig`):

shows.

@Carl Love I agree you. Yet I cannot find any detailed explanation of why "Maple implementation is very inefficient" in the official documentation. (In other words, what I need is not simply a known fact or practical experience.) 
Actually, I read some viewpoints like: GOTOs can be a useful language feature improving program speed, size and code clarity, and instructions like break and continue are just the old goto in sheep's clothing. Is there any difference between Maple's goto and FORTRAN/C/...'s goto?

Another statement (from the Wikipedia article GOTO) is: Functional programming languages such as Scheme generally do not have goto, instead using continuations. But what about Maple (as for the continuation)?

@C_R You can change the third line to 

isolate(DETools:-firint(ode*DEtools:-intfactor(ode, phi(s)), phi(s)), _C1); # instead of c__1, but I don't know why the original one works before

As for the second error message, the ?? should be (1) (which is an equation label).

@ Sorry. What does "previous and more robust" mean? If I understand right, do you mean that the current version is less robust instead? 

Besides, it seems that neither the built-in Optimization package nor the additional GlobalOptimization package is well maintained; I cannot find any relevant news in most recent "Release Notes". (Actually, in some cases, MatLab's Optimization Toolbox and Global Optimization Toolbox are more powerful, but they are not easy-to-use for advanced users that are just familiar with Maple syntax.)