QE on HOL Light.
# #use "Rqe/make.ml";; ... # time REAL_QELIM_CONV`!a b c. (?x. &0<=x pow 3 +a* x pow 2+ b*x+c) `;; CPU time (user): 614.655 val it : thm = |- (!a b c. ?x'. &0 <= x' pow 3 + a * x' pow 2 + b * x' + c) <=> T
# #use "Rqe/make.ml";; ... # time REAL_QELIM_CONV`!a b c. (?x. &0<=x pow 3 +a* x pow 2+ b*x+c) `;; CPU time (user): 614.655 val it : thm = |- (!a b c. ?x'. &0 <= x' pow 3 + a * x' pow 2 + b * x' + c) <=> T