ProofStatus
Specifies the proof status of a Conjecture
Values
CONTR
Contradictory: There are proof attempts that found a proof as well as some that found a counter example. This indicates a malfunction of the reasoning system.
CSA
CounterSatisfiable: A counter example was found.
CSAS
CounterSatisfiable on a subset of axioms: A counter example was found but only a subset of the axioms was used. There is no conclusive result.
ERR
Error: A proof attempt has failed.
OPN
Open: No proof attempt has been finished.
RSO
ResourceOut: The reasoner ran out of time/memory.
THM
Theorem: A proof was found.
UNK
Unknown: There is no solution.