$FO^2$, i.e. two-variable first-order logic, has a NEXPTIME-complete satisfiability problem (see Grädel, Kolaitis and Vardi '97). However, the decidability and complexity of this fragment is proved by that paper in an indirect way, as far as I can tell.
What I need instead is an effective way to solve $FO^2$ satisfiability. What are the actual algorithms and methods available for this logic?
In particular, I would need a tableau-based method for $FO^2$ satisfiability. Is there any resource describing such a thing? Has it ever been developed?