Thank you very much Jan for these helpful and very interesting answers.
Two points before trying again to improve the output details of the Quine program.
First, I explain why such a program would be educational: many students are now alone in front of their computers, if they can use a program that shows us in detail how to get a Quine proof or a Quine counter-model for any propositional formula, it might be useful to them. This brings me to the second point.
It is interesting to note that Quine’s algorithm and Beth’s algorithm (the tree method) have opposite directions: the former goes from the inside out, the latter the reverse, via the negation of the formula submitted to test. Maybe the solution would be to write a program that makes exactly what is to do with Quine’s algorithm: pick an atomic formula (if possible the most common in the formula), replace it by T, and apply the reduction rules from subformulas to subformulas until to be at the level of the main connective, and again make the same thing with replacing the same starting atom by ⊥ . I note that there is no use of predicate subformula in Isabelle Newbie program, and the solution is adding rules for subformulas? I do not know, I am too weak in Prolog. Again, my warmest regards.