Fig. 6
From: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers
Overhead of proof-related stages (assembly, postprocessing, checking, and overall) relative to solving time, for MallobSatP64 with parallel proof production (left) and for MallobSatP1600 (right). Note the logarithmic scaling