State of the Art for the Monadic Class?
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.