To verify automated theorem provers (ATP), datasets from for instance TPTP are used (tptp.org). Now, I am interested in verifying our ATP. Currently, I am only focussed on solving statements with Intuitionistic propositional logic at this time, so www.iltp.de provides a dataset in the TPTP format. Is there a straight forward way to translate this list of statements to Coq language? I need to get these statements into strings of plaintext, as the ATP interfaces with coq over sertop.
Alternatively, is there another dataset that contains statements that can be solved using intuitionistic propositional logic? I have looked through the dataset CoqGym provides but I did not find any proper indication of what was IPL.
Thank you for your help!