Data : a formula
If the formula is syntactically wrong, the system prints an error message.
If the formula is provable, its proof is displayed.
If the formula is not provable, the prover gives a counter-model.
The prover is implemented in
Last Modified : 20-Nov-2019