Weekly benchmark · latest branches

Lean 4 tactic benchmark

9 tactics compared across 12 theorem suites. Each tactic runs in its own isolated Lake project on its latest branch and that branch's Lean toolchain; every column shows the toolchain and commit it ran on.

toolchains v4.24.0 – v4.35.0 · 9 tactics · 12 suites

Changes compared with the 2026-10-19 run. Only unchanged statements count as gains or losses; new goals have no baseline.

Overview

Home turf · each source is its own category

Aesop
Aesop test goals
50 theorems
best hammer 47/50 (94%)
lean-auto
lean-auto regression and translation goals
50 theorems
best auto 46/50 (92%)
Blaster
Lean-blaster regression and SMT goals
50 theorems
best hammer 48/50 (96%)
LeanHammer + Duper
LeanHammer smoke test and Duper dependency tests
50 theorems
best hammer 45/50 (90%)
lean-smt
lean-smt logic, arithmetic, and bitvector tests
50 theorems
best hammer 47/50 (94%)

Shared benchmarks

ITL4
Introduction to Logic
44 theorems
best blaster 44/44 (100%)
MiniF2F
Competition math (integer/number-theory subset)
96 theorems
best blaster 54/96 (56%)
NNG4
Lean Natural Number Game
108 theorems
best blaster 103/108 (95%)
STG4
Lean Set Theory Game
52 theorems
best blaster 49/52 (94%)
UPLCDepth
UPLC concrete evaluation (growing computation)
7 theorems
best aesop 7/7 (100%)
UPLCWidth
UPLC symbolic correctness (growing expressions)
6 theorems
best blaster 6/6 (100%)
Verina
Verified-programming specs (Verina, basic)
108 theorems
best blaster 26/108 (24%)

Overall standing

#tacticsolvedsince last runshare solved
1hammer486/671 (72%)no change 250 new
2blaster477/671 (71%)no change 250 new
3grind409/671 (61%)no change 250 new
4auto378/671 (56%)no change 250 new
5aesop377/671 (56%)no change 250 new
6blaster (only-optimize: 1)252/671 (38%)no change 250 new
7simp164/671 (24%)no change 250 new
8smt +model114/671 (17%)no change 250 new
9omega80/671 (12%)no change 250 new

Versions run

tacticbranchtoolchaincommitbuild
blastermainleanprover/lean4:v4.24.0b729d1014OK
blaster (only-optimize: 1)mainleanprover/lean4:v4.24.0b729d1014OK
smt +modelmainleanprover/lean4:v4.34.079ef7b3d5OK
automainleanprover/lean4:v4.34.16544cf60eOK
aesopstableleanprover/lean4:v4.35.0(via mathlib)OK
hammermainleanprover/lean4:v4.34.093734d624OK
omegastableleanprover/lean4:v4.35.0(core)OK
grindstableleanprover/lean4:v4.35.0(core)OK
simpstableleanprover/lean4:v4.35.0(core)OK

Suite details

Home turf categories

Aesop · 50 theorems

Aesop test goals

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster28/50 (56%)50 new goals
3019
blaster (only-optimize: 1)10/50 (20%)50 new goals
0040
smt +model5/50 (10%)50 new goals
0045
auto28/50 (56%)50 new goals
0022
aesop40/50 (80%)50 new goals
0010
hammer47/50 (94%)50 new goals
003
omega6/50 (12%)50 new goals
0044
grind44/50 (88%)50 new goals
006
simp13/50 (26%)50 new goals
0037
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
aesop_l43 ✓ 1613 ms ✓ 1629 ms ✓ 2194 ms ✓ 1364 ms ✓ 1154 ms ✓ 2665 ms ✓ 771 ms ✓ 803 ms ✓ 775 ms
aesop_l80 ✓ 1748 ms ✗ FAIL ✗ FAIL ✓ 1367 ms ✓ 1189 ms ✓ 2735 ms ✗ FAIL ✓ 774 ms ✗ FAIL
auxdecl_l32 ✗ FAIL ✗ FAIL ✓ 2258 ms ✓ 1408 ms ✗ FAIL ✓ 3025 ms ✗ FAIL ✓ 800 ms ✗ FAIL
bigstep_l62 ✓ 1671 ms ✗ FAIL ✗ FAIL ✓ 1385 ms ✗ FAIL ✓ 3241 ms ✗ FAIL ✓ 767 ms ✗ FAIL
case_10_l12 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1194 ms ✓ 2662 ms ✗ FAIL ✓ 787 ms ✗ FAIL
case_126_l9 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1194 ms ✓ 2821 ms ✗ FAIL ✓ 782 ms ✗ FAIL
constructorequations_l14 ✓ 1713 ms ✓ 1627 ms ✗ FAIL ✓ 1381 ms ✓ 1295 ms ✓ 2759 ms ✗ FAIL ✓ 768 ms ✗ FAIL
constructorequations_l17 ✓ 1607 ms ✓ 1628 ms ✗ FAIL ✓ 1386 ms ✓ 1192 ms ✓ 2813 ms ✗ FAIL ✓ 771 ms ✗ FAIL
constructorequations_l20 ✓ 1703 ms ✗ FAIL ✗ FAIL ✓ 1357 ms ✓ 1161 ms ✓ 2836 ms ✗ FAIL ✓ 775 ms ✗ FAIL
destructproducts_l48 ✓ 1634 ms ✓ 1599 ms ✗ FAIL ✓ 1354 ms ✓ 1163 ms ✓ 2703 ms ✗ FAIL ✓ 765 ms ✗ FAIL
equality_chain ✓ 1678 ms ✗ FAIL ✗ FAIL ✓ 1348 ms ✓ 1195 ms ✓ 2710 ms ✗ FAIL ✓ 770 ms ✗ FAIL
erasesimp_l12 ✓ 1614 ms ✓ 1664 ms ✓ 2242 ms ✓ 1404 ms ✗ FAIL ✓ 2785 ms ✓ 775 ms ✓ 767 ms ✗ FAIL
ext_l12 ✓ 1692 ms ✗ FAIL ✗ FAIL ✓ 1447 ms ✓ 1171 ms ✓ 2864 ms ✗ FAIL ✓ 782 ms ✗ FAIL
ext_l9 ✓ 1702 ms ✗ FAIL ✗ FAIL ✓ 1436 ms ✓ 1225 ms ✓ 2688 ms ✗ FAIL ✓ 770 ms ✗ FAIL
indent_l13 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
list_l194 ✓ 1652 ms ✓ 1627 ms ✗ FAIL ✓ 1413 ms ✓ 1183 ms ✓ 2730 ms ✗ FAIL ✓ 773 ms ✓ 767 ms
list_l198 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1200 ms ✓ 2707 ms ✗ FAIL ✗ FAIL ✓ 771 ms
list_l202 ✓ 1682 ms ✗ FAIL ✗ FAIL ✓ 1377 ms ✓ 1190 ms ✓ 2787 ms ✗ FAIL ✓ 767 ms ✗ FAIL
list_l207 ✓ 1694 ms ✗ FAIL ✗ FAIL ✓ 1390 ms ✓ 1219 ms ✓ 2745 ms ✗ FAIL ✓ 781 ms ✓ 769 ms
list_l215 ✓ 1765 ms ✗ FAIL ✗ FAIL ✓ 1420 ms ✓ 1176 ms ✓ 2694 ms ✗ FAIL ✓ 768 ms ✓ 766 ms
list_l219 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
list_l231 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1239 ms ✓ 2851 ms ✗ FAIL ✓ 772 ms ✓ 784 ms
list_l235 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1194 ms ✓ 2727 ms ✗ FAIL ✓ 769 ms ✓ 765 ms
list_l239 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1231 ms ✓ 2709 ms ✗ FAIL ✓ 774 ms ✓ 766 ms
list_l243 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1184 ms ✓ 2808 ms ✗ FAIL ✓ 767 ms ✗ FAIL
list_l253 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3025 ms ✗ FAIL ✓ 766 ms ✗ FAIL
list_l258 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1231 ms ✓ 2781 ms ✗ FAIL ✓ 766 ms ✗ FAIL
list_l262 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1259 ms ✓ 2838 ms ✗ FAIL ✓ 770 ms ✗ FAIL
list_l270 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1254 ms ✓ 2845 ms ✗ FAIL ✓ 766 ms ✗ FAIL
list_l274 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1211 ms ✓ 2832 ms ✗ FAIL ✓ 769 ms ✗ FAIL
list_l278 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1167 ms ✓ 2697 ms ✗ FAIL ✓ 770 ms ✓ 809 ms
list_l282 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1216 ms ✓ 2842 ms ✗ FAIL ✓ 781 ms ✗ FAIL
list_l286 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1203 ms ✓ 2863 ms ✗ FAIL ✓ 769 ms ✓ 771 ms
list_l411 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
list_l89 ✓ 1619 ms ✓ 1681 ms ✗ FAIL ✓ 1496 ms ✓ 1247 ms ✓ 2778 ms ✗ FAIL ✗ FAIL ✓ 765 ms
list_l93 ✓ 1655 ms ✓ 1638 ms ✗ FAIL ✗ FAIL ✓ 1227 ms ✓ 2779 ms ✗ FAIL ✓ 763 ms ✓ 767 ms
metas_l14 ✓ 1680 ms ✗ FAIL ✗ FAIL ✓ 1467 ms ✓ 1216 ms ✓ 2964 ms ✗ FAIL ✓ 771 ms ✗ FAIL
metas_l23 ✓ 1688 ms ✗ FAIL ✗ FAIL ✓ 1448 ms ✓ 1302 ms ✓ 2859 ms ✗ FAIL ✓ 824 ms ✗ FAIL
metas_l26 ✓ 1715 ms ✗ FAIL ✗ FAIL ✓ 1470 ms ✓ 1323 ms ✓ 2898 ms ✗ FAIL ✓ 899 ms ✗ FAIL
metas_l34 ✓ 1736 ms ✗ FAIL ✗ FAIL ✓ 1436 ms ✓ 1347 ms ✓ 2881 ms ✗ FAIL ✓ 775 ms ✗ FAIL
mvarsininitialgoal_l11 ✓ 1669 ms ✗ FAIL ✗ FAIL ✓ 1446 ms ✗ FAIL ✓ 2799 ms ✓ 773 ms ✓ 824 ms ✗ FAIL
nonormsimp_l19 ✓ 1626 ms ✓ 1636 ms ✓ 2208 ms ✓ 1428 ms ✓ 1267 ms ✓ 2726 ms ✓ 777 ms ✓ 766 ms ✓ 771 ms
relation_chain ✓ 1722 ms ✗ FAIL ✗ FAIL ✓ 1418 ms ✓ 1294 ms ✓ 2901 ms ✗ FAIL ✓ 774 ms ✗ FAIL
seqcalcprover_l27 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1253 ms ✓ 2685 ms ✗ FAIL ✓ 774 ms ✗ FAIL
seqcalcprover_l30 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2699 ms ✗ FAIL ✗ FAIL ✗ FAIL
subst_l49 ✓ 1613 ms ✓ 1620 ms ✗ FAIL ✓ 1454 ms ✓ 1214 ms ✓ 2740 ms ✓ 771 ms ✓ 765 ms ✗ FAIL
subst_l81 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1203 ms ✓ 2716 ms ✗ FAIL ✓ 764 ms ✗ FAIL
tacgen_l6 ✓ 1701 ms ✗ FAIL ✓ 2181 ms ✓ 1441 ms ✗ FAIL ✓ 3360 ms ✓ 775 ms ✓ 788 ms ✗ FAIL
tauto_l12 ✓ 1701 ms ✗ FAIL ✗ FAIL ✓ 1495 ms ✓ 1396 ms ✓ 2963 ms ✗ FAIL ✓ 782 ms ✗ FAIL
witness ✓ 1688 ms ✗ FAIL ✗ FAIL ✓ 1441 ms ✓ 1248 ms ✓ 2802 ms ✗ FAIL ✓ 762 ms ✗ FAIL

lean-auto · 50 theorems

