Test "perf/magma-list-pair-n7"
Expected: 👍 accept · Size: 582.4 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 1.0 m · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 7 with an inline List operation table satisfies
x ◇ y = z ◇ (w ◇ u) but not x = x ◇ x. Checking the certificate evaluates
the decidable instance over all 7^5 ≈ 17k five-tuples; every ◇ unfolds to
a linear lookup into the list.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). The small end of the list-table
family; magma-list-pair-n21 is the same workload at a larger scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 524 ms | (÷2.9) | 1.1 GB | (×2.8) | |
| sokonanoda | 👍 | 540 ms | (÷2.9) | 1.1 GB | (×2.8) | |
| nanoclo | 👍 | 418 ms | (÷3.7) | 411.7 MB | (+7%) | |
| con-ron | 👍 | 1.4 s | (-12%) | 957.5 MB | (×2.5) | |
| lazylean | 👍 | 512 ms | (÷3.0) | 128.4 MB | (÷3.0) | |
| nanoda | 👍 | 1.3 s | (-19%) | 322.4 MB | (-16%) | |
| nanobruijn | 👍 | 1.4 s | (-9%) | 318.3 MB | (-18%) | |
| con-leche | 👍 | 2.7 s | (+76%) | 496.4 MB | (+29%) | |
| eink0rn | 👍 | 1.6 s | (+1%) | 758.6 MB | (+97%) | |
| ind-models | 👍 | 1.6 s | (+6%) | 421.4 MB | (+9%) | |
| official | 👍 | 1.5 s | (0%) | 385.9 MB | (0%) | |
| lean4lean | 👍 | 2.1 s | (+38%) | 420.7 MB | (+9%) | |
| tenet | 👍 | 2.1 s | (+36%) | 866.3 MB | (×2.2) | |
| nanoclo-fortran | 👍 | 1.2 s | (-19%) | 818.9 MB | (×2.1) | |
| lean4cobol | 👍 | 26.3 s | (×17) | 534.9 MB | (+39%) | |
| evmlean | 🚫 | 306 ms | 106.1 MB | |||
| mini | 💥 | 1.3 m | 74.5 MB | |||
| overfull | 💥 | 1.7 m | 49.3 MB | |||
| kiota | 👍 | 1.4 s | (-10%) | 559.2 MB | (+45%) | |
| canonical-min | 🚫 | 422 ms | 1.1 GB | |||
| rpylean | 👍 | 6.2 s | (×4.0) | 2.6 GB | (×6.8) | |
| vow-lean-kernel | 💥 | 31.3 s | 146.4 MB | |||
| official-v4.28.0 | 👍 | 2.2 s | (+41%) | 507.6 MB | (+32%) | |
| still-nanoda | 👍 | 1.2 s | (-22%) | 322.4 MB | (-16%) | |
| nyaya | 💥 | 5.0 s | 698.6 MB | |||
| parse-only | 👍 | 59 ms | (÷26) | 69.8 MB | (÷5.5) |