For example, if F is the conjunction of several boolean predicates, F = F[1] F[2] F[p], and each F[i] depends only on a small subset of the variables x[1], ..., x[n], then the reject procedure could simply check the terms F[i] that depend only on variables x[1], ..., x[k], and return true if any of those terms returns false. In fact, reject needs only check those terms that do depend on x[k], since the terms that depend only on x[1], ..., x[k-1] will have been tested further up in the search tree.