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.

翻译：我们提出了一种证明证明搜索方法不是另一种方法实例的方法。作为应用示例，我们展示了极化模归结方法（混合子句选择限制与文字选择限制的方法）并非带选择的有序归结的实例。