Test "perf/refute-cheap-last"
Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.29.1 · Timeout: 50.0 s · 📄 Declaration · 🔗 Source
The declaration to check claims
(count #n, false) = (count #(n+1), true)
and must be rejected: refute-cheap-first.lean with the components swapped,
so the cheap refutation sits behind the expensive one for a checker that
visits components left to right.
N=200 in the Lean source. From Courant and Leroy, POPL 2026, §10.
| Checker | Result | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| mathgraph | ✋ | 3 ms | (÷61) | 45.9 MB | (-33%) | |
| sokonanoda | ✋ | 3 ms | (÷61) | 41.9 MB | (-39%) | |
| nanoclo | ✋ | 21 ms | (÷8.6) | 53.7 MB | (-22%) | |
| con-ron | ✋ | 28 ms | (÷6.5) | 65.0 MB | (-5%) | |
| lazylean | ✋ | 10 ms | (÷17) | 23.2 MB | (÷3.0) | |
| nanoda | ✋ | 5 ms | (÷33) | 3.4 MB | (÷20) | |
| nanobruijn | ✋ | 24 ms | (÷7.5) | 10.3 MB | (÷6.7) | |
| con-leche | ✋ | 13 ms | (÷13) | 26.0 MB | (÷2.6) | |
| eink0rn | ✋ | 97 ms | (-46%) | 56.6 MB | (-18%) | |
| ind-models | ✋ | 723 ms | (×4.0) | 107.7 MB | (+57%) | |
| official | ✋ | 181 ms | (0%) | 68.6 MB | (0%) | |
| lean4lean | ✋ | 1.3 s | (×7.2) | 106.7 MB | (+56%) | |
| tenet | ✋ | 566 ms | (×3.1) | 118.9 MB | (+73%) | |
| nanoclo-fortran | ✋ | 32 ms | (÷5.7) | 5.7 MB | (÷12) | |
| lean4cobol | ✋ | 3.9 s | (×22) | 16.6 MB | (÷4.1) | |
| evmlean | 🚫 | 1.9 s | 135.1 MB | |||
| mini | 💥 | 1.6 m | 77.0 MB | |||
| overfull | 💥 | 1.5 m | 48.2 MB | |||
| kiota | ✋ | 9 ms | (÷19) | 11.3 MB | (÷6.1) | |
| canonical-min | 🚫 | 388 ms | 1.1 GB | |||
| rpylean | ✋ | 277 ms | (+53%) | 38.0 MB | (-45%) | |
| vow-lean-kernel | ✋ | 138 ms | (-24%) | 11.2 MB | (÷6.2) | |
| official-v4.28.0 | ✋ | 773 ms | (×4.3) | 76.0 MB | (+11%) | |
| still-nanoda | ✋ | 34 ms | (÷5.4) | 3.5 MB | (÷19) | |
| nyaya | 💥 | 2.0 m | 16.0 MB | |||
| parse-only | 👍 | 28 ms | 65.7 MB |