Stop the verification process if some ATP finds a positive answer, that is, the problem results to be a theorem.
Stop the verification process if some ATP finds a positive answer, that is, the problem results to be a theorem.