Abstract. This paper describes a proof search procedure for propositional nonclausal resolution based on a new weighting strategy that utilizes search methods for propositional satisfiability (SAT solvers) and stochastic local search techniques for constructing countermodels. Key words: automated reasoning, non-clausal resolution, propositional satisfiability