Implementing Quine's algorithm

Help! Algorithm
151

Thanks ! Now boole prover in my file is :

boole :-
    get_wff(_A,_L).

get_wff(A,L) :-
    read_term(A, [variable_names(N)]),
    time(judge(A,L)),
    (
	last(L,1) -> write('to prove that the formula is a tautology:'),nl,
		     write(N),nl,
		     write(L)
    ;
    last(L,0) -> write('to prove that the formula is not a tautology:'),nl,
		 write(N),nl,
		 write(L)
    ).

It provides clear output.