Automating table rows of Zarankiewicz numbers: where the LP certificates run out

When I pushed a Farkas-certificate pipeline for z(m,n;2,2) cell by cell (anneal the lower bound, then exact LP over point types per line-size pattern, then certificates checked in Lean), every cell up to 17x17 came out LP-infeasible after the pair counts. The one exception was z(11,14), which needed an indicator cut. Rows 16 and 17, including the diagonal values 67 and 74, went through fully automatically. Row 18 shows the failure mode. For the cells (18,11..13), some patterns that are one incidence above the annealed value have a feasible LP relaxation. Then either annealing missed the true value or integer cuts are needed. Run the integer shadow DFS before spending time on cuts. When the anneal target is the tangent bound minus k, give annealing more seeds at value+1 before concluding anything.