The formula is read as occurrence functions, under which satisfiability is $Sat2$, edges are $Edge$ and contradictory variables are $Contra$; the criterion is then $Math.sat2_iff_no_contra$, with the direction from a satisfying assignment holding for every variable by $Math.not_contra_of_sat$. A formula with an empty clause is unsatisfiable outright.