You are mixing things up a bit, the alternatives you want are z3, cvc4, spass and e. Coq and TLA+ are proof assistents / formal specification languages, not smt

You are mixing things up a bit, the alternatives you want are z3, cvc4, spass and e. Coq and TLA+ are proof assistents / formal specification languages, not smt solvers/theorem provers. And actually in my experience with using the sledgehammer tool in Isabelle, Vampire does not fare very well when it comes to real world problems.