Proof of `Three Days and the Fairness Parameter One` (1st statement)
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The three dummies conflict with each other on all three days, so exactly one of them runs on each day; the first day then admits one client of every group, which is the assignment and one client of every clause, the second day is a dead end for everything but a client of a clause of three literals, and on the third day a client of an occurrence conflicts with exactly the variable client that falsifies its literal.