Создание SAT-решателя на основе Гребнера на языке Prolog

Я пытаюсь создать решатель SAT, который преобразует конъюнктивную нормальную форму (CNF) с реализацией логических баз Гробнера:

а) Отрицание конкретной переменной, например. -x будет преобразовано в 1+x.
b) Добавление той же переменной приведет к 0. Например. x + x = 0. (необходимо использовать XOR).
c) Умножение одной и той же переменной приведет к одной и той же переменной. например x*x = x.

На данный момент я все еще пытаюсь понять, как начать, так как ввод должен быть в текстовом файле, как у них на соревнованиях SAT, где он выглядит следующим образом:

p cnf 3 4 
1 3 -2 0
3 1 0
-1 2 0
2 3 1 0

Спасибо.

РЕДАКТИРОВАТЬ

parser :-
    open(File, read, Stream),
    read_literals(Stream,Literals),
    close(Stream),
    read_clauses(Literals,[],Clauses),
    write(Clauses).

read_literals(Stream,Literals) :-
    get_char(Stream,C),
    read_literals(C,Stream,Literals).

read_literals(end_of_file,_Stream,Literals) :-
    !,
    Literals = [].

read_literals(' ',Stream,Literals) :-
    !,
    read_literals(Stream,Literals).

read_line_then_literals('\n',Stream,Literals) :-
    !,
    read_literals(Stream,Literals).

read_line_then_literals(_C,Stream,Literals) :- 
    read_line_then_literals(Stream,Literals).

read_literal_then_literals(Stream,As,Literals) :-
    get_char(Stream,C),
    read_literal_then_literals(C,Stream,As,Literals). 

read_literal_then_literals(C,Stream,As,Literals) :-
    digit(C),
    !,
    name(C,[A]),
    read_literal_then_literals(Stream,[A|As],Literals).

read_literal_then_literals(C,Stream,As,Literals) :-
    reverse(As,RevAs),
    name(Literal,RevAs), 
    Literals = [Literal|Rest_Literals],
    read_literals(C,Stream,Rest_Literals).

digit('0').
digit('1').
digit('2').
digit('3').
digit('4').
digit('5').
digit('6').
digit('7').
digit('8').
digit('9').

read_clauses([],[],[]).

read_clauses([0|Literals],Clause,Clauses) :-
    !,
    reverse(Clause,RevClause),
    Clauses=[RevClause|RestClauses],
    read_clauses(Literals,[],RestClauses).

read_clauses([Literal|Literals],Clause,Clauses) :- 
    read_clauses(Literals,[Literal|Clause],Clauses).