Test "perf/magma-list-pair-n21"
Expected: 👍 accept · Size: 581.8 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 4.3 m · 📄 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 ◇ y = z ◇ w but not x = x ◇ x. Checking the certificate evaluates the
decidable instance over all 21^4 ≈ 195k four-tuples; every ◇ unfolds to a
linear lookup into the list. The widest search space of the magma family.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). magma-list-pair-n7 is the same
workload at a smaller scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 7.1 s | (÷2.4) | 11.6 GB | (×3.3) | |
| sokonanoda | 👍 | 7.3 s | (÷2.3) | 11.6 GB | (×3.3) | |
| nanoclo | 👍 | 14.4 s | (-16%) | 5.3 GB | (+50%) | |
| nanoda | 👍 | 14.3 s | (-17%) | 4.1 GB | (+14%) | |
| con-ron | 👍 | 27.4 s | (+60%) | 4.8 GB | (+33%) | |
| nanobruijn | 👍 | 15.6 s | (-9%) | 3.5 GB | (-3%) | |
| con-leche | 👍 | 29.9 s | (+75%) | 5.3 GB | (+48%) | |
| eink0rn | 👍 | 22.5 s | (+31%) | 4.5 GB | (+26%) | |
| ind-models | 👍 | 17.5 s | (+2%) | 3.6 GB | (+1%) | |
| official | 👍 | 17.1 s | (0%) | 3.6 GB | (0%) | |
| lean4lean | 👍 | 23.6 s | (+38%) | 3.7 GB | (+4%) | |
| tenet | 👍 | 29.4 s | (+72%) | 5.8 GB | (+64%) | |
| nanoclo-fortran | 👍 | 13.3 s | (-22%) | 10.4 GB | (×2.9) | |
| lean4cobol | 👍 | 4.8 m | (×17) | 5.2 GB | (+46%) | |
| evmlean | 🚫 | 306 ms | 105.9 MB | |||
| mini | 🚫 | 59 ms | 72.7 MB | |||
| overfull | 💥 | 1.3 m | 48.6 MB | |||
| kiota | 👍 | 15.3 s | (-11%) | 7.1 GB | (+99%) | |
| canonical-min | 🚫 | 421 ms | 1.1 GB | |||
| rpylean | 👍 | 1.2 m | (×4.1) | 6.5 GB | (+82%) | |
| vow-lean-kernel | 💥 | 20.1 s | 81.2 MB | |||
| official-v4.28.0 | 👍 | 23.8 s | (+39%) | 4.7 GB | (+32%) | |
| still-nanoda | 👍 | 13.7 s | (-20%) | 4.1 GB | (+14%) | |
| nyaya | 💥 | 5.1 s | 696.7 MB | |||
| parse-only | 👍 | 59 ms | (÷291) | 67.3 MB | (÷54) |