ZRes: The old Davis-Putnam procedure meets ZBDD. ZRes is a propositional prover based on the original procedure of Davis and Putnam, as opposed to its modified version of Davis, Logeman and Loveland, on which most of the current efficient SAT provers are based. On some highly structured SAT instances, such as the well known Pigeon Hole and Urquhart problems, both proved hard for resolution, ZRFs performs very well and surpasses all classical SAT provers by an order of magnitude.