I must tell you frankly Jan that even if I am really interested by your question, I am afraid to miss time. Feel free to use the file quine-boole.pl that I just published. I plan to pubish another question here, on another webpage about Wang’s algorithm in Prolog. This work has been done and published here by Ben Hudson, and the prover seems to me correct, but it can certainly be still improved by good Prolog programmers:
See now: