| Filter | Option | Prover | Version | Thm% | CoS% | Uniq | ST⌀ | STΣ | Thm | CoS | Maybe | Empty | Err | Found |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| * | * | all | * | 62.993 | 25.265 | 6 | 0.076 | 138.96 | 1309 | 525 | 244 | 0 | 2078 | |
| * | * | ag0 | * | 62.223 | 20.645 | 5 | 0.077 | 133.09 | 1293 | 429 | 356 | 0 | 2078 | |
| * | * | nmu | * | 62.127 | 22.281 | 3 | 0.074 | 130.36 | 1291 | 463 | 324 | 0 | 2078 | |
| * | * | pla | * | 61.501 | 21.944 | 2 | 0.073 | 127.16 | 1278 | 456 | 344 | 0 | 2078 | |
| * | * | pgr | * | 61.261 | 22.810 | 8 | 0.075 | 130.71 | 1273 | 474 | 331 | 0 | 2078 | |
| * | * | ag5 | * | 61.116 | 19.153 | 1 | 0.075 | 124.81 | 1270 | 398 | 410 | 0 | 2078 | |
| * | * | red | * | 60.250 | 20.404 | 0 | 0.072 | 120.77 | 1252 | 424 | 402 | 0 | 2078 | |
| * | * | plr | * | 59.769 | 17.613 | 3 | 0.075 | 120.09 | 1242 | 366 | 470 | 0 | 2078 | |
| * | * | neg | * | 59.721 | 19.682 | 1 | 0.072 | 119.29 | 1241 | 409 | 428 | 0 | 2078 | |
| * | * | mom | * | 58.807 | 17.324 | 1 | 0.073 | 115.65 | 1222 | 360 | 496 | 0 | 2078 | |
| * | * | non | * | 58.566 | 16.987 | 0 | 0.073 | 114.12 | 1217 | 353 | 508 | 0 | 2078 | |
| any | 66.169 | 31.328 | 1375 | 651 | 2078 |
| Prover | Sum% | Sum | G+2 | G1+2 | G-1+2 | G+2M | Alt |
| eval-*-*-all-* | 62.993 | 1309 | |||||
| eval-*-*-ag0-* | 64.581 | 1342 | |||||
| eval-*-*-pgr-* | 65.351 | 1358 | |||||
| eval-*-*-pla-* | 65.592 | 1363 | |||||
| eval-*-*-plr-* | 65.784 | 1367 | |||||
| eval-*-*-nmu-* | 65.929 | 1370 | |||||
| eval-*-*-red-* | 66.025 | 1372 | = eval-*-*-neg-* = eval-*-*-ag5-* | ||||
| eval-*-*-neg-* | 66.073 | 1373 | = eval-*-*-ag5-* = eval-*-*-mom-* | ||||
| eval-*-*-ag5-* | 66.121 | 1374 | = eval-*-*-mom-* | ||||
| eval-*-*-mom-* | 66.169 | 1375 |