lean-auto regression and translation goals

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster36/50 (72%)50 new goals
1013
blaster (only-optimize: 1)23/50 (46%)50 new goals
0027
smt +model14/50 (28%)50 new goals
0036
auto46/50 (92%)50 new goals
004
aesop40/50 (80%)50 new goals
0010
hammer46/50 (92%)50 new goals
004
omega12/50 (24%)50 new goals
0038
grind38/50 (76%)50 new goals
0012
simp25/50 (50%)50 new goals
0025
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
add_reorder ✓ 1695 ms ✗ FAIL ✓ 2246 ms ✓ 1394 ms ✗ FAIL ✓ 3810 ms ✓ 773 ms ✓ 774 ms ✗ FAIL
excluded_middle_variant ✓ 1783 ms ✗ FAIL ✓ 2190 ms ✓ 1418 ms ✗ FAIL ✓ 2971 ms ✗ FAIL ✓ 763 ms ✗ FAIL
nested_identity ✓ 1775 ms ✗ FAIL ✗ FAIL ✓ 1383 ms ✓ 1212 ms ✓ 2735 ms ✗ FAIL ✓ 765 ms ✗ FAIL
smttranslation_bitvec_l12 ✓ 1760 ms ✓ 1762 ms ✓ 2193 ms ✓ 1415 ms ✓ 1179 ms ✓ 2932 ms ✗ FAIL ✓ 809 ms ✓ 764 ms
smttranslation_bitvec_l15 ✓ 1637 ms ✓ 1619 ms ✗ FAIL ✓ 1421 ms ✓ 1181 ms ✓ 2752 ms ✗ FAIL ✓ 768 ms ✓ 761 ms
smttranslation_bitvec_l18 ✓ 1649 ms ✓ 1697 ms ✗ FAIL ✓ 1452 ms ✗ FAIL ✓ 2825 ms ✗ FAIL ✓ 791 ms ✗ FAIL
smttranslation_bitvec_l21 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1409 ms ✗ FAIL ✓ 3756 ms ✗ FAIL ✓ 785 ms ✗ FAIL
smttranslation_bitvec_l24 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1404 ms ✓ 1197 ms ✓ 2786 ms ✗ FAIL ✓ 763 ms ✓ 769 ms
smttranslation_bitvec_l27 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1382 ms ✓ 1180 ms ✓ 2789 ms ✗ FAIL ✓ 766 ms ✓ 762 ms
smttranslation_bitvec_l30 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1405 ms ✓ 1224 ms ✓ 2863 ms ✗ FAIL ✓ 785 ms ✗ FAIL
smttranslation_bitvec_l36 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1633 ms ✓ 1263 ms ✓ 2819 ms ✗ FAIL ✓ 770 ms ✓ 770 ms
smttranslation_bitvec_l42 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1442 ms ✓ 1217 ms ✓ 2811 ms ✗ FAIL ✓ 811 ms ✗ FAIL
smttranslation_bitvec_l46 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1429 ms ✓ 1284 ms ✓ 2933 ms ✗ FAIL ✓ 813 ms ✗ FAIL
smttranslation_boolnatint_l10 ✓ 1626 ms ✓ 1648 ms ✓ 2275 ms ✓ 1372 ms ✓ 1209 ms ✓ 2808 ms ✓ 766 ms ✓ 764 ms ✓ 765 ms
smttranslation_boolnatint_l12 ✓ 1621 ms ✓ 1611 ms ✓ 2248 ms ✓ 1363 ms ✓ 1178 ms ✓ 2862 ms ✗ FAIL ✓ 762 ms ✓ 763 ms
smttranslation_boolnatint_l14 ✓ 1639 ms ✓ 1631 ms ✗ FAIL ✓ 1435 ms ✓ 1193 ms ✓ 2802 ms ✓ 775 ms ✓ 770 ms ✓ 772 ms
smttranslation_boolnatint_l16 ✓ 1619 ms ✓ 1676 ms ✓ 2192 ms ✓ 1391 ms ✓ 1215 ms ✓ 2812 ms ✗ FAIL ✓ 763 ms ✓ 765 ms
smttranslation_boolnatint_l18 ✓ 1624 ms ✓ 1651 ms ✗ FAIL ✓ 1432 ms ✓ 1211 ms ✓ 2843 ms ✓ 768 ms ✓ 770 ms ✗ FAIL
smttranslation_boolnatint_l20 ✓ 1628 ms ✓ 1658 ms ✓ 2252 ms ✓ 1411 ms ✓ 1204 ms ✓ 2885 ms ✓ 766 ms ✓ 765 ms ✓ 766 ms
smttranslation_boolnatint_l23 ✓ 1633 ms ✓ 1694 ms ✓ 2210 ms ✓ 1425 ms ✓ 1185 ms ✓ 2825 ms ✓ 773 ms ✓ 773 ms ✓ 760 ms
smttranslation_boolnatint_l26 ✓ 1690 ms ✗ FAIL ✗ FAIL ✓ 1423 ms ✓ 1207 ms ✓ 2806 ms ✓ 774 ms ✓ 779 ms ✗ FAIL
smttranslation_boolnatint_l28 ✓ 1639 ms ✓ 1647 ms ✓ 2171 ms ✓ 1415 ms ✓ 1226 ms ✓ 3140 ms ✓ 772 ms ✓ 764 ms ✓ 771 ms
smttranslation_boolnatint_l30 ✓ 1695 ms ✓ 1618 ms ✗ FAIL ✓ 1451 ms ✓ 1215 ms ✓ 2874 ms ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l113 ✓ 1647 ms ✓ 1638 ms ✗ FAIL ✓ 1425 ms ✓ 1219 ms ✓ 2795 ms ✗ FAIL ✓ 764 ms ✓ 763 ms
smttranslation_inductive_l12 ✓ 1667 ms ✗ FAIL ✗ FAIL ✓ 1392 ms ✓ 1216 ms ✓ 2863 ms ✗ FAIL ✓ 766 ms ✓ 774 ms
smttranslation_inductive_l14 ✓ 1718 ms ✗ FAIL ✗ FAIL ✓ 1392 ms ✓ 1208 ms ✓ 2961 ms ✗ FAIL ✓ 763 ms ✗ FAIL
smttranslation_inductive_l16 ✓ 1656 ms ✗ FAIL ✗ FAIL ✓ 1420 ms ✓ 1249 ms ✓ 3007 ms ✗ FAIL ✓ 768 ms ✗ FAIL
smttranslation_inductive_l23 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l53 ✓ 1699 ms ✗ FAIL ✗ FAIL ✓ 1433 ms ✓ 1265 ms ✓ 2792 ms ✗ FAIL ✓ 765 ms ✗ FAIL
smttranslation_inductive_l58 ✓ 1712 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1205 ms ✓ 2700 ms ✗ FAIL ✓ 773 ms ✓ 766 ms
smttranslation_inductive_l61 ✓ 1819 ms ✗ FAIL ✗ FAIL ✓ 1413 ms ✓ 1204 ms ✓ 2735 ms ✗ FAIL ✓ 825 ms ✓ 784 ms
smttranslation_inductive_l64 ✓ 1758 ms ✗ FAIL ✗ FAIL ✓ 1400 ms ✓ 1168 ms ✓ 2717 ms ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l74 ✓ 1704 ms ✓ 1673 ms ✗ FAIL ✓ 1371 ms ✓ 1221 ms ✓ 2623 ms ✗ FAIL ✓ 784 ms ✓ 770 ms
smttranslation_names_l15 ✓ 1640 ms ✓ 1633 ms ✓ 2217 ms ✓ 1377 ms ✓ 1223 ms ✓ 2736 ms ✓ 767 ms ✓ 766 ms ✓ 767 ms
smttranslation_string_l11 ✓ 1603 ms ✓ 1616 ms ✗ FAIL ✓ 1377 ms ✓ 1271 ms ✓ 2741 ms ✗ FAIL ✓ 765 ms ✓ 771 ms
smttranslation_string_l13 ✓ 1725 ms ✗ FAIL ✗ FAIL ✓ 1379 ms ✓ 1315 ms ✓ 2698 ms ✗ FAIL ✓ 778 ms ✗ FAIL
smttranslation_string_l16 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l22 ✓ 1702 ms ✓ 1659 ms ✗ FAIL ✓ 1360 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l25 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l9 ✓ 1634 ms ✓ 1648 ms ✗ FAIL ✓ 1346 ms ✓ 1163 ms ✓ 2879 ms ✗ FAIL ✓ 764 ms ✓ 760 ms
test_regression_l35 ✓ 1628 ms ✓ 1638 ms ✗ FAIL ✓ 1366 ms ✓ 1166 ms ✓ 3048 ms ✓ 763 ms ✓ 766 ms ✗ FAIL
test_regression_l45 ✓ 1696 ms ✗ FAIL ✗ FAIL ✓ 1366 ms ✓ 1170 ms ✓ 2795 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_regression_l63 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1391 ms ✓ 1169 ms ✓ 2597 ms ✗ FAIL ✗ FAIL ✓ 763 ms
test_regression_l66 ✗ FAIL ✗ FAIL ✓ 2173 ms ✓ 1366 ms ✓ 1185 ms ✓ 2801 ms ✗ FAIL ✗ FAIL ✓ 767 ms
test_regression_l69 ✓ 1614 ms ✓ 1641 ms ✓ 2225 ms ✓ 1366 ms ✓ 1180 ms ✓ 2764 ms ✗ FAIL ✗ FAIL ✓ 768 ms
test_regression_l72 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1370 ms ✓ 1170 ms ✓ 3212 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l76 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1381 ms ✗ FAIL ✓ 3653 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l79 ✓ 1599 ms ✓ 1659 ms ✗ FAIL ✓ 1433 ms ✗ FAIL ✓ 3379 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l83 ✓ 1653 ms ✓ 1667 ms ✓ 2215 ms ✓ 1389 ms ✓ 1153 ms ✓ 2990 ms ✓ 772 ms ✓ 813 ms ✓ 771 ms
test_regression_l89 ✓ 1629 ms ✓ 1612 ms ✓ 2197 ms ✓ 1357 ms ✓ 1162 ms ✓ 2777 ms ✓ 778 ms ✓ 762 ms ✓ 762 ms

Blaster · 50 theorems

Lean-blaster regression and SMT goals

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster47/50 (94%)50 new goals
300
blaster (only-optimize: 1)25/50 (50%)50 new goals
0025
smt +model17/50 (34%)50 new goals
0033
auto37/50 (74%)50 new goals
0013
aesop38/50 (76%)50 new goals
0012
hammer48/50 (96%)50 new goals
002
omega17/50 (34%)50 new goals
0033
grind37/50 (74%)50 new goals
0013
simp25/50 (50%)50 new goals
0025
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
fixedissues_issue12_l9 ✓ 1649 ms ✓ 1688 ms ✗ FAIL ✗ FAIL ✓ 1414 ms ✓ 3555 ms ✗ FAIL ✓ 783 ms ✗ FAIL
fixedissues_issue14_l12 ✓ 1807 ms ✗ FAIL ✗ FAIL ✓ 1457 ms ✓ 1310 ms ✓ 3098 ms ✗ FAIL ✓ 760 ms ✓ 762 ms
fixedissues_issue17_l11 ✓ 1687 ms ✗ FAIL ✓ 2189 ms ✓ 1408 ms ✓ 1294 ms ✓ 3244 ms ✗ FAIL ✗ FAIL ✓ 805 ms
fixedissues_issue18_l13 ✓ 1749 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue20_l18 ✓ 1662 ms ✗ FAIL ✗ FAIL ✓ 1420 ms ✓ 1327 ms ✓ 2981 ms ✗ FAIL ✓ 782 ms ✗ FAIL
fixedissues_issue20_l26 ✓ 1671 ms ✗ FAIL ✗ FAIL ✓ 1414 ms ✓ 1282 ms ✓ 3084 ms ✗ FAIL ✓ 771 ms ✗ FAIL
fixedissues_issue26_l41 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4393 ms ✗ FAIL ✓ 845 ms ✗ FAIL
fixedissues_issue26_l49 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3184 ms ✗ FAIL ✓ 834 ms ✗ FAIL
fixedissues_issue28_l12 ✓ 1701 ms ✓ 1734 ms ✓ 2151 ms ✓ 1455 ms ✗ FAIL ✓ 3756 ms ✓ 773 ms ✓ 783 ms ✗ FAIL
fixedissues_issue28_l13 ✓ 1612 ms ✓ 1641 ms ✓ 2160 ms ✓ 1516 ms ✗ FAIL ✓ 3808 ms ✓ 764 ms ✓ 769 ms ✗ FAIL
fixedissues_issue31_l12 ✓ 1650 ms ✓ 1663 ms ✗ FAIL ✗ FAIL ✓ 1294 ms ✓ 3120 ms ✗ FAIL ✗ FAIL ✓ 775 ms
fixedissues_issue31_l30 ✓ 1645 ms ✓ 1697 ms ✗ FAIL ✗ FAIL ✓ 1301 ms ✓ 3152 ms ✗ FAIL ✗ FAIL ✓ 819 ms
fixedissues_issue31_l57 ✓ 1680 ms ✓ 1679 ms ✗ FAIL ✗ FAIL ✓ 1287 ms ✓ 2992 ms ✗ FAIL ✗ FAIL ✓ 781 ms
fixedissues_issue34_l14 ✓ 1703 ms ✓ 1700 ms ✗ FAIL ✓ 1419 ms ✓ 1324 ms ✓ 3037 ms ✗ FAIL ✓ 771 ms ✓ 771 ms
fixedissues_issue34_l18 ✓ 1704 ms ✓ 1777 ms ✗ FAIL ✓ 1440 ms ✓ 1283 ms ✓ 3022 ms ✗ FAIL ✓ 778 ms ✓ 764 ms
fixedissues_issue35_l29 ✓ 1728 ms ✗ FAIL ✗ FAIL ✓ 1427 ms ✓ 1277 ms ✓ 3467 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue35_l35 ✓ 1711 ms ✗ FAIL ✗ FAIL ✓ 1411 ms ✓ 1266 ms ✓ 2987 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue35_l42 ✓ 1727 ms ✗ FAIL ✗ FAIL ✓ 1408 ms ✓ 1274 ms ✓ 2962 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue5_l18 ✓ 1727 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3840 ms ✗ FAIL ✓ 842 ms ✗ FAIL
fixedissues_issue6_l11 ✓ 1679 ms ✓ 1749 ms ✗ FAIL ✓ 1434 ms ✓ 1249 ms ✓ 2930 ms ✗ FAIL ✓ 768 ms ✗ FAIL
fixedissues_issue6_l14 ✓ 1687 ms ✓ 1722 ms ✗ FAIL ✓ 1394 ms ✓ 1218 ms ✓ 2871 ms ✗ FAIL ✓ 767 ms ✗ FAIL
fixedissues_issue7_l10 ✓ 1714 ms ✓ 1736 ms ✗ FAIL ✗ FAIL ✓ 1248 ms ✓ 2927 ms ✗ FAIL ✓ 817 ms ✓ 768 ms
fixedissues_issue7_l11 ✓ 1755 ms ✓ 1725 ms ✗ FAIL ✗ FAIL ✓ 1261 ms ✓ 2965 ms ✗ FAIL ✓ 777 ms ✓ 780 ms
fixedissues_issue9_l10 ✓ 1844 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1300 ms ✓ 2952 ms ✗ FAIL ✓ 797 ms ✗ FAIL
funext_poly ✓ 1770 ms ✗ FAIL ✗ FAIL ✓ 1429 ms ✓ 1254 ms ✓ 2896 ms ✗ FAIL ✓ 771 ms ✗ FAIL
int_neg_positive ✓ 1689 ms ✓ 1700 ms ✓ 2156 ms ✓ 1390 ms ✓ 1245 ms ✓ 3048 ms ✓ 772 ms ✓ 789 ms ✓ 766 ms
list_set_length ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1239 ms ✓ 2816 ms ✗ FAIL ✓ 777 ms ✓ 771 ms
smt_smteqarith_l12 ✓ 1680 ms ✗ FAIL ✓ 2225 ms ✓ 1419 ms ✓ 1282 ms ✓ 2934 ms ✓ 780 ms ✓ 775 ms ✗ FAIL
smt_smteqarith_l13 ✓ 1721 ms ✗ FAIL ✓ 2236 ms ✓ 1407 ms ✗ FAIL ✓ 3432 ms ✓ 770 ms ✓ 778 ms ✗ FAIL
smt_smteqarith_l14 ✓ 1712 ms ✗ FAIL ✓ 2372 ms ✓ 1413 ms ✓ 1258 ms ✓ 2952 ms ✓ 775 ms ✓ 777 ms ✗ FAIL
smt_smtltarith_l6 ✓ 1756 ms ✗ FAIL ✓ 2185 ms ✓ 1401 ms ✓ 1249 ms ✓ 2823 ms ✓ 772 ms ✓ 829 ms ✓ 768 ms
smt_smtltarith_l7 ✓ 1712 ms ✗ FAIL ✓ 2181 ms ✓ 1418 ms ✓ 1231 ms ✓ 2909 ms ✓ 773 ms ✓ 793 ms ✓ 823 ms
smt_smtltarith_l9 ✓ 1674 ms ✓ 1702 ms ✓ 2160 ms ✓ 1398 ms ✓ 1226 ms ✓ 2842 ms ✓ 776 ms ✓ 798 ms ✓ 767 ms
smt_smtpredqualifier_l8 ✓ 1809 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smt_smtrecfun_l11 ✓ 1709 ms ✓ 1705 ms ✗ FAIL ✓ 1423 ms ✓ 1248 ms ✓ 2858 ms ✗ FAIL ✓ 781 ms ✓ 774 ms
smt_smtrecfun_l9 ✓ 1697 ms ✓ 1729 ms ✗ FAIL ✓ 1431 ms ✓ 1232 ms ✓ 2895 ms ✗ FAIL ✓ 774 ms ✓ 771 ms
smtnat_smtnatadd_l11 ✓ 1660 ms ✓ 1674 ms ✓ 2183 ms ✓ 1433 ms ✓ 1248 ms ✓ 2873 ms ✓ 768 ms ✓ 783 ms ✓ 771 ms
smtnat_smtnatadd_l16 ✓ 1690 ms ✓ 1691 ms ✓ 2282 ms ✓ 1410 ms ✓ 1241 ms ✓ 2908 ms ✓ 772 ms ✓ 776 ms ✓ 771 ms
smtnat_smtnatadd_l9 ✓ 1770 ms ✓ 1701 ms ✓ 2134 ms ✓ 1400 ms ✓ 1338 ms ✓ 2827 ms ✓ 788 ms ✓ 783 ms ✓ 774 ms
smtnat_smtnatdiv_l11 ✓ 1746 ms ✗ FAIL ✗ FAIL ✓ 1404 ms ✗ FAIL ✓ 7686 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatdiv_l13 ✓ 1701 ms ✗ FAIL ✗ FAIL ✓ 1422 ms ✗ FAIL ✓ 2899 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatdiv_l9 ✓ 1697 ms ✗ FAIL ✗ FAIL ✓ 1461 ms ✗ FAIL ✓ 4596 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatmod_l11 ✓ 1615 ms ✓ 1624 ms ✗ FAIL ✓ 1407 ms ✓ 1258 ms ✓ 2845 ms ✓ 771 ms ✓ 764 ms ✓ 822 ms
smtnat_smtnatmod_l9 ✓ 2553 ms ✗ FAIL ✗ FAIL ✓ 1537 ms ✗ FAIL ✓ 4507 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatmul_l11 ✓ 1642 ms ✓ 1640 ms ✓ 2167 ms ✓ 1390 ms ✓ 1237 ms ✓ 2869 ms ✓ 770 ms ✓ 767 ms ✓ 769 ms
smtnat_smtnatmul_l9 ✓ 1652 ms ✓ 1678 ms ✓ 2181 ms ✓ 1412 ms ✓ 1217 ms ✓ 2815 ms ✓ 772 ms ✓ 770 ms ✓ 772 ms
smtnat_smtnatpow_l11 ✓ 1648 ms ✓ 1690 ms ✗ FAIL ✓ 1450 ms ✓ 1268 ms ✓ 2887 ms ✗ FAIL ✓ 784 ms ✗ FAIL
smtnat_smtnatpow_l9 ✓ 1672 ms ✓ 1697 ms ✗ FAIL ✓ 1416 ms ✓ 1277 ms ✓ 2948 ms ✗ FAIL ✓ 773 ms ✓ 768 ms
smtnat_smtnatsub_l11 ✓ 1713 ms ✗ FAIL ✓ 2236 ms ✓ 1425 ms ✓ 1241 ms ✓ 2869 ms ✓ 774 ms ✓ 781 ms ✓ 772 ms
smtnat_smtnatsub_l9 ✓ 1690 ms ✓ 1644 ms ✓ 2248 ms ✓ 1415 ms ✓ 1235 ms ✓ 2846 ms ✓ 776 ms ✓ 768 ms ✓ 768 ms

