Test "perf/magma-list-pair-n7"
Expected: 👍 accept · Size: 583.6 KB · Lines: 11.0 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 60.0 s · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 261 ms | (÷6.5) | 425.0 MB | (0%) | |
| nano-lean | 👍 | 267 ms | (÷6.3) | 353.8 MB | (-17%) | |
| sokonanoda | 👍 | 383 ms | (÷4.4) | 745.8 MB | (+75%) | |
| pestka | 👍 | 316 ms | (÷5.3) | 98.9 MB | (÷4.3) | |
| kefir | 👍 | 247 ms | (÷6.8) | 131.5 MB | (÷3.2) | |
| nanoclo | 👍 | 403 ms | (÷4.2) | 375.5 MB | (-12%) | |
| kefir-wasm | 👍 | 756 ms | (÷2.2) | 257.2 MB | (-40%) | |
| con-ron | 👍 | 1.38 s | (-18%) | 526.0 MB | (+24%) | |
| con-agua | 👍 | 2.15 s | (+28%) | 342.7 MB | (-19%) | |
| nanoda | 👍 | 1.27 s | (-24%) | 339.3 MB | (-20%) | |
| lazylean | 👍 | 540 ms | (÷3.1) | 128.4 MB | (÷3.3) | |
| con-leche | 👍 | 2.81 s | (+67%) | 475.2 MB | (+12%) | |
| pestka-wasm | 👍 | 1.61 s | (-5%) | 673.4 MB | (+58%) | |
| tenet-jvm | 👍 | 2.56 s | (+52%) | 601.7 MB | (+41%) | |
| eink0rn | 👍 | 1.70 s | (+1%) | 798.7 MB | (+88%) | |
| official | 👍 | 1.69 s | (0%) | 425.6 MB | (0%) | |
| ind-models | 👍 | 1.80 s | (+7%) | 465.6 MB | (+9%) | |
| lean4lean | 👍 | 2.28 s | (+35%) | 458.6 MB | (+8%) | |
| tenet | 👍 | 2.41 s | (+43%) | 777.9 MB | (+83%) | |
| tenet-hs | 👍 | 3.29 s | (+95%) | 571.2 MB | (+34%) | |
| ocaml4lean | 👍 | 3.14 s | (+86%) | 593.0 MB | (+39%) | |
| lean4cobol | 👍 | 29.2 s | (×17) | 536.1 MB | (+26%) | |
| evmlean | 🚫 | 306 ms | 103.9 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | ⌛ | 0 ms | 0 B | |||
| canonical-min | 🚫 | 422 ms | 1.1 GB | |||
| kiota | 👍 | 1.40 s | (-17%) | 687.2 MB | (+61%) | |
| metalean-slow | 🚫 | 61.2 ms | 75.2 MB | |||
| nanobruijn | 👍 | 1.53 s | (-9%) | 338.5 MB | (-20%) | |
| metalean-fast | 👍 | 3.26 s | (+93%) | 550.4 MB | (+29%) | |
| nanoclo-fortran | 👍 | 1.25 s | (-26%) | 811.9 MB | (+91%) | |
| rpylean | 👍 | 6.35 s | (×3.8) | 2.6 GB | (×6.3) | |
| mathgraph | 👍 | 532 ms | (÷3.2) | 1.1 GB | (×2.6) | |
| parse-only | 👍 | 59.0 ms | (÷29) | 68.2 MB | (÷6.2) |