Ekstrakto est un outil permettant de traduire des preuves au format TSTP en preuves lambdapi. Il génère des fichiers TPTP pour chaque étape de la preuve TSTP, ainsi qu'un fichier de signature lambdapi et un fichier de preuve lambdapi complet. Il peut ensuite être utilisé avec des preuves automatisées pour générer des fichiers de preuve lambdapi pour chaque étape.