LeanHammer + Duper · 50 theorems

LeanHammer smoke test and Duper dependency tests

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster37/50 (74%)50 new goals
2011
blaster (only-optimize: 1)33/50 (66%)50 new goals
0017
smt +model5/50 (10%)50 new goals
0045
auto38/50 (76%)50 new goals
0012
aesop36/50 (72%)50 new goals
0014
hammer45/50 (90%)50 new goals
005
omega0/50 (0%)50 new goals
0050
grind34/50 (68%)50 new goals
0016
simp10/50 (20%)50 new goals
0040
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
fluidsuptests_l13 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3273 ms ✗ FAIL ✗ FAIL ✗ FAIL
fluidsuptests_l19 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3085 ms ✗ FAIL ✓ 787 ms ✗ FAIL
fluidsuptests_l9 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3294 ms ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l101 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1467 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l104 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1452 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l108 ✓ 1640 ms ✓ 1635 ms ✗ FAIL ✓ 1429 ms ✓ 1290 ms ✓ 2828 ms ✗ FAIL ✓ 760 ms ✓ 767 ms
temp2_l111 ✓ 1654 ms ✓ 1658 ms ✗ FAIL ✗ FAIL ✓ 1258 ms ✓ 2766 ms ✗ FAIL ✓ 786 ms ✓ 768 ms
temp2_l116 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1250 ms ✓ 2920 ms ✗ FAIL ✓ 789 ms ✗ FAIL
temp2_l131 ✓ 1704 ms ✗ FAIL ✗ FAIL ✓ 1418 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l53 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1194 ms ✓ 2690 ms ✗ FAIL ✗ FAIL ✓ 765 ms
temp2_l77 ✓ 1623 ms ✓ 1613 ms ✓ 2185 ms ✓ 1409 ms ✓ 1223 ms ✓ 3084 ms ✗ FAIL ✓ 770 ms ✓ 760 ms
temp2_l82 ✓ 1636 ms ✓ 1632 ms ✓ 2185 ms ✓ 1415 ms ✓ 1215 ms ✓ 3068 ms ✗ FAIL ✓ 774 ms ✓ 769 ms
temp2_l90 ✓ 1685 ms ✗ FAIL ✓ 2239 ms ✓ 1389 ms ✓ 1246 ms ✓ 3194 ms ✗ FAIL ✓ 764 ms ✗ FAIL
temp2_l94 ✓ 1674 ms ✗ FAIL ✓ 2237 ms ✓ 1414 ms ✓ 1227 ms ✓ 2993 ms ✗ FAIL ✓ 815 ms ✗ FAIL
temp_l29 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1201 ms ✓ 2978 ms ✗ FAIL ✗ FAIL ✓ 844 ms
test_boolsimp_l10 ✓ 1667 ms ✓ 1618 ms ✗ FAIL ✓ 1400 ms ✗ FAIL ✓ 3811 ms ✗ FAIL ✓ 797 ms ✗ FAIL
test_boolsimp_l13 ✓ 1611 ms ✓ 1607 ms ✗ FAIL ✓ 1379 ms ✗ FAIL ✓ 3388 ms ✗ FAIL ✓ 778 ms ✗ FAIL
test_boolsimp_l16 ✓ 1620 ms ✓ 1632 ms ✗ FAIL ✓ 1410 ms ✓ 1260 ms ✓ 2850 ms ✗ FAIL ✓ 768 ms ✗ FAIL
test_boolsimp_l19 ✓ 1639 ms ✓ 1662 ms ✗ FAIL ✓ 1392 ms ✓ 1287 ms ✓ 2891 ms ✗ FAIL ✓ 781 ms ✗ FAIL
test_boolsimp_l22 ✓ 1606 ms ✓ 1632 ms ✗ FAIL ✓ 1406 ms ✓ 1227 ms ✓ 2813 ms ✗ FAIL ✓ 766 ms ✗ FAIL
test_boolsimp_l25 ✓ 1696 ms ✓ 1653 ms ✗ FAIL ✓ 1398 ms ✓ 1191 ms ✓ 2907 ms ✗ FAIL ✓ 767 ms ✗ FAIL
test_boolsimp_l28 ✓ 1748 ms ✓ 1641 ms ✗ FAIL ✓ 1400 ms ✓ 1173 ms ✓ 2800 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l31 ✓ 1638 ms ✓ 1589 ms ✗ FAIL ✓ 1415 ms ✓ 1198 ms ✓ 2801 ms ✗ FAIL ✓ 768 ms ✗ FAIL
test_boolsimp_l34 ✓ 1651 ms ✓ 1731 ms ✗ FAIL ✓ 1405 ms ✓ 1268 ms ✓ 2775 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l37 ✓ 1758 ms ✓ 1739 ms ✗ FAIL ✓ 1404 ms ✓ 1211 ms ✓ 2716 ms ✗ FAIL ✓ 765 ms ✗ FAIL
test_boolsimp_l40 ✓ 1715 ms ✓ 1694 ms ✗ FAIL ✓ 1397 ms ✓ 1269 ms ✓ 2749 ms ✗ FAIL ✓ 785 ms ✗ FAIL
test_boolsimp_l43 ✓ 1688 ms ✓ 1685 ms ✗ FAIL ✓ 1418 ms ✓ 1174 ms ✓ 2819 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l46 ✓ 1667 ms ✓ 1631 ms ✗ FAIL ✓ 1413 ms ✓ 1184 ms ✓ 2835 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l49 ✓ 1628 ms ✓ 1633 ms ✗ FAIL ✓ 1394 ms ✓ 1205 ms ✓ 2725 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l52 ✓ 1636 ms ✓ 1634 ms ✗ FAIL ✓ 1395 ms ✓ 1169 ms ✓ 2790 ms ✗ FAIL ✓ 763 ms ✗ FAIL
test_boolsimp_l55 ✓ 1653 ms ✓ 1627 ms ✗ FAIL ✓ 1402 ms ✓ 1164 ms ✓ 2832 ms ✗ FAIL ✓ 766 ms ✗ FAIL
test_boolsimp_l58 ✓ 1623 ms ✓ 1638 ms ✗ FAIL ✓ 1411 ms ✓ 1196 ms ✓ 2855 ms ✗ FAIL ✓ 796 ms ✗ FAIL
test_boolsimp_l61 ✓ 1630 ms ✓ 1614 ms ✗ FAIL ✓ 1412 ms ✓ 1212 ms ✓ 2984 ms ✗ FAIL ✓ 831 ms ✗ FAIL
test_boolsimp_l64 ✓ 1671 ms ✓ 1634 ms ✗ FAIL ✓ 1388 ms ✓ 1189 ms ✓ 2971 ms ✗ FAIL ✓ 771 ms ✗ FAIL
test_boolsimp_l67 ✓ 1639 ms ✓ 1655 ms ✗ FAIL ✓ 1372 ms ✓ 1175 ms ✓ 2818 ms ✗ FAIL ✓ 765 ms ✗ FAIL
test_boolsimp_l7 ✓ 1681 ms ✓ 1672 ms ✗ FAIL ✓ 1369 ms ✓ 1221 ms ✓ 2774 ms ✗ FAIL ✓ 778 ms ✗ FAIL
test_boolsimp_l70 ✓ 1699 ms ✓ 1650 ms ✗ FAIL ✓ 1358 ms ✓ 1174 ms ✓ 2713 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l73 ✓ 1630 ms ✓ 1630 ms ✗ FAIL ✓ 1370 ms ✓ 1147 ms ✓ 2864 ms ✗ FAIL ✓ 774 ms ✗ FAIL
test_higher_order_l16 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3520 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_higher_order_l29 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4082 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l11 ✓ 1632 ms ✓ 1632 ms ✗ FAIL ✓ 1375 ms ✓ 1191 ms ✓ 2664 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l15 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1391 ms ✗ FAIL ✓ 2973 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l21 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l27 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l33 ✓ 1754 ms ✗ FAIL ✗ FAIL ✓ 1398 ms ✗ FAIL ✓ 3122 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l37 ✓ 1674 ms ✓ 1619 ms ✗ FAIL ✓ 1379 ms ✓ 1222 ms ✓ 2643 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_inhabitationreasoning_l54 ✓ 1617 ms ✓ 1638 ms ✗ FAIL ✗ FAIL ✓ 1198 ms ✓ 2680 ms ✗ FAIL ✓ 772 ms ✓ 768 ms
test_inhabitationreasoning_l7 ✓ 1714 ms ✓ 1640 ms ✗ FAIL ✓ 1386 ms ✓ 1237 ms ✓ 2631 ms ✗ FAIL ✗ FAIL ✓ 765 ms
test_inhabitationreasoning_l9 ✓ 1631 ms ✓ 1631 ms ✗ FAIL ✓ 1372 ms ✓ 1237 ms ✓ 2610 ms ✗ FAIL ✗ FAIL ✓ 764 ms
true_smoke ✓ 1636 ms ✓ 1615 ms ✓ 2209 ms ✓ 1363 ms ✓ 1232 ms ✓ 2659 ms ✗ FAIL ✓ 758 ms ✓ 764 ms

