Finiteness conjecture for non-singular unsatisfiable hitting clause-sets

A clause-set is hitting if every two distinct clauses $C,C'$ clash in at least one variable, that is, $\lvert C\cap\overline{C'}\rvert\geq 1$. A clause-set is non-singular in the sense used in the paper, and its deficiency is denoted by $k\in\mathbb{N}$. Two clause-sets have the same isomorphism type when they are isomorphic under the relevant variable and clause structure.

Finiteness conjecture. For every deficiency $k\in\mathbb{N}$, there are only finitely many isomorphism types of non-singular unsatisfiable hitting clause-sets.

This is presented as the main conjecture motivating the classification of minimally unsatisfiable clause-sets by deficiency, especially the classification of unsatisfiable hitting clause-sets. The supplied text gives no resolution, so the conjecture remains open.