It is a hot research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL (brute force lifting) algorithm is the most effective one among all the existing approaches, but its time overhead is very large due to one call to SAT (boolean satisfiability problem) solver per candidate variable to be eliminated. So a faster algorithm based on refutation analysis and incremental SAT is proposed. The counterexample minimization problem is first translated into a set of SAT instances for each free variable v, to determine if v can prevent the counterexample. Then refutation analysis on those UNSAT (unsatisfiable) instances is performed, to extract the set of variables that lead to refutation. All variables that don’t belong to this set can be eliminated directly as irrelevant variables. At the same time, the incremental SAT approach is employed to share conflict clauses between similar instances, such that the overlapped state space can be prevented from being searched repeatedly. Theoretical analysis and experimental result show that this approach run much faster than BFL algorithm, and with minor lost in reduction rate.