The two halves of the paper's Section 4. From a satisfying assignment, $lemma3$ builds the schedule: each variable job goes on the machine opposing its value, freeing the agreeing machine for the selected literal of every clause that variable satisfies, and the remaining jobs of a clause are distributed over its own three machines by the transposition exchanging the selected literal with the first.

Conversely $lemma4$ reads the assignment off a schedule. $observation4$ first shows that the two wrapper jobs of each literal share a machine — all three wrappers of one side pairwise overlap, so they are spread bijectively over the clause's machines, and the evenness of the deadlines forces that bijection to be the identity. Machine $0$ of the clause is then blocked for two literals, and the third literal job has nowhere to go but its variable machine, which pins the variable job to the opposite one.