In one-stable-matching/: Proof of Theorem 3.

glucose-model.cnf and lingeling-model.cnf are exactly the same model,
but they were generated by different versions of our code, so the
ordering of the clauses and variables is different. We provide both
so that the glucose and lingeling runs could be reproduced exactly.

In two-stable-matchings/: Proof of Theorem 4.

Here, we used the same CNF file for glucose and lingeling. Note that
the output of glucose is truncated because the original file is 459 MB.
We provide the first 1000 lines and the last 1000.

