{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R140",
  "content_hash": null,
  "slug": "cgr127-artifact-exhaustive-size-12-search",
  "type": "artifact",
  "title": "Complete colored search excluding an independent 12-set",
  "summary": "Inline Python visits 117,239 search nodes and exhausts every possible 12-clique branch in the complement.",
  "relevance": "This supplies a computation, dataset, or executable check used to assess the target problem.",
  "relevance_source": "derived",
  "body": "The program constructs the 42-element cube set directly, then builds all 127 adjacency rows of \\(G\\) and \\(\\overline G\\). Each row is a 127-bit integer. It checks primality of 127, the size and negation closure of the cube set, graph symmetry, every degree, and all 55 pairs of the displayed independent set before beginning the upper-bound search.\n\nAt each search node, `color_sort` greedily partitions the candidate-induced subgraph of \\(\\overline G\\) into independent color classes. A clique uses at most one vertex of each class. The color number attached to each vertex therefore bounds the size of a clique in the corresponding candidate prefix. The search processes vertices in reverse color order. It explores the branch containing the current vertex, removes that vertex, then proceeds to the next branch. If the selected depth plus the prefix color bound is below 12, the whole prefix is safely discarded. These are the only cutoffs.\n\nThe full run finds no clique of order 12. It visits 117,239 nodes and makes 117,238 recursive branches. The node counts by selected depth are\n\\[\n[1,94,2306,18163,48068,38101,9387,1034,85,0,0,0,0].\n\\]\nEvery terminal node ends at a coloring-bound cutoff. A SHA-256 trace mixes each node, branch, and cutoff with its depth and full 127-bit candidate mask, ending at `60d93eb7946529959e490bd7358c5826dd9b791496371ea4113efb5e5ae77452`. The stable eleven-line output has SHA-256 digest `d8211716032b2b4106352be3cc946ae5c6e85ae39dab2c25534b801e83e6242d`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "bounded",
    "statement": "all cliques of order 12 in the complement of the cubic-residue graph on Z/127Z",
    "bounds": {
      "modulus": {
        "min": 127,
        "max": 127
      },
      "candidate_vertices": {
        "min": 127,
        "max": 127
      },
      "target_clique_size": {
        "min": 12,
        "max": 12
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_exhaustive_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later, standard library only",
    "citation": {
      "url": "https://www.cs.rit.edu/~spr/PUBL/dim09talk.pdf",
      "locator": "Inline CPython source below, executed on 2026-07-24"
    },
    "inline_source": [
      "from hashlib import sha256",
      "P=127",
      "TARGET=12",
      "WIDTH=(P+7)//8",
      "WITNESS=(10,13,27,41,44,55,70,85,96,111,126)",
      "ALL=(1<<P)-1",
      "CUBES=tuple(sorted({pow(x,3,P) for x in range(1,P)}))",
      "assert P>2 and all(P%d for d in range(2,int(P**0.5)+1))",
      "assert len(CUBES)==42 and P-1 in CUBES",
      "cube_set=set(CUBES)",
      "graph=[]",
      "for x in range(P):",
      "    row=0",
      "    for y in range(P):",
      "        if x!=y and (x-y)%P in cube_set:",
      "            row |= 1<<y",
      "    graph.append(row)",
      "assert all(bin(row).count('1')==42 for row in graph)",
      "assert all(((graph[x]>>y)&1)==((graph[y]>>x)&1)",
      "           for x in range(P) for y in range(P))",
      "complement=[ALL ^ graph[x] ^ (1<<x) for x in range(P)]",
      "assert all(bin(row).count('1')==84 for row in complement)",
      "assert all(not ((graph[x]>>y)&1)",
      "           for i,x in enumerate(WITNESS) for y in WITNESS[i+1:])",
      "assert all(((complement[x]>>y)&1)",
      "           for i,x in enumerate(WITNESS) for y in WITNESS[i+1:])",
      "visits=[0]*(TARGET+1)",
      "branches=[0]*(TARGET+1)",
      "bound_prunes=[0]*(TARGET+1)",
      "exhausted=[0]*(TARGET+1)",
      "trace=sha256()",
      "found=[]",
      "",
      "def event(tag,depth,aux,candidates):",
      "    trace.update(tag)",
      "    trace.update(bytes((depth,aux)))",
      "    trace.update(candidates.to_bytes(WIDTH,'little'))",
      "",
      "def color_sort(candidates):",
      "    order=[]",
      "    bounds=[]",
      "    uncolored=candidates",
      "    color=0",
      "    while uncolored:",
      "        color += 1",
      "        available=uncolored",
      "        while available:",
      "            bit=available & -available",
      "            vertex=bit.bit_length()-1",
      "            order.append(vertex)",
      "            bounds.append(color)",
      "            uncolored ^= bit",
      "            available ^= bit",
      "            available &= ~complement[vertex]",
      "    return order,bounds",
      "",
      "def search(candidates,chosen):",
      "    depth=len(chosen)",
      "    visits[depth]+=1",
      "    event(b'E',depth,0,candidates)",
      "    if depth==TARGET:",
      "        found[:]=chosen",
      "        return True",
      "    order,bounds=color_sort(candidates)",
      "    for i in range(len(order)-1,-1,-1):",
      "        if depth+bounds[i] < TARGET:",
      "            bound_prunes[depth]+=1",
      "            event(b'P',depth,bounds[i],candidates)",
      "            return False",
      "        vertex=order[i]",
      "        bit=1<<vertex",
      "        branches[depth]+=1",
      "        event(b'B',depth,vertex,candidates)",
      "        if search(candidates & complement[vertex],chosen+[vertex]):",
      "            return True",
      "        candidates ^= bit",
      "    exhausted[depth]+=1",
      "    event(b'X',depth,0,candidates)",
      "    return False",
      "",
      "has_twelve=search(ALL,[])",
      "assert not has_twelve and not found",
      "cube_serial=(','.join(map(str,CUBES))+'\\n').encode()",
      "graph_serial=b''.join(row.to_bytes(WIDTH,'little') for row in graph)",
      "comp_serial=b''.join(row.to_bytes(WIDTH,'little') for row in complement)",
      "witness_serial=(','.join(map(str,WITNESS))+'\\n').encode()",
      "print('graph vertices 127 degree 42 edges 2667 complement_degree 84')",
      "print('cubes_sha256',sha256(cube_serial).hexdigest())",
      "print('graph_rows_sha256',sha256(graph_serial).hexdigest())",
      "print('complement_rows_sha256',sha256(comp_serial).hexdigest())",
      "print('witness_size 11 pairs_checked 55 sha256',",
      "      sha256(witness_serial).hexdigest())",
      "print('target_size 12 found 0')",
      "print('visits',sum(visits),'by_depth',','.join(map(str,visits)))",
      "print('branches',sum(branches),'by_depth',','.join(map(str,branches)))",
      "print('bound_prunes',sum(bound_prunes),'by_depth',",
      "      ','.join(map(str,bound_prunes)))",
      "print('exhausted',sum(exhausted),'by_depth',",
      "      ','.join(map(str,exhausted)))",
      "print('trace_sha256',trace.hexdigest())"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://www.cs.rit.edu/~spr/PUBL/dim09talk.pdf",
    "locator": "Inline CPython source below, executed on 2026-07-24"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R141",
      "title": "The independence number is 11",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "R142",
      "title": "This is a known Ramsey graph, not an open instance",
      "object_type": "claim",
      "relation": "tests",
      "direction": "outgoing"
    },
    {
      "slug": "R143",
      "title": "The candidate defines a simple undirected 42-regular graph",
      "object_type": "claim",
      "relation": "uses",
      "direction": "outgoing"
    },
    {
      "slug": "cubic-residue-graph-127-independence",
      "title": "cubic residue graph 127 independence",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}