Proof Generation for Saturating First-Order Theorem Provers

First-order Automated Theorem Proving (ATP) is one of the oldest and most developed areas of automated reasoning. Today, the most widely used first-order provers are fully automatic and process first-order logic with equality. Many state-of-the-art ATP systems consist of a clausifier, translating a full first-orde