Test "perf/magma-string-pair-n9"
Expected: 👍 accept · Size: 16.5 MB · Lines: 342.4 k · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 2.2 m · 📄 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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | 👍 | 1.1 s | (÷6.8) | 1.5 GB | (+67%) | |
| sokonanoda | 👍 | 1.2 s | (÷6.5) | 1.4 GB | (+65%) | |
| nanoclo | 👍 | 2.4 s | (÷3.1) | 925.6 MB | (+4%) | |
| nanoda | 👍 | 5.8 s | (-24%) | 571.3 MB | (-36%) | |
| con-ron | 👍 | 10.1 s | (+33%) | 911.7 MB | (+2%) | |
| nanobruijn | 👍 | 5.1 s | (-33%) | 540.2 MB | (-40%) | |
| con-leche | 👍 | 11.5 s | (+51%) | 992.1 MB | (+11%) | |
| eink0rn | 👍 | 5.5 s | (-28%) | 1002.5 MB | (+12%) | |
| ind-models | 👍 | 8.6 s | (+13%) | 930.4 MB | (+4%) | |
| official | 👍 | 7.6 s | (0%) | 893.6 MB | (0%) | |
| lean4lean | 👍 | 10.9 s | (+43%) | 925.8 MB | (+4%) | |
| tenet | 👍 | 13.7 s | (+80%) | 1.9 GB | (×2.1) | |
| nanoclo-fortran | 👍 | 4.4 s | (-42%) | 1.5 GB | (+67%) | |
| lean4cobol | 👍 | 1.9 m | (×15) | 722.5 MB | (-19%) | |
| evmlean | 🚫 | 305 ms | 103.1 MB | |||
| mini | 🚫 | 39 ms | 73.5 MB | |||
| overfull | 💥 | 1.6 m | 49.2 MB | |||
| kiota | 👍 | 44.9 s | (×5.9) | 942.7 MB | (+5%) | |
| canonical-min | 🚫 | 1.4 s | 1.1 GB | |||
| rpylean | 👍 | 23.9 s | (×3.1) | 3.0 GB | (×3.4) | |
| vow-lean-kernel | 💥 | 50.1 s | 243.4 MB | |||
| official-v4.28.0 | 👍 | 28.6 s | (×3.7) | 1.5 GB | (+72%) | |
| still-nanoda | 👍 | 6.5 s | (-15%) | 568.6 MB | (-36%) | |
| nyaya | ✋ | 1.5 s | 175.1 MB | |||
| parse-only | 👍 | 923 ms | (÷8.3) | 96.1 MB | (÷9.3) |