Advanced Search

Question: could be or could not be

Question:could be or could not be

sursumCorda 1079 Maple 2024
realdomain coulditbe smtlib satisfiable
September 16 2024
1

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

expr := Or(And(-p^2 + 3*q < 0, p < 0, p^2 - 4*q < 0, Or(And(p < 0, -q < 0), p < 0, q < 0), Or(And(-2*p^2 + 3*q < 0, -q^2 < 0), And(p <= 0, Or(-2*p^2 + 3*q < 0, q^2 < 0))), Or(And(Or(And(p < 0, -q < 0), p < 0, q < 0), Or(And(-2*p^2 + 3*q < 0, -q^2 < 0), And(p <= 0, Or(-2*p^2 + 3*q < 0, q^2 < 0)))), And(p < 0, -q < 0), p < 0, q < 0, And(2*p^2 - 3*q < 0, -q^2 < 0), And(-p <= 0, Or(2*p^2 - 3*q < 0, q^2 < 0))), -2*p^5 + 15*p^3*q - 27*p*q^2 <= 0, p^2*q^2 - 4*q^3 = 0), And(p^2 - 3*q = 0, p < 0, -2*p^2 + 3*q < 0, Or(And(p < 0, -2*p^2 + 3*q < 0), p < 0, 2*p^2 - 3*q < 0), 2*p^3 - 9*p*q = 0), And(-p^2 + 3*q < 0, Or(And(p < 0, p^2 - 4*q < 0), p < 0, -p^2 + 4*q < 0), p < 0, -q < 0, Or(And(-2*p^2 + 3*q < 0, -q^2 < 0), And(-p <= 0, Or(-2*p^2 + 3*q < 0, q^2 < 0))), Or(And(p < 0, -q < 0, Or(And(-2*p^2 + 3*q < 0, -q^2 < 0), And(-p <= 0, Or(-2*p^2 + 3*q < 0, q^2 < 0)))), And(p < 0, -q < 0), And(2*p^2 - 3*q < 0, -q^2 < 0), And(p <= 0, Or(2*p^2 - 3*q < 0, q^2 < 0))), 2*p^5 - 15*p^3*q + 27*p*q^2 <= 0, p^2*q^2 - 4*q^3 = 0)):

According to coulditbe, expr is satisfiable: 

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

But according to SMTLIB:-Satisfiable, expr 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?). 
Please Wait...