The decision procedure of theory of closed real field is in NP-hard? The decision procedure of theory of closed real field  refers to https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers
Yes, even in the purely existential case. See https://en.wikipedia.org/wiki/Existential_theory_of_the_reals