{
  "harness": "sj-harness 0.3.0",
  "host": {
    "platform": "darwin",
    "arch": "arm64",
    "node": "v26.10.0"
  },
  "command": {
    "command": "echo \"sj_harness_582890bab67e7b2b_lean $(lean --version 2>&1 | head -n 1)\"\n(cd .sj-proofs && lean --root=. -o SJProof0.olean SJProof0.lean); echo \"sj_harness_582890bab67e7b2b_exit0 $?\"",
    "from": "checker",
    "files": [
      "proofs/SB3.lean"
    ]
  },
  "engine": {
    "name": "docker",
    "version": "29.4.0"
  },
  "limits": {
    "minutes": 15,
    "memory": "12030m",
    "cpus": 12,
    "pids": 4096
  },
  "image": {
    "plan": {
      "from": "Dockerfile",
      "file": "env/Dockerfile"
    },
    "ref": "sj-harness:9c514e2f79760091",
    "id": "sha256:2c3d715ac75b0d1d68fdbd80d38c0d783812bf56e68aeb6fdd57bd59e48d257c",
    "digests": [],
    "reused": false,
    "seconds": 150.955
  },
  "result": {
    "exitCode": 0,
    "timedOut": false,
    "outOfMemory": false,
    "startedAt": "2026-10-07T06:07:21.777Z",
    "finishedAt": "2026-10-07T06:07:48.825Z",
    "seconds": 27.048
  },
  "judges": [
    {
      "checker": "lean4",
      "limits": {
        "minutes": 15,
        "memory": "12030m",
        "cpus": 12,
        "pids": 4096
      },
      "image": {
        "plan": {
          "from": "judge",
          "image": {
            "checker": "lean4",
            "toolchain": "leanprover/lean4:v4.34.1"
          }
        },
        "ref": "sj-harness:06e9c5b60df7148d",
        "id": "sha256:09b6b08a944470b323fb5401232a3f5811de0ef818063b177e4200b1afde849e",
        "digests": [],
        "reused": true,
        "seconds": 0.054
      },
      "command": "LEAN_PATH=\"$(cat /opt/sj-lean/lean-path)\" lean --run judge/Judge.lean '{\"out\":\"/work/compiled\",\"asks\":[{\"module\":\"SJProof0\",\"theorem\":[\"SB\",\"sb3_hamiltonian_cycle\"]}]}'",
      "result": {
        "exitCode": 0,
        "timedOut": false,
        "outOfMemory": false,
        "startedAt": "2026-10-07T06:07:49.011Z",
        "finishedAt": "2026-10-07T06:08:07.794Z",
        "seconds": 18.783
      }
    }
  ]
}