| Str | Args | Cluster | Add | Prems | Prover | Thm% | CoS% | Uniq | ST⌀ | STΣ | Thm | CoS | Maybe | Empty | Err | Found |
|---|
| seq | d_u_div_exps | 0 | * | * | * | 30.791 | 0.000 | 3 | 0.088 | 48.39 | 553 | 0 | 1242 | 1 | | 1796 |
| seq | d_u_div_s | 0 | * | * | * | 30.735 | 0.000 | 5 | 0.096 | 53.12 | 552 | 0 | 1242 | 2 | | 1796 |
| pgrank | u_div_s | 0 | * | * | * | 30.624 | 0.000 | 6 | 0.099 | 54.44 | 550 | 0 | 1214 | 32 | | 1796 |
| seq | d_u_div_s2 | 0 | * | * | * | 30.512 | 0.000 | 3 | 0.086 | 47.37 | 548 | 0 | 1246 | 2 | | 1796 |
| pgrank | du_div_s | 0 | * | * | * | 30.290 | 0.000 | 2 | 0.086 | 46.99 | 544 | 0 | 1245 | 7 | | 1796 |
| maxcut | default | 0 | * | * | * | 30.178 | 0.000 | 1 | 0.082 | 44.40 | 542 | 0 | 1251 | 3 | | 1796 |
| pgrank | u | 0 | * | * | * | 30.122 | 0.000 | 9 | 0.105 | 56.84 | 541 | 0 | 1254 | 1 | | 1796 |
| seq | d2_div_s | 0 | * | * | * | 29.955 | 0.000 | 6 | 0.091 | 49.01 | 538 | 0 | 1258 | 0 | | 1796 |
| epcl | default | 0 | * | * | * | 29.677 | 0.000 | 0 | 0.081 | 43.34 | 533 | 0 | 1262 | 1 | | 1796 |
| pgrank | du | 0 | * | * | * | 29.454 | 0.000 | 3 | 0.084 | 44.50 | 529 | 0 | 1266 | 1 | | 1796 |
| pgrank | d_div_s | 0 | * | * | * | 29.120 | 0.000 | 5 | 0.095 | 49.68 | 523 | 0 | 1244 | 29 | | 1796 |
| default | default | 0 | * | * | * | 28.786 | 0.000 | 1 | 0.079 | 41.01 | 517 | 0 | 1279 | 0 | | 1796 |
| pgrank | d | 0 | * | * | * | 27.728 | 0.000 | 4 | 0.089 | 44.17 | 498 | 0 | 1280 | 18 | | 1796 |
| seq | u2_div_s | 0 | * | * | * | 27.339 | 0.000 | 9 | 0.100 | 49.01 | 491 | 0 | 1299 | 6 | | 1796 |
| all | default | 0 | * | * | * | 21.047 | 0.000 | 26 | 0.161 | 60.74 | 378 | 0 | 1346 | 72 | | 1796 |
| any | | | | | | 40.813 | 0.000 | | | | 733 | 0 | | | | 1796 |
Greedy sequence
| Prover | Sum% | Sum | G+2 | G1+2 | G-1+2 | G+2M | Alt |
| seq-d_u_div_exps-0-*-*-* | 30.791 | 553 | | | | | |
| all-default-0-*-*-* | 33.964 | 610 | | | | | |
| pgrank-u-0-*-*-* | 36.303 | 652 | | | | | |
| seq-d_u_div_s-0-*-*-* | 37.639 | 676 | | | | | |
| pgrank-d_div_s-0-*-*-* | 38.530 | 692 | | | | | |
| seq-u2_div_s-0-*-*-* | 39.198 | 704 | | | | | |
| pgrank-u_div_s-0-*-*-* | 39.644 | 712 | | | | | |
| seq-d2_div_s-0-*-*-* | 39.978 | 718 | | | | | |
| pgrank-d-0-*-*-* | 40.200 | 722 | | | | | = pgrank-du-0-*-*-* |
| pgrank-du-0-*-*-* | 40.423 | 726 | | | | | |
| seq-d_u_div_s2-0-*-*-* | 40.590 | 729 | | | | | |
| pgrank-du_div_s-0-*-*-* | 40.702 | 731 | | | | | |
| default-default-0-*-*-* | 40.757 | 732 | | | | | = maxcut-default-0-*-*-* |
| maxcut-default-0-*-*-* | 40.813 | 733 | | | | | |