Recently PolyPaver has gained support for a variant of the TPTP language similar to the variant supported by MetiTarski.
I have also added two example formulas in TPTP format that PolyPaver can prove.
One was generated by Why3 and the other one an edited version of a formula from the MetiTarski collection.
PolyPaver