9 tactics compared across 5 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.
| # | tactic | solved | |
|---|---|---|---|
| 1 | blaster | 276/408 (68%) | |
| 2 | grind | 214/408 (52%) | |
| 3 | hammer | 201/408 (49%) | |
| 4 | auto | 180/408 (44%) | |
| 5 | aesop | 171/408 (42%) | |
| 6 | blaster (only-optimize: 1) | 126/408 (31%) | |
| 7 | simp | 74/408 (18%) | |
| 8 | omega | 40/408 (10%) | |
| 9 | smt +model | 33/408 (8%) |
| tactic | branch | toolchain | commit | build |
|---|---|---|---|---|
| blaster | main | leanprover/lean4:v4.24.0 | 402f6d22c | OK |
| blaster (only-optimize: 1) | main | leanprover/lean4:v4.24.0 | 402f6d22c | OK |
| smt +model | main | leanprover/lean4:v4.32.0-rc1 | 3c6faf56d | OK |
| auto | main | leanprover/lean4:v4.32.0-rc1 | dcc3ecf8f | OK |
| aesop | stable | leanprover/lean4:v4.31.0 | (via mathlib) | OK |
| hammer | main | leanprover/lean4:v4.30.0 | 3ef50193c | OK |
| omega | stable | leanprover/lean4:v4.31.0 | (core) | OK |
| grind | stable | leanprover/lean4:v4.31.0 | (core) | OK |
| simp | stable | leanprover/lean4:v4.31.0 | (core) | OK |
| tactic | solved | breakdown | timeout | env | fail |
|---|---|---|---|---|---|
| blaster | 44/44 (100%) | 0 | 0 | 0 | |
| blaster (only-optimize: 1) | 26/44 (59%) | 0 | 0 | 18 | |
| smt +model | 6/44 (14%) | 0 | 0 | 38 | |
| auto | 44/44 (100%) | 0 | 0 | 0 | |
| aesop | 44/44 (100%) | 0 | 0 | 0 | |
| hammer | 44/44 (100%) | 0 | 0 | 0 | |
| omega | 1/44 (2%) | 0 | 0 | 43 | |
| grind | 44/44 (100%) | 0 | 0 | 0 | |
| simp | 5/44 (11%) | 0 | 0 | 39 |
| theorem | blaster v4.24.0 · 402f6d22c |
blaster (only-optimize: 1) v4.24.0 · 402f6d22c |
smt +model v4.32.0-rc1 · 3c6faf56d |
auto v4.32.0-rc1 · dcc3ecf8f |
aesop v4.31.0 · (via mathlib) |
hammer v4.30.0 · 3ef50193c |
omega v4.31.0 · (core) |
grind v4.31.0 · (core) |
simp v4.31.0 · (core) |
|---|---|---|---|---|---|---|---|---|---|
| AndIntro_01 | ✓ 1634 ms | ✓ 1685 ms | ✗ FAIL | ✓ 1763 ms | ✓ 1300 ms | ✓ 3162 ms | ✓ 927 ms | ✓ 929 ms | ✗ FAIL |
| AndIntro_02 | ✓ 1681 ms | ✓ 1666 ms | ✗ FAIL | ✓ 1773 ms | ✓ 1306 ms | ✓ 3231 ms | ✗ FAIL | ✓ 930 ms | ✗ FAIL |
| AndIntro_03 | ✓ 1653 ms | ✓ 1655 ms | ✗ FAIL | ✓ 1787 ms | ✓ 1323 ms | ✓ 3115 ms | ✗ FAIL | ✓ 931 ms | ✗ FAIL |
| AndIntro_04 | ✓ 1660 ms | ✓ 1713 ms | ✗ FAIL | ✓ 1799 ms | ✓ 1331 ms | ✓ 3144 ms | ✗ FAIL | ✓ 934 ms | ✗ FAIL |
| AndIntro_05 | ✓ 1722 ms | ✓ 1658 ms | ✗ FAIL | ✓ 1763 ms | ✓ 1318 ms | ✓ 3150 ms | ✗ FAIL | ✓ 931 ms | ✗ FAIL |
| AndIntro_06 | ✓ 1651 ms | ✓ 1666 ms | ✗ FAIL | ✓ 1770 ms | ✓ 1326 ms | ✓ 3374 ms | ✗ FAIL | ✓ 928 ms | ✗ FAIL |
| AndIntro_07 | ✓ 1689 ms | ✓ 1682 ms | ✗ FAIL | ✓ 1783 ms | ✓ 1325 ms | ✓ 3245 ms | ✗ FAIL | ✓ 931 ms | ✗ FAIL |
| AndIntro_08 | ✓ 1653 ms | ✓ 1661 ms | ✗ FAIL | ✓ 1767 ms | ✓ 1340 ms | ✓ 3301 ms | ✗ FAIL | ✓ 929 ms | ✗ FAIL |
| IffIntro_01 | ✓ 1669 ms | ✓ 1657 ms | ✗ FAIL | ✓ 1771 ms | ✓ 1332 ms | ✓ 3161 ms | ✗ FAIL | ✓ 930 ms | ✗ FAIL |
| IffIntro_02 | ✓ 1645 ms | ✓ 1674 ms | ✗ FAIL | ✓ 1765 ms | ✓ 1360 ms | ✓ 3153 ms | ✗ FAIL | ✓ 931 ms | ✗ FAIL |
| IffIntro_03 | ✓ 1727 ms | ✗ FAIL | ✗ FAIL | ✓ 1775 ms | ✓ 1347 ms | ✓ 3293 ms | ✗ FAIL | ✓ 930 ms | ✗ FAIL |
| IffIntro_04 | ✓ 1712 ms | ✗ FAIL | ✗ FAIL | ✓ 1770 ms | ✓ 1388 ms | ✓ 3235 ms | ✗ FAIL | ✓ 926 ms | ✗ FAIL |
| IffIntro_05 | ✓ 1714 ms | ✗ FAIL | ✗ FAIL | ✓ 1777 ms | ✓ 1392 ms | ✓ 3274 ms | ✗ FAIL | ✓ 937 ms | ✗ FAIL |
| IffIntro_06 | ✓ 1733 ms | ✗ FAIL | ✗ FAIL | ✓ 1781 ms | ✓ 1361 ms | ✓ 3187 ms | ✗ FAIL | ✓ 930 ms | ✗ FAIL |
| IffIntro_07 | ✓ 1705 ms | ✗ FAIL | ✓ 1740 ms | ✓ 1768 ms | ✓ 1362 ms | ✓ 3249 ms | ✗ FAIL | ✓ 934 ms | ✓ 927 ms |
| ImpIntro_01 | ✓ 1691 ms | ✓ 1731 ms | ✗ FAIL | ✓ 1754 ms | ✓ 1333 ms | ✓ 3106 ms | ✗ FAIL | ✓ 928 ms | ✗ FAIL |
| ImpIntro_02 | ✓ 1677 ms | ✓ 1669 ms | ✓ 1678 ms | ✓ 1762 ms | ✓ 1330 ms | ✓ 3105 ms | ✗ FAIL | ✓ 959 ms | ✓ 937 ms |
| ImpIntro_03 | ✓ 1665 ms | ✓ 1698 ms | ✓ 1674 ms | ✓ 1760 ms | ✓ 1338 ms | ✓ 3162 ms | ✗ FAIL | ✓ 924 ms | ✗ FAIL |
| ImpIntro_04 | ✓ 1743 ms | ✗ FAIL | ✗ FAIL | ✓ 1801 ms | ✓ 1340 ms | ✓ 3109 ms | ✗ FAIL | ✓ 926 ms | ✗ FAIL |
| ImpIntro_05 | ✓ 1664 ms | ✓ 1640 ms | ✗ FAIL | ✓ 1815 ms | ✓ 1344 ms | ✓ 3170 ms | ✗ FAIL | ✓ 930 ms | ✗ FAIL |
| ImpIntro_06 | ✓ 1703 ms | ✗ FAIL | ✗ FAIL | ✓ 1783 ms | ✓ 1334 ms | ✓ 3119 ms | ✗ FAIL | ✓ 939 ms | ✗ FAIL |
| ImpIntro_07 | ✓ 1696 ms | ✗ FAIL | ✗ FAIL | ✓ 1763 ms | ✓ 1350 ms | ✓ 3131 ms | ✗ FAIL | ✓ 932 ms | ✗ FAIL |
| ImpIntro_08 | ✓ 1740 ms | ✗ FAIL | ✗ FAIL | ✓ 1756 ms | ✓ 1354 ms | ✓ 3119 ms | ✗ FAIL | ✓ 927 ms | ✗ FAIL |
| ImpIntro_09 | ✓ 1658 ms | ✓ 1687 ms | ✓ 1673 ms | ✓ 1757 ms | ✓ 1345 ms | ✓ 3153 ms | ✗ FAIL | ✓ 927 ms | ✓ 932 ms |
| NotIntro_01 | ✓ 1711 ms | ✓ 1650 ms | ✓ 1690 ms | ✓ 1749 ms | ✓ 1326 ms | ✓ 3095 ms | ✗ FAIL | ✓ 923 ms | ✓ 929 ms |
| NotIntro_02 | ✓ 1679 ms | ✓ 1686 ms | ✗ FAIL | ✓ 1759 ms | ✓ 1325 ms | ✓ 3214 ms | ✗ FAIL | ✓ 948 ms | ✗ FAIL |
| NotIntro_03 | ✓ 1662 ms | ✓ 1680 ms | ✗ FAIL | ✓ 1750 ms | ✓ 1328 ms | ✓ 3208 ms | ✗ FAIL | ✓ 940 ms | ✗ FAIL |
| NotIntro_04 | ✓ 1687 ms | ✓ 1657 ms | ✓ 1677 ms | ✓ 1765 ms | ✓ 1334 ms | ✓ 3184 ms | ✗ FAIL | ✓ 943 ms | ✓ 949 ms |
| NotIntro_05 | ✓ 1700 ms | ✗ FAIL | ✗ FAIL | ✓ 1808 ms | ✓ 1325 ms | ✓ 3196 ms | ✗ FAIL | ✓ 935 ms | ✗ FAIL |
| NotIntro_06 | ✓ 1739 ms | ✓ 1741 ms | ✗ FAIL | ✓ 1772 ms | ✓ 1333 ms | ✓ 3128 ms | ✗ FAIL | ✓ 966 ms | ✗ FAIL |
| NotIntro_07 | ✓ 1723 ms | ✗ FAIL | ✗ FAIL | ✓ 1768 ms | ✓ 1351 ms | ✓ 3147 ms | ✗ FAIL | ✓ 1010 ms | ✗ FAIL |
| NotIntro_08 | ✓ 1670 ms | ✓ 1663 ms | ✗ FAIL | ✓ 1804 ms | ✓ 1328 ms | ✓ 3166 ms | ✗ FAIL | ✓ 976 ms | ✗ FAIL |
| NotIntro_09 | ✓ 1737 ms | ✗ FAIL | ✗ FAIL | ✓ 1758 ms | ✓ 1334 ms | ✓ 3187 ms | ✗ FAIL | ✓ 979 ms | ✗ FAIL |
| NotIntro_10 | ✓ 1744 ms | ✗ FAIL | ✗ FAIL | ✓ 1750 ms | ✓ 1348 ms | ✓ 3200 ms | ✗ FAIL | ✓ 977 ms | ✗ FAIL |
| NotIntro_11 | ✓ 1700 ms | ✓ 1681 ms | ✗ FAIL | ✓ 1743 ms | ✓ 1354 ms | ✓ 3236 ms | ✗ FAIL | ✓ 961 ms | ✗ FAIL |
| NotIntro_12 | ✓ 1750 ms | ✗ FAIL | ✗ FAIL | ✓ 1768 ms | ✓ 1346 ms | ✓ 3237 ms | ✗ FAIL | ✓ 984 ms | ✗ FAIL |
| OrIntro_01 | ✓ 1679 ms | ✓ 1652 ms | ✗ FAIL | ✓ 1739 ms | ✓ 1343 ms | ✓ 3163 ms | ✗ FAIL | ✓ 972 ms | ✗ FAIL |
| OrIntro_02 | ✓ 1631 ms | ✓ 1628 ms | ✗ FAIL | ✓ 1729 ms | ✓ 1343 ms | ✓ 3173 ms | ✗ FAIL | ✓ 954 ms | ✗ FAIL |
| OrIntro_03 | ✓ 1704 ms | ✗ FAIL | ✗ FAIL | ✓ 1727 ms | ✓ 1358 ms | ✓ 3141 ms | ✗ FAIL | ✓ 932 ms | ✗ FAIL |
| OrIntro_04 | ✓ 1655 ms | ✓ 1650 ms | ✗ FAIL | ✓ 1724 ms | ✓ 1340 ms | ✓ 3185 ms | ✗ FAIL | ✓ 958 ms | ✗ FAIL |
| OrIntro_05 | ✓ 1717 ms | ✗ FAIL | ✗ FAIL | ✓ 1742 ms | ✓ 1340 ms | ✓ 3166 ms | ✗ FAIL | ✓ 982 ms | ✗ FAIL |
| OrIntro_06 | ✓ 1743 ms | ✗ FAIL | ✗ FAIL | ✓ 1744 ms | ✓ 1325 ms | ✓ 3232 ms | ✗ FAIL | ✓ 964 ms | ✗ FAIL |
| OrIntro_07 | ✓ 1643 ms | ✓ 1678 ms | ✗ FAIL | ✓ 1748 ms | ✓ 1323 ms | ✓ 3245 ms | ✗ FAIL | ✓ 1027 ms | ✗ FAIL |
| OrIntro_08 | ✓ 1683 ms | ✗ FAIL | ✗ FAIL | ✓ 1747 ms | ✓ 1354 ms | ✓ 3122 ms | ✗ FAIL | ✓ 1010 ms | ✗ FAIL |
| tactic | solved | breakdown | timeout | env | fail |
|---|---|---|---|---|---|
| blaster | 54/96 (56%) | 22 | 0 | 20 | |
| blaster (only-optimize: 1) | 17/96 (18%) | 0 | 0 | 79 | |
| smt +model | 9/96 (9%) | 2 | 0 | 85 | |
| auto | 32/96 (33%) | 0 | 0 | 64 | |
| aesop | 23/96 (24%) | 0 | 0 | 73 | |
| hammer | 25/96 (26%) | 36 | 0 | 35 | |
| omega | 30/96 (31%) | 0 | 0 | 66 | |
| grind | 35/96 (36%) | 1 | 0 | 60 | |
| simp | 17/96 (18%) | 0 | 0 | 79 |
| theorem | blaster v4.24.0 · 402f6d22c |
blaster (only-optimize: 1) v4.24.0 · 402f6d22c |
smt +model v4.32.0-rc1 · 3c6faf56d |
auto v4.32.0-rc1 · dcc3ecf8f |
aesop v4.31.0 · (via mathlib) |
hammer v4.30.0 · 3ef50193c |
omega v4.31.0 · (core) |
grind v4.31.0 · (core) |
simp v4.31.0 · (core) |
|---|---|---|---|---|---|---|---|---|---|
| numbertheory_4x3m7y3neq2003 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12_2001_p5 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_1124 | ✓ 5087 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5408 ms | ✓ 5355 ms | ✗ FAIL |
| mathd_numbertheory_299 | ✓ 5220 ms | ✓ 5182 ms | ✓ 4973 ms | ✓ 4992 ms | ✓ 5197 ms | ✓ 7371 ms | ✓ 5284 ms | ✓ 5314 ms | ✓ 5261 ms |
| imo_1977_p6 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| numbertheory_x5neqy2p4 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_430 | ✓ 5112 ms | ✗ FAIL | ✗ FAIL | ✓ 5065 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5170 ms | ✗ FAIL |
| mathd_algebra_459 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| induction_12dvd4expnp1p20 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_1997_p5 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_277 | ✓ 5369 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_559 | ✓ 5083 ms | ✗ FAIL | ✗ FAIL | ✓ 5014 ms | ✗ FAIL | ✗ FAIL | ✓ 5187 ms | ✓ 5215 ms | ✗ FAIL |
| induction_nfactltnexpnm1ngt3 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| numbertheory_notEquiv2i2jasqbsqdiv8 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_12 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5108 ms | ✓ 5108 ms | ✓ 8121 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_345 | ✓ 5088 ms | ✓ 5129 ms | ✓ 5174 ms | ✓ 5061 ms | ✓ 5107 ms | ✓ 7836 ms | ✓ 5164 ms | ✓ 5138 ms | ✓ 5092 ms |
| mathd_numbertheory_328 | ✓ 5062 ms | ✓ 5100 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5110 ms | ✓ 5153 ms | ✗ FAIL |
| mathd_numbertheory_765 | ✓ 5211 ms | ✗ FAIL | ✗ FAIL | ✓ 5146 ms | ✗ FAIL | ✗ FAIL | ✓ 5178 ms | ✓ 5131 ms | ✗ FAIL |
| imo_1959_p1 | ✓ 5264 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_175 | ✓ 5031 ms | ✓ 5016 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5227 ms | ✓ 5233 ms | ✗ FAIL |
| numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_1992_p1 | ✓ 9176 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_1982_p1 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| aime_1987_p5 | ✓ 5323 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_728 | ✓ 5103 ms | ✓ 5089 ms | ✗ FAIL | ✓ 5059 ms | ✓ 5022 ms | ✓ 7850 ms | ✓ 5252 ms | ✓ 5215 ms | ✓ 5327 ms |
| aime_1994_p3 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_293 | ✓ 5133 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5525 ms | ✓ 5461 ms | ✗ FAIL |
| mathd_numbertheory_769 | ✓ 5104 ms | ✓ 5015 ms | ✗ FAIL | ✓ 4987 ms | ✓ 5145 ms | ✓ 7774 ms | ✓ 5387 ms | ✓ 5551 ms | ✓ 5467 ms |
| mathd_numbertheory_5 | ✓ 5076 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_207 | ✓ 5073 ms | ✓ 5013 ms | ✗ FAIL | ✓ 5032 ms | ✓ 5025 ms | ✓ 7668 ms | ✓ 5297 ms | ✓ 5295 ms | ✓ 5313 ms |
| mathd_numbertheory_342 | ✓ 5027 ms | ✓ 4979 ms | ✓ 5060 ms | ✓ 5036 ms | ✓ 5035 ms | ✓ 7725 ms | ✓ 5321 ms | ✓ 5372 ms | ✓ 5312 ms |
| mathd_numbertheory_483 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5079 ms | ✓ 7537 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12a_2003_p5 | ✓ 5170 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_495 | ✓ 5923 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_algebra_296 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✓ 5040 ms | ✓ 5019 ms | ✓ 7988 ms | ✗ FAIL | ✓ 5450 ms | ✓ 5508 ms |
| mathd_numbertheory_247 | ✓ 5104 ms | ✗ FAIL | ✗ FAIL | ✓ 5015 ms | ✗ FAIL | ✗ FAIL | ✓ 5483 ms | ✓ 5510 ms | ✗ FAIL |
| numbertheory_2pownm1prime_nprime | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_algebra_392 | ✓ 5125 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_314 | ✓ 5062 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5399 ms | ✗ FAIL |
| amc12b_2002_p7 | ✓ 5232 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_457 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12_2000_p12 | ✓ 5092 ms | ✗ FAIL | ⏱ TIMEOUT | ✓ 4979 ms | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_135 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5296 ms | ✓ 8212 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_1981_p6 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_34 | ✓ 5035 ms | ✗ FAIL | ✗ FAIL | ✓ 4945 ms | ✗ FAIL | ✗ FAIL | ✓ 5309 ms | ✓ 5192 ms | ✗ FAIL |
| mathd_algebra_170 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_618 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_algebra_76 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5155 ms | ✗ FAIL |
| mathd_numbertheory_99 | ✓ 5089 ms | ✗ FAIL | ✗ FAIL | ✓ 4981 ms | ✗ FAIL | ✗ FAIL | ✓ 5179 ms | ✓ 5108 ms | ✗ FAIL |
| mathd_numbertheory_233 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 7695 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_1984_p6 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_2001_p6 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_321 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 7596 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| induction_pprime_pdvdapowpma | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_229 | ✓ 5002 ms | ✓ 5005 ms | ✗ FAIL | ✓ 4943 ms | ✓ 5100 ms | ✓ 7731 ms | ✓ 5063 ms | ✓ 5078 ms | ✓ 5237 ms |
| mathd_numbertheory_100 | ✓ 5130 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12b_2002_p4 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12a_2002_p6 | ✓ 5111 ms | ✗ FAIL | ✓ 5416 ms | ✓ 5000 ms | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_551 | ✓ 5053 ms | ✓ 5215 ms | ✓ 5334 ms | ✓ 4916 ms | ✓ 5025 ms | ✓ 7694 ms | ✓ 5074 ms | ✓ 5245 ms | ✓ 5065 ms |
| mathd_algebra_304 | ✓ 5224 ms | ✓ 5370 ms | ✗ FAIL | ✓ 4946 ms | ✓ 5073 ms | ✓ 7480 ms | ✓ 5050 ms | ✓ 5104 ms | ✓ 5076 ms |
| amc12a_2021_p8 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| algebra_ineq_nto1onlt2m1on | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_341 | ✓ 5377 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 4963 ms | ✓ 7583 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_711 | ✓ 5776 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12_2000_p1 | ✓ 5342 ms | ✗ FAIL | ✗ FAIL | ✓ 4940 ms | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_212 | ✓ 5167 ms | ✓ 5281 ms | ✗ FAIL | ✓ 4957 ms | ✓ 5197 ms | ✓ 7536 ms | ✓ 5295 ms | ✓ 5590 ms | ✓ 5541 ms |
| mathd_numbertheory_320 | ✓ 5339 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5535 ms | ✓ 5530 ms | ✗ FAIL |
| mathd_algebra_125 | ✓ 5277 ms | ✗ FAIL | ✗ FAIL | ✓ 5016 ms | ✗ FAIL | ✗ FAIL | ✓ 5438 ms | ✓ 5491 ms | ✗ FAIL |
| induction_11div10tonmn1ton | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_254 | ✓ 5152 ms | ✓ 5161 ms | ✓ 5329 ms | ✓ 4940 ms | ✓ 4830 ms | ✓ 7517 ms | ✓ 5340 ms | ✓ 5487 ms | ✓ 5505 ms |
| amc12_2000_p6 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| imo_2019_p1 | ⏱ TIMEOUT | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| aime_1984_p7 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL |
| numbertheory_3pow2pownm1mod2pownp3eq2pownp2 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_85 | ✓ 5088 ms | ✓ 5108 ms | ✗ FAIL | ✓ 5091 ms | ✓ 4793 ms | ✓ 7332 ms | ✓ 5489 ms | ✓ 5522 ms | ✓ 5385 ms |
| amc12_2001_p21 | ✓ 6738 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12b_2002_p2 | ✓ 5161 ms | ✗ FAIL | ✗ FAIL | ✓ 5109 ms | ✓ 4829 ms | ✓ 7415 ms | ✗ FAIL | ✓ 5267 ms | ✗ FAIL |
| mathd_numbertheory_517 | ✓ 5063 ms | ✓ 5070 ms | ✓ 5160 ms | ✓ 5018 ms | ✓ 4779 ms | ✓ 7450 ms | ✓ 5473 ms | ✓ 5484 ms | ✓ 5268 ms |
| mathd_numbertheory_521 | ✓ 5210 ms | ✗ FAIL | ✗ FAIL | ✓ 4979 ms | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_algebra_289 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5142 ms | ✓ 7844 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| amc12a_2021_p3 | ✓ 5301 ms | ✗ FAIL | ✗ FAIL | ✓ 5055 ms | ✗ FAIL | ✗ FAIL | ✓ 5231 ms | ✓ 5312 ms | ✗ FAIL |
| mathd_numbertheory_66 | ✓ 5202 ms | ✓ 5161 ms | ✓ 5228 ms | ✓ 5023 ms | ✓ 4811 ms | ✓ 7383 ms | ✓ 5244 ms | ✓ 5165 ms | ✓ 5232 ms |
| mathd_numbertheory_235 | ✓ 5134 ms | ✓ 5115 ms | ✓ 5287 ms | ✓ 5012 ms | ✓ 4813 ms | ✓ 7653 ms | ✓ 5252 ms | ✓ 5276 ms | ✓ 5301 ms |
| mathd_numbertheory_234 | ✓ 5322 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| numbertheory_aoddbdiv4asqpbsqmod8eq1 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_222 | ✓ 5350 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_541 | ✓ 5532 ms | ✗ FAIL | ✗ FAIL | ✓ 5177 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_algebra_314 | ✓ 5310 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 4984 ms | ✓ 7400 ms | ✓ 5129 ms | ✓ 5122 ms | ✓ 5204 ms |
| mathd_numbertheory_150 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_296 | ✓ 13457 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| numbertheory_exk2powkeqapb2mulbpa2_aeq1 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mathd_numbertheory_185 | ✓ 5195 ms | ✗ FAIL | ✗ FAIL | ✓ 5099 ms | ✗ FAIL | ✗ FAIL | ✓ 5276 ms | ✓ 5207 ms | ✗ FAIL |
| mathd_numbertheory_582 | ✓ 5260 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 5140 ms | ✓ 5384 ms | ✗ FAIL |
| tactic | solved | breakdown | timeout | env | fail |
|---|---|---|---|---|---|
| blaster | 103/108 (95%) | 5 | 0 | 0 | |
| blaster (only-optimize: 1) | 59/108 (55%) | 0 | 0 | 49 | |
| smt +model | 17/108 (16%) | 0 | 0 | 91 | |
| auto | 100/108 (93%) | 0 | 0 | 8 | |
| aesop | 67/108 (62%) | 0 | 0 | 41 | |
| hammer | 97/108 (90%) | 2 | 0 | 9 | |
| omega | 7/108 (6%) | 0 | 0 | 101 | |
| grind | 93/108 (86%) | 0 | 0 | 15 | |
| simp | 37/108 (34%) | 0 | 0 | 71 |
| theorem | blaster v4.24.0 · 402f6d22c |
blaster (only-optimize: 1) v4.24.0 · 402f6d22c |
smt +model v4.32.0-rc1 · 3c6faf56d |
auto v4.32.0-rc1 · dcc3ecf8f |
aesop v4.31.0 · (via mathlib) |
hammer v4.30.0 · 3ef50193c |
omega v4.31.0 · (core) |
grind v4.31.0 · (core) |
simp v4.31.0 · (core) |
|---|---|---|---|---|---|---|---|---|---|
| zero_add | ✓ 1743 ms | ✓ 1752 ms | ✗ FAIL | ✓ 1789 ms | ✓ 1377 ms | ✓ 3366 ms | ✗ FAIL | ✓ 975 ms | ✓ 993 ms |
| succ_add | ✓ 1769 ms | ✗ FAIL | ✗ FAIL | ✓ 1796 ms | ✗ FAIL | ✓ 3613 ms | ✓ 995 ms | ✓ 1000 ms | ✗ FAIL |
| add_comm | ✓ 1732 ms | ✓ 1752 ms | ✗ FAIL | ✓ 1782 ms | ✗ FAIL | ✓ 3656 ms | ✗ FAIL | ✓ 1009 ms | ✗ FAIL |
| add_assoc | ✓ 1790 ms | ✗ FAIL | ✗ FAIL | ✓ 1801 ms | ✗ FAIL | ✓ 3352 ms | ✗ FAIL | ✓ 1017 ms | ✗ FAIL |
| add_right_comm | ✓ 1794 ms | ✗ FAIL | ✗ FAIL | ✓ 1842 ms | ✗ FAIL | ✓ 3365 ms | ✗ FAIL | ✓ 1058 ms | ✗ FAIL |
| add_right_cancel | ✓ 1757 ms | ✓ 1744 ms | ✗ FAIL | ✓ 1811 ms | ✓ 1361 ms | ✓ 3228 ms | ✗ FAIL | ✓ 1053 ms | ✓ 1028 ms |
| add_left_cancel | ✓ 1730 ms | ✓ 1704 ms | ✗ FAIL | ✓ 1806 ms | ✓ 1354 ms | ✓ 3276 ms | ✗ FAIL | ✓ 1077 ms | ✓ 1042 ms |
| add_left_eq_self | ✓ 1734 ms | ✗ FAIL | ✗ FAIL | ✓ 1789 ms | ✓ 1339 ms | ✓ 3239 ms | ✗ FAIL | ✓ 1027 ms | ✓ 1023 ms |
| add_right_eq_self | ✓ 1731 ms | ✗ FAIL | ✗ FAIL | ✓ 1784 ms | ✓ 1319 ms | ✓ 3296 ms | ✗ FAIL | ✓ 1027 ms | ✓ 1017 ms |
| add_right_eq_zero | ✓ 1754 ms | ✗ FAIL | ✗ FAIL | ✓ 1773 ms | ✓ 1315 ms | ✓ 3354 ms | ✗ FAIL | ✓ 1047 ms | ✗ FAIL |
| add_left_eq_zero | ✓ 1723 ms | ✗ FAIL | ✗ FAIL | ✓ 1773 ms | ✓ 1324 ms | ✓ 3260 ms | ✗ FAIL | ✓ 1030 ms | ✓ 999 ms |
| mul_le_mul_right | ✓ 1699 ms | ✗ FAIL | ✗ FAIL | ✓ 1791 ms | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_left_ne_zero | ✓ 1684 ms | ✗ FAIL | ✗ FAIL | ✓ 1781 ms | ✓ 1347 ms | ✓ 3335 ms | ✗ FAIL | ✓ 1003 ms | ✗ FAIL |
| eq_succ_of_ne_zero | ✓ 1700 ms | ✗ FAIL | ✗ FAIL | ✓ 1767 ms | ✗ FAIL | ✓ 3540 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| one_le_of_ne_zero | ✓ 1643 ms | ✓ 1766 ms | ✗ FAIL | ✓ 1774 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1007 ms | ✗ FAIL |
| le_mul_right | ✓ 1752 ms | ✗ FAIL | ✗ FAIL | ✓ 1791 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_right_eq_one | ✓ 1754 ms | ✗ FAIL | ✗ FAIL | ✓ 1793 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_ne_zero | ✓ 1679 ms | ✓ 1681 ms | ✗ FAIL | ✓ 1791 ms | ✗ FAIL | ✓ 3581 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_eq_zero | ✓ 1796 ms | ✗ FAIL | ✗ FAIL | ✓ 1785 ms | ✗ FAIL | ✓ 3580 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_left_cancel | ✓ 1681 ms | ✓ 1697 ms | ✗ FAIL | ✓ 1794 ms | ✗ FAIL | ✓ 3889 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| mul_right_eq_self | ✓ 1737 ms | ✗ FAIL | ✗ FAIL | ✓ 1805 ms | ✗ FAIL | ✓ 3610 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| add_left_comm | ✓ 1754 ms | ✗ FAIL | ✗ FAIL | ✓ 1795 ms | ✗ FAIL | ✓ 3504 ms | ✗ FAIL | ✓ 979 ms | ✗ FAIL |
| add_algo1 | ✓ 1755 ms | ✗ FAIL | ✗ FAIL | ✓ 1778 ms | ✗ FAIL | ✓ 4006 ms | ✗ FAIL | ✓ 976 ms | ✗ FAIL |
| add_algo2 | ✓ 1699 ms | ✗ FAIL | ✗ FAIL | ✓ 1816 ms | ✗ FAIL | ✓ 10560 ms | ✗ FAIL | ✓ 1006 ms | ✗ FAIL |
| add_algo3 | ✓ 1754 ms | ✗ FAIL | ✗ FAIL | ✓ 1808 ms | ✗ FAIL | ✓ 10705 ms | ✗ FAIL | ✓ 976 ms | ✗ FAIL |
| pred05 | ✓ 1756 ms | ✓ 1698 ms | ✗ FAIL | ✓ 1788 ms | ✓ 1395 ms | ✓ 3225 ms | ✗ FAIL | ✓ 987 ms | ✗ FAIL |
| succ_ne_zero | ✓ 1736 ms | ✓ 1787 ms | ✗ FAIL | ✓ 1772 ms | ✓ 1402 ms | ✓ 3299 ms | ✓ 971 ms | ✓ 975 ms | ✓ 976 ms |
| succ_ne_succ | ✓ 1741 ms | ✓ 1704 ms | ✗ FAIL | ✓ 1776 ms | ✓ 1374 ms | ✓ 3138 ms | ✗ FAIL | ✓ 995 ms | ✗ FAIL |
| decide | ✓ 1694 ms | ✓ 1712 ms | ✗ FAIL | ✓ 1788 ms | ✓ 1396 ms | ✓ 3141 ms | ✗ FAIL | ✓ 1012 ms | ✓ 1002 ms |
| decide2 | ✓ 1710 ms | ✓ 1708 ms | ✗ FAIL | ✓ 1786 ms | ✓ 1391 ms | ✓ 3079 ms | ✗ FAIL | ✓ 978 ms | ✓ 991 ms |
| exact | ✓ 1817 ms | ✓ 1726 ms | ✗ FAIL | ✓ 1809 ms | ✓ 1419 ms | ✓ 3089 ms | ✓ 1008 ms | ✓ 1043 ms | ✗ FAIL |
| exact2 | ✓ 1673 ms | ✓ 1736 ms | ✗ FAIL | ✓ 1780 ms | ✓ 1457 ms | ✓ 3168 ms | ✗ FAIL | ✓ 959 ms | ✗ FAIL |
| apply | ✓ 1704 ms | ✓ 1685 ms | ✗ FAIL | ✓ 1778 ms | ✓ 1399 ms | ✓ 3084 ms | ✗ FAIL | ✓ 969 ms | ✗ FAIL |
| succ_inj | ✓ 1703 ms | ✓ 1728 ms | ✗ FAIL | ✓ 1782 ms | ✓ 1419 ms | ✓ 3132 ms | ✗ FAIL | ✓ 968 ms | ✗ FAIL |
| succ_inj2 | ✓ 1747 ms | ✓ 1724 ms | ✗ FAIL | ✓ 1792 ms | ✓ 1424 ms | ✓ 3152 ms | ✗ FAIL | ✓ 982 ms | ✗ FAIL |
| intro | ✓ 1739 ms | ✓ 1705 ms | ✗ FAIL | ✓ 1775 ms | ✓ 1402 ms | ✓ 3092 ms | ✗ FAIL | ✓ 976 ms | ✓ 1000 ms |
| intro2 | ✓ 1687 ms | ✓ 1694 ms | ✗ FAIL | ✓ 1790 ms | ✓ 1430 ms | ✓ 3329 ms | ✗ FAIL | ✓ 961 ms | ✓ 961 ms |
| NE | ✓ 1674 ms | ✓ 1686 ms | ✗ FAIL | ✓ 1784 ms | ✓ 1433 ms | ✓ 3191 ms | ✗ FAIL | ✓ 999 ms | ✗ FAIL |
| zero_ne_one | ✓ 1687 ms | ✓ 1685 ms | ✗ FAIL | ✓ 1765 ms | ✓ 1411 ms | ✓ 3083 ms | ✗ FAIL | ✓ 962 ms | ✓ 949 ms |
| one_ne_zero | ✓ 1699 ms | ✓ 1742 ms | ✗ FAIL | ✓ 1771 ms | ✓ 1387 ms | ✓ 3143 ms | ✗ FAIL | ✓ 971 ms | ✓ 959 ms |
| two_add_two_ne_five | ✓ 1783 ms | ✓ 1671 ms | ✓ 1804 ms | ✓ 1766 ms | ✓ 1396 ms | ✓ 3143 ms | ✓ 967 ms | ✓ 968 ms | ✓ 962 ms |
| le_refl | ✓ 1715 ms | ✓ 1668 ms | ✗ FAIL | ✓ 1751 ms | ✓ 1378 ms | ✓ 3050 ms | ✗ FAIL | ✓ 956 ms | ✓ 950 ms |
| zero_le | ✓ 1665 ms | ✓ 1665 ms | ✗ FAIL | ✓ 1748 ms | ✓ 1428 ms | ✓ 3156 ms | ✗ FAIL | ✓ 964 ms | ✓ 990 ms |
| le_succ_self | ✓ 1679 ms | ✓ 1696 ms | ✗ FAIL | ✓ 1753 ms | ✓ 1391 ms | ✓ 3126 ms | ✗ FAIL | ✓ 966 ms | ✓ 971 ms |
| le_trans | ✓ 1753 ms | ✗ FAIL | ✗ FAIL | ✓ 1748 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 997 ms | ✗ FAIL |
| le_zero | ✓ 1672 ms | ✓ 1711 ms | ✗ FAIL | ✓ 1758 ms | ✓ 1415 ms | ✓ 3106 ms | ✗ FAIL | ✓ 977 ms | ✗ FAIL |
| le_antisymm | ✓ 1775 ms | ✗ FAIL | ✗ FAIL | ✓ 1750 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 988 ms | ✗ FAIL |
| or_symm | ✓ 1688 ms | ✓ 1715 ms | ✗ FAIL | ✓ 1757 ms | ✓ 1414 ms | ✓ 3200 ms | ✗ FAIL | ✓ 1005 ms | ✗ FAIL |
| le_total | ✓ 1747 ms | ✗ FAIL | ✗ FAIL | ✓ 1732 ms | ✗ FAIL | ✓ 3194 ms | ✗ FAIL | ✓ 966 ms | ✗ FAIL |
| succ_le_succ | ✓ 1729 ms | ✓ 1687 ms | ✗ FAIL | ✓ 1745 ms | ✓ 1398 ms | ✓ 3146 ms | ✗ FAIL | ✓ 988 ms | ✗ FAIL |
| le_one | ✓ 1740 ms | ✗ FAIL | ✗ FAIL | ✓ 1773 ms | ✗ FAIL | ✓ 3527 ms | ✗ FAIL | ✓ 981 ms | ✗ FAIL |
| le_two | ✓ 1752 ms | ✗ FAIL | ✗ FAIL | ✓ 1767 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 987 ms | ✗ FAIL |
| one_add_le_self | ✓ 1761 ms | ✓ 1720 ms | ✗ FAIL | ✓ 1805 ms | ✓ 1400 ms | ✓ 3148 ms | ✗ FAIL | ✓ 955 ms | ✓ 943 ms |
| refl | ✓ 1795 ms | ✓ 1796 ms | ✗ FAIL | ✓ 1799 ms | ✓ 1393 ms | ✓ 3060 ms | ✗ FAIL | ✓ 934 ms | ✓ 937 ms |
| le_implies_le_plus_one | ✓ 1882 ms | ✗ FAIL | ✗ FAIL | ✓ 1779 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 975 ms | ✗ FAIL |
| mul_one | ✓ 1806 ms | ✓ 1790 ms | ✗ FAIL | ✓ 1774 ms | ✓ 1415 ms | ✓ 3316 ms | ✗ FAIL | ✓ 944 ms | ✓ 944 ms |
| zero_mul | ✓ 1749 ms | ✓ 1723 ms | ✗ FAIL | ✓ 1787 ms | ✓ 1394 ms | ✓ 3304 ms | ✗ FAIL | ✓ 942 ms | ✓ 961 ms |
| succ_mul | ✓ 1783 ms | ✗ FAIL | ✗ FAIL | ✓ 1785 ms | ✗ FAIL | ✓ 3459 ms | ✗ FAIL | ✓ 967 ms | ✗ FAIL |
| mul_comm | ✓ 1744 ms | ✓ 1793 ms | ✗ FAIL | ✓ 1787 ms | ✗ FAIL | ✓ 3417 ms | ✗ FAIL | ✓ 953 ms | ✗ FAIL |
| one_mul | ✓ 1776 ms | ✓ 1703 ms | ✗ FAIL | ✓ 1781 ms | ✓ 1389 ms | ✓ 3400 ms | ✗ FAIL | ✓ 959 ms | ✓ 979 ms |
| two_mul | ✓ 1756 ms | ✗ FAIL | ✗ FAIL | ✓ 1765 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 940 ms | ✗ FAIL |
| mul_add | ✓ 1773 ms | ✗ FAIL | ✗ FAIL | ✓ 1777 ms | ✗ FAIL | ✓ 3384 ms | ✗ FAIL | ✓ 957 ms | ✗ FAIL |
| add_mul | ✓ 1797 ms | ✗ FAIL | ✗ FAIL | ✓ 1780 ms | ✗ FAIL | ✓ 3368 ms | ✗ FAIL | ✓ 970 ms | ✗ FAIL |
| mul_assoc | ✓ 1760 ms | ✗ FAIL | ✗ FAIL | ✓ 1784 ms | ✗ FAIL | ✓ 3282 ms | ✗ FAIL | ✓ 967 ms | ✗ FAIL |
| product_not_zero_of_not_zero | ✓ 1760 ms | ✓ 1731 ms | ✗ FAIL | ✓ 1787 ms | ✗ FAIL | ✓ 4336 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| MyNat.eq_zero_or_eq_zero_of_mul_eq_zero | ✓ 1791 ms | ✗ FAIL | ✗ FAIL | ✓ 1786 ms | ✗ FAIL | ✓ 3688 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| product_zero_iff_zero | ✓ 1792 ms | ✗ FAIL | ✗ FAIL | ✓ 1791 ms | ✗ FAIL | ✓ 3717 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| MyNat.mul_left_cancel | ✓ 1718 ms | ✓ 1751 ms | ✗ FAIL | ✓ 1787 ms | ✗ FAIL | ✓ 3726 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| MyNat.mul_left_comm | ✓ 1766 ms | ✗ FAIL | ✗ FAIL | ✓ 1815 ms | ✗ FAIL | ✓ 3235 ms | ✗ FAIL | ✓ 975 ms | ✗ FAIL |
| P_and_Q_implies_PANDQ | ✓ 1806 ms | ✓ 1775 ms | ✗ FAIL | ✓ 1804 ms | ✓ 1341 ms | ✓ 3379 ms | ✗ FAIL | ✓ 955 ms | ✗ FAIL |
| and_symm | ✓ 1770 ms | ✓ 1795 ms | ✓ 1701 ms | ✓ 1762 ms | ✓ 1314 ms | ✓ 3320 ms | ✗ FAIL | ✓ 951 ms | ✗ FAIL |
| and_trans | ✓ 1766 ms | ✓ 1735 ms | ✓ 1686 ms | ✓ 1768 ms | ✓ 1319 ms | ✓ 3272 ms | ✗ FAIL | ✓ 947 ms | ✗ FAIL |
| iff_trans | ✓ 1786 ms | ✗ FAIL | ✓ 1729 ms | ✓ 1765 ms | ✓ 1321 ms | ✓ 3563 ms | ✗ FAIL | ✓ 975 ms | ✗ FAIL |
| Q_implies_PORQ | ✓ 1730 ms | ✓ 1715 ms | ✓ 1694 ms | ✓ 1784 ms | ✓ 1293 ms | ✓ 3253 ms | ✗ FAIL | ✓ 949 ms | ✗ FAIL |
| or_trans | ✓ 1710 ms | ✓ 1733 ms | ✓ 1670 ms | ✓ 1773 ms | ✓ 1317 ms | ✓ 3439 ms | ✗ FAIL | ✓ 956 ms | ✗ FAIL |
| and_or_distrib_left | ✓ 1786 ms | ✗ FAIL | ✓ 1716 ms | ✓ 1767 ms | ✓ 1334 ms | ✓ 3361 ms | ✗ FAIL | ✓ 950 ms | ✗ FAIL |
| contra | ✓ 1769 ms | ✓ 1753 ms | ✓ 1687 ms | ✓ 1770 ms | ✓ 1329 ms | ✓ 3310 ms | ✗ FAIL | ✓ 945 ms | ✓ 943 ms |
| implies_trad | ✓ 1805 ms | ✗ FAIL | ✓ 1710 ms | ✓ 1756 ms | ✓ 1291 ms | ✓ 3266 ms | ✗ FAIL | ✓ 973 ms | ✗ FAIL |
| level01 | ✓ 1780 ms | ✓ 1797 ms | ✗ FAIL | ✓ 1769 ms | ✓ 1303 ms | ✓ 3461 ms | ✗ FAIL | ✓ 950 ms | ✗ FAIL |
| level02 | ✓ 1740 ms | ✓ 1764 ms | ✓ 1673 ms | ✓ 1748 ms | ✓ 1333 ms | ✓ 3318 ms | ✗ FAIL | ✓ 945 ms | ✓ 951 ms |
| level03 | ✓ 1739 ms | ✓ 1747 ms | ✗ FAIL | ✓ 1774 ms | ✓ 1348 ms | ✓ 3331 ms | ✗ FAIL | ✓ 944 ms | ✗ FAIL |
| level04 | ✓ 1742 ms | ✓ 1737 ms | ✗ FAIL | ✓ 1762 ms | ✓ 1320 ms | ✓ 3413 ms | ✗ FAIL | ✓ 959 ms | ✗ FAIL |
| level05 | ✓ 1734 ms | ✓ 1796 ms | ✓ 1757 ms | ✓ 1770 ms | ✓ 1329 ms | ✓ 3359 ms | ✗ FAIL | ✓ 950 ms | ✗ FAIL |
| level06 | ✓ 1820 ms | ✗ FAIL | ✓ 1728 ms | ✓ 1765 ms | ✓ 1318 ms | ✓ 3304 ms | ✗ FAIL | ✓ 967 ms | ✗ FAIL |
| level07 | ✓ 1836 ms | ✗ FAIL | ✓ 1694 ms | ✓ 1788 ms | ✓ 1361 ms | ✓ 3319 ms | ✗ FAIL | ✓ 950 ms | ✗ FAIL |
| level08 | ✓ 1820 ms | ✗ FAIL | ✓ 1720 ms | ✓ 1773 ms | ✓ 1361 ms | ✓ 3324 ms | ✗ FAIL | ✓ 941 ms | ✗ FAIL |
| level09 | ✓ 1870 ms | ✗ FAIL | ✗ FAIL | ✓ 1794 ms | ✓ 1362 ms | ✓ 3331 ms | ✗ FAIL | ✓ 951 ms | ✗ FAIL |
| zero_pow_zero | ✓ 1764 ms | ✓ 1782 ms | ✗ FAIL | ✓ 1779 ms | ✓ 1343 ms | ✓ 3270 ms | ✗ FAIL | ✓ 939 ms | ✓ 954 ms |
| zero_pow_any | ✓ 1798 ms | ✗ FAIL | ✗ FAIL | ✓ 1780 ms | ✓ 1347 ms | ✓ 3202 ms | ✗ FAIL | ✓ 951 ms | ✓ 941 ms |
| any_pow_one | ✓ 1880 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1383 ms | ✓ 3235 ms | ✗ FAIL | ✓ 938 ms | ✓ 948 ms |
| one_pow_any | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1385 ms | ✓ 3175 ms | ✗ FAIL | ✓ 946 ms | ✓ 941 ms |
| pow_two | ✓ 1827 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3276 ms | ✗ FAIL | ✓ 957 ms | ✗ FAIL |
| pow_add | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3345 ms | ✗ FAIL | ✓ 958 ms | ✗ FAIL |
| mul_pow | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3282 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| pow_pow | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3671 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| add_sq | ✓ 1817 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 989 ms | ✗ FAIL |
| level10 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| level01rfl | ✓ 1677 ms | ✓ 1674 ms | ✗ FAIL | ✓ 1844 ms | ✓ 1371 ms | ✓ 3390 ms | ✗ FAIL | ✓ 946 ms | ✓ 937 ms |
| level02rw | ✓ 1691 ms | ✓ 1697 ms | ✗ FAIL | ✓ 1787 ms | ✓ 1356 ms | ✓ 3166 ms | ✗ FAIL | ✓ 981 ms | ✗ FAIL |
| level03_two_eq_succ_succ_zero | ✓ 1658 ms | ✓ 1661 ms | ✓ 1669 ms | ✓ 1778 ms | ✓ 1374 ms | ✓ 3187 ms | ✓ 938 ms | ✓ 956 ms | ✓ 934 ms |
| level04_rw_backwards | ✓ 1676 ms | ✓ 1673 ms | ✓ 1693 ms | ✓ 1788 ms | ✓ 1371 ms | ✓ 3139 ms | ✓ 944 ms | ✓ 933 ms | ✓ 937 ms |
| level05_add_zero | ✓ 1712 ms | ✓ 1738 ms | ✗ FAIL | ✓ 1797 ms | ✓ 1366 ms | ✓ 3212 ms | ✗ FAIL | ✓ 938 ms | ✓ 937 ms |
| level06_add_zero2 | ✓ 1684 ms | ✓ 1682 ms | ✗ FAIL | ✓ 1797 ms | ✓ 1350 ms | ✓ 3238 ms | ✗ FAIL | ✓ 934 ms | ✓ 944 ms |
| succ_eq_add_one | ✓ 1674 ms | ✓ 1662 ms | ✓ 1692 ms | ✓ 1796 ms | ✓ 1375 ms | ✓ 3406 ms | ✓ 955 ms | ✓ 952 ms | ✓ 944 ms |
| level08_two_add_two | ✓ 1674 ms | ✓ 1655 ms | ✗ FAIL | ✓ 1799 ms | ✓ 1391 ms | ✓ 3355 ms | ✗ FAIL | ✓ 949 ms | ✓ 931 ms |
| l11_accrfl | ✓ 1766 ms | ✗ FAIL | ✗ FAIL | ✓ 1826 ms | ✗ FAIL | ✓ 10413 ms | ✗ FAIL | ✓ 957 ms | ✗ FAIL |
| decide01 | ✓ 1648 ms | ✓ 1646 ms | ✗ FAIL | ✓ 1817 ms | ✓ 1343 ms | ✓ 3222 ms | ✗ FAIL | ✓ 941 ms | ✓ 937 ms |
| decode02 | ✓ 1660 ms | ✓ 1676 ms | ✗ FAIL | ✓ 1804 ms | ✓ 1360 ms | ✓ 3211 ms | ✗ FAIL | ✓ 937 ms | ✓ 936 ms |
| tactic | solved | breakdown | timeout | env | fail |
|---|---|---|---|---|---|
| blaster | 49/52 (94%) | 2 | 0 | 1 | |
| blaster (only-optimize: 1) | 13/52 (25%) | 0 | 0 | 39 | |
| smt +model | 0/52 (0%) | 0 | 0 | 52 | |
| auto | 4/52 (8%) | 0 | 0 | 48 | |
| aesop | 35/52 (67%) | 0 | 0 | 17 | |
| hammer | 31/52 (60%) | 3 | 0 | 18 | |
| omega | 1/52 (2%) | 0 | 0 | 51 | |
| grind | 41/52 (79%) | 2 | 0 | 9 | |
| simp | 15/52 (29%) | 0 | 0 | 37 |
| theorem | blaster v4.24.0 · 402f6d22c |
blaster (only-optimize: 1) v4.24.0 · 402f6d22c |
smt +model v4.32.0-rc1 · 3c6faf56d |
auto v4.32.0-rc1 · dcc3ecf8f |
aesop v4.31.0 · (via mathlib) |
hammer v4.30.0 · 3ef50193c |
omega v4.31.0 · (core) |
grind v4.31.0 · (core) |
simp v4.31.0 · (core) |
|---|---|---|---|---|---|---|---|---|---|
| compl_union | ✓ 1958 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1600 ms | ✓ 3204 ms | ✗ FAIL | ✓ 1464 ms | ✓ 1453 ms |
| compl_inter | ✓ 1988 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3284 ms | ✗ FAIL | ✓ 1462 ms | ✗ FAIL |
| inter_distrib_left | ✓ 1939 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1638 ms | ✓ 3234 ms | ✗ FAIL | ✓ 1572 ms | ✗ FAIL |
| union_distrib_left | ✓ 1962 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1628 ms | ✓ 3349 ms | ✗ FAIL | ✓ 1486 ms | ✗ FAIL |
| union_sub_inter_sub | ✓ 1940 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| contra | ✓ 1913 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1474 ms | ✗ FAIL |
| mem_compl_iff | ✓ 1863 ms | ✓ 1861 ms | ✗ FAIL | ✗ FAIL | ✓ 1610 ms | ✓ 3430 ms | ✗ FAIL | ✓ 1450 ms | ✓ 1520 ms |
| compl_subset_compl_of_subs | ✓ 1962 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1576 ms | ✓ 3423 ms | ✗ FAIL | ✓ 1456 ms | ✓ 1464 ms |
| compl_compl2 | ✓ 1919 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1552 ms | ✓ 3596 ms | ✗ FAIL | ✓ 1485 ms | ✓ 1464 ms |
| comp_sub_iff | ✓ 1935 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1543 ms | ✓ 3426 ms | ✗ FAIL | ✗ FAIL | ✓ 1443 ms |
| helloWorld | ✓ 2063 ms | ✗ FAIL | ✗ FAIL | ✓ 2067 ms | ✓ 1565 ms | ✓ 3460 ms | ✓ 1444 ms | ✓ 1464 ms | ✗ FAIL |
| comp_union | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| comp_inter | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| common_elt | ✓ 1982 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| three_fam | ✓ 1941 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1471 ms | ✗ FAIL |
| union_int_comp_union | ✓ 1949 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1480 ms | ✗ FAIL |
| union_int_union | ✓ 1964 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| union_int_comp_int | ✓ 1989 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL |
| singleton | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| inter_sub | ✓ 1939 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1532 ms | ✗ FAIL |
| inter_sub_inter | ✓ 1969 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1458 ms | ✗ FAIL |
| inter_pair | ✓ 2045 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1567 ms | ✓ 3412 ms | ✗ FAIL | ✓ 1508 ms | ✓ 1437 ms |
| inter_union | ✓ 2007 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1737 ms | ✓ 3266 ms | ✗ FAIL | ✓ 1487 ms | ✗ FAIL |
| sub_inter | ✓ 2039 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1600 ms | ✓ 3469 ms | ✗ FAIL | ✓ 1468 ms | ✓ 1446 ms |
| eltwise_union | ✓ 2073 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| prove_exists | ✓ 1969 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1563 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| sub_union | ✓ 1915 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1463 ms | ✗ FAIL |
| union_sub_union | ✓ 1905 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1443 ms | ✗ FAIL |
| union_pair | ✓ 1961 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1546 ms | ✓ 3200 ms | ✗ FAIL | ✓ 1522 ms | ✓ 1449 ms |
| union_union | ✓ 1937 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1836 ms | ✓ 3243 ms | ✗ FAIL | ✓ 1487 ms | ✗ FAIL |
| union_sub | ✓ 1999 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1549 ms | ✓ 3342 ms | ✗ FAIL | ✓ 1467 ms | ✓ 1474 ms |
| eltwise_inter | ✓ 1990 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1708 ms | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL |
| and_thm | ✓ 1919 ms | ✓ 1923 ms | ✗ FAIL | ✓ 2032 ms | ✓ 1568 ms | ✓ 3253 ms | ✗ FAIL | ✓ 1440 ms | ✗ FAIL |
| elt_inter_elt_right | ✓ 1926 ms | ✓ 1882 ms | ✗ FAIL | ✗ FAIL | ✓ 1556 ms | ✓ 3133 ms | ✗ FAIL | ✓ 1445 ms | ✗ FAIL |
| inter_sub_left | ✓ 1893 ms | ✓ 1901 ms | ✗ FAIL | ✗ FAIL | ✓ 1554 ms | ✓ 3159 ms | ✗ FAIL | ✓ 1494 ms | ✓ 1479 ms |
| prove_and | ✓ 1862 ms | ✓ 1868 ms | ✗ FAIL | ✗ FAIL | ✓ 1591 ms | ✓ 3161 ms | ✗ FAIL | ✓ 1479 ms | ✗ FAIL |
| sub_int | ✓ 1956 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1579 ms | ✓ 3322 ms | ✗ FAIL | ✓ 1485 ms | ✗ FAIL |
| inter_subset_swap | ✓ 2037 ms | ✓ 1922 ms | ✗ FAIL | ✗ FAIL | ✓ 1591 ms | ✓ 3159 ms | ✗ FAIL | ✓ 1494 ms | ✓ 1490 ms |
| inter_comm | ✓ 1914 ms | ✓ 1936 ms | ✗ FAIL | ✗ FAIL | ✓ 1587 ms | ✓ 3275 ms | ✗ FAIL | ✓ 1553 ms | ✗ FAIL |
| inter_assoc | ✓ 1995 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1578 ms | ✓ 3286 ms | ✗ FAIL | ✓ 1498 ms | ✗ FAIL |
| subset_exact | ✓ 1904 ms | ✓ 1876 ms | ✗ FAIL | ✓ 2038 ms | ✓ 1577 ms | ✓ 3279 ms | ✗ FAIL | ✓ 1442 ms | ✓ 1470 ms |
| sub_hyp | ✓ 2011 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1615 ms | ✗ FAIL | ✗ FAIL | ✓ 1440 ms | ✗ FAIL |
| subset_have | ✓ 1908 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1629 ms | ✗ FAIL | ✗ FAIL | ✓ 1442 ms | ✗ FAIL |
| subset_imp | ✓ 1947 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1603 ms | ✗ FAIL | ✗ FAIL | ✓ 1521 ms | ✗ FAIL |
| Subset.refl | ✓ 1951 ms | ✓ 2013 ms | ✗ FAIL | ✗ FAIL | ✓ 1564 ms | ✓ 3152 ms | ✗ FAIL | ✓ 1472 ms | ✓ 1501 ms |
| Subset.trans | ✓ 2019 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1484 ms | ✗ FAIL |
| union_or | ✓ 1936 ms | ✓ 1932 ms | ✗ FAIL | ✓ 1995 ms | ✓ 1588 ms | ✓ 3157 ms | ✗ FAIL | ✓ 1455 ms | ✗ FAIL |
| sub_union_2 | ✓ 1948 ms | ✓ 1929 ms | ✗ FAIL | ✗ FAIL | ✓ 1570 ms | ✓ 3441 ms | ✗ FAIL | ✓ 1460 ms | ✓ 1440 ms |
| union_cases | ✓ 2049 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1585 ms | ✓ 3334 ms | ✗ FAIL | ✓ 1485 ms | ✗ FAIL |
| union_subset_swap | ✓ 1961 ms | ✓ 1960 ms | ✗ FAIL | ✗ FAIL | ✓ 1576 ms | ✓ 3296 ms | ✗ FAIL | ✓ 1443 ms | ✓ 1443 ms |
| union_comm | ✓ 1914 ms | ✓ 1865 ms | ✗ FAIL | ✗ FAIL | ✓ 1573 ms | ✓ 3215 ms | ✗ FAIL | ✓ 1439 ms | ✗ FAIL |
| union_assoc | ✓ 1936 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 1576 ms | ✓ 3192 ms | ✗ FAIL | ✓ 1438 ms | ✗ FAIL |
| tactic | solved | breakdown | timeout | env | fail |
|---|---|---|---|---|---|
| blaster | 26/108 (24%) | 13 | 0 | 69 | |
| blaster (only-optimize: 1) | 11/108 (10%) | 4 | 0 | 93 | |
| smt +model | 1/108 (1%) | 0 | 8 | 99 | |
| auto | 0/108 (0%) | 0 | 8 | 100 | |
| aesop | 2/108 (2%) | 1 | 8 | 97 | |
| hammer | 4/108 (4%) | 57 | 3 | 44 | |
| omega | 1/108 (1%) | 0 | 8 | 99 | |
| grind | 1/108 (1%) | 0 | 8 | 99 | |
| simp | 0/108 (0%) | 0 | 8 | 100 |
| theorem | blaster v4.24.0 · 402f6d22c |
blaster (only-optimize: 1) v4.24.0 · 402f6d22c |
smt +model v4.32.0-rc1 · 3c6faf56d |
auto v4.32.0-rc1 · dcc3ecf8f |
aesop v4.31.0 · (via mathlib) |
hammer v4.30.0 · 3ef50193c |
omega v4.31.0 · (core) |
grind v4.31.0 · (core) |
simp v4.31.0 · (core) |
|---|---|---|---|---|---|---|---|---|---|
| verina_basic_1 | ✓ 5128 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_10 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_100 | ✓ 5281 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_101 | ✓ 1700 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_102 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_103 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_104 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_105 | ✗ FAIL | ✗ FAIL | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⏱ TIMEOUT | ⊘ ENV | ⊘ ENV | ⊘ ENV |
| verina_basic_106 | ✗ FAIL | ✗ FAIL | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⏱ TIMEOUT | ⊘ ENV | ⊘ ENV | ⊘ ENV |
| verina_basic_107 | ✓ 1703 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_108 | ⏱ TIMEOUT | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_11 | ✓ 1778 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_12 | ✓ 1644 ms | ✓ 1655 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_13 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_14 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_15 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_16 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_17 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_18 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_19 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_2 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_26 | ✓ 1710 ms | ✓ 1697 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_27 | ✗ FAIL | ✗ FAIL | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⊘ ENV |
| verina_basic_28 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_29 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_3 | ✓ 5269 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_30 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_31 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_32 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_33 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_34 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_35 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_36 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_37 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_38 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_41 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_42 | ✓ 1756 ms | ✓ 1747 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_43 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_44 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_45 | ✓ 1827 ms | ✓ 1878 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_46 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_47 | ✓ 1826 ms | ✗ FAIL | ✓ 1804 ms | ✗ FAIL | ✓ 1406 ms | ✓ 3626 ms | ✓ 1065 ms | ✓ 1066 ms | ✗ FAIL |
| verina_basic_48 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_49 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_5 | ✓ 1702 ms | ✓ 1694 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_50 | ✓ 5372 ms | ✓ 5384 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_55 | ✓ 1783 ms | ✓ 1793 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_56 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_57 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_58 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_59 | ✓ 1781 ms | ✓ 1769 ms | ✗ FAIL | ✗ FAIL | ✓ 1364 ms | ✓ 3430 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_6 | ✓ 5551 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_63 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_64 | ✗ FAIL | ✗ FAIL | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⏱ TIMEOUT | ⊘ ENV | ⊘ ENV | ⊘ ENV |
| verina_basic_65 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_66 | ✓ 5394 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_70 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_71 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ 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 | ✓ 1722 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_77 | ⏱ TIMEOUT | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_78 | ✓ 1764 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_79 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_8 | ✓ 1736 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_80 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_81 | ✓ 5443 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 | ⏱ TIMEOUT | ⊘ ENV | ⊘ ENV | ⊘ ENV |
| verina_basic_84 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_85 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_86 | ✗ FAIL | ✗ FAIL | ⊘ ENV | ⊘ ENV | ⊘ ENV | ⏱ TIMEOUT | ⊘ 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 | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_9 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_90 | ⏱ TIMEOUT | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_91 | ✓ 1654 ms | ✓ 1660 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3733 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_92 | ✓ 1697 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 | ✓ 1636 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✓ 3535 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_97 | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_98 | ✓ 1650 ms | ✓ 1659 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ⏱ TIMEOUT | ✗ FAIL | ✗ FAIL | ✗ FAIL |
| verina_basic_99 | ✓ 5142 ms | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL | ✗ FAIL |
Smt/Translate.lean), thrown on any lambda term. It is a translator gap, not a solver limitation — cvc5 itself supports higher-order reasoning and lambdas. It accounts for several STG4 failures.Tip: click any cell for its status and (for ENV) the exact Lean error.