State of the Art for the Monadic Class? Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete.

However, problems like SAT and SMT have fast algorithms for solving them, despite the theoretical bounds. 

I'm wondering, is there research analogous to SAT/SMT for monadic first order logic? What is the "state of the art" in this case, and are there algorithms which are efficient in practice, despite hitting the theoretical limits in the worst case?
I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS. 

In particular see the thesis of Ann-Christin Knoll, On Resolution
Decision Procedures
for the Monadic Fragment and Guarded Negation
Fragment. This implements what you want, though I couldn't find the implementation online.