Legyen

tetszőleges klózhalmaz. A teljes szintek módszere a következőképpen állítja elő a levezetéshez a rezolvenseket:

Ezzel a módszerrel sok egyforma klóz jelenik meg a rezolvensek között, sőt olyan rezolvens klózok is a klózhalmazba kerülhetnek, amelyekre a továbblépésben biztosan nincs szükség. E problémák megoldására született meg a törlési stratégia.

Minden

esetén az

klózhalmazból el kell hagyni a fölösleges klózokat: a tautológiákat és azokat, amelyeket más klózok ,,tartalmaznak''.

Definíció Jelölje

és

rendre a

és a

klózok literáljainak halmazát. Egy

klóz befoglalja a

klózt, ha van olyan

termhelyettesítés, hogy

.

a befoglalt klóz.

Példa Legyen

és

. Ekkor

és

. Ha

, akkor

.

, tehát

befoglalja

-t.

A tautológiákat és a befoglalt klózokat meg kell találni. A tautológiákat a faktorizáció segítségével fedhetjük fel. A befoglalási teszt azonban nem olyan egyszerű.

7.4.2.1. Befoglalási algoritmus

Legyenek

és

klózok. Legyen

, ahol

a

-ben előforduló változók és

sem

-ben, sem

-ben elő nem forduló különböző konstansszimbólumok. Tegyük fel, hogy

.

1. 

   ,

   

   ,

   

   ,

2. Ha

   

   , akkor vége:

   

   befoglalja

   

   -t. Egyébként

   Equation 7.. 

   

   
   

3. Ha

   

   üres, akkor vége:

   

   nem foglalja be

   

   -t. Egyébként

   

   , és folytatás a 2. lépéssel.

Példa Befoglalja-e

a

-t?

Equation 7.. 

változói az

és a

. Legyen

. Ekkor

Equation 7.. 

1. 

   ,

   

   .

2. Mivel

   

   , azt kapjuk, hogy

   Equation 7.. 

   

   
   

3. Mivel

   

   és az

   

   , az eljárást folytatva kapjuk, hogy

   

   .

4. Mivel

   

   , az eljárásnak vége:

   

   befoglalja

   

   -t.