Test "perf/magma-string-pair-n9"
Expected: 👍 accept · Size: 16.6 MB · Lines: 344.3 k · lean4export: 3.1.0 · Lean: 4.34.1 · Timeout: 2.17 min · 📄 Declaration · 🔗 Source
Countermodel certificate for an equational-theories implication, closed by
decide. A magma on Fin 9 with the operation table encoded as a String
satisfies x ◇ y = (((z ◇ w) ◇ y) ◇ x) ◇ y but not
x ◇ y = ((z ◇ (z ◇ y)) ◇ x) ◇ y. Checking the certificate evaluates the
decidable instance over all 9^4 ≈ 6.5k four-tuples, decoding each table
entry out of the string on every lookup. The heaviest of the string-table
tests.
From a corpus of certificates generated for the SAIR math distillation
challenge (equational theories track). magma-string-n4 is the same
workload at a smaller scale.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| logos-kernel | 👍 | 672 ms | (÷12) | 866.0 MB | (-13%) | |
| nano-lean | 👍 | 517 ms | (÷16) | 541.8 MB | (-46%) | |
| sokonanoda | 👍 | 841 ms | (÷9.8) | 886.3 MB | (-11%) | |
| pestka | 👍 | 1.05 s | (÷7.8) | 221.6 MB | (÷4.5) | |
| kefir | 👍 | 1.36 s | (÷6.0) | 232.9 MB | (÷4.3) | |
| nanoclo | 👍 | 1.51 s | (÷5.5) | 419.8 MB | (÷2.4) | |
| kefir-wasm | 👍 | 2.62 s | (÷3.1) | 398.1 MB | (÷2.5) | |
| con-ron | 👍 | 5.31 s | (-35%) | 784.5 MB | (-22%) | |
| con-agua | 👍 | 8.15 s | (-1%) | 661.4 MB | (-34%) | |
| nanoda | 👍 | 6.08 s | (-26%) | 564.2 MB | (-44%) | |
| lazylean | 👍 | 3.43 s | (÷2.4) | 158.2 MB | (÷6.3) | |
| con-leche | 👍 | 11.8 s | (+44%) | 966.4 MB | (-3%) | |
| pestka-wasm | 👍 | 4.33 s | (-47%) | 852.1 MB | (-15%) | |
| tenet-jvm | 👍 | 14.8 s | (+80%) | 2.4 GB | (×2.4) | |
| eink0rn | 👍 | 5.99 s | (-27%) | 1.0 GB | (+6%) | |
| official | 👍 | 8.22 s | (0%) | 999.6 MB | (0%) | |
| ind-models | 👍 | 8.80 s | (+7%) | 1.0 GB | (+3%) | |
| lean4lean | 👍 | 11.8 s | (+43%) | 1.0 GB | (+3%) | |
| tenet | 👍 | 13.3 s | (+62%) | 2.2 GB | (×2.3) | |
| tenet-hs | 👍 | 15.0 s | (+82%) | 894.7 MB | (-10%) | |
| ocaml4lean | 👍 | 11.4 s | (+39%) | 1.3 GB | (+31%) | |
| lean4cobol | 👍 | 2.07 min | (×15) | 1.1 GB | (+8%) | |
| evmlean | 🚫 | 307 ms | 104.5 MB | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| vow-lean-kernel | ⌛ | 0 ms | 0 B | |||
| mini | 🚫 | 38.8 ms | 73.7 MB | |||
| canonical-min | 🚫 | 1.38 s | 1.1 GB | |||
| kiota | 👍 | 6.64 s | (-19%) | 1.0 GB | (+6%) | |
| metalean-slow | 🚫 | 771 ms | 82.8 MB | |||
| nanobruijn | 👍 | 5.58 s | (-32%) | 539.8 MB | (-46%) | |
| metalean-fast | 👍 | 15.6 s | (+90%) | 1.2 GB | (+18%) | |
| nanoclo-fortran | 👍 | 4.47 s | (-46%) | 1.5 GB | (+51%) | |
| rpylean | 👍 | 25.0 s | (×3.0) | 2.8 GB | (×2.8) | |
| mathgraph | 👍 | 1.13 s | (÷7.3) | 1.5 GB | (+50%) | |
| parse-only | 👍 | 926 ms | (÷8.9) | 95.6 MB | (÷10) |