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.7) | 1.4 GB | (+66%) | |
| sokonanoda | 👍 | 1.2 s | (÷6.5) | 1.4 GB | (+66%) | |
| nanoclo | 👍 | 1.5 s | (÷5.0) | 422.0 MB | (÷2.1) | |
| con-ron | 👍 | 5.0 s | (-34%) | 853.9 MB | (-4%) | |
| lazylean | 👍 | 3.5 s | (÷2.2) | 157.6 MB | (÷5.7) | |
| nanoda | 👍 | 5.8 s | (-24%) | 570.1 MB | (-36%) | |
| nanobruijn | 👍 | 5.1 s | (-33%) | 544.8 MB | (-39%) | |
| con-leche | 👍 | 11.5 s | (+51%) | 988.0 MB | (+11%) | |
| eink0rn | 👍 | 5.5 s | (-28%) | 996.2 MB | (+11%) | |
| 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.5 MB | (+4%) | |
| tenet | 👍 | 13.1 s | (+72%) | 1.7 GB | (+95%) | |
| nanoclo-fortran | 👍 | 4.4 s | (-42%) | 1.5 GB | (+69%) | |
| lean4cobol | 👍 | 1.9 m | (×15) | 722.3 MB | (-19%) | |
| evmlean | 🚫 | 307 ms | 105.2 MB | |||
| mini | 🚫 | 39 ms | 73.5 MB | |||
| overfull | 💥 | 1.7 m | 49.0 MB | |||
| kiota | 👍 | 44.9 s | (×5.9) | 944.2 MB | (+6%) | |
| canonical-min | 🚫 | 1.4 s | 1.1 GB | |||
| rpylean | 👍 | 23.9 s | (×3.1) | 3.0 GB | (×3.4) | |
| vow-lean-kernel | 💥 | 57.3 s | 308.5 MB | |||
| official-v4.28.0 | 👍 | 28.5 s | (×3.7) | 1.5 GB | (+72%) | |
| still-nanoda | 👍 | 6.5 s | (-15%) | 572.1 MB | (-36%) | |
| nyaya | ✋ | 1.5 s | 174.8 MB | |||
| parse-only | 👍 | 923 ms | (÷8.3) | 95.7 MB | (÷9.3) |