Table 7 Statistics on proof production and checking. Ratios are given as a multiple of the solving time. We list minima, maxima, medians, means, and the 10th and 90th percentiles—using the arithmetic mean for absolutes and the geometric mean for ratios

Ratio

1 node asm

138

0.014

0.111

0.395

0.438

1.941

7.026

1 node chk

138

0.010

0.051

0.422

0.367

1.849

6.534

1 node asm+chk

138

0.066

0.249

0.783

0.870

3.587

13.560

20 nodes asm

162

0.018

0.196

0.971

1.085

5.620

35.202

20 nodes chk

157

0.019

0.130

2.489

1.681

10.155

86.608

20 nodes asm+chk

157

0.148

0.412

3.584

2.906

15.872

121.810

38-c. Gims. checking

68

0.272

1.283

7.057

12.186

159.859

279.848

Absolute

1-node proof size (GB)

138

0.000

0.065

0.801

2.764

9.132

49.533

20-node proof size (GB)

163

0.000

0.214

3.126

11.645

30.957

233.880

38-c. Gims. proof size (GB)

110

0.000

0.191

0.702

1.784

5.029

10.804

1-node pruning factor

138

1.439

1.816

5.368

10.334

134.032

591.218

20-node pruning factor

162

1.884

5.375

28.366

36.377

400.098

7124.047