Impressive and very elegant code. Congratulations Jan !
That is very very nice. An explanation both of how your Prolog code works and how it translates what Boole showed would be also very useful for people who, like me, have not your skills, but you are certainly too much busy for that. Take it as a simple suggestion, not a request.
Please, can you give me (again?) the reference of your quotation (3.1 Boole’s Method)? !
I was lucky ! 
Bad news dear Jan, I just made a test with a big formula, and boole2 does not pass it:
?- time(judge(((( a0 =< f) * ((( b20 =< b0) =< a20) * ((( b0 =< a1) =< a0) * (
(( b1 =< a2) =< a1) * ((( b2 =< a3) =< a2) * ((( b3 =< a4) =< a3) *
((( b4 =< a5) =< a4) * ((( b5 =< a6) =< a5) * ((( b6 =< a7) =< a6)
* ((( b7 =< a8) =< a7) * ((( b8 =< a9) =< a8) * ((( b9 =< a10) =<
a9) * ((( b10 =< a11) =< a10) * ( (( b11 =< a12) =< a11) * ((( b12
=< a13) =< a12) * ((( b13 =< a14) =< a13) * ((( b14 =< a15) =< a14)
* ((( b15 =< a16) =< a15) * ((( b16 =< a17) =< a16) * ((( b17 =<
a18) =< a17) * ((( b18 =< a19) =< a18) * ((b19 =< a20) =< a19))))
)))))))))))))))))) =< f) * (((( b19 =< a20) =< a19)
* ((( b18 =< a19) =< a18) * ((( b17 =< a18) =< a17) * ((( b16 =<
a17) =< a16) * ((( b15 =< a16) =< a15) * ((( b14 =< a15) =< a14) * (
(( b13 =< a14) =< a13) * ((( b12 =< a13) =< a12) * ((( b11 =< a12)
=< a11) * ((( b10 =< a11) =< a10) * ((( b9 =< a10) =< a9) * ((( b8
=< a9) =< a8) * ((( b7 =< a8) =< a7) * ((( b6 =< a7) =< a6) * (((
b5 =< a6) =< a5) * ((( b4 =< a5) =< a4) * ((( b3 =< a4) =< a3) * ((
( b2 =< a3) =< a2) * ((( b1 =< a2) =< a1) * ((( b0 =< a1) =< a0) * (
(( b20 =< b0) =< a20) * ( a0 =< f)))))))))))))))))))))) =< f),L)).
| | | | | | | | | | | | | | | | % 169,017,800 inferences, 19.373 CPU in 19.374 seconds (100% CPU, 8724274 Lips)
ERROR: Stack limit (1.0Gb) exceeded
ERROR: Stack sizes: local: 4Kb, global: 0.7Gb, trail: 0.2Gb
ERROR: Stack depth: 93, last-call: 62%, Choice points: 6
ERROR: In:
ERROR: [93] user:eval(<compound (*)/2>, _1506)
ERROR: [92] user:eval(<compound (*)/2>, _1538)
ERROR: [91] user:eval(<compound (*)/2>, _1570)
ERROR: [90] user:eval(<compound (*)/2>, _1602)
ERROR: [89] user:eval(<compound (*)/2>, _1634)
ERROR:
ERROR: Use the --stack_limit=size[KMG] command line option or
ERROR: ?- set_prolog_flag(stack_limit, 2_147_483_648). to double the limit.
^ Exception: (12) setup_call_catcher_cleanup(system:true, prolog_statistics:catch(user:judge(((a0=<f)*((... =< ...)*(... * ...))=<f)*(((... =< ...)=<a19)*((... =< ...)*(... * ...))=<f), _10), _850, (report(t(1599064504.854738, 18.787530322, 145645749), 10), throw(_850))), _1816, prolog_statistics:(_872=true)) ?
I guessed that you won’t be surprised !
I am not sure that f is falsum. But I am sure that boole.pl passed the test ! :
?- time(judge(
(((( A0 =< F) * ((( B20 =< B0) =< A20) * ((( B0 =< A1) =< A0) * (
(( B1 =< A2) =< A1) * ((( B2 =< A3) =< A2) * ((( B3 =< A4) =< A3) *
((( B4 =< A5) =< A4) * ((( B5 =< A6) =< A5) * ((( B6 =< A7) =< A6)
* ((( B7 =< A8) =< A7) * ((( B8 =< A9) =< A8) * ((( B9 =< A10) =<
A9) * ((( B10 =< A11) =< A10) * ( (( B11 =< A12) =< A11) * ((( B12
=< A13) =< A12) * ((( B13 =< A14) =< A13) * ((( B14 =< A15) =< A14)
* ((( B15 =< A16) =< A15) * ((( B16 =< A17) =< A16) * ((( B17 =<
A18) =< A17) * ((( B18 =< A19) =< A18) * ((B19 =< A20) =< A19))))
)))))))))))))))))) =< F) * (((( B19 =< A20) =< A19)
* ((( B18 =< A19) =< A18) * ((( B17 =< A18) =< A17) * ((( B16 =<
A17) =< A16) * ((( B15 =< A16) =< A15) * ((( B14 =< A15) =< A14) * (
(( B13 =< A14) =< A13) * ((( B12 =< A13) =< A12) * ((( B11 =< A12)
=< A11) * ((( B10 =< A11) =< A10) * ((( B9 =< A10) =< A9) * ((( B8
=< A9) =< A8) * ((( B7 =< A8) =< A7) * ((( B6 =< A7) =< A6) * (((
B5 =< A6) =< A5) * ((( B4 =< A5) =< A4) * ((( B3 =< A4) =< A3) * ((
( B2 =< A3) =< A2) * ((( B1 =< A2) =< A1) * ((( B0 =< A1) =< A0) * (
(( B20 =< B0) =< A20) * ( A0 =< F)))))))))))))))))))))) =< F)),L)).
| | | | | | | | | | | | | | | | | % 41,646 inferences, 0.010 CPU in 0.010 seconds (100% CPU, 4210173 Lips)
L = [((A0=<F)*(((B20=<B0)=<A20)*(((B0=<A1)=<A0)*(((B1=<A2)=<A1)*(((... =< ...)=<A2)*((... =< ...)*(... * ...))))))=<F)*(((B19=<A20)=<A19)*(((B18=<A19)=<A18)*(((B17=<A18)=<A17)*(((B16=<A17)=<A16)*(((... =< ...)=<A15)*((... =< ...)*(... * ...))))))=<F), (((B20=<B0)=<A20)*(~ (B0=<A1)*(((... =< ...)=<A1)*((... =< ...)*(... * ...))))=<F)*(((B19=<A20)=<A19)*(((B18=<A19)=<A18)*(((... =< ...)=<A17)*((... =< ...)*(... * ...))))=<F)*((F*(((B20=<B0)=<A20)*(((... =< ...)=<A1)*((... =< ...)*(... * ...))))=<F)*(((B19=<A20)=<A19)*(((B18=<A19)=<A18)*(((... =< ...)=<A17)*((... =< ...)*(... * ...))))=<F)), (A20*(~ ... * (... * ...))=<F)*(((... =< ...)=<A19)*((... =< ...)*(... * ...))=<F)*((F*(A20*(... * ...))=<F)*(((... =< ...)=<A19)*((... =< ...)*(... * ...))=<F))*(((B0=<A20)*(~ ... * (... * ...))=<F)*(((... =< ...)=<A19)*((... =< ...)*(... * ...))=<F)*((F*((... =< ...)*(... * ...))=<F)*(((... =< ...)=<A19)*((... =< ...)*(... * ...))=<F))), (~ ... * (... * ...)=<F)*((... =< ...)*(... * ...)=<F)*((F*(... * ...)=<F)*((... =< ...)*(... * ...)=<F))*((... * ... =< F)*(... * ... =< F)*((... * ... =< F)*(... * ... =< F))*((... * ... =< F)*(... * ... =< F)*((... * ... =< F)*(... * ... =< F)))), (... * ... =< F)*(... * ... =< F)*((... =< ...)*(... =< ...)*((... =< ...)*(... =< ...)))*((... =< ...)*(... =< ...)*((... =< ...)*(... =< ...))*((... =< ...)*(... =< ...)*((... =< ...)*(... =< ...)))), ~ (... * ...)* ~ (... * ...)*(~ (... * ...)* ~ (... * ...)), ~ ... * ~ ... * (~ ... * ~ ...), ... * ... * (... * ...), ... * ...|...].
Prolog variables are best suited for this work !
And the fact that boole.pl passed the test is also a positive reply to this question, IMHO.
I am not at all a computer scientist, but I suppose that storage of variables and storage of atoms are not the same in Prolog and that the former is less expensive than the latter? I risk an explanation that I do not understand in details, of course.
41,645 inferences with boole.pl using variables and judge/2 and much more i.e. 169,017,800 inferences with boole2.pl (atoms).
I will give to my students this formula to test at hand, it is a good test, no? 
It comes from the following library : http://iltp.de/formulae.html that I mentioned in this discussion here: Implementing Quine's algorithm .
Another good news: boole.pl passed also the test with a very big disjunction that is not valid:
% 2,866,875 inferences, 0.813 CPU in 0.813 seconds (100% CPU, 3525251 Lips)
Immediately no, but there are many similar in this library. It has a name like Q431342 … 
By the way, note that an additional commentary is necessary with judge/2 , because valid or not, the formula test ends with …|…] and in this case we do not know if the formula is valid or not.
Quine’s Method of Logic is a wonderful book.
If I write in bool.pl
quine(A) :-
judge(A,L),
write(L).
I get an ugly output, by contrast with judge/2 :
?- quine(C).
[_4788,0]
true.
?- judge(C,L).
L = [C, 0].
What it the work around to use only quine(Formula) as input and not judge(Formula, L) that is a little less convenient, and nevertheless getting the same output that this latter?
That’s only a detail. Bonne soirée Jan !
It would be of course a good project also to implement Quine’s method for monadic predicate.
Do you give up the project of pretty printing proofs à la Quine from your boole.pl ? It would be nice to get the format that Quine gave, but I do not know if it is possible or not (and if it is not possible, it would be interesting to understand why). I note that I never saw a truth-table generator in Prolog that provides the truth-tables of subformulas and I wonder if Quine’s method meets the same difficulty or if it just an implementation problem. I bet on this last option.
I realize that I did not answer to your question. But the reply is at the beginning of this web-page:
Last point: it seems to me Jan, that the solution that you gave with taut/3 and falsify/1 is already rather good and very near from the format of Quine’s proof. I add that the prover is also very efficient.