Existing implementation of Scott's reduction?

Question

As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the fact that any sentence in $\mathrm{FO^2}$ can be reduced to Scott's Normal form in polynomial time. The Scott's Normal form is given as $$\forall x \forall y \alpha(x,y) \land \bigwedge_{i=1}^{m} \forall x \exists y \beta_{i}(x,y) $$ Does anyone know of existing code base where scott's reduction is implemented, i.e I input an arbitrary $\mathrm{FO^2}$ sentence and get it's Scott's Normal Form?

Answer 1

You might check the FO2 solver by Tomer Kotek et. al (ICDT 2017): https://forsyte.at/alumni/kotek/fo2-solver/

as well as an FO2 solver by Tony Tan and his students (LICS 2021): https://arxiv.org/abs/2104.10621

Answering the question, the authors implemented an improved version of Scott Normal Form, called therein "Skolemized Scott Normal Form". All the details are available here: https://arxiv.org/pdf/1610.02101.pdf