I have a quite complex expression (where and are real numbers): 

According to coulditbe, is satisfiable: 

_EnvTry := 'hard':
coulditbe(expr) assuming real;
 = 
                              true

But according to SMTLIB:-Satisfiable, is not satisfiable: 

SMTLIB:-Satisfiable(expr) assuming real;
 = 
                             false

Why are the two results opposite? 

For reference, below is the output from RealDomain:-solve: 

RealDomain:-solve(expr);
 = 
               /           1  2\                 
              { p = p, q = - p  }, {p = p, q = 0}
               \           4   /                 

I also tried using RealDomain:-simplify, yet the output remains almost unchanged (Why?). 

A classic result states that the equation x³＋px²＋qx＋r＝0 with real coefficients p, q, r has positive roots iff p＜0, q＞0, r＜0 and -27r² - 2p(2p² - 9q)r + q²(p² - 4q) ⩾ 0 (see for example this question). 
However, Maple appears unable to find the condition: 

a, b, c := allvalues(RootOf(x^3 + p*x^2 + q*x + r, x), 'implicit'):
RealDomain:-solve({a, b, c} >~ 0, [p, q, r]);
 = 
Warning, solutions may have been lost
                               []

Is there a way to get the above conditions in Maple with as little human intervention as possible (I mean, without a priori knowledge of the theory of polynomials)? 

Edit. An interesting problem is when these three positive roots can further be the lengths of sides of a triangle. For reference, here are some (unenlightening) results from some other software: 

The help page of interface('longdelim') states: 

If I set , the Maple Input

try f:=0 catch:end try;

can be converted into 

via , but why is

use f=0 in f+1 end use;

still converted into

 instead of “use f = 0 in f + 1 end”? 

According to the documentation, 

So the code below works as expected: 

f0 := proc(x::Not(2), y::2) [[x], [y]] end:
f0(1, 2);
                           [[1], [2]]

f0(2, 2);
Error, invalid input: f0 expects its 1st argument, x, to be of type Not(2), but received 2

The code below also works as expected: 

f1 := proc(x::depends(Not(y)), y::2) [[x], [y]] end:
f1(1, 2);
                           [[1], [2]]

f1(2, 2);
Error, invalid input: f1 expects its 1st argument, x, to be of type Not(2), but received 2

The code below works as desired as well: 

f2 := proc(x::seq(Not(2)), y::2) [[x], [y]] end:
f2(0, 1, 2);
                         [[0, 1], [2]]

f2(2, 1, 2);
                           [[], [2]]

However, the following code does not work: 

f3 := proc(x::seq(depends(Not(y))), y::2) [[x], [y]] end:
f3(0, 1, 2);
Error, invalid input: NULL uses a 2nd argument, y (of type 2), which is missing
f3(2, 1, 2);
Error, invalid input: NULL uses a 2nd argument, y (of type 2), which is missing

I believe that the output of  and  should be the same as that of  and  respectively. Did I miss something? 

In the Standard interface, the length of an expression that display in the worksheet can be limited using the Options dialog: Options Dialog - Precision Tab - Maple Help. However, I would like to know if I can change this option programmatically. The closest interface variables are elisiontermsbefore, elisiontermsafter and termelisionthreshold, but as the aforementioned help page states, they control the “term elision” and are not the same as “expression length limit”. So, is this possible?