Prolog SAT Solver

Я пытаюсь построить простой Пролог SAT решатель. Моя идея состоит в том, что пользователь должен ввести логическую формулу для решения в CNF (Conjuctive Normal Form) с использованием списков Пролога, например (A или B) и (B или C) должны быть представлены как sat ([[A, B] , [B, C]]) и Prolog переходит к поиску значений для A, B, C.

Мой следующий код не работает, и я не понимаю, почему. В этой строке трассировки Call: (7) sat ([[true, true]])? Я ожидал start_solve_clause ([_ G609, _G612]]) .

Заявление об отказе от ответственности: Извините за дрянной код, который я даже не знал о Prolog или проблеме SAT несколько дней назад.

PS: Совет по решению SAT приветствуется.

Trace

sat([[X, Y, Z], [X, Y]]).
Call: (6) sat([[_G609, _G612, _G615], [_G609, _G612]]) ? creep
Call: (7) start_solve_clause([_G609, _G612, _G615]) ? creep
Call: (8) solve_clause([_G615], _G726) ? creep
Call: (9) or(_G725, _G615, true) ? creep
Exit: (9) or(true, true, true) ? creep
Exit: (8) solve_clause([true], true) ? creep
Call: (8) or(_G609, _G612, true) ? creep
Exit: (8) or(true, true, true) ? creep
Exit: (7) start_solve_clause([true, true, true]) ? creep
Call: (7) sat([[true, true]]) ?  

Источник пролога

% Knowledge base
or(true, true, true).
or(false, false, false).
or(true, false, true).
or(false, true, true).

or(not(true), true, true).
or(not(false), false, true).
or(not(true), false, false).
or(not(false), true, true).

or(true, not(true), true).
or(false, not(false), true).
or(true, not(false), true).
or(false, not(true), false).

% SAT solver
sat([]).
sat([Clause | Tail]) :- start_solve_clause(Clause), sat(Tail).

% Clause solver
start_solve_clause([Var1, Var2 | Tail]) :- solve_clause(Tail, Result), or(Var1, Var2, Result).

solve_clause([X | []], Result) :- or(Result, X, true).
solve_clause([X | Tail], Result) :- solve_clause(Tail, Result2), or(Result, X, Result2).