Test "perf/magma-list-deep-n21"
Expected: 👍 accept · Size: 1.1 MB · Lines: 21.8 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 80.0 s · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 264 ms | (÷10) | 318.1 MB | (÷2.1) | |
| nano-lean | 👍 | 51.3 ms | (÷53) | 146.5 MB | (÷4.6) | |
| sokonanoda | 👍 | 286 ms | (÷9.4) | 476.4 MB | (-29%) | |
| pestka | 👍 | 128 ms | (÷21) | 25.2 MB | (÷26) | |
| kefir | 👍 | 79.6 ms | (÷34) | 31.1 MB | (÷21) | |
| nanoclo | 👍 | 166 ms | (÷16) | 153.9 MB | (÷4.3) | |
| kefir-wasm | 👍 | 565 ms | (÷4.8) | 132.9 MB | (÷5.0) | |
| con-ron | 👍 | 1.87 s | (-31%) | 368.9 MB | (-45%) | |
| con-agua | 👍 | 2.89 s | (+7%) | 262.1 MB | (÷2.5) | |
| nanoda | 👍 | 2.10 s | (-22%) | 271.0 MB | (÷2.5) | |
| lazylean | 👍 | 389 ms | (÷6.9) | 30.8 MB | (÷22) | |
| con-leche | 👍 | 3.93 s | (+46%) | 595.5 MB | (-11%) | |
| pestka-wasm | 👍 | 478 ms | (÷5.6) | 412.0 MB | (-38%) | |
| tenet-jvm | 👍 | 4.94 s | (+83%) | 1.0 GB | (+59%) | |
| eink0rn | 👍 | 1.91 s | (-29%) | 706.1 MB | (+6%) | |
| official | 👍 | 2.69 s | (0%) | 667.8 MB | (0%) | |
| ind-models | 👍 | 2.83 s | (+5%) | 705.7 MB | (+6%) | |
| lean4lean | 👍 | 3.51 s | (+30%) | 714.7 MB | (+7%) | |
| tenet | 👍 | 3.41 s | (+26%) | 1.3 GB | (+93%) | |
| tenet-hs | 👍 | 6.24 s | (×2.3) | 722.3 MB | (+8%) | |
| ocaml4lean | 👍 | 4.98 s | (+85%) | 786.7 MB | (+18%) | |
| lean4cobol | 👍 | 45.7 s | (×17) | 364.2 MB | (-45%) | |
| evmlean | 🚫 | 307 ms | 105.0 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 83.8 ms | 76.1 MB | |||
| canonical-min | 🚫 | 456 ms | 1.1 GB | |||
| kiota | 👍 | 2.09 s | (-22%) | 375.1 MB | (-44%) | |
| metalean-slow | 🚫 | 134 ms | 79.8 MB | |||
| nanobruijn | 👍 | 1.94 s | (-28%) | 250.4 MB | (÷2.7) | |
| metalean-fast | 👍 | 5.01 s | (+86%) | 752.5 MB | (+13%) | |
| nanoclo-fortran | 👍 | 930 ms | (÷2.9) | 463.9 MB | (-31%) | |
| rpylean | 👍 | 6.25 s | (×2.3) | 1.4 GB | (×2.1) | |
| mathgraph | 👍 | 356 ms | (÷7.6) | 754.1 MB | (+13%) | |
| parse-only | 👍 | 89.8 ms | (÷30) | 69.3 MB | (÷9.6) |