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 | 👍 | 542 ms | (÷2.8) | 1.1 GB | (×2.8) | |
| nanoclo | 👍 | 716 ms | (÷2.2) | 632.3 MB | (+64%) | |
| nanoda | 👍 | 1.3 s | (-19%) | 322.3 MB | (-16%) | |
| con-ron | 👍 | 2.4 s | (+57%) | 440.5 MB | (+14%) | |
| nanobruijn | 👍 | 1.4 s | (-9%) | 320.1 MB | (-17%) | |
| con-leche | 👍 | 2.7 s | (+75%) | 496.4 MB | (+29%) | |
| eink0rn | 👍 | 1.6 s | (+2%) | 758.1 MB | (+96%) | |
| ind-models | 👍 | 1.6 s | (+6%) | 420.7 MB | (+9%) | |
| official | 👍 | 1.5 s | (0%) | 385.9 MB | (0%) | |
| lean4lean | 👍 | 2.1 s | (+37%) | 420.4 MB | (+9%) | |
| tenet | 👍 | 2.4 s | (+53%) | 702.7 MB | (+82%) | |
| nanoclo-fortran | 👍 | 1.2 s | (-19%) | 808.5 MB | (×2.1) | |
| lean4cobol | 👍 | 26.3 s | (×17) | 534.8 MB | (+39%) | |
| evmlean | 🚫 | 306 ms | 105.3 MB | |||
| mini | 💥 | 1.3 m | 73.5 MB | |||
| overfull | 💥 | 1.6 m | 49.4 MB | |||
| kiota | 👍 | 1.4 s | (-10%) | 559.3 MB | (+45%) | |
| canonical-min | 🚫 | 421 ms | 1.1 GB | |||
| rpylean | 👍 | 6.2 s | (×4.0) | 2.6 GB | (×6.8) | |
| vow-lean-kernel | 💥 | 19.9 s | 81.1 MB | |||
| official-v4.28.0 | 👍 | 2.2 s | (+41%) | 507.2 MB | (+31%) | |
| still-nanoda | 👍 | 1.2 s | (-22%) | 322.4 MB | (-16%) | |
| nyaya | 💥 | 5.0 s | 698.7 MB | |||
| parse-only | 👍 | 59 ms | (÷26) | 69.3 MB | (÷5.6) |