Debugging of TPTP is made difficult by the translation of the entirety of SUMO being written to a single file for each language. I feel it would be a bit more clear if we created a separate file for the translation of each constituent.
As for running vampire, we can just create a SUMO.tptp/tff/thf file containing include statements for all the constituent files.
I don't know if this would cause any second order consequences, so this should be approved before implementation.
Debugging of TPTP is made difficult by the translation of the entirety of SUMO being written to a single file for each language. I feel it would be a bit more clear if we created a separate file for the translation of each constituent.
As for running vampire, we can just create a SUMO.tptp/tff/thf file containing include statements for all the constituent files.
I don't know if this would cause any second order consequences, so this should be approved before implementation.