# Expressing Symmetry Breaking in DRAT Proofs

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

### Ramsey number four

CNF formula

DRAT proof (bubble sort)

DRAT proof (Batcher's Merge-Exchange)

### Erdos Discrepancy Conjecture

CNF formula

DRAT proof

DRAT proof (trimmed)

### Two-Pigeons-Per-Hole

6: CNF formula DRAT proof optimized DRAT proof

7: CNF formula DRAT proof optimized DRAT proof

8: CNF formula DRAT proof optimized DRAT proof

9: CNF formula DRAT proof optimized DRAT proof

10: CNF formula DRAT proof optimized DRAT proof

11: CNF formula DRAT proof (zipped) optimized DRAT proof

12: CNF formula DRAT proof (zipped) optimized DRAT proof

### Proof checking tools

DRAT-trim, visit the homepage for download and usage.

The zip file containing the files used to verify DRAT proofs in ACL2.