Test "perf/magma-list-deep-n36"
Expected: 👍 accept · Size: 1.2 MB · Lines: 23.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 6.50 min · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 36 with an inline List operation table satisfies
x = y ◇ (y ◇ (x ◇ (y ◇ x))) but not x = x ◇ (x ◇ x). The search space is
only 36^2 tuples, but each side of the equation nests the operation five
deep, so every tuple expands into a long chain of linear list lookups. The
heaviest test of the magma family.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). magma-list-deep-n21 is the same
workload at a smaller scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 3.43 s | (÷10) | 4.4 GB | (-45%) | |
| nano-lean | 👍 | 433 ms | (÷82) | 453.4 MB | (÷18) | |
| sokonanoda | 👍 | 3.72 s | (÷9.5) | 4.6 GB | (-41%) | |
| pestka | 👍 | 1.26 s | (÷28) | 38.4 MB | (÷209) | |
| kefir | 👍 | 451 ms | (÷78) | 74.4 MB | (÷108) | |
| nanoclo | 👍 | 1.23 s | (÷29) | 743.1 MB | (÷11) | |
| kefir-wasm | 👍 | 1.05 s | (÷34) | 193.3 MB | (÷42) | |
| con-ron | 👍 | 22.3 s | (-37%) | 2.5 GB | (÷3.2) | |
| con-agua | 👍 | 34.7 s | (-2%) | 2.3 GB | (÷3.4) | |
| nanoda | 👍 | 37.6 s | (+6%) | 2.5 GB | (÷3.2) | |
| lazylean | 👍 | 5.22 s | (÷6.8) | 46.1 MB | (÷175) | |
| con-leche | 👍 | 46.9 s | (+32%) | 7.3 GB | (-6%) | |
| pestka-wasm | 👍 | 1.78 s | (÷20) | 629.1 MB | (÷13) | |
| tenet-jvm | 👍 | 58.1 s | (+64%) | 7.6 GB | (-3%) | |
| eink0rn | 👍 | 38.1 s | (+8%) | 8.9 GB | (+13%) | |
| official | 👍 | 35.4 s | (0%) | 7.9 GB | (0%) | |
| ind-models | 👍 | 35.4 s | (0%) | 7.8 GB | (-1%) | |
| lean4lean | 👍 | 47.0 s | (+33%) | 7.9 GB | (+1%) | |
| tenet | 👍 | 76.7 s | (×2.2) | 11.9 GB | (+52%) | |
| tenet-hs | 👍 | 3.65 min | (×6.2) | 816.4 MB | (÷9.9) | |
| ocaml4lean | 👍 | 63.0 s | (+78%) | 8.8 GB | (+12%) | |
| lean4cobol | 👍 | 10.1 min | (×17) | 5.5 GB | (-31%) | |
| evmlean | 🚫 | 307 ms | 104.6 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 83.8 ms | 75.8 MB | |||
| canonical-min | 🚫 | 460 ms | 1.1 GB | |||
| kiota | 👍 | 28.3 s | (-20%) | 4.4 GB | (-44%) | |
| metalean-slow | 🚫 | 137 ms | 80.1 MB | |||
| nanobruijn | 👍 | 26.7 s | (-25%) | 2.7 GB | (÷2.9) | |
| metalean-fast | 💥 | 2.18 min | 6.7 GB | |||
| nanoclo-fortran | 👍 | 11.2 s | (÷3.2) | 5.8 GB | (-26%) | |
| rpylean | 👍 | 2.87 min | (×4.8) | 4.7 GB | (-40%) | |
| mathgraph | 👍 | 4.60 s | (÷7.7) | 7.5 GB | (-5%) | |
| parse-only | 👍 | 92.7 ms | (÷382) | 70.0 MB | (÷115) |