lean-smt · 50 theorems

lean-smt logic, arithmetic, and bitvector tests

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster41/50 (82%)50 new goals
108
blaster (only-optimize: 1)23/50 (46%)50 new goals
0027
smt +model40/50 (80%)50 new goals
0010
auto39/50 (78%)50 new goals
0011
aesop39/50 (78%)50 new goals
0011
hammer47/50 (94%)50 new goals
003
omega5/50 (10%)50 new goals
0045
grind42/50 (84%)50 new goals
008
simp17/50 (34%)50 new goals
0033
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
auto_l6 ✓ 1600 ms ✓ 1641 ms ✗ FAIL ✓ 1418 ms ✓ 1265 ms ✓ 2868 ms ✗ FAIL ✓ 806 ms ✓ 769 ms
bitvec_add_l5 ✗ FAIL ✗ FAIL ✓ 2342 ms ✓ 1515 ms ✓ 1248 ms ✓ 2814 ms ✗ FAIL ✓ 783 ms ✗ FAIL
bitvec_bitwiseac_l7 ✗ FAIL ✗ FAIL ✓ 2181 ms ✓ 1468 ms ✗ FAIL ✓ 2874 ms ✗ FAIL ✓ 770 ms ✗ FAIL
bitvec_shift_l5 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4959 ms ✗ FAIL ✓ 838 ms ✗ FAIL
bitvec_xorcomm_l3 ✗ FAIL ✗ FAIL ✓ 2184 ms ✓ 1407 ms ✗ FAIL ✓ 3004 ms ✗ FAIL ✓ 774 ms ✗ FAIL
bool_addition_l3 ✓ 1630 ms ✓ 1616 ms ✓ 2160 ms ✓ 1380 ms ✓ 1246 ms ✓ 2914 ms ✗ FAIL ✓ 771 ms ✗ FAIL
bool_assoc_l3 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
bool_comm_l3 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
bool_cong_l3 ✓ 1700 ms ✗ FAIL ✓ 2273 ms ✗ FAIL ✓ 1261 ms ✓ 2888 ms ✗ FAIL ✓ 768 ms ✗ FAIL
bool_conjunction_l3 ✓ 1653 ms ✓ 1673 ms ✓ 2220 ms ✓ 1388 ms ✓ 1265 ms ✓ 2866 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_disjunctivesyllogism_l3 ✓ 1676 ms ✗ FAIL ✓ 2294 ms ✓ 1371 ms ✓ 1249 ms ✓ 2962 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_exists_l3 ✓ 1738 ms ✗ FAIL ✓ 2181 ms ✓ 1347 ms ✓ 1280 ms ✓ 2929 ms ✗ FAIL ✗ FAIL ✓ 765 ms
bool_falsum_l3 ✓ 1606 ms ✓ 1635 ms ✓ 2198 ms ✓ 1380 ms ✓ 1241 ms ✓ 2922 ms ✗ FAIL ✓ 763 ms ✓ 762 ms
bool_hypotheticalsyllogism_l3 ✓ 1728 ms ✗ FAIL ✓ 2223 ms ✓ 1377 ms ✓ 1236 ms ✓ 2909 ms ✗ FAIL ✓ 770 ms ✗ FAIL
bool_modusponens_l3 ✓ 1618 ms ✓ 1623 ms ✗ FAIL ✓ 1351 ms ✓ 1245 ms ✓ 2982 ms ✗ FAIL ✓ 769 ms ✗ FAIL
bool_modusponens_l3_2 ✓ 1626 ms ✓ 1626 ms ✓ 2231 ms ✓ 1342 ms ✓ 1253 ms ✓ 2900 ms ✗ FAIL ✓ 772 ms ✗ FAIL
bool_modustollens_l3 ✓ 1633 ms ✓ 1650 ms ✓ 2266 ms ✓ 1361 ms ✓ 1241 ms ✓ 2952 ms ✗ FAIL ✓ 778 ms ✗ FAIL
bool_propext_l3 ✓ 1691 ms ✗ FAIL ✓ 2276 ms ✗ FAIL ✓ 1237 ms ✓ 2923 ms ✗ FAIL ✓ 792 ms ✓ 775 ms
bool_refl_l3 ✓ 1650 ms ✓ 1696 ms ✓ 2251 ms ✗ FAIL ✓ 1257 ms ✓ 3078 ms ✗ FAIL ✓ 769 ms ✓ 771 ms
bool_resolution_l3 ✓ 1720 ms ✗ FAIL ✓ 2291 ms ✓ 1375 ms ✓ 1235 ms ✓ 3455 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_simplification_l3 ✓ 1698 ms ✗ FAIL ✓ 2312 ms ✓ 1349 ms ✓ 1261 ms ✓ 3243 ms ✗ FAIL ✓ 774 ms ✗ FAIL
bool_symm_l3 ✓ 1648 ms ✓ 1702 ms ✓ 2303 ms ✗ FAIL ✓ 1252 ms ✓ 3163 ms ✗ FAIL ✓ 759 ms ✗ FAIL
bool_trans_l3 ✓ 1708 ms ✗ FAIL ✓ 2314 ms ✗ FAIL ✓ 1349 ms ✓ 3319 ms ✗ FAIL ✓ 768 ms ✗ FAIL
bool_triv_l3 ✓ 1632 ms ✓ 1669 ms ✓ 2248 ms ✓ 1349 ms ✓ 1248 ms ✓ 3187 ms ✗ FAIL ✓ 765 ms ✓ 766 ms
bool_triv_l3_2 ✓ 1693 ms ✓ 1700 ms ✓ 2337 ms ✓ 1365 ms ✓ 1239 ms ✓ 3238 ms ✗ FAIL ✓ 762 ms ✓ 766 ms
bool_triv_l3_3 ✓ 1640 ms ✓ 1627 ms ✓ 2331 ms ✓ 1347 ms ✓ 1262 ms ✓ 2968 ms ✗ FAIL ✓ 761 ms ✓ 762 ms
bool_verum_l3 ✓ 1653 ms ✓ 1668 ms ✓ 2319 ms ✓ 1380 ms ✓ 1285 ms ✓ 3124 ms ✗ FAIL ✓ 764 ms ✓ 784 ms
euf_example_l3 ✗ FAIL ✗ FAIL ✓ 2306 ms ✓ 1391 ms ✓ 1256 ms ✓ 3112 ms ✗ FAIL ✓ 769 ms ✗ FAIL
euf_issue100_l3 ✓ 1688 ms ✗ FAIL ✗ FAIL ✓ 1381 ms ✓ 1305 ms ✓ 3081 ms ✗ FAIL ✓ 782 ms ✗ FAIL
euf_issue97_l3 ✓ 1651 ms ✓ 1661 ms ✓ 2301 ms ✓ 1389 ms ✓ 1310 ms ✓ 3020 ms ✗ FAIL ✓ 769 ms ✓ 768 ms
int_arith_l3 ✓ 1728 ms ✗ FAIL ✗ FAIL ✓ 1401 ms ✗ FAIL ✓ 2900 ms ✗ FAIL ✗ FAIL ✗ FAIL
int_cong_l3 ✓ 1688 ms ✗ FAIL ✓ 2293 ms ✓ 1361 ms ✓ 1283 ms ✓ 2902 ms ✗ FAIL ✓ 772 ms ✗ FAIL
int_forallexists_l3 ✓ 1805 ms ✗ FAIL ✓ 2269 ms ✓ 1388 ms ✗ FAIL ✓ 3449 ms ✗ FAIL ✗ FAIL ✗ FAIL
int_linarith_l6 ✓ 1617 ms ✓ 1615 ms ✓ 2292 ms ✓ 1400 ms ✓ 1255 ms ✓ 2893 ms ✗ FAIL ✓ 766 ms ✗ FAIL
int_neg_l3 ✓ 1611 ms ✓ 1632 ms ✓ 2280 ms ✓ 1459 ms ✓ 1300 ms ✓ 3084 ms ✓ 769 ms ✓ 764 ms ✓ 762 ms
int_square_nonnegative ✓ 1782 ms ✗ FAIL ✓ 2265 ms ✓ 1440 ms ✗ FAIL ✓ 6393 ms ✗ FAIL ✗ FAIL ✗ FAIL
issues_reconstructarithsumub_l3 ✓ 1847 ms ✗ FAIL ✓ 2596 ms ✓ 1697 ms ✗ FAIL ✓ 3752 ms ✓ 824 ms ✓ 876 ms ✗ FAIL
modus_tollens ✓ 1668 ms ✓ 1623 ms ✓ 2294 ms ✓ 1457 ms ✓ 1305 ms ✓ 2802 ms ✗ FAIL ✓ 764 ms ✗ FAIL
nat_cong_l3 ✓ 1667 ms ✗ FAIL ✓ 2246 ms ✓ 1453 ms ✓ 1277 ms ✓ 2927 ms ✗ FAIL ✓ 763 ms ✗ FAIL
nat_exists_l3 ✓ 1631 ms ✓ 1630 ms ✓ 2295 ms ✓ 1435 ms ✓ 1261 ms ✓ 2783 ms ✗ FAIL ✗ FAIL ✓ 771 ms
nat_exists_l3_2 ✓ 1744 ms ✗ FAIL ✓ 2222 ms ✓ 1470 ms ✓ 1227 ms ✓ 2762 ms ✗ FAIL ✓ 767 ms ✓ 764 ms
nat_forall_l3 ✓ 1635 ms ✓ 1600 ms ✓ 2208 ms ✓ 1404 ms ✓ 1249 ms ✓ 2797 ms ✓ 774 ms ✓ 769 ms ✓ 769 ms
nat_neqzero_l3 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
rat_linarith_l63 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4175 ms ✗ FAIL ✓ 773 ms ✗ FAIL
resolution ✓ 1699 ms ✗ FAIL ✓ 2248 ms ✓ 1371 ms ✓ 1295 ms ✓ 2829 ms ✗ FAIL ✓ 770 ms ✗ FAIL
unit_embedding_l32 ✓ 1618 ms ✓ 1690 ms ✓ 2244 ms ✓ 1445 ms ✓ 1237 ms ✓ 2826 ms ✓ 768 ms ✓ 766 ms ✓ 767 ms
unit_int_l19 ✓ 1597 ms ✓ 1625 ms ✓ 2230 ms ✓ 1400 ms ✓ 1260 ms ✓ 2665 ms ✓ 767 ms ✓ 764 ms ✓ 763 ms
unit_normalize_l28 ✓ 1619 ms ✓ 1631 ms ✓ 2276 ms ✓ 1394 ms ✓ 1203 ms ✓ 2745 ms ✗ FAIL ✓ 763 ms ✓ 761 ms
unit_quant_l6 ✓ 1681 ms ✗ FAIL ✓ 2235 ms ✓ 1396 ms ✓ 1236 ms ✓ 2768 ms ✗ FAIL ✓ 767 ms ✗ FAIL
unit_rat_l63 ✓ 1632 ms ✓ 1608 ms ✗ FAIL ✗ FAIL ✓ 1190 ms ✓ 2728 ms ✗ FAIL ✓ 775 ms ✗ FAIL

Shared benchmarks

ITL4 · 44 theorems

