Given a formula, the software builds a proof or an interpretation that falsifies it.
Given a formula and proof, the software annotates the proof by indicating the rules applied.
Given a list of clauses, as well as limits on the time of proof and the size of the clauses,
the software tries to build a proof of the empty clause within the imposed limits.
Given a formula, the software translates the formula into a S4-formula and either builds a proof of its translation
into S4 or provides a falsifying interpretation.