Mizar CNF Problems and Prover9 Proofs (1439 New Bounties)

by BlakeKeiller, Sunday, September 12, 2021, 16:32 (84 days ago) @ BlakeKeiller

The problems look good to me. One minor thing I noticed: the clauses are reversed from the .cnf file to the .mg file. The order doesn't matter, of course, but just in case someone else is trying to see the correspondence I thought I'd point it out.

This weekend I used the bounty fund to place a bounty of (almost) 25 bars on each of these 1436 problems. For people who want to solve some of them, I'd suggest downloading the .tgz file in the OP and trying to use Prover9 and the distributed lisp files to obtain a Megalodon proof and then use Megalodon to obtain a Proofgold proof.

There are roughly 3800 blocks remaining during the phase where 25 bars of the reward goes into the bounty fund. More suggestions for problems to place bounties on are welcome.