@dharr Thanks. As you can see, edges may overlap, so it is not a visually appealing layout of this graph. It is hoped that a aesthetic drawing in a hierarchical fashion has minimal edge crossing (like the examples from Mathematica and MATLAB).

@Carl Love Thanks!

subs[eval](
    `is/internal/SMTLIB_max_sys_size`= `is/internal/SMTLIB_max_sys_size`/2,
    eval(`is/internal/SMTLIB`)
):

works well, but it seems that none of 

eval(
    eval(`is/internal/SMTLIB`),
    `is/internal/SMTLIB_max_sys_size`= `is/internal/SMTLIB_max_sys_size`/2
):
algsubs(
    `is/internal/SMTLIB_max_sys_size`= `is/internal/SMTLIB_max_sys_size`/2,
    eval(`is/internal/SMTLIB`)
):
applyrule(
    `is/internal/SMTLIB_max_sys_size`= `is/internal/SMTLIB_max_sys_size`/2,
    eval(`is/internal/SMTLIB`)
):

works. 

 Yes, just for fun. Although we don't know how Mathematica implements the RandomPoint, a similar function Random`RandomPointVector can still be viewed in Mathematica. (Note that these are not the same as Maple's geom3d[randpoint] and linalg[randvector].) If one has the license of MMA, one may run the following code in its interface: 

GeneralUtilities`PrintDefinitions[Random`RandomPointVector]; 
GeneralUtilities`PrintDefinitions[Region`RandomPointDump`SymbolicRegionRandom];
(*Mathematica style*)

But until now, Maple still haven't had a built-in subroutine that can generate a list of (pseudorandom) points uniformly in an arbitrary valid parameter-free region in general.

@Markiyan Hirnyk Well, I have just checked the latest how Maple's performance compares to Mathematica. MMA now claims that median performance for random number generation shows Mathematica to be more than 20 times faster than Maple. However, I'm not sure if such tests are fair. Interestingly, MMA also summarizes the new features in each Maple release. I have to admit that its marketing ploy is quite powerful.

@Carl Love Now I see. It's really an intricate maze. Thanks again.

@acer Thanks anew. But what does [5,7,1,2,5,1,1,2,1,2,1,2,1]=10 mean?

Furthermore, whilst the help page says that the is command makes calls to the SMTLIB package to help compute some answers involving real variables, the help page does say that MathematicalFunctions[Is] only manipulates its input before sending it to the corresponding lowercase command is (and so does MathematicalFunctions[Coulditbe]). However,@Carl Love  has shown that the new command MathematicalFunctions[Coulditbe], in effect, might not perform basically the same operation as the standard coulditbe command. That's queer indeed.

@Carl Love Many thanks. I think that it should be 

# resume
MathematicalFunctions:-Assume(V[] ::~ real);
MathematicalFunctions:-Coulditbe(And(d1[]));

This time it becomes rather time-consuming; I have to abort it manually after thousands of seconds.
In this case, solve is useful indeed. But if there are not no solutions (which means ⇏), solve will run for too long, and coulditbe fails again. For instance, considering 

d3:= {p1, p2, S4 <= 1};
_EnvTry := hard: 
(coulditbe(`and`(d2[])) assuming V[] ::~ real); # FAIL

As for MathematicalFunctions:-Coulditbe, it seems that we need to take a longer time—maybe several hours or even more. However, this may not be acceptable for the user.

@Carl Love Sorry for late reply. I am testing it.

@acer Thanks. I would like there to be such new capabilities in a future release (like Maple 2024) if possible.

Ordinarily, SMTLIB[Satisfiable] is inapplicable to general situations (and does not support some elementary functions). The implicit objective of my question is to eliminate quantifiers and then to produce an equivalent quantifier-free formula. (SMTLIB[Satisfiable] thus no longer pertains if the result is not simply true or false.) Insofar as I know it, this functionality has been implemented in Maple as RegularChains[SemiAlgebraicSetTools][QuantifierElimination], but those formulae appearing in statements are all interpreted over ℝ (and do not support something as well). Moreover, the command seems to perform badly as yet on certain slightly complicated statements such as F₁⇏R₃ (although a trivial counterexample exists). 
Incidentally, doing the same thing (e.g., QE4C and QE4R), by contrast, is much easier in Mathematica. In my opinion, there is still considerable room for improvement in Maple.

@acer I'm not sure. In accordance with MathematicalFunctions/Is, Is(A, B, ...) = not Coulditbe(Not(A), Not(B), Not(...)); accordingly, is( F1 and not F2 )＝not coulditbe( not F1 or F2 ). In addition, the help page of is explains that the coulditbe routine returns true if there is a set of such parameter values for which the proposition is true. So, not is( F1 and not F2 ) assuming real just suggests ∃ (instead of ⇒'s ∀). For example, considering 

R3 := a*b*c*d >1 and a*b*c + a*b*d + a*c*d + b*c*d > 0:

((not is(F1 and not R3)) assuming real); # ture

However, F1⇏R3, for the point (a, b, c, d) = (1, 1, 1, 1) (which is in F1) doesn't satisfy R3.

BTW, it seems that SMTLIB[Satisfiable] is another extension of coulditbe.

@Carl Love Thanks for your kind explanation.
I find that there exists one function HamiltonianSAT in showstat(GraphTheory:-IsHamiltonian) (or print(GraphTheory:-IsHamiltonian)). Is it possible to call a built-in but undocumented function by the Maple standard interface in general?

@Carl Love Thanks for your comments. The reason why I try different methods is that, recently, I read an old essay on Mathematica which claims that if one large graph is Hamiltonian, then running ChvátalQ may be faster than running native Combinatorica`HamiltonianQ. So I want to test the same thing in Maple.

