The extension rule based theorem proving methods are inverse methods to resolution in a sense that they check the satisfiability by determining whether all the maximum terms of the clause set can be deduced. IER (improved extension rule) algorithm is incomplete as it cannot determine the satisfiability of the clause set when the subspace of the clause set is unsatisfiable. In this condition, calling ER (extension rule) algorithms is still needed. After a thorough investigation on the maximum terms space of the clause set, this paper develops a decomposition method for decomposing the maximum terms space of the clause set. The study on extension rule also results in the PSER (partial semi-extension rule) algorithm for determining the satisfiability of a partial space of the maximum terms. When the IER determines the subspace is unsatisfiable, PSER can be used to determine the satisfiability of the complementary space, thereby, the satisfiability of the clause set can be obtained. Based on the above progress, this paper further introduces DPSER (degree partial semi-extension rule) theorem proving method. Results show that the proposed DPSER and IPSER outperform both the directional resolution algorithm DR and the extension rule based algorithms IER and NER.