Introduction to Logic

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster44/44 (100%)no change
000
blaster (only-optimize: 1)26/44 (59%)no change
0018
smt +model6/44 (14%)no change
0038
auto44/44 (100%)no change
000
aesop44/44 (100%)no change
000
hammer44/44 (100%)no change
000
omega1/44 (2%)no change
0043
grind44/44 (100%)no change
000
simp5/44 (11%)no change
0039
Explore theorem results 44 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
AndIntro_01 ✓ 1683 ms ✓ 1652 ms ✗ FAIL ✓ 1914 ms ✓ 1345 ms ✓ 2706 ms ✓ 1245 ms ✓ 1236 ms ✗ FAIL
AndIntro_02 ✓ 1670 ms ✓ 1634 ms ✗ FAIL ✓ 1912 ms ✓ 1341 ms ✓ 2642 ms ✗ FAIL ✓ 1253 ms ✗ FAIL
AndIntro_03 ✓ 1652 ms ✓ 1672 ms ✗ FAIL ✓ 1922 ms ✓ 1352 ms ✓ 2610 ms ✗ FAIL ✓ 1238 ms ✗ FAIL
AndIntro_04 ✓ 1646 ms ✓ 1676 ms ✗ FAIL ✓ 1918 ms ✓ 1341 ms ✓ 2612 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
AndIntro_05 ✓ 1640 ms ✓ 1654 ms ✗ FAIL ✓ 1921 ms ✓ 1360 ms ✓ 2636 ms ✗ FAIL ✓ 1327 ms ✗ FAIL
AndIntro_06 ✓ 1674 ms ✓ 1712 ms ✗ FAIL ✓ 1910 ms ✓ 1323 ms ✓ 2647 ms ✗ FAIL ✓ 1231 ms ✗ FAIL
AndIntro_07 ✓ 1662 ms ✓ 1657 ms ✗ FAIL ✓ 1913 ms ✓ 1332 ms ✓ 2683 ms ✗ FAIL ✓ 1266 ms ✗ FAIL
AndIntro_08 ✓ 1649 ms ✓ 1642 ms ✗ FAIL ✓ 1937 ms ✓ 1344 ms ✓ 2693 ms ✗ FAIL ✓ 1270 ms ✗ FAIL
IffIntro_01 ✓ 1682 ms ✓ 1680 ms ✗ FAIL ✓ 1913 ms ✓ 1335 ms ✓ 2703 ms ✗ FAIL ✓ 1253 ms ✗ FAIL
IffIntro_02 ✓ 1654 ms ✓ 1644 ms ✗ FAIL ✓ 1918 ms ✓ 1368 ms ✓ 2747 ms ✗ FAIL ✓ 1233 ms ✗ FAIL
IffIntro_03 ✓ 1704 ms ✗ FAIL ✗ FAIL ✓ 1954 ms ✓ 1305 ms ✓ 2801 ms ✗ FAIL ✓ 1236 ms ✗ FAIL
IffIntro_04 ✓ 1740 ms ✗ FAIL ✗ FAIL ✓ 1924 ms ✓ 1337 ms ✓ 2723 ms ✗ FAIL ✓ 1242 ms ✗ FAIL
IffIntro_05 ✓ 1759 ms ✗ FAIL ✗ FAIL ✓ 1953 ms ✓ 1332 ms ✓ 2742 ms ✗ FAIL ✓ 1250 ms ✗ FAIL
IffIntro_06 ✓ 1686 ms ✗ FAIL ✗ FAIL ✓ 1941 ms ✓ 1337 ms ✓ 2725 ms ✗ FAIL ✓ 1241 ms ✗ FAIL
IffIntro_07 ✓ 1736 ms ✗ FAIL ✓ 2043 ms ✓ 1937 ms ✓ 1421 ms ✓ 2766 ms ✗ FAIL ✓ 1223 ms ✓ 1299 ms
ImpIntro_01 ✓ 1689 ms ✓ 1655 ms ✗ FAIL ✓ 1915 ms ✓ 1378 ms ✓ 2674 ms ✗ FAIL ✓ 1227 ms ✗ FAIL
ImpIntro_02 ✓ 1704 ms ✓ 1658 ms ✓ 1963 ms ✓ 1908 ms ✓ 1374 ms ✓ 2661 ms ✗ FAIL ✓ 1239 ms ✓ 1280 ms
ImpIntro_03 ✓ 1643 ms ✓ 1641 ms ✓ 1998 ms ✓ 1910 ms ✓ 1406 ms ✓ 2645 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
ImpIntro_04 ✓ 1692 ms ✗ FAIL ✗ FAIL ✓ 1921 ms ✓ 1423 ms ✓ 2725 ms ✗ FAIL ✓ 1234 ms ✗ FAIL
ImpIntro_05 ✓ 1656 ms ✓ 1638 ms ✗ FAIL ✓ 1917 ms ✓ 1439 ms ✓ 2676 ms ✗ FAIL ✓ 1234 ms ✗ FAIL
ImpIntro_06 ✓ 1689 ms ✗ FAIL ✗ FAIL ✓ 1921 ms ✓ 1406 ms ✓ 2744 ms ✗ FAIL ✓ 1342 ms ✗ FAIL
ImpIntro_07 ✓ 1695 ms ✗ FAIL ✗ FAIL ✓ 1914 ms ✓ 1404 ms ✓ 2703 ms ✗ FAIL ✓ 1238 ms ✗ FAIL
ImpIntro_08 ✓ 1701 ms ✗ FAIL ✗ FAIL ✓ 1909 ms ✓ 1406 ms ✓ 2749 ms ✗ FAIL ✓ 1237 ms ✗ FAIL
ImpIntro_09 ✓ 1608 ms ✓ 1642 ms ✓ 1960 ms ✓ 1910 ms ✓ 1405 ms ✓ 2739 ms ✗ FAIL ✓ 1248 ms ✓ 1225 ms
NotIntro_01 ✓ 1681 ms ✓ 1682 ms ✓ 2002 ms ✓ 1903 ms ✓ 1369 ms ✓ 2727 ms ✗ FAIL ✓ 1229 ms ✓ 1229 ms
NotIntro_02 ✓ 1637 ms ✓ 1638 ms ✗ FAIL ✓ 1909 ms ✓ 1374 ms ✓ 2790 ms ✗ FAIL ✓ 1262 ms ✗ FAIL
NotIntro_03 ✓ 1643 ms ✓ 1656 ms ✗ FAIL ✓ 1915 ms ✓ 1421 ms ✓ 2765 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
NotIntro_04 ✓ 1731 ms ✓ 1662 ms ✓ 1958 ms ✓ 1905 ms ✓ 1414 ms ✓ 2880 ms ✗ FAIL ✓ 1279 ms ✓ 1308 ms
NotIntro_05 ✓ 1713 ms ✗ FAIL ✗ FAIL ✓ 1919 ms ✓ 1400 ms ✓ 2754 ms ✗ FAIL ✓ 1233 ms ✗ FAIL
NotIntro_06 ✓ 1655 ms ✓ 1690 ms ✗ FAIL ✓ 1907 ms ✓ 1397 ms ✓ 2741 ms ✗ FAIL ✓ 1239 ms ✗ FAIL
NotIntro_07 ✓ 1782 ms ✗ FAIL ✗ FAIL ✓ 1916 ms ✓ 1400 ms ✓ 2795 ms ✗ FAIL ✓ 1241 ms ✗ FAIL
NotIntro_08 ✓ 1680 ms ✓ 1690 ms ✗ FAIL ✓ 1906 ms ✓ 1392 ms ✓ 2811 ms ✗ FAIL ✓ 1220 ms ✗ FAIL
NotIntro_09 ✓ 1782 ms ✗ FAIL ✗ FAIL ✓ 1908 ms ✓ 1363 ms ✓ 3032 ms ✗ FAIL ✓ 1245 ms ✗ FAIL
NotIntro_10 ✓ 1676 ms ✗ FAIL ✗ FAIL ✓ 1915 ms ✓ 1385 ms ✓ 2982 ms ✗ FAIL ✓ 1260 ms ✗ FAIL
NotIntro_11 ✓ 1649 ms ✓ 1684 ms ✗ FAIL ✓ 1917 ms ✓ 1380 ms ✓ 3068 ms ✗ FAIL ✓ 1300 ms ✗ FAIL
NotIntro_12 ✓ 1759 ms ✗ FAIL ✗ FAIL ✓ 1906 ms ✓ 1414 ms ✓ 2974 ms ✗ FAIL ✓ 1250 ms ✗ FAIL
OrIntro_01 ✓ 1639 ms ✓ 1664 ms ✗ FAIL ✓ 1911 ms ✓ 1418 ms ✓ 2650 ms ✗ FAIL ✓ 1307 ms ✗ FAIL
OrIntro_02 ✓ 1706 ms ✓ 1718 ms ✗ FAIL ✓ 1908 ms ✓ 1437 ms ✓ 2699 ms ✗ FAIL ✓ 1237 ms ✗ FAIL
OrIntro_03 ✓ 1719 ms ✗ FAIL ✗ FAIL ✓ 1929 ms ✓ 1409 ms ✓ 2704 ms ✗ FAIL ✓ 1242 ms ✗ FAIL
OrIntro_04 ✓ 1626 ms ✓ 1732 ms ✗ FAIL ✓ 1913 ms ✓ 1405 ms ✓ 2852 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
OrIntro_05 ✓ 1801 ms ✗ FAIL ✗ FAIL ✓ 1919 ms ✓ 1422 ms ✓ 2820 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
OrIntro_06 ✓ 1763 ms ✗ FAIL ✗ FAIL ✓ 1920 ms ✓ 1408 ms ✓ 2887 ms ✗ FAIL ✓ 1249 ms ✗ FAIL
OrIntro_07 ✓ 1683 ms ✓ 1708 ms ✗ FAIL ✓ 1922 ms ✓ 1407 ms ✓ 2860 ms ✗ FAIL ✓ 1225 ms ✗ FAIL
OrIntro_08 ✓ 1697 ms ✗ FAIL ✗ FAIL ✓ 1921 ms ✓ 1405 ms ✓ 2775 ms ✗ FAIL ✓ 1221 ms ✗ FAIL

MiniF2F · 96 theorems

Competition math (integer/number-theory subset)

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster54/96 (56%)no change
22020
blaster (only-optimize: 1)17/96 (18%)no change
0079
smt +model9/96 (9%)no change
2085
auto32/96 (33%)no change
0064
aesop23/96 (24%)no change
0073
hammer40/96 (42%)no change
0056
omega30/96 (31%)no change
0066
grind35/96 (36%)no change
1060
simp17/96 (18%)no change
0079
Explore theorem results 96 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
numbertheory_4x3m7y3neq2003 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12_2001_p5 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_1124 ✓ 5425 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7273 ms ✓ 5470 ms ✓ 5256 ms ✗ FAIL
mathd_numbertheory_299 ✓ 5263 ms ✓ 5357 ms ✓ 5749 ms ✓ 5383 ms ✓ 5210 ms ✓ 6789 ms ✓ 5519 ms ✓ 5397 ms ✓ 5397 ms
imo_1977_p6 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_x5neqy2p4 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_430 ✓ 5130 ms ✗ FAIL ✗ FAIL ✓ 5367 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5318 ms ✗ FAIL
mathd_algebra_459 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
induction_12dvd4expnp1p20 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_1997_p5 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_277 ✓ 5714 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_559 ✓ 5585 ms ✗ FAIL ✗ FAIL ✓ 5600 ms ✗ FAIL ✓ 8784 ms ✓ 5689 ms ✓ 5609 ms ✗ FAIL
induction_nfactltnexpnm1ngt3 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_notEquiv2i2jasqbsqdiv8 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_12 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5526 ms ✓ 5397 ms ✓ 6810 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_345 ✓ 5174 ms ✓ 5197 ms ✓ 5707 ms ✓ 5582 ms ✓ 5390 ms ✓ 6750 ms ✓ 5340 ms ✓ 5432 ms ✓ 5345 ms
mathd_numbertheory_328 ✓ 4957 ms ✓ 5062 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8984 ms ✓ 5320 ms ✓ 5408 ms ✗ FAIL
mathd_numbertheory_765 ✓ 5064 ms ✗ FAIL ✗ FAIL ✓ 5676 ms ✗ FAIL ✓ 8256 ms ✓ 5431 ms ✓ 5363 ms ✗ FAIL
imo_1959_p1 ✓ 5217 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_175 ✓ 4987 ms ✓ 4946 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5382 ms ✓ 5525 ms ✗ FAIL
numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_1992_p1 ✓ 8761 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_1982_p1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
aime_1987_p5 ✓ 5483 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_728 ✓ 4911 ms ✓ 5504 ms ✗ FAIL ✓ 5564 ms ✓ 5392 ms ✓ 7083 ms ✓ 5444 ms ✓ 5401 ms ✓ 5441 ms
aime_1994_p3 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_293 ✓ 5304 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7512 ms ✓ 5455 ms ✓ 5406 ms ✗ FAIL
mathd_numbertheory_769 ✓ 5032 ms ✓ 5012 ms ✗ FAIL ✓ 5598 ms ✓ 5282 ms ✓ 7201 ms ✓ 5334 ms ✓ 5227 ms ✓ 5284 ms
mathd_numbertheory_5 ✓ 5057 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_207 ✓ 5208 ms ✓ 5062 ms ✗ FAIL ✓ 5490 ms ✓ 5309 ms ✓ 6957 ms ✓ 5206 ms ✓ 5320 ms ✓ 5278 ms
mathd_numbertheory_342 ✓ 5113 ms ✓ 4958 ms ✓ 5606 ms ✓ 5350 ms ✓ 5248 ms ✓ 7280 ms ✓ 5350 ms ✓ 5309 ms ✓ 5316 ms
mathd_numbertheory_483 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5248 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12a_2003_p5 ✓ 5090 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_495 ✓ 6072 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_296 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✓ 5469 ms ✓ 5066 ms ✓ 7506 ms ✗ FAIL ✓ 5515 ms ✓ 5497 ms
mathd_numbertheory_247 ✓ 5591 ms ✗ FAIL ✗ FAIL ✓ 5513 ms ✗ FAIL ✓ 8804 ms ✓ 5323 ms ✓ 5293 ms ✗ FAIL
numbertheory_2pownm1prime_nprime ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7175 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_392 ✓ 5218 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_314 ✓ 5105 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7332 ms ✗ FAIL ✓ 5258 ms ✗ FAIL
amc12b_2002_p7 ✓ 5103 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_457 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12_2000_p12 ✓ 5062 ms ✗ FAIL ⏱ TIMEOUT ✓ 5409 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_135 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5452 ms ✓ 7180 ms ✗ FAIL ✗ FAIL ✗ FAIL
imo_1981_p6 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_34 ✓ 5109 ms ✗ FAIL ✗ FAIL ✓ 5503 ms ✗ FAIL ✓ 8361 ms ✓ 5478 ms ✓ 5441 ms ✗ FAIL
mathd_algebra_170 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_618 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12a_2020_p4 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_435 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
algebra_others_exirrpowirrrat ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_76 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8328 ms ✗ FAIL ✓ 5448 ms ✗ FAIL
mathd_numbertheory_99 ✓ 5246 ms ✗ FAIL ✗ FAIL ✓ 5475 ms ✗ FAIL ✓ 7354 ms ✓ 5548 ms ✓ 5464 ms ✗ FAIL
mathd_numbertheory_233 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_1984_p6 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_2001_p6 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_321 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
induction_pprime_pdvdapowpma ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_229 ✓ 5066 ms ✓ 5012 ms ✗ FAIL ✓ 5367 ms ✓ 5118 ms ✓ 6765 ms ✓ 5294 ms ✓ 5155 ms ✓ 5190 ms
mathd_numbertheory_100 ✓ 4945 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7846 ms ✗ FAIL ✗ FAIL ✗ FAIL
amc12b_2002_p4 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12a_2002_p6 ✓ 5102 ms ✗ FAIL ✓ 5905 ms ✓ 5419 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_551 ✓ 5113 ms ✓ 5005 ms ✓ 5796 ms ✓ 5382 ms ✓ 5043 ms ✓ 6688 ms ✓ 5159 ms ✓ 5077 ms ✓ 5119 ms
mathd_algebra_304 ✓ 5088 ms ✓ 4969 ms ✗ FAIL ✓ 5345 ms ✓ 5067 ms ✓ 6648 ms ✓ 5106 ms ✓ 5115 ms ✓ 5156 ms
amc12a_2021_p8 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
algebra_ineq_nto1onlt2m1on ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_341 ✓ 5144 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5060 ms ✓ 6908 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_711 ✓ 5664 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12_2000_p1 ✓ 5110 ms ✗ FAIL ✗ FAIL ✓ 5340 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_212 ✓ 5162 ms ✓ 5082 ms ✗ FAIL ✓ 5393 ms ✓ 5116 ms ✓ 6924 ms ✓ 5255 ms ✓ 5317 ms ✓ 5218 ms
mathd_numbertheory_320 ✓ 5121 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7284 ms ✓ 5236 ms ✓ 5314 ms ✗ FAIL
mathd_algebra_125 ✓ 5172 ms ✗ FAIL ✗ FAIL ✓ 5409 ms ✗ FAIL ✓ 7479 ms ✓ 5311 ms ✓ 5315 ms ✗ FAIL
induction_11div10tonmn1ton ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_254 ✓ 4999 ms ✓ 5051 ms ✓ 5991 ms ✓ 5334 ms ✓ 4923 ms ✓ 6989 ms ✓ 5301 ms ✓ 5132 ms ✓ 5262 ms
amc12_2000_p6 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_2019_p1 ⏱ TIMEOUT ✗ FAIL ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
aime_1984_p7 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ⏱ TIMEOUT ✗ FAIL
numbertheory_3pow2pownm1mod2pownp3eq2pownp2 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_85 ✓ 5098 ms ✓ 5188 ms ✗ FAIL ✓ 5435 ms ✓ 5100 ms ✓ 6647 ms ✓ 5347 ms ✓ 5262 ms ✓ 5404 ms
amc12_2001_p21 ✓ 6660 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12b_2002_p2 ✓ 5182 ms ✗ FAIL ✗ FAIL ✓ 5281 ms ✓ 5093 ms ✓ 6670 ms ✗ FAIL ✓ 5265 ms ✗ FAIL
mathd_numbertheory_517 ✓ 5108 ms ✓ 5079 ms ✓ 5722 ms ✓ 5302 ms ✓ 4921 ms ✓ 6747 ms ✓ 5260 ms ✓ 5279 ms ✓ 5195 ms
mathd_numbertheory_521 ✓ 5187 ms ✗ FAIL ✗ FAIL ✓ 5280 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_289 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5318 ms ✓ 6796 ms ✗ FAIL ✗ FAIL ✗ FAIL
amc12a_2021_p3 ✓ 5017 ms ✗ FAIL ✗ FAIL ✓ 5295 ms ✗ FAIL ✓ 8232 ms ✓ 5144 ms ✓ 5117 ms ✗ FAIL
mathd_numbertheory_66 ✓ 4937 ms ✓ 4861 ms ✓ 5676 ms ✓ 5258 ms ✓ 5020 ms ✓ 6701 ms ✓ 5261 ms ✓ 5094 ms ✓ 5272 ms
mathd_numbertheory_235 ✓ 5103 ms ✓ 5115 ms ✓ 5747 ms ✓ 5277 ms ✓ 4980 ms ✓ 6709 ms ✓ 5246 ms ✓ 5102 ms ✓ 5150 ms
mathd_numbertheory_234 ✓ 5113 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_aoddbdiv4asqpbsqmod8eq1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_222 ✓ 5018 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8118 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_541 ✓ 5457 ms ✗ FAIL ✗ FAIL ✓ 5435 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_314 ✓ 4942 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4948 ms ✓ 7123 ms ✓ 5242 ms ✓ 5315 ms ✓ 5317 ms
mathd_numbertheory_150 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_296 ✓ 12747 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_exk2powkeqapb2mulbpa2_aeq1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_185 ✓ 5080 ms ✗ FAIL ✗ FAIL ✓ 5291 ms ✗ FAIL ✓ 8672 ms ✓ 5445 ms ✓ 5448 ms ✗ FAIL
mathd_numbertheory_582 ✓ 4966 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8143 ms ✓ 5482 ms ✓ 5303 ms ✗ FAIL

