The collection of formulas used for the experimental evaluation in "How to discover short, shorter, and the shortest proofs of unsatisfiability: a branch-and-bound approach for resolution proof length minimization." Directory structure: full: synthetic formulas, including the random 3-CNFs, random graph coloring, and SMUs from Peitl & Szeider (2021). small and small-opt: collections with the same structure but smaller and without the SMUs; small-opt additionally excludes everything except 3-CNFs. proofmin-sat-competition-2002: a subset of unsatisfiable SAT Competition 2002 formulas solved within 15 seconds with an addition of their subsets produced by MUSer2.