"hypothesis" to annotate a TPTP formula. Is there some difference from Metis's point of view? Best regards, --=20 Andr=C3=A9s