In this paper, we describe a new algorithm for the problem of checking whether a real-time system has a Partially Clairvoyant schedule (PCS). Existing algorithms for the PCS problem are predicated on sequential quantifier elimination, i.e., the innermost quantifier is eliminated first, followed by the next one and so on. Our technique is radically different in that the quantifiers in the schedulability specification are eliminated in
. We demonstrate the usefulness of this technique by achieving significant performance improvement over a wide range of inputs. Additionally, the analysis developed for the new procedure may find applications in domains such as finite model theory and classical logic.