# 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