Crate mrs_proof 

Proof objects and TSTP output for automated theorem proving.

After a refutation is found, this crate:

1. Extracts the proof DAG by tracing back from the empty clause through ClauseSource::Inference parent pointers (extract).
2. Formats the proof in TSTP format for verification by external tools (tstp).

Modules

elaborate

Post-refutation proof elaborator.

extract

Proof extraction from the clause store.

tstp

TSTP format output for proofs.