  We introduce a method to prove that a proof search method is not an instance
of another. As an example of application, we show that Polarized resolution
modulo, a method that mixes clause selection restrictions and literal selection
restrictions, is not an instance of Ordered resolution with selection.