NNG4 · 108 theorems

Lean Natural Number Game

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster103/108 (95%)no change
500
blaster (only-optimize: 1)59/108 (55%)no change
0049
smt +model17/108 (16%)no change
0091
auto100/108 (93%)no change
008
aesop67/108 (62%)no change
0041
hammer103/108 (95%)no change
005
omega7/108 (6%)no change
00101
grind93/108 (86%)no change
0015
simp37/108 (34%)no change
0071
Explore theorem results 108 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
zero_add ✓ 1672 ms ✓ 1694 ms ✗ FAIL ✓ 2620 ms ✓ 1267 ms ✓ 3631 ms ✗ FAIL ✓ 1261 ms ✓ 1250 ms
succ_add ✓ 1796 ms ✗ FAIL ✗ FAIL ✓ 2004 ms ✗ FAIL ✓ 3040 ms ✓ 1256 ms ✓ 1214 ms ✗ FAIL
add_comm ✓ 1638 ms ✓ 1714 ms ✗ FAIL ✓ 2011 ms ✗ FAIL ✓ 2980 ms ✗ FAIL ✓ 1208 ms ✗ FAIL
add_assoc ✓ 1764 ms ✗ FAIL ✗ FAIL ✓ 1987 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✓ 1191 ms ✗ FAIL
add_right_comm ✓ 1725 ms ✗ FAIL ✗ FAIL ✓ 2015 ms ✗ FAIL ✓ 2912 ms ✗ FAIL ✓ 1371 ms ✗ FAIL
add_right_cancel ✓ 1729 ms ✓ 1699 ms ✗ FAIL ✓ 1983 ms ✓ 1244 ms ✓ 3004 ms ✗ FAIL ✓ 1228 ms ✓ 1185 ms
add_left_cancel ✓ 1746 ms ✓ 1704 ms ✗ FAIL ✓ 1995 ms ✓ 1234 ms ✓ 2810 ms ✗ FAIL ✓ 1221 ms ✓ 1226 ms
add_left_eq_self ✓ 1765 ms ✗ FAIL ✗ FAIL ✓ 2016 ms ✓ 1235 ms ✓ 2800 ms ✗ FAIL ✓ 1292 ms ✓ 1273 ms
add_right_eq_self ✓ 1719 ms ✗ FAIL ✗ FAIL ✓ 2013 ms ✓ 1233 ms ✓ 2846 ms ✗ FAIL ✓ 1272 ms ✓ 1247 ms
add_right_eq_zero ✓ 1749 ms ✗ FAIL ✗ FAIL ✓ 1973 ms ✓ 1260 ms ✓ 2921 ms ✗ FAIL ✓ 1290 ms ✗ FAIL
add_left_eq_zero ✓ 1733 ms ✗ FAIL ✗ FAIL ✓ 1984 ms ✓ 1280 ms ✓ 2823 ms ✗ FAIL ✓ 1239 ms ✓ 1214 ms
mul_le_mul_right ✓ 1746 ms ✗ FAIL ✗ FAIL ✓ 1989 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_left_ne_zero ✓ 1738 ms ✗ FAIL ✗ FAIL ✓ 2004 ms ✓ 1302 ms ✓ 2855 ms ✗ FAIL ✓ 1209 ms ✗ FAIL
eq_succ_of_ne_zero ✓ 1804 ms ✗ FAIL ✗ FAIL ✓ 2043 ms ✗ FAIL ✓ 3647 ms ✗ FAIL ✗ FAIL ✗ FAIL
one_le_of_ne_zero ✓ 1723 ms ✓ 1765 ms ✗ FAIL ✓ 1977 ms ✗ FAIL ✓ 2816 ms ✗ FAIL ✓ 1214 ms ✗ FAIL
le_mul_right ✓ 1858 ms ✗ FAIL ✗ FAIL ✓ 2004 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mul_right_eq_one ✓ 1773 ms ✗ FAIL ✗ FAIL ✓ 2008 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mul_ne_zero ✓ 1752 ms ✓ 1735 ms ✗ FAIL ✓ 2004 ms ✗ FAIL ✓ 3557 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_eq_zero ✓ 1826 ms ✗ FAIL ✗ FAIL ✓ 1989 ms ✗ FAIL ✓ 3226 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_left_cancel ✓ 1784 ms ✓ 1792 ms ✗ FAIL ✓ 2034 ms ✗ FAIL ✓ 3866 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_right_eq_self ✓ 1811 ms ✗ FAIL ✗ FAIL ✓ 2015 ms ✗ FAIL ✓ 6749 ms ✗ FAIL ✗ FAIL ✗ FAIL
add_left_comm ✓ 1844 ms ✗ FAIL ✗ FAIL ✓ 1999 ms ✗ FAIL ✓ 2954 ms ✗ FAIL ✓ 1217 ms ✗ FAIL
add_algo1 ✓ 1817 ms ✗ FAIL ✗ FAIL ✓ 1999 ms ✗ FAIL ✓ 3460 ms ✗ FAIL ✓ 1262 ms ✗ FAIL
add_algo2 ✓ 1830 ms ✗ FAIL ✗ FAIL ✓ 2001 ms ✗ FAIL ✓ 4173 ms ✗ FAIL ✓ 1282 ms ✗ FAIL
add_algo3 ✓ 1822 ms ✗ FAIL ✗ FAIL ✓ 2014 ms ✗ FAIL ✓ 3988 ms ✗ FAIL ✓ 1321 ms ✗ FAIL
pred05 ✓ 1725 ms ✓ 1676 ms ✗ FAIL ✓ 2003 ms ✓ 1231 ms ✓ 2898 ms ✗ FAIL ✓ 1350 ms ✗ FAIL
succ_ne_zero ✓ 1695 ms ✓ 1739 ms ✗ FAIL ✓ 1984 ms ✓ 1235 ms ✓ 2793 ms ✓ 1342 ms ✓ 1321 ms ✓ 1333 ms
succ_ne_succ ✓ 1749 ms ✓ 1700 ms ✗ FAIL ✓ 1993 ms ✓ 1265 ms ✓ 2925 ms ✗ FAIL ✓ 1335 ms ✗ FAIL
decide ✓ 1725 ms ✓ 1684 ms ✗ FAIL ✓ 1998 ms ✓ 1245 ms ✓ 2982 ms ✗ FAIL ✓ 1317 ms ✓ 1310 ms
decide2 ✓ 1685 ms ✓ 1713 ms ✗ FAIL ✓ 1998 ms ✓ 1264 ms ✓ 2989 ms ✗ FAIL ✓ 1324 ms ✓ 1308 ms
exact ✓ 1716 ms ✓ 1713 ms ✗ FAIL ✓ 2014 ms ✓ 1272 ms ✓ 3016 ms ✓ 1262 ms ✓ 1270 ms ✗ FAIL
exact2 ✓ 1711 ms ✓ 1668 ms ✗ FAIL ✓ 2021 ms ✓ 1251 ms ✓ 2905 ms ✗ FAIL ✓ 1319 ms ✗ FAIL
apply ✓ 1675 ms ✓ 1709 ms ✗ FAIL ✓ 1983 ms ✓ 1249 ms ✓ 2930 ms ✗ FAIL ✓ 1338 ms ✗ FAIL
succ_inj ✓ 1759 ms ✓ 1701 ms ✗ FAIL ✓ 2055 ms ✓ 1241 ms ✓ 2887 ms ✗ FAIL ✓ 1300 ms ✗ FAIL
succ_inj2 ✓ 1737 ms ✓ 1793 ms ✗ FAIL ✓ 1998 ms ✓ 1254 ms ✓ 3016 ms ✗ FAIL ✓ 1337 ms ✗ FAIL
intro ✓ 1772 ms ✓ 1764 ms ✗ FAIL ✓ 2008 ms ✓ 1255 ms ✓ 2986 ms ✗ FAIL ✓ 1349 ms ✓ 1337 ms
intro2 ✓ 1704 ms ✓ 1757 ms ✗ FAIL ✓ 1988 ms ✓ 1321 ms ✓ 3046 ms ✗ FAIL ✓ 1310 ms ✓ 1302 ms
NE ✓ 1736 ms ✓ 1777 ms ✗ FAIL ✓ 1972 ms ✓ 1305 ms ✓ 3057 ms ✗ FAIL ✓ 1305 ms ✗ FAIL
zero_ne_one ✓ 1660 ms ✓ 1759 ms ✗ FAIL ✓ 1968 ms ✓ 1275 ms ✓ 2987 ms ✗ FAIL ✓ 1310 ms ✓ 1318 ms
one_ne_zero ✓ 1762 ms ✓ 1772 ms ✗ FAIL ✓ 1971 ms ✓ 1303 ms ✓ 2954 ms ✗ FAIL ✓ 1270 ms ✓ 1307 ms
two_add_two_ne_five ✓ 1785 ms ✓ 1735 ms ✓ 1972 ms ✓ 2008 ms ✓ 1309 ms ✓ 3040 ms ✓ 1305 ms ✓ 1304 ms ✓ 1317 ms
le_refl ✓ 1762 ms ✓ 1769 ms ✗ FAIL ✓ 1976 ms ✓ 1259 ms ✓ 2840 ms ✗ FAIL ✓ 1310 ms ✓ 1293 ms
zero_le ✓ 1765 ms ✓ 1778 ms ✗ FAIL ✓ 1988 ms ✓ 1258 ms ✓ 2950 ms ✗ FAIL ✓ 1299 ms ✓ 1270 ms
le_succ_self ✓ 1811 ms ✓ 1784 ms ✗ FAIL ✓ 1999 ms ✓ 1261 ms ✓ 3021 ms ✗ FAIL ✓ 1378 ms ✓ 1313 ms
le_trans ✓ 1737 ms ✗ FAIL ✗ FAIL ✓ 2017 ms ✗ FAIL ✓ 2989 ms ✗ FAIL ✓ 1307 ms ✗ FAIL
le_zero ✓ 1789 ms ✓ 1742 ms ✗ FAIL ✓ 2009 ms ✓ 1259 ms ✓ 3011 ms ✗ FAIL ✓ 1278 ms ✗ FAIL
le_antisymm ✓ 1817 ms ✗ FAIL ✗ FAIL ✓ 2034 ms ✗ FAIL ✓ 2932 ms ✗ FAIL ✓ 1343 ms ✗ FAIL
or_symm ✓ 1807 ms ✓ 1781 ms ✗ FAIL ✓ 2014 ms ✓ 1291 ms ✓ 3010 ms ✗ FAIL ✓ 1331 ms ✗ FAIL
le_total ✓ 1810 ms ✗ FAIL ✗ FAIL ✓ 2027 ms ✗ FAIL ✓ 3053 ms ✗ FAIL ✓ 1314 ms ✗ FAIL
succ_le_succ ✓ 1730 ms ✓ 1762 ms ✗ FAIL ✓ 2018 ms ✓ 1317 ms ✓ 3311 ms ✗ FAIL ✓ 1304 ms ✗ FAIL
le_one ✓ 1810 ms ✗ FAIL ✗ FAIL ✓ 2001 ms ✗ FAIL ✓ 3902 ms ✗ FAIL ✓ 1306 ms ✗ FAIL
le_two ✓ 1805 ms ✗ FAIL ✗ FAIL ✓ 2003 ms ✗ FAIL ✓ 4352 ms ✗ FAIL ✓ 1298 ms ✗ FAIL
one_add_le_self ✓ 1665 ms ✓ 1667 ms ✗ FAIL ✓ 1997 ms ✓ 1336 ms ✓ 3124 ms ✗ FAIL ✓ 1316 ms ✓ 1293 ms
refl ✓ 1682 ms ✓ 1719 ms ✗ FAIL ✓ 2006 ms ✓ 1396 ms ✓ 3140 ms ✗ FAIL ✓ 1283 ms ✓ 1321 ms
le_implies_le_plus_one ✓ 1777 ms ✗ FAIL ✗ FAIL ✓ 2023 ms ✗ FAIL ✓ 3145 ms ✗ FAIL ✓ 1316 ms ✗ FAIL
mul_one ✓ 1672 ms ✓ 1677 ms ✗ FAIL ✓ 2023 ms ✓ 1318 ms ✓ 3171 ms ✗ FAIL ✓ 1277 ms ✓ 1288 ms
zero_mul ✓ 1690 ms ✓ 1699 ms ✗ FAIL ✓ 2005 ms ✓ 1295 ms ✓ 3058 ms ✗ FAIL ✓ 1323 ms ✓ 1300 ms
succ_mul ✓ 1753 ms ✗ FAIL ✗ FAIL ✓ 1996 ms ✗ FAIL ✓ 3175 ms ✗ FAIL ✓ 1333 ms ✗ FAIL
mul_comm ✓ 1646 ms ✓ 1646 ms ✗ FAIL ✓ 1999 ms ✗ FAIL ✓ 2942 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
one_mul ✓ 1694 ms ✓ 1678 ms ✗ FAIL ✓ 2020 ms ✓ 1279 ms ✓ 2966 ms ✗ FAIL ✓ 1309 ms ✓ 1331 ms
two_mul ✓ 1696 ms ✗ FAIL ✗ FAIL ✓ 2067 ms ✗ FAIL ✓ 4583 ms ✗ FAIL ✓ 1289 ms ✗ FAIL
mul_add ✓ 1720 ms ✗ FAIL ✗ FAIL ✓ 2042 ms ✗ FAIL ✓ 3085 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
add_mul ✓ 1743 ms ✗ FAIL ✗ FAIL ✓ 2048 ms ✗ FAIL ✓ 3097 ms ✗ FAIL ✓ 1335 ms ✗ FAIL
mul_assoc ✓ 1805 ms ✗ FAIL ✗ FAIL ✓ 2043 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✓ 1323 ms ✗ FAIL
product_not_zero_of_not_zero ✓ 1711 ms ✓ 1721 ms ✗ FAIL ✓ 2055 ms ✗ FAIL ✓ 3399 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.eq_zero_or_eq_zero_of_mul_eq_zero ✓ 1826 ms ✗ FAIL ✗ FAIL ✓ 2009 ms ✗ FAIL ✓ 3213 ms ✗ FAIL ✗ FAIL ✗ FAIL
product_zero_iff_zero ✓ 1817 ms ✗ FAIL ✗ FAIL ✓ 2017 ms ✗ FAIL ✓ 4038 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.mul_left_cancel ✓ 1748 ms ✓ 1725 ms ✗ FAIL ✓ 2024 ms ✗ FAIL ✓ 3993 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.mul_left_comm ✓ 1765 ms ✗ FAIL ✗ FAIL ✓ 2018 ms ✗ FAIL ✓ 3541 ms ✗ FAIL ✓ 1309 ms ✗ FAIL
P_and_Q_implies_PANDQ ✓ 1718 ms ✓ 1747 ms ✗ FAIL ✓ 1986 ms ✓ 1335 ms ✓ 2929 ms ✗ FAIL ✓ 1313 ms ✗ FAIL
and_symm ✓ 1756 ms ✓ 1726 ms ✓ 2006 ms ✓ 1952 ms ✓ 1333 ms ✓ 2960 ms ✗ FAIL ✓ 1277 ms ✗ FAIL
and_trans ✓ 1735 ms ✓ 1727 ms ✓ 2015 ms ✓ 1955 ms ✓ 1340 ms ✓ 2933 ms ✗ FAIL ✓ 1284 ms ✗ FAIL
iff_trans ✓ 1729 ms ✗ FAIL ✓ 2034 ms ✓ 1962 ms ✓ 1326 ms ✓ 3007 ms ✗ FAIL ✓ 1261 ms ✗ FAIL
Q_implies_PORQ ✓ 1748 ms ✓ 1780 ms ✓ 1988 ms ✓ 1969 ms ✓ 1340 ms ✓ 2907 ms ✗ FAIL ✓ 1274 ms ✗ FAIL
or_trans ✓ 1750 ms ✓ 1755 ms ✓ 1999 ms ✓ 1973 ms ✓ 1329 ms ✓ 2930 ms ✗ FAIL ✓ 1268 ms ✗ FAIL
and_or_distrib_left ✓ 1821 ms ✗ FAIL ✓ 1989 ms ✓ 1973 ms ✓ 1321 ms ✓ 3083 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
contra ✓ 1724 ms ✓ 1741 ms ✓ 1958 ms ✓ 1998 ms ✓ 1390 ms ✓ 2999 ms ✗ FAIL ✓ 1305 ms ✓ 1292 ms
implies_trad ✓ 1797 ms ✗ FAIL ✓ 1983 ms ✓ 2018 ms ✓ 1372 ms ✓ 2997 ms ✗ FAIL ✓ 1269 ms ✗ FAIL
level01 ✓ 1794 ms ✓ 1748 ms ✗ FAIL ✓ 2032 ms ✓ 1327 ms ✗ FAIL ✗ FAIL ✓ 1327 ms ✗ FAIL
level02 ✓ 1756 ms ✓ 1729 ms ✓ 1969 ms ✓ 2022 ms ✓ 1340 ms ✓ 2900 ms ✗ FAIL ✓ 1306 ms ✓ 1314 ms
level03 ✓ 1697 ms ✓ 1767 ms ✗ FAIL ✓ 2012 ms ✓ 1334 ms ✓ 2987 ms ✗ FAIL ✓ 1280 ms ✗ FAIL
level04 ✓ 1742 ms ✓ 1730 ms ✗ FAIL ✓ 2022 ms ✓ 1349 ms ✓ 2981 ms ✗ FAIL ✓ 1245 ms ✗ FAIL
level05 ✓ 1647 ms ✓ 1706 ms ✓ 1976 ms ✓ 1995 ms ✓ 1366 ms ✓ 2954 ms ✗ FAIL ✓ 1287 ms ✗ FAIL
level06 ✓ 1746 ms ✗ FAIL ✓ 2009 ms ✓ 2000 ms ✓ 1322 ms ✓ 2778 ms ✗ FAIL ✓ 1232 ms ✗ FAIL
level07 ✓ 1806 ms ✗ FAIL ✓ 2048 ms ✓ 2008 ms ✓ 1336 ms ✓ 2965 ms ✗ FAIL ✓ 1268 ms ✗ FAIL
level08 ✓ 1812 ms ✗ FAIL ✓ 2037 ms ✓ 1989 ms ✓ 1337 ms ✓ 2976 ms ✗ FAIL ✓ 1304 ms ✗ FAIL
level09 ✓ 1812 ms ✗ FAIL ✗ FAIL ✓ 2031 ms ✓ 1341 ms ✓ 2962 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
zero_pow_zero ✓ 1792 ms ✓ 1740 ms ✗ FAIL ✓ 2034 ms ✓ 1328 ms ✓ 2884 ms ✗ FAIL ✓ 1320 ms ✓ 1301 ms
zero_pow_any ✓ 1836 ms ✗ FAIL ✗ FAIL ✓ 2031 ms ✓ 1328 ms ✓ 2866 ms ✗ FAIL ✓ 1258 ms ✓ 1273 ms
any_pow_one ✓ 1787 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1349 ms ✓ 2945 ms ✗ FAIL ✓ 1293 ms ✓ 1292 ms
one_pow_any ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1354 ms ✓ 2864 ms ✗ FAIL ✓ 1299 ms ✓ 1296 ms
pow_two ✓ 1769 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2796 ms ✗ FAIL ✓ 1294 ms ✗ FAIL
pow_add ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2887 ms ✗ FAIL ✓ 1293 ms ✗ FAIL
mul_pow ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2819 ms ✗ FAIL ✗ FAIL ✗ FAIL
pow_pow ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4154 ms ✗ FAIL ✗ FAIL ✗ FAIL
add_sq ✓ 1830 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4194 ms ✗ FAIL ✓ 1340 ms ✗ FAIL
level10 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
level01rfl ✓ 1785 ms ✓ 1790 ms ✗ FAIL ✓ 2019 ms ✓ 1431 ms ✗ FAIL ✗ FAIL ✓ 1311 ms ✓ 1313 ms
level02rw ✓ 1818 ms ✓ 1784 ms ✗ FAIL ✓ 1991 ms ✓ 1387 ms ✓ 2805 ms ✗ FAIL ✓ 1322 ms ✗ FAIL
level03_two_eq_succ_succ_zero ✓ 1747 ms ✓ 1767 ms ✓ 2037 ms ✓ 1967 ms ✓ 1400 ms ✓ 2791 ms ✓ 1295 ms ✓ 1224 ms ✓ 1218 ms
level04_rw_backwards ✓ 1769 ms ✓ 1748 ms ✓ 2037 ms ✓ 1961 ms ✓ 1375 ms ✓ 2820 ms ✓ 1282 ms ✓ 1269 ms ✓ 1276 ms
level05_add_zero ✓ 1761 ms ✓ 1781 ms ✗ FAIL ✓ 1966 ms ✓ 1425 ms ✓ 2837 ms ✗ FAIL ✓ 1311 ms ✓ 1249 ms
level06_add_zero2 ✓ 1773 ms ✓ 1793 ms ✗ FAIL ✓ 1972 ms ✓ 1389 ms ✓ 2891 ms ✗ FAIL ✓ 1271 ms ✓ 1269 ms
succ_eq_add_one ✓ 1753 ms ✓ 1754 ms ✓ 1949 ms ✓ 1980 ms ✓ 1411 ms ✓ 2872 ms ✓ 1317 ms ✓ 1304 ms ✓ 1269 ms
level08_two_add_two ✓ 1764 ms ✓ 1734 ms ✗ FAIL ✓ 1979 ms ✓ 1431 ms ✓ 3007 ms ✗ FAIL ✓ 1334 ms ✓ 1331 ms
l11_accrfl ✓ 1756 ms ✗ FAIL ✗ FAIL ✓ 1980 ms ✗ FAIL ✓ 3913 ms ✗ FAIL ✓ 1367 ms ✗ FAIL
decide01 ✓ 1695 ms ✓ 1635 ms ✗ FAIL ✓ 1963 ms ✓ 1457 ms ✓ 2786 ms ✗ FAIL ✓ 1253 ms ✓ 1252 ms
decode02 ✓ 1661 ms ✓ 1672 ms ✗ FAIL ✓ 1970 ms ✓ 1410 ms ✓ 2774 ms ✗ FAIL ✓ 1300 ms ✓ 1326 ms

