Test "perf/magma-list-deep-n21"
Expected: 👍 accept · Size: 1.1 MB · Lines: 21.6 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 1.3 m · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 21 with an inline List operation table satisfies
x = (x ◇ x) ◇ (x ◇ (y ◇ y)) but not x = x ◇ (x ◇ x). The search space is
only 21^2 tuples, but each equation nests the operation several deep, so
every tuple expands into a chain of linear list lookups.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). The small end of the deep-nesting
family; magma-list-deep-n36 is the same workload at a larger scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 349 ms | (÷6.5) | 656.0 MB | (+18%) | |
| sokonanoda | 👍 | 364 ms | (÷6.2) | 667.8 MB | (+20%) | |
| nanoclo | 👍 | 602 ms | (÷3.8) | 379.2 MB | (-32%) | |
| nanoda | 👍 | 1.9 s | (-17%) | 216.1 MB | (÷2.6) | |
| con-ron | 👍 | 3.1 s | (+36%) | 518.9 MB | (-7%) | |
| nanobruijn | 👍 | 1.6 s | (-30%) | 207.4 MB | (÷2.7) | |
| con-leche | 👍 | 3.4 s | (+51%) | 598.9 MB | (+7%) | |
| eink0rn | 👍 | 1.4 s | (-39%) | 617.2 MB | (+11%) | |
| ind-models | 👍 | 2.4 s | (+7%) | 589.9 MB | (+6%) | |
| official | 👍 | 2.3 s | (0%) | 557.2 MB | (0%) | |
| lean4lean | 👍 | 3.0 s | (+31%) | 585.4 MB | (+5%) | |
| tenet | 👍 | 2.9 s | (+30%) | 1.1 GB | (+94%) | |
| nanoclo-fortran | 👍 | 896 ms | (÷2.5) | 453.7 MB | (-19%) | |
| lean4cobol | 👍 | 37.9 s | (×17) | 363.9 MB | (-35%) | |
| evmlean | 🚫 | 306 ms | 105.6 MB | |||
| mini | 🚫 | 83 ms | 74.6 MB | |||
| overfull | 💥 | 1.4 m | 48.6 MB | |||
| kiota | 👍 | 1.8 s | (-21%) | 305.7 MB | (-45%) | |
| canonical-min | 🚫 | 455 ms | 1.1 GB | |||
| rpylean | 👍 | 6.1 s | (×2.7) | 1.4 GB | (×2.5) | |
| vow-lean-kernel | 💥 | 44.1 s | 302.7 MB | |||
| official-v4.28.0 | 👍 | 7.5 s | (×3.3) | 959.8 MB | (+72%) | |
| still-nanoda | 👍 | 1.7 s | (-23%) | 215.7 MB | (÷2.6) | |
| nyaya | ✋ | 333 ms | 47.9 MB | |||
| parse-only | 👍 | 89 ms | (÷25) | 69.0 MB | (÷8.1) |