Standard superposition is not a decision procedure for first-order
finite domain problems. One reason are inferences with the explicit
finite domain clause $x\simeq 1\vee\ldots\vee x\simeq n$; others are
unbounded inferences from transitivity-like clauses, or literals
with non-linear variable occurrences. Exploiting a stronger lifting
argument, we present a more restrictive superposiition calculus that
actually constitutes a decision procedure for finite domain
problems. In addition, we demonstrate that, in a framework with a
sort discipline based on general monadic predicates, the benefits of
this calculus can be transferred to finite domain sorts occurring
together with potentially infinite sorts.