STG4 · 52 theorems

Lean Set Theory Game

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster49/52 (94%)no change
201
blaster (only-optimize: 1)13/52 (25%)no change
0039
smt +model0/52 (0%)no change
0052
auto4/52 (8%)no change
0048
aesop35/52 (67%)no change
0017
hammer47/52 (90%)no change
005
omega1/52 (2%)no change
0051
grind41/52 (79%)no change
209
simp15/52 (29%)no change
0037
Explore theorem results 52 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
compl_union ✓ 2002 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1737 ms ✓ 2919 ms ✗ FAIL ✓ 1828 ms ✓ 1905 ms
compl_inter ✓ 1936 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2862 ms ✗ FAIL ✓ 1882 ms ✗ FAIL
inter_distrib_left ✓ 2009 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1777 ms ✓ 2897 ms ✗ FAIL ✓ 1929 ms ✗ FAIL
union_distrib_left ✓ 1973 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1756 ms ✓ 2965 ms ✗ FAIL ✓ 1865 ms ✗ FAIL
union_sub_inter_sub ✓ 1942 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4949 ms ✗ FAIL ✗ FAIL ✗ FAIL
contra ✓ 1947 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3416 ms ✗ FAIL ✓ 1924 ms ✗ FAIL
mem_compl_iff ✓ 1904 ms ✓ 1893 ms ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 2964 ms ✗ FAIL ✓ 1825 ms ✓ 1830 ms
compl_subset_compl_of_subs ✓ 1942 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1737 ms ✓ 2998 ms ✗ FAIL ✓ 1862 ms ✓ 1803 ms
compl_compl2 ✓ 1926 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1752 ms ✓ 2932 ms ✗ FAIL ✓ 1829 ms ✓ 1842 ms
comp_sub_iff ✓ 1924 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1718 ms ✓ 2988 ms ✗ FAIL ✗ FAIL ✓ 1882 ms
helloWorld ✓ 1954 ms ✗ FAIL ✗ FAIL ✓ 2248 ms ✓ 1725 ms ✓ 3048 ms ✓ 1895 ms ✓ 1899 ms ✗ FAIL
comp_union ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
comp_inter ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
common_elt ✓ 1998 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4799 ms ✗ FAIL ✗ FAIL ✗ FAIL
three_fam ✓ 1974 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4404 ms ✗ FAIL ✓ 1931 ms ✗ FAIL
union_int_comp_union ✓ 1976 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 10146 ms ✗ FAIL ✓ 1900 ms ✗ FAIL
union_int_union ✓ 1980 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
union_int_comp_int ✓ 1988 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ⏱ TIMEOUT ✗ FAIL
singleton ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
inter_sub ✓ 1998 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2982 ms ✗ FAIL ✓ 1870 ms ✗ FAIL
inter_sub_inter ✓ 1974 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3065 ms ✗ FAIL ✓ 1794 ms ✗ FAIL
inter_pair ✓ 2020 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1695 ms ✓ 2988 ms ✗ FAIL ✓ 1812 ms ✓ 1770 ms
inter_union ✓ 1992 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1755 ms ✓ 2941 ms ✗ FAIL ✓ 1818 ms ✗ FAIL
sub_inter ✓ 1981 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 3172 ms ✗ FAIL ✓ 1800 ms ✓ 1789 ms
eltwise_union ✓ 1936 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3083 ms ✗ FAIL ✗ FAIL ✗ FAIL
prove_exists ✓ 1927 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1725 ms ✓ 2844 ms ✗ FAIL ✗ FAIL ✗ FAIL
sub_union ✓ 1966 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2992 ms ✗ FAIL ✓ 1842 ms ✗ FAIL
union_sub_union ✓ 1959 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3007 ms ✗ FAIL ✓ 1818 ms ✗ FAIL
union_pair ✓ 2019 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1718 ms ✓ 2985 ms ✗ FAIL ✓ 1850 ms ✓ 1793 ms
union_union ✓ 1923 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1966 ms ✓ 2976 ms ✗ FAIL ✓ 1839 ms ✗ FAIL
union_sub ✓ 2000 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1707 ms ✓ 2916 ms ✗ FAIL ✓ 1838 ms ✓ 1822 ms
eltwise_inter ✓ 2015 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1821 ms ✓ 3130 ms ✗ FAIL ⏱ TIMEOUT ✗ FAIL
and_thm ✓ 1859 ms ✓ 1885 ms ✗ FAIL ✓ 2272 ms ✓ 1681 ms ✓ 2809 ms ✗ FAIL ✓ 1784 ms ✗ FAIL
elt_inter_elt_right ✓ 1889 ms ✓ 1972 ms ✗ FAIL ✗ FAIL ✓ 1678 ms ✓ 2957 ms ✗ FAIL ✓ 1821 ms ✗ FAIL
inter_sub_left ✓ 1889 ms ✓ 1917 ms ✗ FAIL ✗ FAIL ✓ 1728 ms ✓ 2789 ms ✗ FAIL ✓ 1834 ms ✓ 1853 ms
prove_and ✓ 1894 ms ✓ 1873 ms ✗ FAIL ✗ FAIL ✓ 1698 ms ✓ 2809 ms ✗ FAIL ✓ 1853 ms ✗ FAIL
sub_int ✓ 1986 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1672 ms ✓ 2781 ms ✗ FAIL ✓ 1862 ms ✗ FAIL
inter_subset_swap ✓ 1867 ms ✓ 1856 ms ✗ FAIL ✗ FAIL ✓ 1717 ms ✓ 2789 ms ✗ FAIL ✓ 1857 ms ✓ 1845 ms
inter_comm ✓ 1885 ms ✓ 1903 ms ✗ FAIL ✗ FAIL ✓ 1695 ms ✓ 2813 ms ✗ FAIL ✓ 1875 ms ✗ FAIL
inter_assoc ✓ 1919 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1704 ms ✓ 2842 ms ✗ FAIL ✓ 1788 ms ✗ FAIL
subset_exact ✓ 1889 ms ✓ 1890 ms ✗ FAIL ✓ 2202 ms ✓ 1639 ms ✓ 2759 ms ✗ FAIL ✓ 1781 ms ✓ 1779 ms
sub_hyp ✓ 1919 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 2730 ms ✗ FAIL ✓ 1838 ms ✗ FAIL
subset_have ✓ 1975 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1659 ms ✓ 2840 ms ✗ FAIL ✓ 1899 ms ✗ FAIL
subset_imp ✓ 1923 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1663 ms ✓ 2752 ms ✗ FAIL ✓ 1892 ms ✗ FAIL
Subset.refl ✓ 1863 ms ✓ 1925 ms ✗ FAIL ✗ FAIL ✓ 1619 ms ✓ 2758 ms ✗ FAIL ✓ 1881 ms ✓ 1849 ms
Subset.trans ✓ 1968 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2801 ms ✗ FAIL ✓ 1914 ms ✗ FAIL
union_or ✓ 1916 ms ✓ 1885 ms ✗ FAIL ✓ 2204 ms ✓ 1627 ms ✓ 2755 ms ✗ FAIL ✓ 1929 ms ✗ FAIL
sub_union_2 ✓ 1944 ms ✓ 1921 ms ✗ FAIL ✗ FAIL ✓ 1660 ms ✓ 2763 ms ✗ FAIL ✓ 1925 ms ✓ 1938 ms
union_cases ✓ 1931 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1631 ms ✓ 2812 ms ✗ FAIL ✓ 1903 ms ✗ FAIL
union_subset_swap ✓ 1900 ms ✓ 1883 ms ✗ FAIL ✗ FAIL ✓ 1677 ms ✓ 2715 ms ✗ FAIL ✓ 1845 ms ✓ 1887 ms
union_comm ✓ 1876 ms ✓ 1879 ms ✗ FAIL ✗ FAIL ✓ 1687 ms ✓ 2781 ms ✗ FAIL ✓ 1901 ms ✗ FAIL
union_assoc ✓ 1976 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1645 ms ✓ 2811 ms ✗ FAIL ✓ 1861 ms ✗ FAIL

