| Prover | Thm% | CoS% | Uniq | ST⌀ | STΣ | Thm | CoS | Maybe | Empty | Err | Found |
|---|
| 2013-11-28-emptye | 49.509 | 0.000 | 9 | 0.047 | 47.46 | 1008 | 0 | 1028 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-100+named.txte | 45.874 | 0.000 | 2 | 0.026 | 24.45 | 934 | 0 | 1102 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-5+named.txte | 45.678 | 0.000 | 0 | 0.022 | 20.17 | 930 | 0 | 1106 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r1.5-1+named.txte | 45.236 | 0.000 | 1 | 0.023 | 21.11 | 921 | 0 | 1115 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r0.5-1+named.txte | 45.088 | 0.000 | 2 | 0.025 | 23.10 | 918 | 0 | 1118 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5.txte | 44.990 | 0.000 | 0 | 0.021 | 18.90 | 916 | 0 | 1120 | 0 | 0 | 2036 |
| 2013-11-30-pagerank-r1.5.txte | 44.941 | 0.000 | 0 | 0.020 | 18.47 | 915 | 0 | 1121 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-r1.5.txte | 44.941 | 0.000 | 0 | 0.021 | 18.87 | 915 | 0 | 1121 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-10+named.txte | 44.794 | 0.000 | 0 | 0.022 | 19.79 | 912 | 0 | 1124 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r1-1+named.txte | 44.597 | 0.000 | 0 | 0.020 | 18.08 | 908 | 0 | 1128 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-2+named.txte | 44.597 | 0.000 | 0 | 0.021 | 18.79 | 908 | 0 | 1128 | 0 | 0 | 2036 |
| 2013-12-06-PRonly-r1+named.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-PRonly-r1.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-initial-r1-1+named.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-initial-r1-1.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-initial2-r1-1+named.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-initial2-r1-1.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-pagerank-r1+named.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-06-pagerank-r1.txte | 44.548 | 0.000 | 0 | 0.018 | 16.55 | 907 | 0 | 1129 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5+named.txte | 44.008 | 0.000 | 2 | 0.024 | 21.16 | 896 | 0 | 1140 | 0 | 0 | 2036 |
| 2013-11-28-initial-r1.0-1.txte | 43.320 | 0.000 | 3 | 0.025 | 21.64 | 882 | 0 | 1154 | 0 | 0 | 2036 |
| 2013-11-30-pagerank-r1.0.txte | 43.124 | 0.000 | 1 | 0.021 | 18.67 | 878 | 0 | 1158 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.txte | 43.124 | 0.000 | 1 | 0.022 | 18.91 | 878 | 0 | 1158 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1+named.txte | 42.927 | 0.000 | 1 | 0.022 | 18.85 | 874 | 0 | 1162 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5+named.txte | 42.436 | 0.000 | 1 | 0.024 | 20.70 | 864 | 0 | 1172 | 0 | 0 | 2036 |
| 2013-11-30-pagerank-r0.5.txte | 42.387 | 0.000 | 0 | 0.021 | 18.48 | 863 | 0 | 1173 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.5.txte | 42.289 | 0.000 | 1 | 0.021 | 17.68 | 861 | 0 | 1175 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5.txte | 42.043 | 0.000 | 0 | 0.021 | 17.73 | 856 | 0 | 1180 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-r0.5.txte | 41.994 | 0.000 | 0 | 0.020 | 17.51 | 855 | 0 | 1181 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r0.5.txte | 41.306 | 0.000 | 1 | 0.024 | 20.11 | 841 | 0 | 1195 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.txte | 40.570 | 0.000 | 0 | 0.020 | 16.79 | 826 | 0 | 1210 | 0 | 0 | 2036 |
| 2013-11-28-emptyv | 37.426 | 0.000 | 4 | 0.031 | 23.93 | 762 | 0 | 1274 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-5+named.txtv | 34.921 | 0.000 | 0 | 0.015 | 10.73 | 711 | 0 | 1325 | 0 | 0 | 2036 |
| 2013-11-28-emptyz | 34.725 | 0.000 | 12 | 0.052 | 37.10 | 707 | 0 | 0 | 1329 | 0 | 2036 |
| 2013-12-06-PRonly-r1+named.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-PRonly-r1.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-initial-r1-1+named.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-initial-r1-1.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-initial2-r1-1+named.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-initial2-r1-1.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-pagerank-r1+named.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-06-pagerank-r1.txtv | 34.578 | 0.000 | 0 | 0.014 | 9.76 | 704 | 0 | 1332 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r1.5-1+named.txtv | 34.528 | 0.000 | 0 | 0.014 | 9.91 | 703 | 0 | 1333 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-10+named.txtv | 34.479 | 0.000 | 0 | 0.016 | 10.93 | 702 | 0 | 1334 | 0 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-2+named.txtv | 34.381 | 0.000 | 0 | 0.014 | 10.15 | 700 | 0 | 1336 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r0.5-1+named.txtv | 34.136 | 0.000 | 0 | 0.014 | 9.63 | 695 | 0 | 1341 | 0 | 0 | 2036 |
| 2013-12-08-initial2-r1-1+named.txtv | 34.037 | 0.000 | 0 | 0.014 | 9.58 | 693 | 0 | 1340 | 3 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-100+named.txtv | 33.448 | 0.000 | 0 | 0.017 | 11.44 | 681 | 0 | 1355 | 0 | 0 | 2036 |
| 2013-11-28-initial-r1.0-1.txtv | 33.251 | 0.000 | 2 | 0.019 | 13.03 | 677 | 0 | 1359 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5+named.txtv | 33.251 | 0.000 | 0 | 0.015 | 10.40 | 677 | 0 | 1359 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5+named.txtv | 33.006 | 0.000 | 1 | 0.017 | 11.61 | 672 | 0 | 1364 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-r1.5.txtv | 32.613 | 0.000 | 0 | 0.014 | 9.56 | 664 | 0 | 1371 | 1 | 0 | 2036 |
| 2013-11-30-pagerank-r1.5.txtv | 32.564 | 0.000 | 0 | 0.014 | 9.55 | 663 | 0 | 1373 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5.txtv | 32.564 | 0.000 | 0 | 0.014 | 9.54 | 663 | 0 | 1373 | 0 | 0 | 2036 |
| 2013-12-02-pagerank-r1.txtv | 32.367 | 0.000 | 0 | 0.016 | 10.23 | 659 | 0 | 1371 | 6 | 0 | 2036 |
| 2013-12-02-pagerank-r1+named.txtv | 32.318 | 0.000 | 0 | 0.014 | 9.43 | 658 | 0 | 1372 | 6 | 0 | 2036 |
| 2013-11-30-pagerank-r1.0.txtv | 32.220 | 0.000 | 0 | 0.015 | 10.14 | 656 | 0 | 1374 | 6 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5.txtv | 30.992 | 0.000 | 0 | 0.014 | 8.87 | 631 | 0 | 1405 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-r0.5.txtv | 30.992 | 0.000 | 0 | 0.014 | 8.86 | 631 | 0 | 1404 | 1 | 0 | 2036 |
| 2013-11-30-pagerank-r0.5.txtv | 30.894 | 0.000 | 0 | 0.014 | 8.87 | 629 | 0 | 1407 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.txtv | 30.599 | 0.000 | 1 | 0.016 | 10.02 | 623 | 0 | 1412 | 1 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.5.txtv | 30.501 | 0.000 | 0 | 0.015 | 9.17 | 621 | 0 | 1415 | 0 | 0 | 2036 |
| 2013-12-08-pagerank-r1.5.txtz | 30.059 | 0.000 | 0 | 0.019 | 11.62 | 612 | 0 | 0 | 1424 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5.txtz | 30.010 | 0.000 | 0 | 0.019 | 11.60 | 611 | 0 | 0 | 1425 | 0 | 2036 |
| 2013-11-30-pagerank-r1.5.txtz | 29.912 | 0.000 | 0 | 0.019 | 11.58 | 609 | 0 | 0 | 1427 | 0 | 2036 |
| 2013-12-08-initial2-r1.5-1+named.txtz | 29.715 | 0.000 | 0 | 0.017 | 10.43 | 605 | 0 | 0 | 1431 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-2+named.txtz | 29.470 | 0.000 | 0 | 0.017 | 10.30 | 600 | 0 | 0 | 1436 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-5+named.txtz | 29.420 | 0.000 | 0 | 0.018 | 10.60 | 599 | 0 | 0 | 1437 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r0.5.txtv | 29.322 | 0.000 | 0 | 0.014 | 8.61 | 597 | 0 | 1435 | 4 | 0 | 2036 |
| 2013-12-08-initial2-r1-1+named.txtz | 29.273 | 0.000 | 0 | 0.017 | 10.22 | 596 | 0 | 0 | 1440 | 0 | 2036 |
| 2013-12-08-initial2-r0.5-1+named.txtz | 28.733 | 0.000 | 0 | 0.015 | 8.58 | 585 | 0 | 0 | 1451 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5+named.txtz | 28.684 | 0.000 | 3 | 0.025 | 14.61 | 584 | 0 | 0 | 1452 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-10+named.txtz | 28.389 | 0.000 | 0 | 0.018 | 10.34 | 578 | 0 | 0 | 1458 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.5.txtz | 28.045 | 0.000 | 0 | 0.015 | 8.72 | 571 | 0 | 0 | 1465 | 0 | 2036 |
| 2013-11-30-pagerank-r1.0.txtz | 27.750 | 0.000 | 0 | 0.018 | 9.98 | 565 | 0 | 0 | 1471 | 0 | 2036 |
| 2013-12-02-pagerank-r1.txtz | 27.750 | 0.000 | 0 | 0.018 | 9.96 | 565 | 0 | 0 | 1471 | 0 | 2036 |
| 2013-12-02-pagerank-r0.5.txtz | 27.701 | 0.000 | 0 | 0.016 | 8.75 | 564 | 0 | 0 | 1472 | 0 | 2036 |
| 2013-11-30-pagerank-r0.5.txtz | 27.652 | 0.000 | 0 | 0.016 | 8.79 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-PRonly-r1+named.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-PRonly-r1.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-initial-r1-1+named.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-initial-r1-1.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-initial2-r1-1+named.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-initial2-r1-1.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-pagerank-r1+named.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-06-pagerank-r1.txtz | 27.652 | 0.000 | 0 | 0.013 | 7.30 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-08-pagerank-r0.5.txtz | 27.652 | 0.000 | 0 | 0.016 | 8.74 | 563 | 0 | 0 | 1473 | 0 | 2036 |
| 2013-12-02-pagerank-r1.5+named.txtz | 27.161 | 0.000 | 1 | 0.018 | 9.73 | 553 | 0 | 0 | 1483 | 0 | 2036 |
| 2013-11-28-initial-r1.0-1.txtz | 26.817 | 0.000 | 1 | 0.017 | 9.38 | 546 | 0 | 0 | 1490 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r0.5.txtz | 26.228 | 0.000 | 0 | 0.015 | 8.16 | 534 | 0 | 0 | 1502 | 0 | 2036 |
| 2013-12-11-initial2-r1.5-100+named.txtz | 25.196 | 0.000 | 0 | 0.016 | 8.11 | 513 | 0 | 0 | 1523 | 0 | 2036 |
| 2013-12-02-pagerank-r1+named.txtz | 25.147 | 0.000 | 0 | 0.015 | 7.68 | 512 | 0 | 0 | 1524 | 0 | 2036 |
| 2013-12-08-pagerank-no-S-r1.txtz | 24.165 | 0.000 | 1 | 0.017 | 8.56 | 492 | 0 | 0 | 1544 | 0 | 2036 |
| 61.100 | 0.000 | | | | 1244 | 0 | | | | 2036 |
| Prover | Sum% | Sum | G+2 | G1+2 | G-1+2 | G+2M | Alt |
| 2013-11-28-emptye | 49.509 | 1008 | | 1008 | | 1008 | |
| 2013-12-08-initial2-r1.5-1+named.txte | 52.996 | 1079 | 1079 | | 1079 | 1079 | |
| 2013-11-28-emptyz | 55.354 | 1127 | | 1127 | 1127 | 1127 | |
| 2013-12-02-pagerank-r1.5+named.txte | 56.483 | 1150 | 1150 | | 1150 | 1150 | |
| 2013-12-02-pagerank-r0.5.txte | 57.171 | 1164 | | 1164 | 1164 | 1164 | = 2013-12-08-pagerank-r0.5.txte = 2013-11-30-pagerank-r0.5.txte |
| 2013-12-02-pagerank-r0.5+named.txtz | 57.711 | 1175 | 1175 | | 1175 | 1175 | |
| 2013-12-02-pagerank-r1+named.txte | 58.104 | 1183 | | 1183 | 1183 | 1183 | = 2013-12-08-initial2-r0.5-1+named.txte |
| 2013-12-08-initial2-r0.5-1+named.txte | 58.497 | 1191 | 1191 | | 1191 | 1191 | |
| 2013-11-28-emptyv | 58.841 | 1198 | | 1198 | 1198 | 1198 | |
| 2013-11-28-initial-r1.0-1.txte | 59.136 | 1204 | 1204 | | 1204 | 1204 | |
| 2013-12-08-pagerank-r1.5.txtz | 59.381 | 1209 | | 1209 | 1209 | 1209 | = 2013-12-02-pagerank-r1.5.txtz = 2013-11-30-pagerank-r1.5.txtz = 2013-12-11-initial2-r1.5-100+named.txte |
| 2013-12-11-initial2-r1.5-100+named.txte | 59.627 | 1214 | 1214 | | 1214 | 1214 | |
| 2013-12-06-initial2-r1-1.txte | 59.774 | 1217 | | 1217 | 1217 | 1217 | = 2013-12-06-PRonly-r1+named.txte = 2013-12-02-pagerank-r1.txtv = 2013-12-06-initial-r1-1+named.txte = ... (11) |
| 2013-12-02-pagerank-r1.txtv | 59.921 | 1220 | 1220 | | 1220 | 1220 | = 2013-11-30-pagerank-r1.0.txtz = 2013-11-30-pagerank-r1.0.txtv = 2013-12-02-pagerank-r1.txtz |
| 2013-11-30-pagerank-r1.0.txtz | 60.069 | 1223 | | 1223 | 1223 | 1223 | = 2013-12-02-pagerank-r1.txtz |
| 2013-12-11-initial2-r1.5-10+named.txte | 60.167 | 1225 | 1225 | | 1226 | 1225 | = 2013-12-08-initial2-r1.5-1+named.txtz = 2013-12-02-pagerank-r1.txte = 2013-12-08-pagerank-no-S-r1.5.txte = ... (9) |
| 2013-12-08-initial2-r1.5-1+named.txtz | 60.265 | 1227 | | 1227 | 1228 | 1227 | = 2013-12-02-pagerank-r1.txte = 2013-12-08-pagerank-no-S-r1.5.txte = 2013-11-28-initial-r1.0-1.txtv = ... (7) |
| 2013-12-02-pagerank-r1.txte | 60.363 | 1229 | 1229 | | 1230 | 1229 | = 2013-12-08-pagerank-no-S-r1.5.txte = 2013-11-28-initial-r1.0-1.txtv = 2013-12-08-pagerank-no-S-r1.txtv = ... (5) |
| 2013-12-08-pagerank-no-S-r1.5.txte | 60.462 | 1231 | | 1231 | 1232 | 1231 | = 2013-11-28-initial-r1.0-1.txtv = 2013-12-08-pagerank-no-S-r1.txtv = 2013-12-08-pagerank-no-S-r0.5.txte |
| 2013-11-28-initial-r1.0-1.txtv | 60.560 | 1233 | 1233 | | 1233 | 1233 | |
| 2013-11-30-pagerank-r0.5.txtz | 60.609 | 1234 | | 1234 | 1234 | 1234 | = 2013-12-02-pagerank-r0.5+named.txtv = 2013-11-28-initial-r1.0-1.txtz = 2013-12-08-pagerank-no-S-r1.txtz = ... (21) |
| 2013-12-02-pagerank-r0.5+named.txtv | 60.658 | 1235 | 1235 | | 1235 | 1235 | = 2013-11-28-initial-r1.0-1.txtz = 2013-12-08-pagerank-no-S-r1.txtz = 2013-12-02-pagerank-r0.5+named.txte = ... (18) |
| 2013-11-28-initial-r1.0-1.txtz | 60.707 | 1236 | | 1236 | 1236 | 1236 | = 2013-12-08-pagerank-no-S-r1.txtz = 2013-12-02-pagerank-r0.5+named.txte = 2013-12-06-pagerank-r1.txtv = ... (17) |
| 2013-12-08-pagerank-no-S-r1.txtz | 60.756 | 1237 | 1237 | | 1237 | 1237 | = 2013-12-02-pagerank-r0.5+named.txte = 2013-12-06-pagerank-r1.txtv = 2013-12-06-pagerank-r1+named.txtv = ... (16) |
| 2013-12-02-pagerank-r0.5+named.txte | 60.806 | 1238 | | 1238 | 1238 | 1238 | = 2013-12-06-pagerank-r1.txtv = 2013-12-06-pagerank-r1+named.txtv = 2013-12-06-initial-r1-1+named.txtv = ... (15) |
| 2013-12-06-pagerank-r1.txtv | 60.855 | 1239 | 1239 | | 1239 | 1239 | = 2013-12-06-pagerank-r1+named.txtv = 2013-12-06-initial-r1-1+named.txtv = 2013-12-06-PRonly-r1+named.txtv = ... (14) |
| 2013-12-08-initial2-r1-1+named.txtz | 60.904 | 1240 | | 1240 | 1240 | 1240 | = 2013-12-08-pagerank-no-S-r1.txtv = 2013-12-11-initial2-r1.5-10+named.txtz = 2013-12-11-initial2-r1.5-5+named.txtz = ... (6) |
| 2013-12-08-pagerank-no-S-r1.txtv | 60.953 | 1241 | 1241 | | 1241 | 1241 | = 2013-12-02-pagerank-r1.5+named.txtz = 2013-12-08-pagerank-no-S-r0.5.txte = 2013-11-30-pagerank-r1.0.txte |
| 2013-12-02-pagerank-r1.5+named.txtz | 61.002 | 1242 | | 1242 | 1242 | 1242 | = 2013-12-08-pagerank-no-S-r0.5.txte = 2013-11-30-pagerank-r1.0.txte |
| 2013-12-08-pagerank-no-S-r0.5.txte | 61.051 | 1243 | 1243 | | 1243 | 1243 | = 2013-11-30-pagerank-r1.0.txte |
| 2013-11-30-pagerank-r1.0.txte | 61.100 | 1244 | | 1244 | 1244 | 1244 | |