Taelja

Taelja translates refutations produced by resolution and superposition provers into direct, structured, and readable proofs.
It takes TSTP proofs generated by E, Twee, or Vampire and presents them as axioms, a sequence of lemmas, and the goal, where every step is justified by hyperresolution or by a chain of equalities citing the axiom or lemma it uses.

The tool supports the Horn clause fragment and reports any input proof that falls outside it.

Repository:
github.com/kondylidou/Taelja