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-26 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 blaster 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
2blaster478/671 (71%)+1 −0
3grind409/671 (61%)no change
4auto380/671 (57%)no change
5aesop377/671 (56%)no change
6blaster (only-optimize: 1)253/671 (38%)+1 −0
7simp164/671 (24%)no change
8smt +model114/671 (17%)no change
9omega80/671 (12%)no change

Versions run

tacticbranchtoolchaincommitbuild
blastermainleanprover/lean4:v4.24.0a16614e5eOK
blaster (only-optimize: 1)mainleanprover/lean4:v4.24.0a16614e5eOK
smt +modelmainleanprover/lean4:v4.34.0db545bebeCACHED
automainleanprover/lean4:v4.35.030f46ddb9OK
aesopstableleanprover/lean4:v4.35.0(via mathlib)CACHED
hammermainleanprover/lean4:v4.34.093734d624CACHED
omegastableleanprover/lean4:v4.35.0(core)CACHED
grindstableleanprover/lean4:v4.35.0(core)CACHED
simpstableleanprover/lean4:v4.35.0(core)CACHED

Suite details

Home turf categories

Aesop · 50 theorems

Aesop test goals

Source ↗
tacticsolvedsince last runbreakdowntimeoutenvfail
blaster28/50 (56%)no change
3019
blaster (only-optimize: 1)10/50 (20%)no change
0040
smt +model5/50 (10%)no change
0045
auto28/50 (56%)no change
0022
aesop40/50 (80%)no change
0010
hammer47/50 (94%)no change
003
omega6/50 (12%)no change
0044
grind44/50 (88%)no change
006
simp13/50 (26%)no change
0037
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
aesop_l43 ✓ 1287 ms ✓ 1340 ms ✓ 1823 ms ✓ 2148 ms ✓ 1154 ms ✓ 2665 ms ✓ 771 ms ✓ 803 ms ✓ 775 ms
aesop_l80 ✓ 1444 ms ✗ FAIL ✗ FAIL ✓ 2174 ms ✓ 1189 ms ✓ 2735 ms ✗ FAIL ✓ 774 ms ✗ FAIL
auxdecl_l32 ✗ FAIL ✗ FAIL ✓ 1886 ms ✓ 2155 ms ✗ FAIL ✓ 3025 ms ✗ FAIL ✓ 800 ms ✗ FAIL
bigstep_l62 ✓ 1358 ms ✗ FAIL ✗ FAIL ✓ 2124 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 ✓ 1396 ms ✓ 1380 ms ✗ FAIL ✓ 2125 ms ✓ 1295 ms ✓ 2759 ms ✗ FAIL ✓ 768 ms ✗ FAIL
constructorequations_l17 ✓ 1383 ms ✓ 1347 ms ✗ FAIL ✓ 2162 ms ✓ 1192 ms ✓ 2813 ms ✗ FAIL ✓ 771 ms ✗ FAIL
constructorequations_l20 ✓ 1349 ms ✗ FAIL ✗ FAIL ✓ 2193 ms ✓ 1161 ms ✓ 2836 ms ✗ FAIL ✓ 775 ms ✗ FAIL
destructproducts_l48 ✓ 1403 ms ✓ 1328 ms ✗ FAIL ✓ 2184 ms ✓ 1163 ms ✓ 2703 ms ✗ FAIL ✓ 765 ms ✗ FAIL
equality_chain ✓ 1397 ms ✗ FAIL ✗ FAIL ✓ 2166 ms ✓ 1195 ms ✓ 2710 ms ✗ FAIL ✓ 770 ms ✗ FAIL
erasesimp_l12 ✓ 1338 ms ✓ 1370 ms ✓ 1872 ms ✓ 2186 ms ✗ FAIL ✓ 2785 ms ✓ 775 ms ✓ 767 ms ✗ FAIL
ext_l12 ✓ 1451 ms ✗ FAIL ✗ FAIL ✓ 2205 ms ✓ 1171 ms ✓ 2864 ms ✗ FAIL ✓ 782 ms ✗ FAIL
ext_l9 ✓ 1415 ms ✗ FAIL ✗ FAIL ✓ 2190 ms ✓ 1225 ms ✓ 2688 ms ✗ FAIL ✓ 770 ms ✗ FAIL
indent_l13 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
list_l194 ✓ 1394 ms ✓ 1341 ms ✗ FAIL ✓ 2165 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 ✓ 1469 ms ✗ FAIL ✗ FAIL ✓ 2206 ms ✓ 1190 ms ✓ 2787 ms ✗ FAIL ✓ 767 ms ✗ FAIL
list_l207 ✓ 1426 ms ✗ FAIL ✗ FAIL ✓ 2152 ms ✓ 1219 ms ✓ 2745 ms ✗ FAIL ✓ 781 ms ✓ 769 ms
list_l215 ✓ 1461 ms ✗ FAIL ✗ FAIL ✓ 2179 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 ✓ 1356 ms ✓ 1431 ms ✗ FAIL ✓ 2226 ms ✓ 1247 ms ✓ 2778 ms ✗ FAIL ✗ FAIL ✓ 765 ms
list_l93 ✓ 1426 ms ✓ 1318 ms ✗ FAIL ✗ FAIL ✓ 1227 ms ✓ 2779 ms ✗ FAIL ✓ 763 ms ✓ 767 ms
metas_l14 ✓ 1430 ms ✗ FAIL ✗ FAIL ✓ 2156 ms ✓ 1216 ms ✓ 2964 ms ✗ FAIL ✓ 771 ms ✗ FAIL
metas_l23 ✓ 1444 ms ✗ FAIL ✗ FAIL ✓ 2141 ms ✓ 1302 ms ✓ 2859 ms ✗ FAIL ✓ 824 ms ✗ FAIL
metas_l26 ✓ 1422 ms ✗ FAIL ✗ FAIL ✓ 2143 ms ✓ 1323 ms ✓ 2898 ms ✗ FAIL ✓ 899 ms ✗ FAIL
metas_l34 ✓ 1431 ms ✗ FAIL ✗ FAIL ✓ 2150 ms ✓ 1347 ms ✓ 2881 ms ✗ FAIL ✓ 775 ms ✗ FAIL
mvarsininitialgoal_l11 ✓ 1460 ms ✗ FAIL ✗ FAIL ✓ 2162 ms ✗ FAIL ✓ 2799 ms ✓ 773 ms ✓ 824 ms ✗ FAIL
nonormsimp_l19 ✓ 1381 ms ✓ 1425 ms ✓ 1861 ms ✓ 2147 ms ✓ 1267 ms ✓ 2726 ms ✓ 777 ms ✓ 766 ms ✓ 771 ms
relation_chain ✓ 1412 ms ✗ FAIL ✗ FAIL ✓ 2133 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 ✓ 1438 ms ✓ 1405 ms ✗ FAIL ✓ 2175 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 ✓ 1500 ms ✗ FAIL ✓ 1864 ms ✓ 2185 ms ✗ FAIL ✓ 3360 ms ✓ 775 ms ✓ 788 ms ✗ FAIL
tauto_l12 ✓ 1552 ms ✗ FAIL ✗ FAIL ✓ 2201 ms ✓ 1396 ms ✓ 2963 ms ✗ FAIL ✓ 782 ms ✗ FAIL
witness ✓ 1446 ms ✗ FAIL ✗ FAIL ✓ 2160 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%)no change
1013
blaster (only-optimize: 1)23/50 (46%)no change
0027
smt +model14/50 (28%)no change
0036
auto46/50 (92%)no change
004
aesop40/50 (80%)no change
0010
hammer46/50 (92%)no change
004
omega12/50 (24%)no change
0038
grind38/50 (76%)no change
0012
simp25/50 (50%)no change
0025
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
add_reorder ✓ 1374 ms ✗ FAIL ✓ 1861 ms ✓ 2150 ms ✗ FAIL ✓ 3810 ms ✓ 773 ms ✓ 774 ms ✗ FAIL
excluded_middle_variant ✓ 1386 ms ✗ FAIL ✓ 1837 ms ✓ 2146 ms ✗ FAIL ✓ 2971 ms ✗ FAIL ✓ 763 ms ✗ FAIL
nested_identity ✓ 1368 ms ✗ FAIL ✗ FAIL ✓ 2157 ms ✓ 1212 ms ✓ 2735 ms ✗ FAIL ✓ 765 ms ✗ FAIL
smttranslation_bitvec_l12 ✓ 1314 ms ✓ 1318 ms ✓ 1842 ms ✓ 2224 ms ✓ 1179 ms ✓ 2932 ms ✗ FAIL ✓ 809 ms ✓ 764 ms
smttranslation_bitvec_l15 ✓ 1305 ms ✓ 1336 ms ✗ FAIL ✓ 2167 ms ✓ 1181 ms ✓ 2752 ms ✗ FAIL ✓ 768 ms ✓ 761 ms
smttranslation_bitvec_l18 ✓ 1346 ms ✓ 1349 ms ✗ FAIL ✓ 2219 ms ✗ FAIL ✓ 2825 ms ✗ FAIL ✓ 791 ms ✗ FAIL
smttranslation_bitvec_l21 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2156 ms ✗ FAIL ✓ 3756 ms ✗ FAIL ✓ 785 ms ✗ FAIL
smttranslation_bitvec_l24 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2172 ms ✓ 1197 ms ✓ 2786 ms ✗ FAIL ✓ 763 ms ✓ 769 ms
smttranslation_bitvec_l27 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2170 ms ✓ 1180 ms ✓ 2789 ms ✗ FAIL ✓ 766 ms ✓ 762 ms
smttranslation_bitvec_l30 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2194 ms ✓ 1224 ms ✓ 2863 ms ✗ FAIL ✓ 785 ms ✗ FAIL
smttranslation_bitvec_l36 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2435 ms ✓ 1263 ms ✓ 2819 ms ✗ FAIL ✓ 770 ms ✓ 770 ms
smttranslation_bitvec_l42 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2196 ms ✓ 1217 ms ✓ 2811 ms ✗ FAIL ✓ 811 ms ✗ FAIL
smttranslation_bitvec_l46 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2182 ms ✓ 1284 ms ✓ 2933 ms ✗ FAIL ✓ 813 ms ✗ FAIL
smttranslation_boolnatint_l10 ✓ 1297 ms ✓ 1333 ms ✓ 1857 ms ✓ 2169 ms ✓ 1209 ms ✓ 2808 ms ✓ 766 ms ✓ 764 ms ✓ 765 ms
smttranslation_boolnatint_l12 ✓ 1314 ms ✓ 1308 ms ✓ 1824 ms ✓ 2149 ms ✓ 1178 ms ✓ 2862 ms ✗ FAIL ✓ 762 ms ✓ 763 ms
smttranslation_boolnatint_l14 ✓ 1316 ms ✓ 1314 ms ✗ FAIL ✓ 2235 ms ✓ 1193 ms ✓ 2802 ms ✓ 775 ms ✓ 770 ms ✓ 772 ms
smttranslation_boolnatint_l16 ✓ 1297 ms ✓ 1330 ms ✓ 1814 ms ✓ 2223 ms ✓ 1215 ms ✓ 2812 ms ✗ FAIL ✓ 763 ms ✓ 765 ms
smttranslation_boolnatint_l18 ✓ 1355 ms ✓ 1291 ms ✗ FAIL ✓ 2334 ms ✓ 1211 ms ✓ 2843 ms ✓ 768 ms ✓ 770 ms ✗ FAIL
smttranslation_boolnatint_l20 ✓ 1268 ms ✓ 1326 ms ✓ 1859 ms ✓ 2269 ms ✓ 1204 ms ✓ 2885 ms ✓ 766 ms ✓ 765 ms ✓ 766 ms
smttranslation_boolnatint_l23 ✓ 1326 ms ✓ 1348 ms ✓ 1867 ms ✓ 2260 ms ✓ 1185 ms ✓ 2825 ms ✓ 773 ms ✓ 773 ms ✓ 760 ms
smttranslation_boolnatint_l26 ✓ 1412 ms ✗ FAIL ✗ FAIL ✓ 2231 ms ✓ 1207 ms ✓ 2806 ms ✓ 774 ms ✓ 779 ms ✗ FAIL
smttranslation_boolnatint_l28 ✓ 1315 ms ✓ 1344 ms ✓ 1830 ms ✓ 2239 ms ✓ 1226 ms ✓ 3140 ms ✓ 772 ms ✓ 764 ms ✓ 771 ms
smttranslation_boolnatint_l30 ✓ 1334 ms ✓ 1323 ms ✗ FAIL ✓ 2225 ms ✓ 1215 ms ✓ 2874 ms ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l113 ✓ 1304 ms ✓ 1290 ms ✗ FAIL ✓ 2286 ms ✓ 1219 ms ✓ 2795 ms ✗ FAIL ✓ 764 ms ✓ 763 ms
smttranslation_inductive_l12 ✓ 1380 ms ✗ FAIL ✗ FAIL ✓ 2258 ms ✓ 1216 ms ✓ 2863 ms ✗ FAIL ✓ 766 ms ✓ 774 ms
smttranslation_inductive_l14 ✓ 1380 ms ✗ FAIL ✗ FAIL ✓ 2239 ms ✓ 1208 ms ✓ 2961 ms ✗ FAIL ✓ 763 ms ✗ FAIL
smttranslation_inductive_l16 ✓ 1357 ms ✗ FAIL ✗ FAIL ✓ 2238 ms ✓ 1249 ms ✓ 3007 ms ✗ FAIL ✓ 768 ms ✗ FAIL
smttranslation_inductive_l23 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l53 ✓ 1376 ms ✗ FAIL ✗ FAIL ✓ 2152 ms ✓ 1265 ms ✓ 2792 ms ✗ FAIL ✓ 765 ms ✗ FAIL
smttranslation_inductive_l58 ✓ 1431 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1205 ms ✓ 2700 ms ✗ FAIL ✓ 773 ms ✓ 766 ms
smttranslation_inductive_l61 ✓ 1416 ms ✗ FAIL ✗ FAIL ✓ 2203 ms ✓ 1204 ms ✓ 2735 ms ✗ FAIL ✓ 825 ms ✓ 784 ms
smttranslation_inductive_l64 ✓ 1441 ms ✗ FAIL ✗ FAIL ✓ 2250 ms ✓ 1168 ms ✓ 2717 ms ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_inductive_l74 ✓ 1404 ms ✓ 1327 ms ✗ FAIL ✓ 2269 ms ✓ 1221 ms ✓ 2623 ms ✗ FAIL ✓ 784 ms ✓ 770 ms
smttranslation_names_l15 ✓ 1292 ms ✓ 1299 ms ✓ 1882 ms ✓ 2195 ms ✓ 1223 ms ✓ 2736 ms ✓ 767 ms ✓ 766 ms ✓ 767 ms
smttranslation_string_l11 ✓ 1320 ms ✓ 1306 ms ✗ FAIL ✓ 2269 ms ✓ 1271 ms ✓ 2741 ms ✗ FAIL ✓ 765 ms ✓ 771 ms
smttranslation_string_l13 ✓ 1380 ms ✗ FAIL ✗ FAIL ✓ 2290 ms ✓ 1315 ms ✓ 2698 ms ✗ FAIL ✓ 778 ms ✗ FAIL
smttranslation_string_l16 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l22 ✓ 1334 ms ✓ 1337 ms ✗ FAIL ✓ 2121 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l25 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smttranslation_string_l9 ✓ 1306 ms ✓ 1311 ms ✗ FAIL ✓ 2144 ms ✓ 1163 ms ✓ 2879 ms ✗ FAIL ✓ 764 ms ✓ 760 ms
test_regression_l35 ✓ 1314 ms ✓ 1362 ms ✗ FAIL ✓ 2184 ms ✓ 1166 ms ✓ 3048 ms ✓ 763 ms ✓ 766 ms ✗ FAIL
test_regression_l45 ✓ 1405 ms ✗ FAIL ✗ FAIL ✓ 2136 ms ✓ 1170 ms ✓ 2795 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_regression_l63 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2176 ms ✓ 1169 ms ✓ 2597 ms ✗ FAIL ✗ FAIL ✓ 763 ms
test_regression_l66 ✗ FAIL ✗ FAIL ✓ 1834 ms ✓ 2231 ms ✓ 1185 ms ✓ 2801 ms ✗ FAIL ✗ FAIL ✓ 767 ms
test_regression_l69 ✓ 1345 ms ✓ 1318 ms ✓ 1834 ms ✓ 2252 ms ✓ 1180 ms ✓ 2764 ms ✗ FAIL ✗ FAIL ✓ 768 ms
test_regression_l72 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2230 ms ✓ 1170 ms ✓ 3212 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l76 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2172 ms ✗ FAIL ✓ 3653 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l79 ✓ 1399 ms ✓ 1296 ms ✗ FAIL ✓ 2161 ms ✗ FAIL ✓ 3379 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_regression_l83 ✓ 1341 ms ✓ 1436 ms ✓ 1822 ms ✓ 2161 ms ✓ 1153 ms ✓ 2990 ms ✓ 772 ms ✓ 813 ms ✓ 771 ms
test_regression_l89 ✓ 1337 ms ✓ 1305 ms ✓ 1818 ms ✓ 2160 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%)no change
300
blaster (only-optimize: 1)25/50 (50%)no change
0025
smt +model17/50 (34%)no change
0033
auto37/50 (74%)no change
0013
aesop38/50 (76%)no change
0012
hammer48/50 (96%)no change
002
omega17/50 (34%)no change
0033
grind37/50 (74%)no change
0013
simp25/50 (50%)no change
0025
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
fixedissues_issue12_l9 ✓ 1312 ms ✓ 1327 ms ✗ FAIL ✗ FAIL ✓ 1414 ms ✓ 3555 ms ✗ FAIL ✓ 783 ms ✗ FAIL
fixedissues_issue14_l12 ✓ 1367 ms ✗ FAIL ✗ FAIL ✓ 2378 ms ✓ 1310 ms ✓ 3098 ms ✗ FAIL ✓ 760 ms ✓ 762 ms
fixedissues_issue17_l11 ✓ 1340 ms ✗ FAIL ✓ 1876 ms ✓ 2330 ms ✓ 1294 ms ✓ 3244 ms ✗ FAIL ✗ FAIL ✓ 805 ms
fixedissues_issue18_l13 ✓ 1424 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue20_l18 ✓ 1364 ms ✗ FAIL ✗ FAIL ✓ 2348 ms ✓ 1327 ms ✓ 2981 ms ✗ FAIL ✓ 782 ms ✗ FAIL
fixedissues_issue20_l26 ✓ 1338 ms ✗ FAIL ✗ FAIL ✓ 2367 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 ✓ 1326 ms ✓ 1316 ms ✓ 1863 ms ✓ 2133 ms ✗ FAIL ✓ 3756 ms ✓ 773 ms ✓ 783 ms ✗ FAIL
fixedissues_issue28_l13 ✓ 1262 ms ✓ 1258 ms ✓ 1880 ms ✓ 2157 ms ✗ FAIL ✓ 3808 ms ✓ 764 ms ✓ 769 ms ✗ FAIL
fixedissues_issue31_l12 ✓ 1295 ms ✓ 1308 ms ✗ FAIL ✗ FAIL ✓ 1294 ms ✓ 3120 ms ✗ FAIL ✗ FAIL ✓ 775 ms
fixedissues_issue31_l30 ✓ 1278 ms ✓ 1288 ms ✗ FAIL ✗ FAIL ✓ 1301 ms ✓ 3152 ms ✗ FAIL ✗ FAIL ✓ 819 ms
fixedissues_issue31_l57 ✓ 1292 ms ✓ 1297 ms ✗ FAIL ✗ FAIL ✓ 1287 ms ✓ 2992 ms ✗ FAIL ✗ FAIL ✓ 781 ms
fixedissues_issue34_l14 ✓ 1296 ms ✓ 1280 ms ✗ FAIL ✓ 2179 ms ✓ 1324 ms ✓ 3037 ms ✗ FAIL ✓ 771 ms ✓ 771 ms
fixedissues_issue34_l18 ✓ 1333 ms ✓ 1298 ms ✗ FAIL ✓ 2168 ms ✓ 1283 ms ✓ 3022 ms ✗ FAIL ✓ 778 ms ✓ 764 ms
fixedissues_issue35_l29 ✓ 1346 ms ✗ FAIL ✗ FAIL ✓ 2178 ms ✓ 1277 ms ✓ 3467 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue35_l35 ✓ 1374 ms ✗ FAIL ✗ FAIL ✓ 2164 ms ✓ 1266 ms ✓ 2987 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue35_l42 ✓ 1362 ms ✗ FAIL ✗ FAIL ✓ 2170 ms ✓ 1274 ms ✓ 2962 ms ✗ FAIL ✗ FAIL ✗ FAIL
fixedissues_issue5_l18 ✓ 1423 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3840 ms ✗ FAIL ✓ 842 ms ✗ FAIL
fixedissues_issue6_l11 ✓ 1349 ms ✓ 1300 ms ✗ FAIL ✓ 2200 ms ✓ 1249 ms ✓ 2930 ms ✗ FAIL ✓ 768 ms ✗ FAIL
fixedissues_issue6_l14 ✓ 1279 ms ✓ 1307 ms ✗ FAIL ✓ 2166 ms ✓ 1218 ms ✓ 2871 ms ✗ FAIL ✓ 767 ms ✗ FAIL
fixedissues_issue7_l10 ✓ 1320 ms ✓ 1321 ms ✗ FAIL ✗ FAIL ✓ 1248 ms ✓ 2927 ms ✗ FAIL ✓ 817 ms ✓ 768 ms
fixedissues_issue7_l11 ✓ 1298 ms ✓ 1355 ms ✗ FAIL ✗ FAIL ✓ 1261 ms ✓ 2965 ms ✗ FAIL ✓ 777 ms ✓ 780 ms
fixedissues_issue9_l10 ✓ 1510 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1300 ms ✓ 2952 ms ✗ FAIL ✓ 797 ms ✗ FAIL
funext_poly ✓ 1378 ms ✗ FAIL ✗ FAIL ✓ 2193 ms ✓ 1254 ms ✓ 2896 ms ✗ FAIL ✓ 771 ms ✗ FAIL
int_neg_positive ✓ 1327 ms ✓ 1359 ms ✓ 1866 ms ✓ 2129 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 ✓ 1378 ms ✗ FAIL ✓ 1927 ms ✓ 2161 ms ✓ 1282 ms ✓ 2934 ms ✓ 780 ms ✓ 775 ms ✗ FAIL
smt_smteqarith_l13 ✓ 1371 ms ✗ FAIL ✓ 1922 ms ✓ 2227 ms ✗ FAIL ✓ 3432 ms ✓ 770 ms ✓ 778 ms ✗ FAIL
smt_smteqarith_l14 ✓ 1407 ms ✗ FAIL ✓ 1981 ms ✓ 2226 ms ✓ 1258 ms ✓ 2952 ms ✓ 775 ms ✓ 777 ms ✗ FAIL
smt_smtltarith_l6 ✓ 1390 ms ✗ FAIL ✓ 1903 ms ✓ 2201 ms ✓ 1249 ms ✓ 2823 ms ✓ 772 ms ✓ 829 ms ✓ 768 ms
smt_smtltarith_l7 ✓ 1354 ms ✗ FAIL ✓ 1887 ms ✓ 2216 ms ✓ 1231 ms ✓ 2909 ms ✓ 773 ms ✓ 793 ms ✓ 823 ms
smt_smtltarith_l9 ✓ 1309 ms ✓ 1323 ms ✓ 1885 ms ✓ 2173 ms ✓ 1226 ms ✓ 2842 ms ✓ 776 ms ✓ 798 ms ✓ 767 ms
smt_smtpredqualifier_l8 ✓ 1395 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
smt_smtrecfun_l11 ✓ 1290 ms ✓ 1333 ms ✗ FAIL ✓ 2159 ms ✓ 1248 ms ✓ 2858 ms ✗ FAIL ✓ 781 ms ✓ 774 ms
smt_smtrecfun_l9 ✓ 1330 ms ✓ 1315 ms ✗ FAIL ✓ 2167 ms ✓ 1232 ms ✓ 2895 ms ✗ FAIL ✓ 774 ms ✓ 771 ms
smtnat_smtnatadd_l11 ✓ 1316 ms ✓ 1299 ms ✓ 1885 ms ✓ 2162 ms ✓ 1248 ms ✓ 2873 ms ✓ 768 ms ✓ 783 ms ✓ 771 ms
smtnat_smtnatadd_l16 ✓ 1334 ms ✓ 1301 ms ✓ 1831 ms ✓ 2141 ms ✓ 1241 ms ✓ 2908 ms ✓ 772 ms ✓ 776 ms ✓ 771 ms
smtnat_smtnatadd_l9 ✓ 1361 ms ✓ 1324 ms ✓ 1834 ms ✓ 2130 ms ✓ 1338 ms ✓ 2827 ms ✓ 788 ms ✓ 783 ms ✓ 774 ms
smtnat_smtnatdiv_l11 ✓ 1355 ms ✗ FAIL ✗ FAIL ✓ 2157 ms ✗ FAIL ✓ 7686 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatdiv_l13 ✓ 1385 ms ✗ FAIL ✗ FAIL ✓ 2159 ms ✗ FAIL ✓ 2899 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatdiv_l9 ✓ 1363 ms ✗ FAIL ✗ FAIL ✓ 2212 ms ✗ FAIL ✓ 4596 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatmod_l11 ✓ 1288 ms ✓ 1298 ms ✗ FAIL ✓ 2133 ms ✓ 1258 ms ✓ 2845 ms ✓ 771 ms ✓ 764 ms ✓ 822 ms
smtnat_smtnatmod_l9 ✓ 2035 ms ✗ FAIL ✗ FAIL ✓ 2279 ms ✗ FAIL ✓ 4507 ms ✗ FAIL ✗ FAIL ✗ FAIL
smtnat_smtnatmul_l11 ✓ 1286 ms ✓ 1302 ms ✓ 1844 ms ✓ 2149 ms ✓ 1237 ms ✓ 2869 ms ✓ 770 ms ✓ 767 ms ✓ 769 ms
smtnat_smtnatmul_l9 ✓ 1336 ms ✓ 1318 ms ✓ 1854 ms ✓ 2145 ms ✓ 1217 ms ✓ 2815 ms ✓ 772 ms ✓ 770 ms ✓ 772 ms
smtnat_smtnatpow_l11 ✓ 1316 ms ✓ 1444 ms ✗ FAIL ✓ 2176 ms ✓ 1268 ms ✓ 2887 ms ✗ FAIL ✓ 784 ms ✗ FAIL
smtnat_smtnatpow_l9 ✓ 1411 ms ✓ 1324 ms ✗ FAIL ✓ 2155 ms ✓ 1277 ms ✓ 2948 ms ✗ FAIL ✓ 773 ms ✓ 768 ms
smtnat_smtnatsub_l11 ✓ 1393 ms ✗ FAIL ✓ 1950 ms ✓ 2182 ms ✓ 1241 ms ✓ 2869 ms ✓ 774 ms ✓ 781 ms ✓ 772 ms
smtnat_smtnatsub_l9 ✓ 1351 ms ✓ 1332 ms ✓ 1923 ms ✓ 2147 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%)no change
2011
blaster (only-optimize: 1)33/50 (66%)no change
0017
smt +model5/50 (10%)no change
0045
auto38/50 (76%)no change
0012
aesop36/50 (72%)no change
0014
hammer45/50 (90%)no change
005
omega0/50 (0%)no change
0050
grind34/50 (68%)no change
0016
simp10/50 (20%)no change
0040
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
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 ✓ 2160 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l104 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2159 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l108 ✓ 1332 ms ✓ 1310 ms ✗ FAIL ✓ 2174 ms ✓ 1290 ms ✓ 2828 ms ✗ FAIL ✓ 760 ms ✓ 767 ms
temp2_l111 ✓ 1319 ms ✓ 1327 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 ✓ 1366 ms ✗ FAIL ✗ FAIL ✓ 2167 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
temp2_l53 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1194 ms ✓ 2690 ms ✗ FAIL ✗ FAIL ✓ 765 ms
temp2_l77 ✓ 1325 ms ✓ 1343 ms ✓ 1831 ms ✓ 2163 ms ✓ 1223 ms ✓ 3084 ms ✗ FAIL ✓ 770 ms ✓ 760 ms
temp2_l82 ✓ 1365 ms ✓ 1335 ms ✓ 1837 ms ✓ 2167 ms ✓ 1215 ms ✓ 3068 ms ✗ FAIL ✓ 774 ms ✓ 769 ms
temp2_l90 ✓ 1337 ms ✗ FAIL ✓ 1841 ms ✓ 2135 ms ✓ 1246 ms ✓ 3194 ms ✗ FAIL ✓ 764 ms ✗ FAIL
temp2_l94 ✓ 1397 ms ✗ FAIL ✓ 1834 ms ✓ 2147 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 ✓ 1328 ms ✓ 1293 ms ✗ FAIL ✓ 2178 ms ✗ FAIL ✓ 3811 ms ✗ FAIL ✓ 797 ms ✗ FAIL
test_boolsimp_l13 ✓ 1355 ms ✓ 1347 ms ✗ FAIL ✓ 2176 ms ✗ FAIL ✓ 3388 ms ✗ FAIL ✓ 778 ms ✗ FAIL
test_boolsimp_l16 ✓ 1278 ms ✓ 1274 ms ✗ FAIL ✓ 2176 ms ✓ 1260 ms ✓ 2850 ms ✗ FAIL ✓ 768 ms ✗ FAIL
test_boolsimp_l19 ✓ 1363 ms ✓ 1303 ms ✗ FAIL ✓ 2163 ms ✓ 1287 ms ✓ 2891 ms ✗ FAIL ✓ 781 ms ✗ FAIL
test_boolsimp_l22 ✓ 1300 ms ✓ 1307 ms ✗ FAIL ✓ 2183 ms ✓ 1227 ms ✓ 2813 ms ✗ FAIL ✓ 766 ms ✗ FAIL
test_boolsimp_l25 ✓ 1293 ms ✓ 1304 ms ✗ FAIL ✓ 2164 ms ✓ 1191 ms ✓ 2907 ms ✗ FAIL ✓ 767 ms ✗ FAIL
test_boolsimp_l28 ✓ 1315 ms ✓ 1291 ms ✗ FAIL ✓ 2141 ms ✓ 1173 ms ✓ 2800 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l31 ✓ 1356 ms ✓ 1315 ms ✗ FAIL ✓ 2156 ms ✓ 1198 ms ✓ 2801 ms ✗ FAIL ✓ 768 ms ✗ FAIL
test_boolsimp_l34 ✓ 1359 ms ✓ 1318 ms ✗ FAIL ✓ 2165 ms ✓ 1268 ms ✓ 2775 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l37 ✓ 1313 ms ✓ 1284 ms ✗ FAIL ✓ 2143 ms ✓ 1211 ms ✓ 2716 ms ✗ FAIL ✓ 765 ms ✗ FAIL
test_boolsimp_l40 ✓ 1329 ms ✓ 1292 ms ✗ FAIL ✓ 2179 ms ✓ 1269 ms ✓ 2749 ms ✗ FAIL ✓ 785 ms ✗ FAIL
test_boolsimp_l43 ✓ 1326 ms ✓ 1393 ms ✗ FAIL ✓ 2153 ms ✓ 1174 ms ✓ 2819 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l46 ✓ 1289 ms ✓ 1310 ms ✗ FAIL ✓ 2140 ms ✓ 1184 ms ✓ 2835 ms ✗ FAIL ✓ 772 ms ✗ FAIL
test_boolsimp_l49 ✓ 1343 ms ✓ 1367 ms ✗ FAIL ✓ 2177 ms ✓ 1205 ms ✓ 2725 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l52 ✓ 1354 ms ✓ 1346 ms ✗ FAIL ✓ 2152 ms ✓ 1169 ms ✓ 2790 ms ✗ FAIL ✓ 763 ms ✗ FAIL
test_boolsimp_l55 ✓ 1334 ms ✓ 1371 ms ✗ FAIL ✓ 2176 ms ✓ 1164 ms ✓ 2832 ms ✗ FAIL ✓ 766 ms ✗ FAIL
test_boolsimp_l58 ✓ 1323 ms ✓ 1331 ms ✗ FAIL ✓ 2153 ms ✓ 1196 ms ✓ 2855 ms ✗ FAIL ✓ 796 ms ✗ FAIL
test_boolsimp_l61 ✓ 1328 ms ✓ 1291 ms ✗ FAIL ✓ 2190 ms ✓ 1212 ms ✓ 2984 ms ✗ FAIL ✓ 831 ms ✗ FAIL
test_boolsimp_l64 ✓ 1320 ms ✓ 1292 ms ✗ FAIL ✓ 2158 ms ✓ 1189 ms ✓ 2971 ms ✗ FAIL ✓ 771 ms ✗ FAIL
test_boolsimp_l67 ✓ 1328 ms ✓ 1347 ms ✗ FAIL ✓ 2118 ms ✓ 1175 ms ✓ 2818 ms ✗ FAIL ✓ 765 ms ✗ FAIL
test_boolsimp_l7 ✓ 1336 ms ✓ 1375 ms ✗ FAIL ✓ 2139 ms ✓ 1221 ms ✓ 2774 ms ✗ FAIL ✓ 778 ms ✗ FAIL
test_boolsimp_l70 ✓ 1359 ms ✓ 1336 ms ✗ FAIL ✓ 2137 ms ✓ 1174 ms ✓ 2713 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_boolsimp_l73 ✓ 1342 ms ✓ 1347 ms ✗ FAIL ✓ 2155 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 ✓ 1353 ms ✓ 1335 ms ✗ FAIL ✓ 2149 ms ✓ 1191 ms ✓ 2664 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l15 ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2198 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 ✓ 1376 ms ✗ FAIL ✗ FAIL ✓ 2154 ms ✗ FAIL ✓ 3122 ms ✗ FAIL ✗ FAIL ✗ FAIL
test_inhabitationreasoning_l37 ✓ 1307 ms ✓ 1305 ms ✗ FAIL ✓ 2156 ms ✓ 1222 ms ✓ 2643 ms ✗ FAIL ✓ 770 ms ✗ FAIL
test_inhabitationreasoning_l54 ✓ 1315 ms ✓ 1369 ms ✗ FAIL ✗ FAIL ✓ 1198 ms ✓ 2680 ms ✗ FAIL ✓ 772 ms ✓ 768 ms
test_inhabitationreasoning_l7 ✓ 1413 ms ✓ 1335 ms ✗ FAIL ✓ 2136 ms ✓ 1237 ms ✓ 2631 ms ✗ FAIL ✗ FAIL ✓ 765 ms
test_inhabitationreasoning_l9 ✓ 1348 ms ✓ 1311 ms ✗ FAIL ✓ 2146 ms ✓ 1237 ms ✓ 2610 ms ✗ FAIL ✗ FAIL ✓ 764 ms
true_smoke ✓ 1320 ms ✓ 1308 ms ✓ 1840 ms ✓ 2168 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%)no change
108
blaster (only-optimize: 1)23/50 (46%)no change
0027
smt +model40/50 (80%)no change
0010
auto41/50 (82%)no change
009
aesop39/50 (78%)no change
0011
hammer47/50 (94%)no change
003
omega5/50 (10%)no change
0045
grind42/50 (84%)no change
008
simp17/50 (34%)no change
0033
Explore theorem results 50 goals × 9 tactics
theorem
blaster
v4.24.0 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
auto_l6 ✓ 1321 ms ✓ 1328 ms ✗ FAIL ✓ 2130 ms ✓ 1265 ms ✓ 2868 ms ✗ FAIL ✓ 806 ms ✓ 769 ms
bitvec_add_l5 ✗ FAIL ✗ FAIL ✓ 1994 ms ✓ 2198 ms ✓ 1248 ms ✓ 2814 ms ✗ FAIL ✓ 783 ms ✗ FAIL
bitvec_bitwiseac_l7 ✗ FAIL ✗ FAIL ✓ 1851 ms ✓ 2158 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 ✓ 1832 ms ✓ 2167 ms ✗ FAIL ✓ 3004 ms ✗ FAIL ✓ 774 ms ✗ FAIL
bool_addition_l3 ✓ 1277 ms ✓ 1301 ms ✓ 1876 ms ✓ 2171 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 ✓ 1361 ms ✗ FAIL ✓ 1905 ms ✗ FAIL ✓ 1261 ms ✓ 2888 ms ✗ FAIL ✓ 768 ms ✗ FAIL
bool_conjunction_l3 ✓ 1259 ms ✓ 1268 ms ✓ 1851 ms ✓ 2321 ms ✓ 1265 ms ✓ 2866 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_disjunctivesyllogism_l3 ✓ 1373 ms ✗ FAIL ✓ 1855 ms ✓ 2341 ms ✓ 1249 ms ✓ 2962 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_exists_l3 ✓ 1359 ms ✗ FAIL ✓ 1881 ms ✓ 2211 ms ✓ 1280 ms ✓ 2929 ms ✗ FAIL ✗ FAIL ✓ 765 ms
bool_falsum_l3 ✓ 1309 ms ✓ 1336 ms ✓ 1883 ms ✓ 2123 ms ✓ 1241 ms ✓ 2922 ms ✗ FAIL ✓ 763 ms ✓ 762 ms
bool_hypotheticalsyllogism_l3 ✓ 1377 ms ✗ FAIL ✓ 1880 ms ✓ 2187 ms ✓ 1236 ms ✓ 2909 ms ✗ FAIL ✓ 770 ms ✗ FAIL
bool_modusponens_l3 ✓ 1299 ms ✓ 1313 ms ✗ FAIL ✓ 2156 ms ✓ 1245 ms ✓ 2982 ms ✗ FAIL ✓ 769 ms ✗ FAIL
bool_modusponens_l3_2 ✓ 1301 ms ✓ 1300 ms ✓ 1918 ms ✓ 2169 ms ✓ 1253 ms ✓ 2900 ms ✗ FAIL ✓ 772 ms ✗ FAIL
bool_modustollens_l3 ✓ 1304 ms ✓ 1304 ms ✓ 1888 ms ✓ 2181 ms ✓ 1241 ms ✓ 2952 ms ✗ FAIL ✓ 778 ms ✗ FAIL
bool_propext_l3 ✓ 1417 ms ✗ FAIL ✓ 1870 ms ✗ FAIL ✓ 1237 ms ✓ 2923 ms ✗ FAIL ✓ 792 ms ✓ 775 ms
bool_refl_l3 ✓ 1321 ms ✓ 1330 ms ✓ 1845 ms ✗ FAIL ✓ 1257 ms ✓ 3078 ms ✗ FAIL ✓ 769 ms ✓ 771 ms
bool_resolution_l3 ✓ 1376 ms ✗ FAIL ✓ 1865 ms ✓ 2239 ms ✓ 1235 ms ✓ 3455 ms ✗ FAIL ✓ 766 ms ✗ FAIL
bool_simplification_l3 ✓ 1354 ms ✗ FAIL ✓ 1830 ms ✓ 2268 ms ✓ 1261 ms ✓ 3243 ms ✗ FAIL ✓ 774 ms ✗ FAIL
bool_symm_l3 ✓ 1312 ms ✓ 1303 ms ✓ 1891 ms ✗ FAIL ✓ 1252 ms ✓ 3163 ms ✗ FAIL ✓ 759 ms ✗ FAIL
bool_trans_l3 ✓ 1355 ms ✗ FAIL ✓ 1854 ms ✗ FAIL ✓ 1349 ms ✓ 3319 ms ✗ FAIL ✓ 768 ms ✗ FAIL
bool_triv_l3 ✓ 1298 ms ✓ 1293 ms ✓ 1827 ms ✓ 2350 ms ✓ 1248 ms ✓ 3187 ms ✗ FAIL ✓ 765 ms ✓ 766 ms
bool_triv_l3_2 ✓ 1288 ms ✓ 1306 ms ✓ 1826 ms ✓ 2273 ms ✓ 1239 ms ✓ 3238 ms ✗ FAIL ✓ 762 ms ✓ 766 ms
bool_triv_l3_3 ✓ 1308 ms ✓ 1299 ms ✓ 1853 ms ✓ 2196 ms ✓ 1262 ms ✓ 2968 ms ✗ FAIL ✓ 761 ms ✓ 762 ms
bool_verum_l3 ✓ 1295 ms ✓ 1298 ms ✓ 1827 ms ✓ 2232 ms ✓ 1285 ms ✓ 3124 ms ✗ FAIL ✓ 764 ms ✓ 784 ms
euf_example_l3 ✗ FAIL ✗ FAIL ✓ 1857 ms ✓ 2331 ms ✓ 1256 ms ✓ 3112 ms ✗ FAIL ✓ 769 ms ✗ FAIL
euf_issue100_l3 ✓ 1358 ms ✗ FAIL ✗ FAIL ✓ 2274 ms ✓ 1305 ms ✓ 3081 ms ✗ FAIL ✓ 782 ms ✗ FAIL
euf_issue97_l3 ✓ 1303 ms ✓ 1304 ms ✓ 1823 ms ✓ 2278 ms ✓ 1310 ms ✓ 3020 ms ✗ FAIL ✓ 769 ms ✓ 768 ms
int_arith_l3 ✓ 1357 ms ✗ FAIL ✗ FAIL ✓ 2294 ms ✗ FAIL ✓ 2900 ms ✗ FAIL ✗ FAIL ✗ FAIL
int_cong_l3 ✓ 1342 ms ✗ FAIL ✓ 1871 ms ✓ 2220 ms ✓ 1283 ms ✓ 2902 ms ✗ FAIL ✓ 772 ms ✗ FAIL
int_forallexists_l3 ✓ 1348 ms ✗ FAIL ✓ 1845 ms ✓ 2293 ms ✗ FAIL ✓ 3449 ms ✗ FAIL ✗ FAIL ✗ FAIL
int_linarith_l6 ✓ 1315 ms ✓ 1312 ms ✓ 1857 ms ✓ 2310 ms ✓ 1255 ms ✓ 2893 ms ✗ FAIL ✓ 766 ms ✗ FAIL
int_neg_l3 ✓ 1312 ms ✓ 1296 ms ✓ 1833 ms ✓ 2284 ms ✓ 1300 ms ✓ 3084 ms ✓ 769 ms ✓ 764 ms ✓ 762 ms
int_square_nonnegative ✓ 1370 ms ✗ FAIL ✓ 1869 ms ✓ 2323 ms ✗ FAIL ✓ 6393 ms ✗ FAIL ✗ FAIL ✗ FAIL
issues_reconstructarithsumub_l3 ✓ 1487 ms ✗ FAIL ✓ 2141 ms ✓ 2525 ms ✗ FAIL ✓ 3752 ms ✓ 824 ms ✓ 876 ms ✗ FAIL
modus_tollens ✓ 1313 ms ✓ 1293 ms ✓ 1842 ms ✓ 2254 ms ✓ 1305 ms ✓ 2802 ms ✗ FAIL ✓ 764 ms ✗ FAIL
nat_cong_l3 ✓ 1345 ms ✗ FAIL ✓ 1845 ms ✓ 2315 ms ✓ 1277 ms ✓ 2927 ms ✗ FAIL ✓ 763 ms ✗ FAIL
nat_exists_l3 ✓ 1299 ms ✓ 1303 ms ✓ 1859 ms ✓ 2291 ms ✓ 1261 ms ✓ 2783 ms ✗ FAIL ✗ FAIL ✓ 771 ms
nat_exists_l3_2 ✓ 1413 ms ✗ FAIL ✓ 1862 ms ✓ 2305 ms ✓ 1227 ms ✓ 2762 ms ✗ FAIL ✓ 767 ms ✓ 764 ms
nat_forall_l3 ✓ 1309 ms ✓ 1313 ms ✓ 1832 ms ✓ 2190 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 ✓ 2280 ms ✗ FAIL ✓ 4175 ms ✗ FAIL ✓ 773 ms ✗ FAIL
resolution ✓ 1436 ms ✗ FAIL ✓ 1841 ms ✓ 2264 ms ✓ 1295 ms ✓ 2829 ms ✗ FAIL ✓ 770 ms ✗ FAIL
unit_embedding_l32 ✓ 1356 ms ✓ 1338 ms ✓ 1823 ms ✓ 2346 ms ✓ 1237 ms ✓ 2826 ms ✓ 768 ms ✓ 766 ms ✓ 767 ms
unit_int_l19 ✓ 1339 ms ✓ 1359 ms ✓ 1836 ms ✓ 2186 ms ✓ 1260 ms ✓ 2665 ms ✓ 767 ms ✓ 764 ms ✓ 763 ms
unit_normalize_l28 ✓ 1335 ms ✓ 1313 ms ✓ 1828 ms ✓ 2151 ms ✓ 1203 ms ✓ 2745 ms ✗ FAIL ✓ 763 ms ✓ 761 ms
unit_quant_l6 ✓ 1388 ms ✗ FAIL ✓ 1861 ms ✓ 2141 ms ✓ 1236 ms ✓ 2768 ms ✗ FAIL ✓ 767 ms ✗ FAIL
unit_rat_l63 ✓ 1328 ms ✓ 1329 ms ✗ FAIL ✓ 2147 ms ✓ 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
AndIntro_01 ✓ 1325 ms ✓ 1324 ms ✗ FAIL ✓ 2125 ms ✓ 1345 ms ✓ 2706 ms ✓ 1245 ms ✓ 1236 ms ✗ FAIL
AndIntro_02 ✓ 1320 ms ✓ 1323 ms ✗ FAIL ✓ 2135 ms ✓ 1341 ms ✓ 2642 ms ✗ FAIL ✓ 1253 ms ✗ FAIL
AndIntro_03 ✓ 1317 ms ✓ 1331 ms ✗ FAIL ✓ 2144 ms ✓ 1352 ms ✓ 2610 ms ✗ FAIL ✓ 1238 ms ✗ FAIL
AndIntro_04 ✓ 1466 ms ✓ 1318 ms ✗ FAIL ✓ 2116 ms ✓ 1341 ms ✓ 2612 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
AndIntro_05 ✓ 1336 ms ✓ 1328 ms ✗ FAIL ✓ 2132 ms ✓ 1360 ms ✓ 2636 ms ✗ FAIL ✓ 1327 ms ✗ FAIL
AndIntro_06 ✓ 1352 ms ✓ 1337 ms ✗ FAIL ✓ 2120 ms ✓ 1323 ms ✓ 2647 ms ✗ FAIL ✓ 1231 ms ✗ FAIL
AndIntro_07 ✓ 1331 ms ✓ 1331 ms ✗ FAIL ✓ 2159 ms ✓ 1332 ms ✓ 2683 ms ✗ FAIL ✓ 1266 ms ✗ FAIL
AndIntro_08 ✓ 1327 ms ✓ 1319 ms ✗ FAIL ✓ 2119 ms ✓ 1344 ms ✓ 2693 ms ✗ FAIL ✓ 1270 ms ✗ FAIL
IffIntro_01 ✓ 1308 ms ✓ 1334 ms ✗ FAIL ✓ 2119 ms ✓ 1335 ms ✓ 2703 ms ✗ FAIL ✓ 1253 ms ✗ FAIL
IffIntro_02 ✓ 1316 ms ✓ 1307 ms ✗ FAIL ✓ 2134 ms ✓ 1368 ms ✓ 2747 ms ✗ FAIL ✓ 1233 ms ✗ FAIL
IffIntro_03 ✓ 1389 ms ✗ FAIL ✗ FAIL ✓ 2151 ms ✓ 1305 ms ✓ 2801 ms ✗ FAIL ✓ 1236 ms ✗ FAIL
IffIntro_04 ✓ 1390 ms ✗ FAIL ✗ FAIL ✓ 2124 ms ✓ 1337 ms ✓ 2723 ms ✗ FAIL ✓ 1242 ms ✗ FAIL
IffIntro_05 ✓ 1388 ms ✗ FAIL ✗ FAIL ✓ 2155 ms ✓ 1332 ms ✓ 2742 ms ✗ FAIL ✓ 1250 ms ✗ FAIL
IffIntro_06 ✓ 1389 ms ✗ FAIL ✗ FAIL ✓ 2132 ms ✓ 1337 ms ✓ 2725 ms ✗ FAIL ✓ 1241 ms ✗ FAIL
IffIntro_07 ✓ 1358 ms ✗ FAIL ✓ 1891 ms ✓ 2121 ms ✓ 1421 ms ✓ 2766 ms ✗ FAIL ✓ 1223 ms ✓ 1299 ms
ImpIntro_01 ✓ 1312 ms ✓ 1322 ms ✗ FAIL ✓ 2124 ms ✓ 1378 ms ✓ 2674 ms ✗ FAIL ✓ 1227 ms ✗ FAIL
ImpIntro_02 ✓ 1316 ms ✓ 1355 ms ✓ 1826 ms ✓ 2106 ms ✓ 1374 ms ✓ 2661 ms ✗ FAIL ✓ 1239 ms ✓ 1280 ms
ImpIntro_03 ✓ 1323 ms ✓ 1316 ms ✓ 1875 ms ✓ 2113 ms ✓ 1406 ms ✓ 2645 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
ImpIntro_04 ✓ 1370 ms ✗ FAIL ✗ FAIL ✓ 2106 ms ✓ 1423 ms ✓ 2725 ms ✗ FAIL ✓ 1234 ms ✗ FAIL
ImpIntro_05 ✓ 1339 ms ✓ 1339 ms ✗ FAIL ✓ 2129 ms ✓ 1439 ms ✓ 2676 ms ✗ FAIL ✓ 1234 ms ✗ FAIL
ImpIntro_06 ✓ 1395 ms ✗ FAIL ✗ FAIL ✓ 2137 ms ✓ 1406 ms ✓ 2744 ms ✗ FAIL ✓ 1342 ms ✗ FAIL
ImpIntro_07 ✓ 1356 ms ✗ FAIL ✗ FAIL ✓ 2127 ms ✓ 1404 ms ✓ 2703 ms ✗ FAIL ✓ 1238 ms ✗ FAIL
ImpIntro_08 ✓ 1365 ms ✗ FAIL ✗ FAIL ✓ 2131 ms ✓ 1406 ms ✓ 2749 ms ✗ FAIL ✓ 1237 ms ✗ FAIL
ImpIntro_09 ✓ 1339 ms ✓ 1325 ms ✓ 1850 ms ✓ 2109 ms ✓ 1405 ms ✓ 2739 ms ✗ FAIL ✓ 1248 ms ✓ 1225 ms
NotIntro_01 ✓ 1319 ms ✓ 1299 ms ✓ 1862 ms ✓ 2127 ms ✓ 1369 ms ✓ 2727 ms ✗ FAIL ✓ 1229 ms ✓ 1229 ms
NotIntro_02 ✓ 1317 ms ✓ 1316 ms ✗ FAIL ✓ 2131 ms ✓ 1374 ms ✓ 2790 ms ✗ FAIL ✓ 1262 ms ✗ FAIL
NotIntro_03 ✓ 1326 ms ✓ 1308 ms ✗ FAIL ✓ 2131 ms ✓ 1421 ms ✓ 2765 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
NotIntro_04 ✓ 1311 ms ✓ 1331 ms ✓ 1837 ms ✓ 2139 ms ✓ 1414 ms ✓ 2880 ms ✗ FAIL ✓ 1279 ms ✓ 1308 ms
NotIntro_05 ✓ 1380 ms ✗ FAIL ✗ FAIL ✓ 2112 ms ✓ 1400 ms ✓ 2754 ms ✗ FAIL ✓ 1233 ms ✗ FAIL
NotIntro_06 ✓ 1335 ms ✓ 1348 ms ✗ FAIL ✓ 2172 ms ✓ 1397 ms ✓ 2741 ms ✗ FAIL ✓ 1239 ms ✗ FAIL
NotIntro_07 ✓ 1382 ms ✗ FAIL ✗ FAIL ✓ 2205 ms ✓ 1400 ms ✓ 2795 ms ✗ FAIL ✓ 1241 ms ✗ FAIL
NotIntro_08 ✓ 1332 ms ✓ 1315 ms ✗ FAIL ✓ 2166 ms ✓ 1392 ms ✓ 2811 ms ✗ FAIL ✓ 1220 ms ✗ FAIL
NotIntro_09 ✓ 1394 ms ✗ FAIL ✗ FAIL ✓ 2167 ms ✓ 1363 ms ✓ 3032 ms ✗ FAIL ✓ 1245 ms ✗ FAIL
NotIntro_10 ✓ 1367 ms ✗ FAIL ✗ FAIL ✓ 2171 ms ✓ 1385 ms ✓ 2982 ms ✗ FAIL ✓ 1260 ms ✗ FAIL
NotIntro_11 ✓ 1334 ms ✓ 1313 ms ✗ FAIL ✓ 2172 ms ✓ 1380 ms ✓ 3068 ms ✗ FAIL ✓ 1300 ms ✗ FAIL
NotIntro_12 ✓ 1377 ms ✗ FAIL ✗ FAIL ✓ 2172 ms ✓ 1414 ms ✓ 2974 ms ✗ FAIL ✓ 1250 ms ✗ FAIL
OrIntro_01 ✓ 1352 ms ✓ 1305 ms ✗ FAIL ✓ 2172 ms ✓ 1418 ms ✓ 2650 ms ✗ FAIL ✓ 1307 ms ✗ FAIL
OrIntro_02 ✓ 1323 ms ✓ 1333 ms ✗ FAIL ✓ 2249 ms ✓ 1437 ms ✓ 2699 ms ✗ FAIL ✓ 1237 ms ✗ FAIL
OrIntro_03 ✓ 1378 ms ✗ FAIL ✗ FAIL ✓ 2226 ms ✓ 1409 ms ✓ 2704 ms ✗ FAIL ✓ 1242 ms ✗ FAIL
OrIntro_04 ✓ 1320 ms ✓ 1325 ms ✗ FAIL ✓ 2185 ms ✓ 1405 ms ✓ 2852 ms ✗ FAIL ✓ 1259 ms ✗ FAIL
OrIntro_05 ✓ 1374 ms ✗ FAIL ✗ FAIL ✓ 2247 ms ✓ 1422 ms ✓ 2820 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
OrIntro_06 ✓ 1389 ms ✗ FAIL ✗ FAIL ✓ 2211 ms ✓ 1408 ms ✓ 2887 ms ✗ FAIL ✓ 1249 ms ✗ FAIL
OrIntro_07 ✓ 1322 ms ✓ 1333 ms ✗ FAIL ✓ 2182 ms ✓ 1407 ms ✓ 2860 ms ✗ FAIL ✓ 1225 ms ✗ FAIL
OrIntro_08 ✓ 1408 ms ✗ FAIL ✗ FAIL ✓ 2184 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
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 ✓ 4214 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7273 ms ✓ 5470 ms ✓ 5256 ms ✗ FAIL
mathd_numbertheory_299 ✓ 4144 ms ✓ 4192 ms ✓ 5631 ms ✓ 6072 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 ✓ 4318 ms ✗ FAIL ✗ FAIL ✓ 6058 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 ✓ 4446 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_559 ✓ 4313 ms ✗ FAIL ✗ FAIL ✓ 6039 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 ✓ 6216 ms ✓ 5397 ms ✓ 6810 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_345 ✓ 4382 ms ✓ 4484 ms ✓ 5454 ms ✓ 6007 ms ✓ 5390 ms ✓ 6750 ms ✓ 5340 ms ✓ 5432 ms ✓ 5345 ms
mathd_numbertheory_328 ✓ 4466 ms ✓ 4728 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8984 ms ✓ 5320 ms ✓ 5408 ms ✗ FAIL
mathd_numbertheory_765 ✓ 4531 ms ✗ FAIL ✗ FAIL ✓ 6021 ms ✗ FAIL ✓ 8256 ms ✓ 5431 ms ✓ 5363 ms ✗ FAIL
imo_1959_p1 ✓ 4499 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_175 ✓ 4402 ms ✓ 4387 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 ✓ 7622 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
imo_1982_p1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
aime_1987_p5 ✓ 4483 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_728 ✓ 4382 ms ✓ 4422 ms ✗ FAIL ✓ 5896 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 ✓ 4392 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7512 ms ✓ 5455 ms ✓ 5406 ms ✗ FAIL
mathd_numbertheory_769 ✓ 4309 ms ✓ 4307 ms ✗ FAIL ✓ 5860 ms ✓ 5282 ms ✓ 7201 ms ✓ 5334 ms ✓ 5227 ms ✓ 5284 ms
mathd_numbertheory_5 ✓ 4410 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_207 ✓ 4325 ms ✓ 4333 ms ✗ FAIL ✓ 5971 ms ✓ 5309 ms ✓ 6957 ms ✓ 5206 ms ✓ 5320 ms ✓ 5278 ms
mathd_numbertheory_342 ✓ 4350 ms ✓ 4340 ms ✓ 5461 ms ✓ 5922 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 ✓ 4480 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_495 ✓ 5036 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_296 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✓ 5859 ms ✓ 5066 ms ✓ 7506 ms ✗ FAIL ✓ 5515 ms ✓ 5497 ms
mathd_numbertheory_247 ✓ 4643 ms ✗ FAIL ✗ FAIL ✓ 5916 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 ✓ 4584 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_314 ✓ 4568 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7332 ms ✗ FAIL ✓ 5258 ms ✗ FAIL
amc12b_2002_p7 ✓ 4458 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_457 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12_2000_p12 ✓ 4515 ms ✗ FAIL ⏱ TIMEOUT ✓ 5862 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 ✓ 4527 ms ✗ FAIL ✗ FAIL ✓ 5796 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 ✓ 4252 ms ✗ FAIL ✗ FAIL ✓ 5842 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 ✓ 4248 ms ✓ 4281 ms ✗ FAIL ✓ 5940 ms ✓ 5118 ms ✓ 6765 ms ✓ 5294 ms ✓ 5155 ms ✓ 5190 ms
mathd_numbertheory_100 ✓ 4386 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 ✓ 4282 ms ✗ FAIL ✓ 5675 ms ✓ 6001 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_551 ✓ 4218 ms ✓ 4299 ms ✓ 5531 ms ✓ 5898 ms ✓ 5043 ms ✓ 6688 ms ✓ 5159 ms ✓ 5077 ms ✓ 5119 ms
mathd_algebra_304 ✓ 4208 ms ✓ 4317 ms ✗ FAIL ✓ 5891 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 ✓ 4389 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5060 ms ✓ 6908 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_711 ✓ 4763 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12_2000_p1 ✓ 4668 ms ✗ FAIL ✗ FAIL ✓ 6178 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_212 ✓ 4277 ms ✓ 4197 ms ✗ FAIL ✓ 6176 ms ✓ 5116 ms ✓ 6924 ms ✓ 5255 ms ✓ 5317 ms ✓ 5218 ms
mathd_numbertheory_320 ✓ 4320 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 7284 ms ✓ 5236 ms ✓ 5314 ms ✗ FAIL
mathd_algebra_125 ✓ 4303 ms ✗ FAIL ✗ FAIL ✓ 6152 ms ✗ FAIL ✓ 7479 ms ✓ 5311 ms ✓ 5315 ms ✗ FAIL
induction_11div10tonmn1ton ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_254 ✓ 4162 ms ✓ 4205 ms ✓ 5561 ms ✓ 6016 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 ✓ 4207 ms ✓ 4173 ms ✗ FAIL ✓ 6008 ms ✓ 5100 ms ✓ 6647 ms ✓ 5347 ms ✓ 5262 ms ✓ 5404 ms
amc12_2001_p21 ✓ 5394 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
amc12b_2002_p2 ✓ 4247 ms ✗ FAIL ✗ FAIL ✓ 6065 ms ✓ 5093 ms ✓ 6670 ms ✗ FAIL ✓ 5265 ms ✗ FAIL
mathd_numbertheory_517 ✓ 4169 ms ✓ 4226 ms ✓ 5602 ms ✓ 6021 ms ✓ 4921 ms ✓ 6747 ms ✓ 5260 ms ✓ 5279 ms ✓ 5195 ms
mathd_numbertheory_521 ✓ 4253 ms ✗ FAIL ✗ FAIL ✓ 5926 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_289 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 5318 ms ✓ 6796 ms ✗ FAIL ✗ FAIL ✗ FAIL
amc12a_2021_p3 ✓ 4388 ms ✗ FAIL ✗ FAIL ✓ 6139 ms ✗ FAIL ✓ 8232 ms ✓ 5144 ms ✓ 5117 ms ✗ FAIL
mathd_numbertheory_66 ✓ 4180 ms ✓ 4223 ms ✓ 5672 ms ✓ 6298 ms ✓ 5020 ms ✓ 6701 ms ✓ 5261 ms ✓ 5094 ms ✓ 5272 ms
mathd_numbertheory_235 ✓ 4191 ms ✓ 4431 ms ✓ 5689 ms ✓ 6183 ms ✓ 4980 ms ✓ 6709 ms ✓ 5246 ms ✓ 5102 ms ✓ 5150 ms
mathd_numbertheory_234 ✓ 4345 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_aoddbdiv4asqpbsqmod8eq1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_222 ✓ 4453 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 8118 ms ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_541 ✓ 5065 ms ✗ FAIL ✗ FAIL ✓ 6139 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_algebra_314 ✓ 4562 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 ✓ 10951 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
numbertheory_exk2powkeqapb2mulbpa2_aeq1 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mathd_numbertheory_185 ✓ 4728 ms ✗ FAIL ✗ FAIL ✓ 5925 ms ✗ FAIL ✓ 8672 ms ✓ 5445 ms ✓ 5448 ms ✗ FAIL
mathd_numbertheory_582 ✓ 4693 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
zero_add ✓ 1298 ms ✓ 1366 ms ✗ FAIL ✓ 2388 ms ✓ 1267 ms ✓ 3631 ms ✗ FAIL ✓ 1261 ms ✓ 1250 ms
succ_add ✓ 1417 ms ✗ FAIL ✗ FAIL ✓ 2355 ms ✗ FAIL ✓ 3040 ms ✓ 1256 ms ✓ 1214 ms ✗ FAIL
add_comm ✓ 1300 ms ✓ 1300 ms ✗ FAIL ✓ 2381 ms ✗ FAIL ✓ 2980 ms ✗ FAIL ✓ 1208 ms ✗ FAIL
add_assoc ✓ 1348 ms ✗ FAIL ✗ FAIL ✓ 2390 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✓ 1191 ms ✗ FAIL
add_right_comm ✓ 1324 ms ✗ FAIL ✗ FAIL ✓ 2421 ms ✗ FAIL ✓ 2912 ms ✗ FAIL ✓ 1371 ms ✗ FAIL
add_right_cancel ✓ 1278 ms ✓ 1297 ms ✗ FAIL ✓ 2410 ms ✓ 1244 ms ✓ 3004 ms ✗ FAIL ✓ 1228 ms ✓ 1185 ms
add_left_cancel ✓ 1330 ms ✓ 1331 ms ✗ FAIL ✓ 2399 ms ✓ 1234 ms ✓ 2810 ms ✗ FAIL ✓ 1221 ms ✓ 1226 ms
add_left_eq_self ✓ 1397 ms ✗ FAIL ✗ FAIL ✓ 2432 ms ✓ 1235 ms ✓ 2800 ms ✗ FAIL ✓ 1292 ms ✓ 1273 ms
add_right_eq_self ✓ 1389 ms ✗ FAIL ✗ FAIL ✓ 2394 ms ✓ 1233 ms ✓ 2846 ms ✗ FAIL ✓ 1272 ms ✓ 1247 ms
add_right_eq_zero ✓ 1372 ms ✗ FAIL ✗ FAIL ✓ 2460 ms ✓ 1260 ms ✓ 2921 ms ✗ FAIL ✓ 1290 ms ✗ FAIL
add_left_eq_zero ✓ 1365 ms ✗ FAIL ✗ FAIL ✓ 2373 ms ✓ 1280 ms ✓ 2823 ms ✗ FAIL ✓ 1239 ms ✓ 1214 ms
mul_le_mul_right ✓ 1379 ms ✗ FAIL ✗ FAIL ✓ 2417 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_left_ne_zero ✓ 1374 ms ✗ FAIL ✗ FAIL ✓ 2423 ms ✓ 1302 ms ✓ 2855 ms ✗ FAIL ✓ 1209 ms ✗ FAIL
eq_succ_of_ne_zero ✓ 1415 ms ✗ FAIL ✗ FAIL ✓ 2379 ms ✗ FAIL ✓ 3647 ms ✗ FAIL ✗ FAIL ✗ FAIL
one_le_of_ne_zero ✓ 1350 ms ✓ 1330 ms ✗ FAIL ✓ 2392 ms ✗ FAIL ✓ 2816 ms ✗ FAIL ✓ 1214 ms ✗ FAIL
le_mul_right ✓ 1395 ms ✗ FAIL ✗ FAIL ✓ 2410 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mul_right_eq_one ✓ 1405 ms ✗ FAIL ✗ FAIL ✓ 2406 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
mul_ne_zero ✓ 1339 ms ✓ 1350 ms ✗ FAIL ✓ 2384 ms ✗ FAIL ✓ 3557 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_eq_zero ✓ 1406 ms ✗ FAIL ✗ FAIL ✓ 2387 ms ✗ FAIL ✓ 3226 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_left_cancel ✓ 1378 ms ✓ 1395 ms ✗ FAIL ✓ 2347 ms ✗ FAIL ✓ 3866 ms ✗ FAIL ✗ FAIL ✗ FAIL
mul_right_eq_self ✓ 1407 ms ✗ FAIL ✗ FAIL ✓ 2321 ms ✗ FAIL ✓ 6749 ms ✗ FAIL ✗ FAIL ✗ FAIL
add_left_comm ✓ 1418 ms ✗ FAIL ✗ FAIL ✓ 2232 ms ✗ FAIL ✓ 2954 ms ✗ FAIL ✓ 1217 ms ✗ FAIL
add_algo1 ✓ 1406 ms ✗ FAIL ✗ FAIL ✓ 2346 ms ✗ FAIL ✓ 3460 ms ✗ FAIL ✓ 1262 ms ✗ FAIL
add_algo2 ✓ 1411 ms ✗ FAIL ✗ FAIL ✓ 2261 ms ✗ FAIL ✓ 4173 ms ✗ FAIL ✓ 1282 ms ✗ FAIL
add_algo3 ✓ 1415 ms ✗ FAIL ✗ FAIL ✓ 2303 ms ✗ FAIL ✓ 3988 ms ✗ FAIL ✓ 1321 ms ✗ FAIL
pred05 ✓ 1355 ms ✓ 1342 ms ✗ FAIL ✓ 2195 ms ✓ 1231 ms ✓ 2898 ms ✗ FAIL ✓ 1350 ms ✗ FAIL
succ_ne_zero ✓ 1347 ms ✓ 1344 ms ✗ FAIL ✓ 2229 ms ✓ 1235 ms ✓ 2793 ms ✓ 1342 ms ✓ 1321 ms ✓ 1333 ms
succ_ne_succ ✓ 1351 ms ✓ 1345 ms ✗ FAIL ✓ 2219 ms ✓ 1265 ms ✓ 2925 ms ✗ FAIL ✓ 1335 ms ✗ FAIL
decide ✓ 1339 ms ✓ 1355 ms ✗ FAIL ✓ 2191 ms ✓ 1245 ms ✓ 2982 ms ✗ FAIL ✓ 1317 ms ✓ 1310 ms
decide2 ✓ 1341 ms ✓ 1408 ms ✗ FAIL ✓ 2202 ms ✓ 1264 ms ✓ 2989 ms ✗ FAIL ✓ 1324 ms ✓ 1308 ms
exact ✓ 1371 ms ✓ 1349 ms ✗ FAIL ✓ 2233 ms ✓ 1272 ms ✓ 3016 ms ✓ 1262 ms ✓ 1270 ms ✗ FAIL
exact2 ✓ 1359 ms ✓ 1305 ms ✗ FAIL ✓ 2290 ms ✓ 1251 ms ✓ 2905 ms ✗ FAIL ✓ 1319 ms ✗ FAIL
apply ✓ 1289 ms ✓ 1300 ms ✗ FAIL ✓ 2250 ms ✓ 1249 ms ✓ 2930 ms ✗ FAIL ✓ 1338 ms ✗ FAIL
succ_inj ✓ 1309 ms ✓ 1311 ms ✗ FAIL ✓ 2198 ms ✓ 1241 ms ✓ 2887 ms ✗ FAIL ✓ 1300 ms ✗ FAIL
succ_inj2 ✓ 1339 ms ✓ 1349 ms ✗ FAIL ✓ 2228 ms ✓ 1254 ms ✓ 3016 ms ✗ FAIL ✓ 1337 ms ✗ FAIL
intro ✓ 1331 ms ✓ 1339 ms ✗ FAIL ✓ 2336 ms ✓ 1255 ms ✓ 2986 ms ✗ FAIL ✓ 1349 ms ✓ 1337 ms
intro2 ✓ 1350 ms ✓ 1340 ms ✗ FAIL ✓ 2370 ms ✓ 1321 ms ✓ 3046 ms ✗ FAIL ✓ 1310 ms ✓ 1302 ms
NE ✓ 1331 ms ✓ 1345 ms ✗ FAIL ✓ 2302 ms ✓ 1305 ms ✓ 3057 ms ✗ FAIL ✓ 1305 ms ✗ FAIL
zero_ne_one ✓ 1355 ms ✓ 1339 ms ✗ FAIL ✓ 2199 ms ✓ 1275 ms ✓ 2987 ms ✗ FAIL ✓ 1310 ms ✓ 1318 ms
one_ne_zero ✓ 1339 ms ✓ 1334 ms ✗ FAIL ✓ 2187 ms ✓ 1303 ms ✓ 2954 ms ✗ FAIL ✓ 1270 ms ✓ 1307 ms
two_add_two_ne_five ✓ 1411 ms ✓ 1347 ms ✓ 1830 ms ✓ 2222 ms ✓ 1309 ms ✓ 3040 ms ✓ 1305 ms ✓ 1304 ms ✓ 1317 ms
le_refl ✓ 1340 ms ✓ 1334 ms ✗ FAIL ✓ 2180 ms ✓ 1259 ms ✓ 2840 ms ✗ FAIL ✓ 1310 ms ✓ 1293 ms
zero_le ✓ 1354 ms ✓ 1348 ms ✗ FAIL ✓ 2218 ms ✓ 1258 ms ✓ 2950 ms ✗ FAIL ✓ 1299 ms ✓ 1270 ms
le_succ_self ✓ 1337 ms ✓ 1410 ms ✗ FAIL ✓ 2218 ms ✓ 1261 ms ✓ 3021 ms ✗ FAIL ✓ 1378 ms ✓ 1313 ms
le_trans ✓ 1393 ms ✗ FAIL ✗ FAIL ✓ 2208 ms ✗ FAIL ✓ 2989 ms ✗ FAIL ✓ 1307 ms ✗ FAIL
le_zero ✓ 1296 ms ✓ 1289 ms ✗ FAIL ✓ 2198 ms ✓ 1259 ms ✓ 3011 ms ✗ FAIL ✓ 1278 ms ✗ FAIL
le_antisymm ✓ 1400 ms ✗ FAIL ✗ FAIL ✓ 2183 ms ✗ FAIL ✓ 2932 ms ✗ FAIL ✓ 1343 ms ✗ FAIL
or_symm ✓ 1339 ms ✓ 1345 ms ✗ FAIL ✓ 2184 ms ✓ 1291 ms ✓ 3010 ms ✗ FAIL ✓ 1331 ms ✗ FAIL
le_total ✓ 1397 ms ✗ FAIL ✗ FAIL ✓ 2201 ms ✗ FAIL ✓ 3053 ms ✗ FAIL ✓ 1314 ms ✗ FAIL
succ_le_succ ✓ 1338 ms ✓ 1352 ms ✗ FAIL ✓ 2191 ms ✓ 1317 ms ✓ 3311 ms ✗ FAIL ✓ 1304 ms ✗ FAIL
le_one ✓ 1402 ms ✗ FAIL ✗ FAIL ✓ 2230 ms ✗ FAIL ✓ 3902 ms ✗ FAIL ✓ 1306 ms ✗ FAIL
le_two ✓ 1464 ms ✗ FAIL ✗ FAIL ✓ 2196 ms ✗ FAIL ✓ 4352 ms ✗ FAIL ✓ 1298 ms ✗ FAIL
one_add_le_self ✓ 1332 ms ✓ 1349 ms ✗ FAIL ✓ 2165 ms ✓ 1336 ms ✓ 3124 ms ✗ FAIL ✓ 1316 ms ✓ 1293 ms
refl ✓ 1349 ms ✓ 1339 ms ✗ FAIL ✓ 2136 ms ✓ 1396 ms ✓ 3140 ms ✗ FAIL ✓ 1283 ms ✓ 1321 ms
le_implies_le_plus_one ✓ 1385 ms ✗ FAIL ✗ FAIL ✓ 2111 ms ✗ FAIL ✓ 3145 ms ✗ FAIL ✓ 1316 ms ✗ FAIL
mul_one ✓ 1351 ms ✓ 1350 ms ✗ FAIL ✓ 2130 ms ✓ 1318 ms ✓ 3171 ms ✗ FAIL ✓ 1277 ms ✓ 1288 ms
zero_mul ✓ 1348 ms ✓ 1340 ms ✗ FAIL ✓ 2094 ms ✓ 1295 ms ✓ 3058 ms ✗ FAIL ✓ 1323 ms ✓ 1300 ms
succ_mul ✓ 1399 ms ✗ FAIL ✗ FAIL ✓ 2110 ms ✗ FAIL ✓ 3175 ms ✗ FAIL ✓ 1333 ms ✗ FAIL
mul_comm ✓ 1383 ms ✓ 1330 ms ✗ FAIL ✓ 2144 ms ✗ FAIL ✓ 2942 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
one_mul ✓ 1340 ms ✓ 1405 ms ✗ FAIL ✓ 2141 ms ✓ 1279 ms ✓ 2966 ms ✗ FAIL ✓ 1309 ms ✓ 1331 ms
two_mul ✓ 1402 ms ✗ FAIL ✗ FAIL ✓ 2143 ms ✗ FAIL ✓ 4583 ms ✗ FAIL ✓ 1289 ms ✗ FAIL
mul_add ✓ 1399 ms ✗ FAIL ✗ FAIL ✓ 2137 ms ✗ FAIL ✓ 3085 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
add_mul ✓ 1428 ms ✗ FAIL ✗ FAIL ✓ 2139 ms ✗ FAIL ✓ 3097 ms ✗ FAIL ✓ 1335 ms ✗ FAIL
mul_assoc ✓ 1398 ms ✗ FAIL ✗ FAIL ✓ 2145 ms ✗ FAIL ✓ 2976 ms ✗ FAIL ✓ 1323 ms ✗ FAIL
product_not_zero_of_not_zero ✓ 1342 ms ✓ 1340 ms ✗ FAIL ✓ 2237 ms ✗ FAIL ✓ 3399 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.eq_zero_or_eq_zero_of_mul_eq_zero ✓ 1398 ms ✗ FAIL ✗ FAIL ✓ 2246 ms ✗ FAIL ✓ 3213 ms ✗ FAIL ✗ FAIL ✗ FAIL
product_zero_iff_zero ✓ 1531 ms ✗ FAIL ✗ FAIL ✓ 2214 ms ✗ FAIL ✓ 4038 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.mul_left_cancel ✓ 1346 ms ✓ 1343 ms ✗ FAIL ✓ 2235 ms ✗ FAIL ✓ 3993 ms ✗ FAIL ✗ FAIL ✗ FAIL
MyNat.mul_left_comm ✓ 1444 ms ✗ FAIL ✗ FAIL ✓ 2220 ms ✗ FAIL ✓ 3541 ms ✗ FAIL ✓ 1309 ms ✗ FAIL
P_and_Q_implies_PANDQ ✓ 1340 ms ✓ 1384 ms ✗ FAIL ✓ 2191 ms ✓ 1335 ms ✓ 2929 ms ✗ FAIL ✓ 1313 ms ✗ FAIL
and_symm ✓ 1346 ms ✓ 1352 ms ✓ 1829 ms ✓ 2198 ms ✓ 1333 ms ✓ 2960 ms ✗ FAIL ✓ 1277 ms ✗ FAIL
and_trans ✓ 1332 ms ✓ 1341 ms ✓ 1838 ms ✓ 2182 ms ✓ 1340 ms ✓ 2933 ms ✗ FAIL ✓ 1284 ms ✗ FAIL
iff_trans ✓ 1389 ms ✗ FAIL ✓ 1884 ms ✓ 2156 ms ✓ 1326 ms ✓ 3007 ms ✗ FAIL ✓ 1261 ms ✗ FAIL
Q_implies_PORQ ✓ 1329 ms ✓ 1341 ms ✓ 1850 ms ✓ 2199 ms ✓ 1340 ms ✓ 2907 ms ✗ FAIL ✓ 1274 ms ✗ FAIL
or_trans ✓ 1340 ms ✓ 1331 ms ✓ 1831 ms ✓ 2168 ms ✓ 1329 ms ✓ 2930 ms ✗ FAIL ✓ 1268 ms ✗ FAIL
and_or_distrib_left ✓ 1406 ms ✗ FAIL ✓ 1876 ms ✓ 2164 ms ✓ 1321 ms ✓ 3083 ms ✗ FAIL ✓ 1256 ms ✗ FAIL
contra ✓ 1324 ms ✓ 1325 ms ✓ 1814 ms ✓ 2257 ms ✓ 1390 ms ✓ 2999 ms ✗ FAIL ✓ 1305 ms ✓ 1292 ms
implies_trad ✓ 1396 ms ✗ FAIL ✓ 1921 ms ✓ 2245 ms ✓ 1372 ms ✓ 2997 ms ✗ FAIL ✓ 1269 ms ✗ FAIL
level01 ✓ 1338 ms ✓ 1342 ms ✗ FAIL ✓ 2224 ms ✓ 1327 ms ✗ FAIL ✗ FAIL ✓ 1327 ms ✗ FAIL
level02 ✓ 1333 ms ✓ 1340 ms ✓ 1844 ms ✓ 2237 ms ✓ 1340 ms ✓ 2900 ms ✗ FAIL ✓ 1306 ms ✓ 1314 ms
level03 ✓ 1347 ms ✓ 1546 ms ✗ FAIL ✓ 2277 ms ✓ 1334 ms ✓ 2987 ms ✗ FAIL ✓ 1280 ms ✗ FAIL
level04 ✓ 1332 ms ✓ 1325 ms ✗ FAIL ✓ 2230 ms ✓ 1349 ms ✓ 2981 ms ✗ FAIL ✓ 1245 ms ✗ FAIL
level05 ✓ 1357 ms ✓ 1335 ms ✓ 1840 ms ✓ 2175 ms ✓ 1366 ms ✓ 2954 ms ✗ FAIL ✓ 1287 ms ✗ FAIL
level06 ✓ 1403 ms ✗ FAIL ✓ 1856 ms ✓ 2175 ms ✓ 1322 ms ✓ 2778 ms ✗ FAIL ✓ 1232 ms ✗ FAIL
level07 ✓ 1393 ms ✗ FAIL ✓ 1836 ms ✓ 2157 ms ✓ 1336 ms ✓ 2965 ms ✗ FAIL ✓ 1268 ms ✗ FAIL
level08 ✓ 1391 ms ✗ FAIL ✓ 1871 ms ✓ 2180 ms ✓ 1337 ms ✓ 2976 ms ✗ FAIL ✓ 1304 ms ✗ FAIL
level09 ✓ 1407 ms ✗ FAIL ✗ FAIL ✓ 2218 ms ✓ 1341 ms ✓ 2962 ms ✗ FAIL ✓ 1302 ms ✗ FAIL
zero_pow_zero ✓ 1399 ms ✓ 1358 ms ✗ FAIL ✓ 2168 ms ✓ 1328 ms ✓ 2884 ms ✗ FAIL ✓ 1320 ms ✓ 1301 ms
zero_pow_any ✓ 1387 ms ✗ FAIL ✗ FAIL ✓ 2212 ms ✓ 1328 ms ✓ 2866 ms ✗ FAIL ✓ 1258 ms ✓ 1273 ms
any_pow_one ✓ 1403 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 ✓ 1576 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 ✓ 1416 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4194 ms ✗ FAIL ✓ 1340 ms ✗ FAIL
level10 ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
level01rfl ✓ 1346 ms ✓ 1337 ms ✗ FAIL ✓ 2231 ms ✓ 1431 ms ✗ FAIL ✗ FAIL ✓ 1311 ms ✓ 1313 ms
level02rw ✓ 1344 ms ✓ 1341 ms ✗ FAIL ✓ 2187 ms ✓ 1387 ms ✓ 2805 ms ✗ FAIL ✓ 1322 ms ✗ FAIL
level03_two_eq_succ_succ_zero ✓ 1333 ms ✓ 1394 ms ✓ 1913 ms ✓ 2209 ms ✓ 1400 ms ✓ 2791 ms ✓ 1295 ms ✓ 1224 ms ✓ 1218 ms
level04_rw_backwards ✓ 1396 ms ✓ 1386 ms ✓ 1854 ms ✓ 2194 ms ✓ 1375 ms ✓ 2820 ms ✓ 1282 ms ✓ 1269 ms ✓ 1276 ms
level05_add_zero ✓ 1400 ms ✓ 1418 ms ✗ FAIL ✓ 2171 ms ✓ 1425 ms ✓ 2837 ms ✗ FAIL ✓ 1311 ms ✓ 1249 ms
level06_add_zero2 ✓ 1393 ms ✓ 1399 ms ✗ FAIL ✓ 2211 ms ✓ 1389 ms ✓ 2891 ms ✗ FAIL ✓ 1271 ms ✓ 1269 ms
succ_eq_add_one ✓ 1425 ms ✓ 1354 ms ✓ 1854 ms ✓ 2221 ms ✓ 1411 ms ✓ 2872 ms ✓ 1317 ms ✓ 1304 ms ✓ 1269 ms
level08_two_add_two ✓ 1409 ms ✓ 1407 ms ✗ FAIL ✓ 2226 ms ✓ 1431 ms ✓ 3007 ms ✗ FAIL ✓ 1334 ms ✓ 1331 ms
l11_accrfl ✓ 1506 ms ✗ FAIL ✗ FAIL ✓ 2238 ms ✗ FAIL ✓ 3913 ms ✗ FAIL ✓ 1367 ms ✗ FAIL
decide01 ✓ 1341 ms ✓ 1348 ms ✗ FAIL ✓ 2209 ms ✓ 1457 ms ✓ 2786 ms ✗ FAIL ✓ 1253 ms ✓ 1252 ms
decode02 ✓ 1343 ms ✓ 1337 ms ✗ FAIL ✓ 2221 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
compl_union ✓ 1594 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1737 ms ✓ 2919 ms ✗ FAIL ✓ 1828 ms ✓ 1905 ms
compl_inter ✓ 1621 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2862 ms ✗ FAIL ✓ 1882 ms ✗ FAIL
inter_distrib_left ✓ 1680 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1777 ms ✓ 2897 ms ✗ FAIL ✓ 1929 ms ✗ FAIL
union_distrib_left ✓ 1610 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1756 ms ✓ 2965 ms ✗ FAIL ✓ 1865 ms ✗ FAIL
union_sub_inter_sub ✓ 1595 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4949 ms ✗ FAIL ✗ FAIL ✗ FAIL
contra ✓ 1625 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3416 ms ✗ FAIL ✓ 1924 ms ✗ FAIL
mem_compl_iff ✓ 1548 ms ✓ 1518 ms ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 2964 ms ✗ FAIL ✓ 1825 ms ✓ 1830 ms
compl_subset_compl_of_subs ✓ 1630 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1737 ms ✓ 2998 ms ✗ FAIL ✓ 1862 ms ✓ 1803 ms
compl_compl2 ✓ 1603 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1752 ms ✓ 2932 ms ✗ FAIL ✓ 1829 ms ✓ 1842 ms
comp_sub_iff ✓ 1599 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1718 ms ✓ 2988 ms ✗ FAIL ✗ FAIL ✓ 1882 ms
helloWorld ✓ 1508 ms ✗ FAIL ✗ FAIL ✓ 2456 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 ✓ 1596 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4799 ms ✗ FAIL ✗ FAIL ✗ FAIL
three_fam ✓ 1539 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4404 ms ✗ FAIL ✓ 1931 ms ✗ FAIL
union_int_comp_union ✓ 1564 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 10146 ms ✗ FAIL ✓ 1900 ms ✗ FAIL
union_int_union ✓ 1545 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
union_int_comp_int ✓ 1583 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ⏱ TIMEOUT ✗ FAIL
singleton ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
inter_sub ✓ 1580 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2982 ms ✗ FAIL ✓ 1870 ms ✗ FAIL
inter_sub_inter ✓ 1543 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3065 ms ✗ FAIL ✓ 1794 ms ✗ FAIL
inter_pair ✓ 1573 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1695 ms ✓ 2988 ms ✗ FAIL ✓ 1812 ms ✓ 1770 ms
inter_union ✓ 1567 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1755 ms ✓ 2941 ms ✗ FAIL ✓ 1818 ms ✗ FAIL
sub_inter ✓ 1560 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 3172 ms ✗ FAIL ✓ 1800 ms ✓ 1789 ms
eltwise_union ✓ 1586 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3083 ms ✗ FAIL ✗ FAIL ✗ FAIL
prove_exists ✓ 1561 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1725 ms ✓ 2844 ms ✗ FAIL ✗ FAIL ✗ FAIL
sub_union ✓ 1586 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2992 ms ✗ FAIL ✓ 1842 ms ✗ FAIL
union_sub_union ✓ 1600 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 3007 ms ✗ FAIL ✓ 1818 ms ✗ FAIL
union_pair ✓ 1627 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1718 ms ✓ 2985 ms ✗ FAIL ✓ 1850 ms ✓ 1793 ms
union_union ✓ 1572 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1966 ms ✓ 2976 ms ✗ FAIL ✓ 1839 ms ✗ FAIL
union_sub ✓ 1557 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1707 ms ✓ 2916 ms ✗ FAIL ✓ 1838 ms ✓ 1822 ms
eltwise_inter ✓ 1600 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1821 ms ✓ 3130 ms ✗ FAIL ⏱ TIMEOUT ✗ FAIL
and_thm ✓ 1513 ms ✓ 1516 ms ✗ FAIL ✓ 2463 ms ✓ 1681 ms ✓ 2809 ms ✗ FAIL ✓ 1784 ms ✗ FAIL
elt_inter_elt_right ✓ 1492 ms ✓ 1594 ms ✗ FAIL ✗ FAIL ✓ 1678 ms ✓ 2957 ms ✗ FAIL ✓ 1821 ms ✗ FAIL
inter_sub_left ✓ 1518 ms ✓ 1551 ms ✗ FAIL ✗ FAIL ✓ 1728 ms ✓ 2789 ms ✗ FAIL ✓ 1834 ms ✓ 1853 ms
prove_and ✓ 1643 ms ✓ 1644 ms ✗ FAIL ✗ FAIL ✓ 1698 ms ✓ 2809 ms ✗ FAIL ✓ 1853 ms ✗ FAIL
sub_int ✓ 1705 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1672 ms ✓ 2781 ms ✗ FAIL ✓ 1862 ms ✗ FAIL
inter_subset_swap ✓ 1653 ms ✓ 1631 ms ✗ FAIL ✗ FAIL ✓ 1717 ms ✓ 2789 ms ✗ FAIL ✓ 1857 ms ✓ 1845 ms
inter_comm ✓ 1628 ms ✓ 1580 ms ✗ FAIL ✗ FAIL ✓ 1695 ms ✓ 2813 ms ✗ FAIL ✓ 1875 ms ✗ FAIL
inter_assoc ✓ 1553 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1704 ms ✓ 2842 ms ✗ FAIL ✓ 1788 ms ✗ FAIL
subset_exact ✓ 1486 ms ✓ 1496 ms ✗ FAIL ✓ 2470 ms ✓ 1639 ms ✓ 2759 ms ✗ FAIL ✓ 1781 ms ✓ 1779 ms
sub_hyp ✓ 1529 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1706 ms ✓ 2730 ms ✗ FAIL ✓ 1838 ms ✗ FAIL
subset_have ✓ 1598 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1659 ms ✓ 2840 ms ✗ FAIL ✓ 1899 ms ✗ FAIL
subset_imp ✓ 1548 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1663 ms ✓ 2752 ms ✗ FAIL ✓ 1892 ms ✗ FAIL
Subset.refl ✓ 1467 ms ✓ 1472 ms ✗ FAIL ✗ FAIL ✓ 1619 ms ✓ 2758 ms ✗ FAIL ✓ 1881 ms ✓ 1849 ms
Subset.trans ✓ 1530 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✓ 2801 ms ✗ FAIL ✓ 1914 ms ✗ FAIL
union_or ✓ 1510 ms ✓ 1525 ms ✗ FAIL ✓ 2421 ms ✓ 1627 ms ✓ 2755 ms ✗ FAIL ✓ 1929 ms ✗ FAIL
sub_union_2 ✓ 1517 ms ✓ 1517 ms ✗ FAIL ✗ FAIL ✓ 1660 ms ✓ 2763 ms ✗ FAIL ✓ 1925 ms ✓ 1938 ms
union_cases ✓ 1593 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1631 ms ✓ 2812 ms ✗ FAIL ✓ 1903 ms ✗ FAIL
union_subset_swap ✓ 1563 ms ✓ 1548 ms ✗ FAIL ✗ FAIL ✓ 1677 ms ✓ 2715 ms ✗ FAIL ✓ 1845 ms ✓ 1887 ms
union_comm ✓ 1504 ms ✓ 1535 ms ✗ FAIL ✗ FAIL ✓ 1687 ms ✓ 2781 ms ✗ FAIL ✓ 1901 ms ✗ FAIL
union_assoc ✓ 1647 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 1645 ms ✓ 2811 ms ✗ FAIL ✓ 1861 ms ✗ FAIL

