{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R205",
  "content_hash": null,
  "slug": "ddg9-artifact-exhaustive-nine-search",
  "type": "artifact",
  "title": "Exhaustive nonexistence certificate for nine points",
  "summary": "A deterministic C backtracker visits 7,805,045 admissible prefixes and finds no valid set of size nine.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "Grid points are ordered first by \\(x\\), then by \\(y\\). The recursion adds points with strictly increasing indices, so every nine-element subset has one possible search path. Three 64-bit masks record used squared distances 0 through 128. Before recursing, the program checks that the new distances are mutually different and absent from the masks. It then checks the new point against every pair of selected points with an exact cross product.\n\nNode counts by selected-set size are\n\\[\n[1,73,2701,59535,701441,3234340,3441289,365239,426,0].\n\\]\nTheir sum is 7,805,045. The program considers 76,241,190 candidate extensions. Repeated distances reject 67,073,486, while collinearity rejects 1,362,660 after the distance check. The remaining 7,805,044 extensions are exactly the nonroot nodes in the search tree. No node reaches depth nine.\n\nThe source asserts every counter before printing its canonical trace. The SHA-256 digest of the complete stdout line, including its final newline, is `761705fa45b932b9871e8e5206d9b2bd774fe6abb4def4c28e6910904626482d`. The same executable verifies the eight-point witness before starting the nonexistence search.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "every nine-element subset of the 81 lattice points {0,...,8}^2",
    "bounds": {
      "grid_side": {
        "min": 9,
        "max": 9
      },
      "candidate_set_size": {
        "min": 9,
        "max": 9
      },
      "grid_points": {
        "min": 81,
        "max": 81
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_c_computation",
    "entrypoint": "join source_lines with newline as check.c, then run cc -O3 -std=c11 check.c -o check && ./check",
    "runtime": "ISO C11; approximately one second with Apple clang 21.0.0 at -O3",
    "citation": {
      "url": "https://doi.org/10.1007/BF01299744",
      "locator": "Inline ISO C11 source executed with Apple clang 21.0.0 on 2026-07-24"
    },
    "inline_source": [
      "#include <stdint.h>",
      "#include <stdio.h>",
      "#define V 81",
      "#define TARGET 9",
      "static uint8_t px[V],py[V],dist2[V][V];",
      "static int selected[TARGET];",
      "static uint64_t nodes[TARGET+1],attempts[TARGET],distance_rejects[TARGET],line_rejects[TARGET];",
      "static int search(int start,int depth,uint64_t used0,uint64_t used1,uint64_t used2){",
      "  ++nodes[depth];",
      "  if(depth==TARGET)return 1;",
      "  int last=V-(TARGET-depth);",
      "  for(int p=start;p<=last;p++){",
      "    ++attempts[depth];",
      "    uint64_t add0=0,add1=0,add2=0;",
      "    int ok=1;",
      "    for(int j=0;j<depth;j++){",
      "      int d=dist2[p][selected[j]];",
      "      uint64_t bit=UINT64_C(1)<<(d&63);",
      "      uint64_t *add=d<64?&add0:(d<128?&add1:&add2);",
      "      uint64_t used=d<64?used0:(d<128?used1:used2);",
      "      if((used|*add)&bit){ok=0;break;}",
      "      *add|=bit;",
      "    }",
      "    if(!ok){++distance_rejects[depth];continue;}",
      "    for(int i=0;i<depth&&ok;i++)for(int j=0;j<i;j++){",
      "      int lhs=(int)(px[p]-px[selected[i]])*(int)(py[selected[j]]-py[selected[i]]);",
      "      int rhs=(int)(py[p]-py[selected[i]])*(int)(px[selected[j]]-px[selected[i]]);",
      "      if(lhs==rhs){ok=0;break;}",
      "    }",
      "    if(!ok){++line_rejects[depth];continue;}",
      "    selected[depth]=p;",
      "    if(search(p+1,depth+1,used0|add0,used1|add1,used2|add2))return 1;",
      "  }",
      "  return 0;",
      "}",
      "static int verify_witness(void){",
      "  const int w[8][2]={{6,0},{8,8},{1,1},{1,3},{8,7},{5,7},{5,1},{6,5}};",
      "  uint8_t seen[129]={0};",
      "  for(int i=0;i<8;i++)for(int j=0;j<i;j++){",
      "    int dx=w[i][0]-w[j][0],dy=w[i][1]-w[j][1],d=dx*dx+dy*dy;",
      "    if(seen[d])return 0;",
      "    seen[d]=1;",
      "    for(int k=0;k<j;k++){",
      "      int lhs=(w[i][0]-w[j][0])*(w[k][1]-w[j][1]);",
      "      int rhs=(w[i][1]-w[j][1])*(w[k][0]-w[j][0]);",
      "      if(lhs==rhs)return 0;",
      "    }",
      "  }",
      "  return 1;",
      "}",
      "int main(void){",
      "  int k=0;",
      "  for(int x=0;x<9;x++)for(int y=0;y<9;y++){px[k]=x;py[k]=y;++k;}",
      "  for(int i=0;i<V;i++)for(int j=0;j<V;j++){",
      "    int dx=px[i]-px[j],dy=py[i]-py[j];",
      "    dist2[i][j]=dx*dx+dy*dy;",
      "  }",
      "  if(!verify_witness())return 2;",
      "  int found=search(0,0,0,0,0);",
      "  const uint64_t en[10]={1,73,2701,59535,701441,3234340,3441289,365239,426,0};",
      "  const uint64_t ea[9]={73,2701,67525,1106568,9974369,34927201,27906804,2253984,1965};",
      "  const uint64_t ed[9]={0,0,6412,358627,6328518,30731689,27393297,2252978,1965};",
      "  const uint64_t el[9]={0,0,1578,46500,411511,754223,148268,580,0};",
      "  if(found)return 3;",
      "  for(int d=0;d<=TARGET;d++)if(nodes[d]!=en[d])return 4;",
      "  for(int d=0;d<TARGET;d++)if(attempts[d]!=ea[d]||distance_rejects[d]!=ed[d]||line_rejects[d]!=el[d])return 5;",
      "  printf(\"witness=1 found9=0\");",
      "  for(int d=0;d<=TARGET;d++)printf(\" n%d=%llu\",d,(unsigned long long)nodes[d]);",
      "  for(int d=0;d<TARGET;d++)printf(\" a%d=%llu\",d,(unsigned long long)attempts[d]);",
      "  for(int d=0;d<TARGET;d++)printf(\" d%d=%llu\",d,(unsigned long long)distance_rejects[d]);",
      "  for(int d=0;d<TARGET;d++)printf(\" l%d=%llu\",d,(unsigned long long)line_rejects[d]);",
      "  putchar('\\n');",
      "  return 0;",
      "}"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1007/BF01299744",
    "locator": "Inline ISO C11 source executed with Apple clang 21.0.0 on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R208",
      "title": "The exact value is G_9=8",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "distinct-distance-grid-9",
      "title": "distinct distance grid 9",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}