Fig. 7
From: Producing Proofs of Unsatisfiability with Distributed Clause-Sharing SAT Solvers

Pure solving times (excluding proof assembly and checking times; higher is better), where “Best” denotes the currently best performing configuration of MallobSat and “Proof-like” is equivalent to our proof-producing configuration (“Proof”) except that LRAT output and proof production themselves are kept disabled. Proof-producing approaches are underlined