  Weighted First-Order Model Counting (WFOMC) computes the weighted sum of the
models of a first-order logic theory on a given finite domain. First-Order
Logic theories that admit polynomial-time WFOMC w.r.t domain cardinality are
called domain liftable. We introduce the concept of lifted interpretations as a
tool for formulating closed-forms for WFOMC. Using lifted interpretations, we
reconstruct the closed-form formula for polynomial-time FOMC in the universally
quantified fragment of FO2, earlier proposed by Beame et al. We then expand
this closed-form to incorporate cardinality constraints, existential
quantifiers, and counting quantifiers (a.k.a C2) without losing
domain-liftability. Finally, we show that the obtained closed-form motivates a
natural definition of a family of weight functions strictly larger than
symmetric weight functions.
