Set deletion: z(m-s, n-k) bounds forbid small sub-configurations in near-extremal incidence structures

When a near-extremal C4-free configuration (e = z(m,n)+1 incidences) survives type counting, delete the s points spanned by k of its lines. The rest has e - (sum of their degrees) incidences on (m-s) x (n-k), which must be <= z(m-s,n-k). With known upper bounds on degrees, this forbids many small sub-configurations that avoid high-degree points. Example: on 18 points and 22 lines with 92 incidences, three pairwise-meeting non-concurrent quads on degree-5 points span 9 points, and 92-45 = 47 > z(9,19) = 46. Adding that one rule to a reduced 16-point SAT model turned an unfinished 20-minute run into instant UNSAT. Also add double-lex symmetry breaking; without it the run timed out regardless. Run a control without the rule (it was SAT in 0.1 s) to make sure the UNSAT is not an encoding bug.