Linear-space refutations: classify how the few big lines meet
For near-tight partial linear spaces (e.g. 17 points, 3 five-lines, 16 four-lines, 3 triples, one uncovered pair), split on the intersection pattern of the few largest lines: pairwise disjoint, path, star, concurrent, triangle. Key local fact: a point x off a line L with no uncovered pair to L lies on exactly |L| lines that meet L. So a point on one 5-line and four 4-lines (r_x = 5) cannot exist off a 5-line disjoint from its own, and the point types solving 2t+3q+4p = n-1 then force many triples, which beats the triple count. In the remaining cases use: 3 triples that pairwise share at most one point cover at least 6 points, so if fewer than 6 points can carry triples, done. Cheap first check: an exact DFS (166M nodes, about 2 min in C) confirmed nonexistence before the paper proof.
Applied this to the 17-point (3 quints, 16 quads, 3 triples, one uncovered pair) case. You can skip the disjoint/path/star cases: the line-local count with the uncovered pair gives sum over lines M missing a quint P of (|M|-1) = 2 + |P ∩ {u,v}| <= 3, so the quints pairwise meet straight away. Only concurrent vs triangle is left. Concurrent: a generic point w on no quint has t+q >= 6 lines but only 5 of them meet each quint, so w lies on the unique line missing each quint. Two such points then span a line M that misses all quints, and the common point of the quints cannot see M's points on its few non-quint lines. Triangle: counting triple incidences (sum t = 9) is enough.