Test "perf/magma-list-pair-n21"
Expected: 👍 accept · Size: 583.1 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 4.33 min · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 3.15 s | (÷5.9) | 4.6 GB | (+17%) | |
| nano-lean | 👍 | 3.04 s | (÷6.1) | 2.6 GB | (-35%) | |
| sokonanoda | 👍 | 5.29 s | (÷3.5) | 7.6 GB | (+90%) | |
| pestka | 👍 | 4.04 s | (÷4.6) | 955.0 MB | (÷4.3) | |
| kefir | 👍 | 2.87 s | (÷6.4) | 988.7 MB | (÷4.1) | |
| nanoclo | 👍 | 3.71 s | (÷5.0) | 2.7 GB | (-32%) | |
| kefir-wasm | 👍 | 4.51 s | (÷4.1) | 1.7 GB | (÷2.3) | |
| con-ron | 👍 | 15.2 s | (-18%) | 5.3 GB | (+33%) | |
| con-agua | 👍 | 23.8 s | (+29%) | 4.0 GB | (0%) | |
| nanoda | 👍 | 14.2 s | (-23%) | 4.1 GB | (+2%) | |
| lazylean | 👍 | 6.34 s | (÷2.9) | 1.3 GB | (÷3.0) | |
| con-leche | 👍 | 31.1 s | (+68%) | 5.1 GB | (+28%) | |
| pestka-wasm | 👍 | 16.2 s | (-12%) | 1.8 GB | (÷2.2) | |
| tenet-jvm | 👍 | 19.6 s | (+6%) | 4.8 GB | (+20%) | |
| eink0rn | 👍 | 25.0 s | (+36%) | 5.0 GB | (+25%) | |
| official | 👍 | 18.5 s | (0%) | 4.0 GB | (0%) | |
| ind-models | 👍 | 18.6 s | (+1%) | 4.0 GB | (+1%) | |
| lean4lean | 👍 | 25.3 s | (+37%) | 4.1 GB | (+3%) | |
| tenet | 👍 | 31.3 s | (+69%) | 6.1 GB | (+54%) | |
| tenet-hs | 👍 | 37.4 s | (×2.0) | 2.4 GB | (-39%) | |
| ocaml4lean | 👍 | 32.4 s | (+76%) | 5.4 GB | (+37%) | |
| lean4cobol | 👍 | 5.35 min | (×17) | 8.1 GB | (×2.0) | |
| evmlean | 🚫 | 307 ms | 104.7 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 58.6 ms | 73.1 MB | |||
| canonical-min | 🚫 | 421 ms | 1.1 GB | |||
| kiota | 👍 | 15.4 s | (-17%) | 7.8 GB | (+97%) | |
| metalean-slow | 🚫 | 61.8 ms | 76.2 MB | |||
| nanobruijn | 👍 | 17.0 s | (-8%) | 3.6 GB | (-10%) | |
| metalean-fast | 👍 | 35.9 s | (+95%) | 5.1 GB | (+29%) | |
| nanoclo-fortran | 👍 | 13.3 s | (-28%) | 10.3 GB | (×2.6) | |
| rpylean | 👍 | 72.1 s | (×3.9) | 10.0 GB | (×2.5) | |
| mathgraph | ✋ | 8.69 s | 14.6 GB | |||
| parse-only | 👍 | 59.0 ms | (÷313) | 68.0 MB | (÷60) |