Besides, the help page also says: By setting infolevel[IsHamiltonian] to an integer greater than 1 a message will be displayed stating how the graph was proven, or disproven, to be Hamiltonian. But this setting doesn't work in some cases. (Although I never need such messages, a bug described below does exist.)
Attachment: infolevel[IsHamiltonian].mws

@acer "Strangely" means: Maple can work out 

minimize(x^3 + y^3 + z^3 - 4*x*y*z, x = 0 .. infinity, y = 0 .. infinity) assuming z>0;

correctly, or work out 

minimize(x^3 + y^3 - 4*x*y, x = 0 .. infinity, y = 0 .. infinity); # Put z = 1 here, and remove the constant.

correctly, but Maple give incorrect result for 

minimize(x^2 + y^2 - 4*x*y, x = 0 .. infinity, y = 0 .. infinity); # cubic → quadratic

How about x^n+y^n-4*x*y? 
I don't know why Maple cannot deal with x²+y²-4xy (or more clearly, (x-y)²-2xy).

This may be a serious issue; it turns out that certain Maple's symbolic results (without any warnings) are not always reliable indeed. For a simple problem, we can easily discover potential mistakes, but what about large-scale and complex problems…

@mmcdara Some substitutions can be applied, but unfortunately, they are of no effect. For instance, 

minimize(evalindets(x^3 + y^3 + z^3 - 4*x*y*z, 'symbol', x -> 1/x - 1), [x, y, z] =~ 0 .. 1);

still returns 0. Set [x,y,z]=~10^(-12)..1 may avoid incorrect result. However, I hope that Maple can "prove" the minimum (or infimum) by itself (like Mathematica); otherwise Optimization:-Minimize is certainly the better choice. 

@acer Thanks for your examples. Strangely, 

minimize(x^3 + y^3 + z^3 - 4*x*y*z, x = 0 .. infinity, y = 0 .. infinity) assuming z>0;

returns correct results, but the much easier version 

minimize((x - y)^2 - k*x*y, [x = 0 .. infinity, y = 0 .. infinity]) assuming (k > 0);

still returns wrong results. Any reason?