Is there an implementation for the first-order theory of the reals? I know there exists one technique by Collins based on cylindrical algebraic decomposition but I don't know of any theorem provers that implement it.
The decision procedures implemented by z3 for various arithmetic domains is listed here: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arithmetic.