UPLCDepth · 7 theorems

UPLC concrete evaluation (growing computation)

tacticsolvedsince last runbreakdowntimeoutenvfail
blaster7/7 (100%)+1 −0
000
blaster (only-optimize: 1)7/7 (100%)+1 −0
000
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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
d_sum_1024 ✓ 5833 ms ✓ 5794 ms ✗ FAIL ✗ FAIL ✓ 3109 ms ✓ 4518 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_16 ✓ 1718 ms ✓ 1679 ms ✗ FAIL ✗ FAIL ✓ 1549 ms ✓ 3079 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_16384 ✓ 71394 ms ✓ 70189 ms ✗ FAIL ✗ FAIL ✓ 31881 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_256 ✓ 2620 ms ✓ 2632 ms ✗ FAIL ✗ FAIL ✓ 1818 ms ✓ 3376 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_4 ✓ 1622 ms ✓ 1639 ms ✗ FAIL ✗ FAIL ✓ 1484 ms ✓ 2969 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_4096 ✓ 18640 ms ✓ 18570 ms ✗ FAIL ✗ FAIL ✓ 8398 ms ✓ 8090 ms ✗ FAIL ✗ FAIL ✗ FAIL
d_sum_64 ✓ 1800 ms ✓ 1805 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
w1_add ✓ 1613 ms ✓ 1557 ms ✗ FAIL ✓ 2575 ms ✓ 1504 ms ✓ 4421 ms ✗ FAIL ✗ FAIL ✗ FAIL
w2_mul_distr ✓ 1589 ms ✓ 1612 ms ✗ FAIL ✓ 2588 ms ✓ 1545 ms ✓ 3207 ms ✗ FAIL ✗ FAIL ✗ FAIL
w3_mul_over_add ✓ 1633 ms ✓ 1667 ms ✗ FAIL ✓ 2591 ms ✓ 1503 ms ✓ 3276 ms ✗ FAIL ✗ FAIL ✗ FAIL
w4_linear ✓ 1642 ms ✓ 1653 ms ✗ FAIL ✓ 2578 ms ✓ 1519 ms ✓ 3197 ms ✗ FAIL ✗ FAIL ✗ FAIL
w5_quadratic ✓ 1640 ms ✓ 1657 ms ✗ FAIL ✓ 2635 ms ✓ 1523 ms ✓ 3095 ms ✗ FAIL ✗ FAIL ✗ FAIL
w6_sum6 ✓ 1700 ms ✓ 1639 ms ✗ FAIL ✓ 2639 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 · a16614e5e
blaster (only-optimize: 1)
v4.24.0 · a16614e5e
smt +model
v4.34.0 · db545bebe · cached
auto
v4.35.0 · 30f46ddb9
aesop
v4.35.0 · (via mathlib) · cached
hammer
v4.34.0 · 93734d624 · cached
omega
v4.35.0 · (core) · cached
grind
v4.35.0 · (core) · cached
simp
v4.35.0 · (core) · cached
verina_basic_1 ✓ 4793 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_10 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_100 ✓ 4925 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_101 ✓ 1492 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 ✓ 1393 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_108 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_11 ✓ 1398 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_12 ✓ 1332 ms ✓ 1334 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 ✓ 1384 ms ✓ 1358 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 ✓ 4383 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 ✓ 1337 ms ✓ 1348 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 ✓ 1472 ms ✓ 1484 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_46 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_47 ✓ 1451 ms ✗ FAIL ✓ 2008 ms ✓ 2231 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 ✓ 1329 ms ✓ 1298 ms ✗ FAIL ✗ FAIL ✗ FAIL ✓ 4580 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_50 ✓ 4150 ms ✓ 4402 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 ✓ 1319 ms ✓ 1362 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 ✓ 1342 ms ✓ 1349 ms ✗ FAIL ✓ 2241 ms ✓ 1326 ms ✓ 2886 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_6 ✓ 4480 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 ✓ 4395 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 ✓ 1401 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_77 ⏱ TIMEOUT ⏱ TIMEOUT ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_78 ✓ 1493 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_79 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_8 ✓ 1469 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 ✓ 4478 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 ✓ 1354 ms ✓ 1354 ms ✗ FAIL ✓ 2297 ms ✗ FAIL ✓ 3269 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_92 ✓ 1453 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 ✓ 1389 ms ✓ 1371 ms ✗ FAIL ✓ 2307 ms ✗ FAIL ✓ 3496 ms ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_97 ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_98 ✓ 1403 ms ✓ 1335 ms ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL ✗ FAIL
verina_basic_99 ✓ 4293 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.