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.0 s | (÷2.4) | 11.6 GB | (×3.2) | |
| sokonanoda | 👍 | 7.3 s | (÷2.4) | 11.6 GB | (×3.3) | |
| nanoclo | 👍 | 4.1 s | (÷4.2) | 3.1 GB | (-13%) | |
| con-ron | 👍 | 15.0 s | (-12%) | 5.4 GB | (+51%) | |
| lazylean | 👍 | 6.0 s | (÷2.9) | 1.3 GB | (÷2.7) | |
| nanoda | 👍 | 14.3 s | (-17%) | 4.1 GB | (+14%) | |
| nanobruijn | 👍 | 15.6 s | (-9%) | 3.5 GB | (-3%) | |
| con-leche | 👍 | 29.9 s | (+75%) | 5.3 GB | (+48%) | |
| eink0rn | 👍 | 22.3 s | (+30%) | 4.5 GB | (+25%) | |
| ind-models | 👍 | 17.5 s | (+2%) | 3.6 GB | (+1%) | |
| official | 👍 | 17.1 s | (0%) | 3.6 GB | (0%) | |
| lean4lean | 👍 | 23.7 s | (+38%) | 3.7 GB | (+4%) | |
| tenet | 👍 | 29.4 s | (+72%) | 5.7 GB | (+61%) | |
| nanoclo-fortran | 👍 | 13.3 s | (-22%) | 10.3 GB | (×2.9) | |
| lean4cobol | 👍 | 4.8 m | (×17) | 5.2 GB | (+46%) | |
| evmlean | 🚫 | 305 ms | 103.2 MB | |||
| mini | 🚫 | 59 ms | 73.8 MB | |||
| overfull | 💥 | 1.7 m | 49.4 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 | 💥 | 26.4 s | 146.3 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.5 MB | (÷54) |