Tableau method for two-variable first-order logic $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?
You might check the FO2 solver by Tomer Kotek: https://forsyte.at/alumni/kotek/fo2-solver/ This is the only existing FO2 solver (Tony Tan with his student have a paper under submission, in which they proposed another algorithm, based on probabilistic methods).
I'm not aware of any tableaux algorithm for FO2.