Short Proofs without New Variables

This page will provide access to proofs and tools presented in our CADE-26 paper.

Pigeon Hole Formulas

10: CNF formula PR proof
11: CNF formula PR proof
12: CNF formula PR proof
13: CNF formula PR proof
20: CNF formula PR proof
30: CNF formula PR proof
40: CNF formula PR proof
40: CNF formula PR proof

Two-Pigeons-Per-Hole

8: CNF formula PR proof
12: CNF formula PR proof
16: CNF formula PR proof
20: CNF formula PR proof

PR Proof checking tool

DPR-trim

Compile: gcc dpr-trim.c -O2 -o dpr-trim

Run: ./dpr-trim formula.cnf formula.pr