One of the reasons Prover9 became so popular among mathematicians is its extremely user friendly syntax.

The drawback is that problems written in that syntax cannot be passed on to other ATP systems.

Our tool translates from Prover9 to TPTP or to the Waldmeister syntax. This will be a package for ProverX.

Produced with Carlos Sousa.