Table 1 Performance of (S)equential, (P)arallel, and (C)loud solvers in terms of solved instances (#), also divided in satisfiable and unsatisfiable instances, and PAR-2 score, i.e., the arithmetic mean running time where timeouts are counted as solved in twice the time limit

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