Table 2 Statistics on proof production and checking, considering a prior DRAT-based approach [27] (64 threads), our approach at 64 threads with sequential (Seq.) and parallel (Par.) proof production, and our approach at the cloud scale (Cld., 1600 threads)

DRAT check

81

0.512

1.725

7.442

10.370

67.065

169.869

Seq. assembly

139

0.019

0.305

1.376

1.387

5.747

13.289

Seq. postprocessing

139

0.001

0.012

0.131

0.112

0.790

2.218

Seq. checking

139

0.007

0.043

0.572

0.469

3.970

10.980

Seq. asm+post+chk

139

0.037

0.412

2.110

2.129

10.834

26.487

Par. assembly

135

0.059

0.080

0.365

0.408

2.227

7.475

Par. postprocessing

135

0.001

0.016

0.156

0.128

0.861

2.300

Par. checking

135

0.007

0.042

0.622

0.471

3.540

11.645

Par. asm+post+chk

135

0.067

0.167

1.097

1.062

6.611

21.420

Cld. assembly

157

0.121

0.194

1.680

1.204

5.348

43.853

Cld. postprocessing

157

0.003

0.051

0.744

0.634

4.744

35.667

Cld. checking

157

0.032

0.215

3.391

2.499

21.908

135.737

Cld. asm+post+chk

157

0.162

0.579

5.174

4.819

31.968

215.257

DRAT proof size (GB)

139

0.012

0.366

1.236

3.246

8.395

29.308

Seq. proof size (GB)

139

0.016

0.223

2.379

5.384

16.082

46.986

Par. proof size (GB)

135

0.006

0.173

2.034

5.345

13.164

57.739

Cld. proof size (GB)

157

0.016

0.269

4.595

11.138

34.457

92.276

Cld. pruning factor

157

2.080

5.312

16.472

28.319

299.858

8415.070