Test "perf/magma-list-deep-n36"
Expected: 👍 accept · Size: 1.2 MB · Lines: 22.8 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 6.5 m · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 4.5 s | (÷6.5) | 7.7 GB | (+21%) | |
| sokonanoda | 👍 | 4.6 s | (÷6.3) | 7.7 GB | (+21%) | |
| nanoclo | 👍 | 1.2 s | (÷24) | 686.1 MB | (÷9.5) | |
| con-ron | 👍 | 54.6 s | (+87%) | 5.0 GB | (-22%) | |
| lazylean | 👍 | 5.2 s | (÷5.6) | 45.9 MB | (÷142) | |
| nanoda | 👍 | 36.4 s | (+25%) | 2.4 GB | (÷2.6) | |
| nanobruijn | 👍 | 22.0 s | (-25%) | 2.3 GB | (÷2.7) | |
| con-leche | 👍 | 41.4 s | (+42%) | 7.2 GB | (+13%) | |
| eink0rn | 👍 | 22.0 s | (-24%) | 3.7 GB | (-42%) | |
| ind-models | 👍 | 29.9 s | (+2%) | 6.4 GB | (+1%) | |
| official | 👍 | 29.2 s | (0%) | 6.4 GB | (0%) | |
| lean4lean | 👍 | 39.1 s | (+34%) | 6.4 GB | (+1%) | |
| tenet | 👍 | 56.3 s | (+93%) | 8.8 GB | (+38%) | |
| nanoclo-fortran | 👍 | 10.8 s | (÷2.7) | 5.8 GB | (-9%) | |
| lean4cobol | 👍 | 8.3 m | (×17) | 5.5 GB | (-14%) | |
| evmlean | 🚫 | 305 ms | 106.4 MB | |||
| mini | 🚫 | 83 ms | 75.3 MB | |||
| overfull | 💥 | 1.5 m | 48.9 MB | |||
| kiota | 👍 | 23.7 s | (-19%) | 3.7 GB | (-42%) | |
| canonical-min | 🚫 | 458 ms | 1.1 GB | |||
| rpylean | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | 💥 | 37.9 s | 392.9 MB | |||
| official-v4.28.0 | 👍 | 2.1 m | (×4.2) | 11.5 GB | (+81%) | |
| still-nanoda | 👍 | 34.5 s | (+18%) | 2.4 GB | (÷2.6) | |
| nyaya | ✋ | 358 ms | 49.1 MB | |||
| parse-only | 👍 | 92 ms | (÷318) | 69.3 MB | (÷94) |