  We establish a new bridge between propositional logic and elementary number
theory. The main objects are "minimally unsatisfiable clause-sets", short
"MUs", unsatisfiable conjunctive normal forms rendered satisfiable by
elimination of any clause. In other words, irredundant coverings of the boolean
hypercube by subcubes. The main parameter for MUs is the "deficiency" k, the
difference between the number of clauses and the number of variables (the
difference between the number of elements in the covering and the dimension of
the hypercube), and the fundamental fact is that k >= 1 holds.
  A "full clause" in an MU contains all variables (corresponding to a singleton
in the covering). We show the lower bound S_2(k) <= FCM(k), where FCM(k) is the
maximal number of full clauses in MUs of deficiency k, while S_2(k) is the
smallest n such that 2^k divides n!.
  The proof rests on two methods: On the logic-combinatorial side, applying
subsumption resolution and its inverse, a fundamental method since Boole in
1854 introduced the "expansion method". On the arithmetical side, analysing
certain recursions, combining an application-specific recursion with a
recursion from the field of meta-Fibonacci sequences (indeed S_2 equals twice
the Conolly sequence).
  A further tool is the consideration of unsatisfiable "hitting clause-sets"
(UHITs), special cases of MUs, which correspond to the partitions of the
boolean hypercube by subcubes; they are also known as orthogonal or disjoint
DNF tautologies. We actually show the sharper lower bound S_2(k) <= FCH(k),
where FCH(k) is the maximal number of full clauses in UHITs of deficiency k. We
conjecture that for all k holds S_2(k) = FCH(k), which would establish a
surprising connection between the extremal combinatorics of (un)satisfiability
and elementary number theory.
  We apply the lower bound to analyse the structure of MUs and UHITs.
