Horn3SAT is $P$-complete problem under logspace reductions. Since Horn3SAT is in $P$ its complement must have short witnesses. I am looking for natural short proof that a Horn3SAT formula is not satisfiable. Examples for similar problems in $P$ are 2-coloring problem and planarity problem. A graph is not 2-colorable if and only if it contains an odd cycle. A graph is not planar if and only if it contains a subgraph that is a subdivision of $K_5$ or $K_{3,3}$.
Is there a good characterization of Horn3SAT formulas that are not satisfiable? What does constitute a natural short witness for unsatisfiable Horn3SAT formulas?
I am not interested in algorithmic proof such as running an algorithm for deciding Horn3SAT problem. I am only interested in good characterizations similar in spirit to the above two examples.
EDIT: As illustrated by the two examples above, I am only interested in characterizations of the complement set of Horn3SAT in terms of some forbidden structure.