Fig. 4
From: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
Left: Proof merging with seven processes and 14 solvers. Each box represents a process with two local proof sources. Dashed arrows denote communication. Right: Example of merging three streams of LRAT lines into a single stream. Each number i represents an LRAT line describing a clause of ID i