[SMT-LIB] Translators to SMT-LIB format

[Alessandro Armando]

Hi Cesare,

thanks for the prompt reply.

> There is no translator for this yet. But we hope to have one after the 
> summer.

This would be great.

> The main problem with this translation is not so much the syntax of TPTP 
> but the fact that TPTP's logic is unsorted, so a completely automated 
> translation is not possible. We are looking at semi-automatic approaches 
> in which the user manually provides a sorted signature for the benchmarks.

Sounds very reasonable.

Best Regards,

alessandro