UPLCDepth · 7 theorems

UPLC concrete evaluation (growing computation)

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster6/7 (86%)no change
100
blaster (only-optimize: 1)6/7 (86%)no change
100
smt +model0/7 (0%)no change
007
auto0/7 (0%)no change
007
aesop7/7 (100%)no change
000
hammer6/7 (86%)no change
001
omega0/7 (0%)no change
007
grind0/7 (0%)no change
007
simp0/7 (0%)no change
007
Explore theorem results 7 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
d_sum_1024 ✓ 8220 ms ✓ 8161 ms ✗ FAIL ✗ FAIL ✓ 3109 ms ✓ 4518 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_16 ✓ 2069 ms ✓ 2093 ms ✗ FAIL ✗ FAIL ✓ 1549 ms ✓ 3079 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_16384 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✓ 31881 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_256 ✓ 3514 ms ✓ 3476 ms ✗ FAIL ✗ FAIL ✓ 1818 ms ✓ 3376 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_4 ✓ 1974 ms ✓ 2004 ms ✗ FAIL ✗ FAIL ✓ 1484 ms ✓ 2969 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_4096 ✓ 27228 ms ✓ 26822 ms ✗ FAIL ✗ FAIL ✓ 8398 ms ✓ 8090 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_64 ✓ 2331 ms ✓ 2334 ms ✗ FAIL ✗ FAIL ✓ 1586 ms ✓ 3054 ms ✗ FAIL ✗ FAIL ✗ FAIL

UPLCWidth · 6 theorems

UPLC symbolic correctness (growing expressions)

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster6/6 (100%)no change
000
blaster (only-optimize: 1)6/6 (100%)no change
000
smt +model0/6 (0%)no change
006
auto6/6 (100%)no change
000
aesop6/6 (100%)no change
000
hammer6/6 (100%)no change
000
omega0/6 (0%)no change
006
grind0/6 (0%)no change
006
simp0/6 (0%)no change
006
Explore theorem results 6 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
w1_add ✓ 1975 ms ✓ 1975 ms ✗ FAIL ✓ 2383 ms ✓ 1504 ms ✓ 4421 ms ✗ FAIL ✗ FAIL ✗ FAIL
w2_mul_distr ✓ 1990 ms ✓ 2044 ms ✗ FAIL ✓ 2443 ms ✓ 1545 ms ✓ 3207 ms ✗ FAIL ✗ FAIL ✗ FAIL
w3_mul_over_add ✓ 2013 ms ✓ 2012 ms ✗ FAIL ✓ 2450 ms ✓ 1503 ms ✓ 3276 ms ✗ FAIL ✗ FAIL ✗ FAIL
w4_linear ✓ 2014 ms ✓ 2007 ms ✗ FAIL ✓ 2418 ms ✓ 1519 ms ✓ 3197 ms ✗ FAIL ✗ FAIL ✗ FAIL
w5_quadratic ✓ 2100 ms ✓ 1995 ms ✗ FAIL ✓ 2434 ms ✓ 1523 ms ✓ 3095 ms ✗ FAIL ✗ FAIL ✗ FAIL
w6_sum6 ✓ 2051 ms ✓ 2011 ms ✗ FAIL ✓ 2457 ms ✓ 1547 ms ✓ 3172 ms ✗ FAIL ✗ FAIL ✗ FAIL

Verina · 108 theorems

Verified-programming specs (Verina, basic)

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster26/108 (24%)no change
13069
blaster (only-optimize: 1)11/108 (10%)no change
4093
smt +model1/108 (1%)no change
0899
auto4/108 (4%)no change
0896
aesop2/108 (2%)no change
0898
hammer7/108 (6%)no change
0893
omega1/108 (1%)no change
0899
grind1/108 (1%)no change
0899
simp0/108 (0%)no change
08100
Explore theorem results 108 goals × 9 tactics
theorem
blaster
v4.24.0 · b729d1014
blaster (only-optimize: 1)
v4.24.0 · b729d1014
smt +model
v4.34.0 · 79ef7b3d5
auto
v4.34.1 · 6544cf60e
aesop
v4.35.0 · (via mathlib)
hammer
v4.34.0 · 93734d624
omega
v4.35.0 · (core)
grind
v4.35.0 · (core)
simp
v4.35.0 · (core)
verina_basic_1 ✓ 5084 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_10 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_100 ✓ 5064 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_101 ✓ 1719 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_102 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_103 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_104 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_105 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_106 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_107 ✓ 1731 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_108 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_11 ✓ 1827 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_12 ✓ 1683 ms ✓ 1731 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_13 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_14 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_15 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_16 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_17 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_18 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_19 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_2 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_20 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_21 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_22 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_23 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_24 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_25 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_26 ✓ 1677 ms ✓ 1690 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_27 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_28 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_29 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_3 ✓ 5121 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_30 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_31 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_32 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_33 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_34 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_35 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_36 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_37 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_38 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_39 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_4 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_40 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_41 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_42 ✓ 1699 ms ✓ 1804 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7273 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_43 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_44 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_45 ✓ 1828 ms ✓ 1852 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_46 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_47 ✓ 1783 ms ✗ FAIL ✓ 2120 ms ✓ 2171 ms ✓ 1378 ms ✓ 2905 ms ✓ 1300 ms ✓ 1269 ms ✗ FAIL
verina_basic_48 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_49 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_5 ✓ 1687 ms ✓ 1693 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4580 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_50 ✓ 4918 ms ✓ 4926 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_51 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_52 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_53 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_54 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_55 ✓ 1641 ms ✓ 1686 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_56 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_57 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_58 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_59 ✓ 1634 ms ✓ 1639 ms ✗ FAIL ✓ 2163 ms ✓ 1326 ms ✓ 2886 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_6 ✓ 5011 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_60 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_61 ⏱ TIMEOUT ⏱ TIMEOUT ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_62 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_63 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_64 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_65 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_66 ✓ 5228 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_67 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_68 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_69 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_7 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_70 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_71 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_72 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_73 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_74 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_75 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_76 ✓ 1804 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_77 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_78 ✓ 1736 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_79 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_8 ✓ 1680 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4762 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_80 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_81 ✓ 5271 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_82 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_83 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_84 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_85 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_86 ✗ FAIL ✗ FAIL ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV ⊘ ENV
verina_basic_87 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_88 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_89 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_9 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_90 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_91 ✓ 1686 ms ✓ 1676 ms ✗ FAIL ✓ 2208 ms ✗ FAIL ✓ 3269 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_92 ✓ 1762 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_93 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_94 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_95 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_96 ✓ 1654 ms ✓ 1685 ms ✗ FAIL ✓ 2215 ms ✗ FAIL ✓ 3496 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_97 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_98 ✓ 1670 ms ✓ 1664 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_99 ✓ 5119 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL

Reading these results fairly

Tip: click any cell for its status and (for ENV) the exact Lean error.