For sequetial circuits, it is well known that the sets of reachable states may be much smaller than the entire state space, and computing the supersets of reachable states is practically useful due to the less computational complexity than the exact set of the reachable states. Inductive invariant is the one of the method to compute the superset. We first show a way to prove the property of the sequential circuits with inductive invariants. For inductive invariants, it is important to select the subset of flipflops in order to find a small subset of reachable states or prove the property. Unknown value X based analsys is used to find the subset of flipflops. In some HWMCC2017 benchmark circuits, the method can find the subset of flipflops to prove the correctness of the property. The calculation of inductive invariants is formulated with Quantified Boolean Formula. The QBF problem can be solved by repeatedly applying SAT solvers. We also show a way to reduce the number of variables in QBF problems. In the method, we start with smaller inputs LUT and gradually increment the number of inputs in order to reduce variables. The method can significantly reduce the computation time when solving large QBF problem.