Test "perf/refute-cheap-last"
Expected: ✋ reject · Size: 20.5 KB · Lines: 439 · lean4export: 3.1.0 · Lean: 4.34.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 | ⏱️ | 🧠 | |||
|---|---|---|---|---|---|---|
| sokonanoda | ✋ | 2 ms | (÷79) | 38.3 MB | (-44%) | |
| mathgraph | ✋ | 3 ms | (÷60) | 45.9 MB | (-33%) | |
| nanoclo | ✋ | 21 ms | (÷8.6) | 53.8 MB | (-22%) | |
| con-ron | ✋ | 30 ms | (÷6.1) | 61.2 MB | (-11%) | |
| nanobruijn | ✋ | 5 ms | (÷38) | 10.5 MB | (÷6.6) | |
| nanoda | ✋ | 5 ms | (÷33) | 3.6 MB | (÷19) | |
| lazylean | ✋ | 10 ms | (÷18) | 25.8 MB | (÷2.7) | |
| con-leche | ✋ | 17 ms | (÷11) | 22.4 MB | (÷3.1) | |
| eink0rn | ✋ | 97 ms | (-46%) | 57.7 MB | (-16%) | |
| official | ✋ | 180 ms | (0%) | 68.9 MB | (0%) | |
| ind-models | ✋ | 247 ms | (+37%) | 105.8 MB | (+54%) | |
| lean4lean | ✋ | 1.3 s | (×7.2) | 102.9 MB | (+49%) | |
| tenet | ✋ | 567 ms | (×3.1) | 119.5 MB | (+73%) | |
| tenet-hs | ✋ | 195 ms | (+8%) | 73.9 MB | (+7%) | |
| lean4cobol | ✋ | 3.9 s | (×22) | 16.5 MB | (÷4.2) | |
| evmlean | 🚫 | 2.4 s | 276.9 MB | |||
| mini | ⌛ | 0 ms | 0 B | |||
| overfull | ⌛ | 0 ms | 0 B | |||
| metalean-slow | ⌛ | 0 ms | 0 B | |||
| tenet-jvm | ✋ | 626 ms | (×3.5) | 126.5 MB | (+84%) | |
| nanoclo-fortran | ✋ | 32 ms | (÷5.7) | 5.8 MB | (÷12) | |
| kiota | ✋ | 9 ms | (÷20) | 11.5 MB | (÷6.0) | |
| metalean-fast | ✋ | 206 ms | (+14%) | 76.3 MB | (+11%) | |
| canonical-min | 🚫 | 388 ms | 1.1 GB | |||
| rpylean | ✋ | 270 ms | (+50%) | 37.9 MB | (-45%) | |
| vow-lean-kernel | ✋ | 138 ms | (-24%) | 11.3 MB | (÷6.1) | |
| parse-only | 👍 | 28 ms | 66.3 MB |