Пример 1. Нека Γ се състои от четирите дизюнкта {A,B}, {¬A,B}, {A,¬B} и {¬A,¬B}, където A и B са две различни затворени атомарни формули. Тогава има точно 11 затворени дизюнкта, изводими от Γ, а именно четирите дизюнкта, съставящи Γ, и още дизюнктите {B}, {A}, {B,¬B}, {¬A,A}, {¬A}, {¬B}, ∅ (разбира се изводимостта на празния дизюнкт позволява да заключим, че множеството Γ не е изпълнимо).

    Ще казваме, че един затворен дизюнкт D следва от дадено множество Γ от затворени дизюнкти, ако D е верен във всеки модел за Γ, т.е. ако не съществува модел за Γ, в който дизюнктът D да не е верен. Ясно е, че едно множество от затворени дизюнкти няма модел точно тогава, когато от това множество следва празният дизюнкт.

    Знаем, че непосредствената резолвента на кои да е два затворени дизюнкта, верни в дадена структура, също е вярна в тази структура. Поради това всеки затворен дизюнкт, изводим от дадено множество от затворени дизюнкти, следва от това множество. Обратното не е вярно. Например от множество Γ, състоящо се само от един дизюнкт, не е изводим никой друг дизюнкт (дори в особения случай, когато въпросният дизюнкт има непосредствена резолвента със самия себе си), обаче, ако изключим някои съвсем специални случаи, съществуват и други дизюнкти, които следват от Γ.

    За един затворен дизюнкт D ще казваме, че той е почти изводим от дадено множество Γ от затворени дизюнкти, ако D съдържа като подмножество някой дизюнкт, изводим от Γ, или сред елементите на D има два взаимно противоположни литерала. Очевидно всеки такъв дизюнкт следва от Γ. Оказва се обаче, че е вярно и обратното. В лема 3 по-долу ще докажем въпросното обратно твърдение при предположение, че множеството Γ е крайно, но с помощта на теоремата за компактност бихме могли лесно да се освободим от това предположение.

    Лема 1. Ако един затворен дизюнкт D е почти изводим от дадено множество Γ от затворени дизюнкти, то всеки затворен дизюнкт, който съдържа D, също е почти изводим от Γ.

    Доказателство. Твърдението следва директно от дефиницията за почти изводимост.  _□

    Лема 2. Нека Γ е множество от затворени дизюнкти, D₁ и D₂ са затворени дизюнкти, почти изводими от Γ, и D е непосредствена резолвента на D₁ и D₂. Тогава дизюнктът D също е почти изводим от Γ.

    Доказателство. Всеки един от двата дизюнкта D₁ и D₂ съдържа като подмножество някой дизюнкт, изводим от Γ, или съдържа сред елементите си два взаимно противоположни литерала. Освен това D е обединение на D₁\{L₁} и D₂\{L₂}), където L₁ и L₂ са противоположни литерали, принадлежащи съответно на D₁ и на D₂. Да разгледаме най-напред случая, когато съществуват изводими от Γ затворени дизюнкти D₁ и D₂, съдържащи се съответно в D₁ и в D₂. Ако L₁ принадлежи на D₁ и L₂ принадлежи на D₂, то обединението на D₁\{L₁} и D₂\{L₂} е дизюнкт, който е изводим от Γ и се съдържа в D. Ако L₁ не принадлежи на D₁, то изводимият от Γ дизюнкт D₁ се съдържа в D₁\{L₁}, а следователно и в D. Аналогично се вижда, че ако L₂ не принадлежи на D₂, то D₂ се съдържа в D. И така, във всички подслучаи на разглеждания дотук случай се оказва, че D съдържа като подмножество някой дизюнкт, изводим от Γ, и следователно D е почти изводим от Γ. Да предположим сега, че в D₁ има два взаимно противоположни литерала. Ако те и двата са различни от L₁, то те принадлежат на D₁\{L₁}, а значи и на D, тъй че сред елементите на D има два взаимно противоположни литерала и значи D е почти изводим от Γ. Ако пък единият от въпросните два взаимно противоположни литерала е L₁, то другият е L₂, поради което L₂ принадлежи на D₁\{L₁} и значи всички елементи на почти изводимия от Γ дизюнкт D₂ принадлежат на D, тъй че D е почти изводим от Γ съгласно лема 1. Аналогично се разглежда и случаят, когато в D₂ има два взаимно противоположни литерала.  _□

    Лема 3. Нека Γ е крайно множество от затворени дизюнкти. Тогава всеки затворен дизюнкт, който следва от Γ, е почти изводим от Γ.

    Доказателство. Ще си послужим с индукция относно броя на дизюнктите в Γ. Ако този брой е 0, то затворените дизюнкти, които следват от Γ, са верни във всяка структура. Лесно се вижда обаче, че когато един затворен дизюнкт е верен във всяка структура, сред елементите на този дизюнкт има непременно два взаимно противоположни литерала и значи дизюнктът е почти изводим от Γ. И наистина, нека D е затворен дизюнкт, който е верен във всяка структура. Тогава той ще бъде верен и в онази ербранова структура, в която верни сред затворените атомарни формули са точно онези с отрицание, принадлежащо на Γ. Значи някой елемент на Γ ще бъде верен в нея, а лесно е да се съобрази, че този елемент ще бъде атомарна формула, на която и отрицанието принадлежи на Γ. Да предположим сега, че заключението на лемата е вярно при даден брой n на елементите на Γ, и да разгледаме произволно множество Γ от n+1 затворени дизюнкти. Да означим с D′ някой от тези дизюнкти, а с Γ′  -  множеството на останалите n дизюнкти от Γ. Нека D е произволен затворен дизюнкт, който следва от Γ. За произволен литерал L да се условим да означаваме неговия противоположен с −L. Лесно се съобразява, че за всеки литерал L, принадлежащ на D′, дизюнктът {−L}∪D следва от множеството Γ′, поради което е почти изводим от Γ′, а значи и от Γ. Оттук се вижда, че ако за някой литерал от D′ неговият противоположен принадлежи на D, то дизюнктът D е почти изводим от Γ (даже и от Γ′). Оттук нататък ще предполагаме, че D не съдържа противоположния литерал на никой литерал от D′. Ако D съдържа  D′, то разбира се D е почти изводим от Γ (защото D′ е изводим от Γ). Ще се занимаем сега със случая, когато D не съдържа  D′. Нека разликата  D′\D има k елемента L₁, …, L_k. Да разгледаме (k+1)-членната редица от дизюнкти 

    Следствие. Ако не съществува модел за дадено множество от затворени дизюнкти, то празният дизюнкт е изводим от това множество.

    Доказателство. Нека е дадено едно множество от затворени дизюнкти, което няма модел. По теоремата за компактност някое крайно подмножество Γ на това множество също няма модел. Според току-що доказаната лема празният дизюнкт е почти изводим от Γ, но това е възможно само в случай че той е изводим от Γ, а значи и от първоначално даденото множество от дизюнкти.  _□

    Ако Γ е множество от какви да е (не непременно затворени) дизюнкти един (не непременно затворен) дизюнкт ще наричаме изводим от Γ, ако той може да бъде получен от дизюнкти, принадлежащи на Γ, чрез някакъв (евентуално нулев) брой образувания на резолвента (не непременно непосредствена). Понеже всяка резолвента на затворени дизюнкти е пак затворен дизюнкт и е тяхна непосредствена резолвента, ясно е, че ако всички дизюнкти от Γ са затворени, то един дизюнкт е изводим от Γ в смисъл на тази дефиниция точно тогава, когато е затворен и е изводим от Γ в смисъл на дефиницията, дадена в началото.

    Теорема за пълнота на резолюцията. Ако не съществува модел за дадено множество от дизюнкти, то празният дизюнкт е изводим от това множество.

    Доказателство. Нека Γ е множество от дизюнкти, за което не съществува модел. На първо време ще предположим, че в сигнатурата, с която работим, има поне една константа. Да означим с Γ^o множеството на всички затворени частни случаи на дизюнктите от Γ. Множеството Γ^o е неизпълнимо и значи по доказаното по-горе следствие празният дизюнкт е изводим от Γ^o. Оттук получаваме, че той е изводим и от множеството Γ. За целта можем да използваме лесно доказуемото твърдение, че всеки дизюнкт, изводим от Γ^o, е частен случай на дизюнкт, изводим от Γ (използваме още, че празният дизюнкт не е частен случай на никой друг дизюнкт). Ако пък се случи сигнатурата да е без константи, можем да я разширим чрез добавяне на някоя константа α. Множеството Γ няма да притежава модел и при работа с така разширената сигнатура, следователно при работа с нея празният дизюнкт ще бъде изводим от множеството Γ. За да заключим оттук, че празният дизюнкт е изводим от Γ и при работа с първоначалната сигнатура, ние, грубо казано, ще покажем как константата α може да бъде елиминирана чрез замяната й с подходяща променлива. Нека ξ е дадена променлива. Доказва се, че субституцията [ξ/α] осъществява обратимо изображение на множеството на всички атомарни формули в първоначалната сигнатура върху множеството на онези атомарни формули в разширената, на които ξ не е сред променливите (за целта най-напред се доказва аналогично твърдение за термове). Ясно е тогава, че същата субституция осъществява обратимо изображение на множеството на всички дизюнкти в първоначалната сигнатура върху множеството на онези дизюнкти в разширената, на които ξ не е сред променливите. Ако означим това изображение с T_ξ, доказва се още следното: за всеки дизюнкт D, изводим от Γ при работа с разширената сигнатура, може да се намери такова крайно множество Ξ₀ от променливи, съдържащо променливите на D, че за всяка променлива ξ, непринадлежаща на Ξ₀, първообразът на D относно T_ξ е изводим от Γ при работа с първоначалната сигнатура (Ξ₀ е, тъй да се каже, множеството на променливите, използвани при извеждането на D). Накрая това се прилага в случая, когато D е празният дизюнкт.  _□

    Забележка. Теоремата за пълнота, която доказахме, допуска значително уточняване в следната насока: вместо какви да е резолвенти достатъчно е да образуваме специални, при които използваните частни случаи на дизюнктите се търсят чрез подходящо прилагане на метода на унификацията.