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.
“My” program? It is your program, Jan. I would be very happy to be able to write such a program. Unfortunately, “ce n’est pas demain la veille”. 
I will have a look on sat/1 and labeling/1.
Here is the boole-quine.pl prover in the last corrected version that I can publish.
/*
This prover is the work of Jan Burse. I changed only the symbols for operators, that's it.
See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830
and also https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in?noredirect=1#comment112667699_63505466
the boole.pl original file is here: https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl
*/
:- use_module(library(statistics)).
:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).
eval(A, A) :- var(A), !.
eval(A => B, R) :- !, eval(A, X), eval(B, Y), simp(X => Y, R).
eval(A <=> B, R) :- !, eval(A, X), eval(B, Y), simp(X <=> Y, R).
eval(A v B, R) :- !, eval(A, X), eval(B, Y), simp(X v Y, R).
eval(A & B, R) :- !, eval(A, X), eval(B, Y), simp(X & Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
simp(A, A) :- var(A), !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, X) :- B == 0, !, simp(~A, X).
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A <=> B, X) :- A == 0, !, simp(~B, X).
simp(A <=> B, X) :- B == 0, !, simp(~A, X).
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A v B, B) :- A == 0, !.
simp(A v B, A) :- B == 0, !.
simp(A v _, 1) :- A == 1, !.
simp(_ v B, 1) :- B == 1, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
simp(A & B, B) :- A == 1, !.
simp(A & B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).
judge(A, [B|R]) :-
eval(A, B),
term_variables(B, L),
judge(B, L, R).
% Boole prover : boole/2
% First, write "boole" + Enter.
% Second, write your formula + Enter.
judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]),
judge(C & D, R).
boole :-
get_wff(_A,_L).
get_wff(A,L) :-
read_term(A, [variable_names(_N)]),
time(judge(A,L)),
last(L,R),
(
last(L,1) -> write('to prove that the formula is a tautology, i.e. that its truth value is always '),
write(R),write(' .'),nl,nl,nl,
boole
;
last(L,0) -> write('to prove that the formula is not a tautology, i.e. that its truth value can be '),
write(R),write(' .'),nl,nl,nl,
boole
).
/*
Examples:
?- true.
?- boole.
|: A => A.
% 22 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 758202 Lips)
to prove that the formula is a tautology, i.e. that its truth value is always 1 .
|: A => B.
% 30 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 623662 Lips)
to prove that the formula is not a tautology, i.e. that its truth value can be 0 .
|: halt.
% 3 inferences, 0.000 CPU in 0.000 seconds (90% CPU, 53834 Lips)
false.
?-
*/
/*
falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).
falsify(0,_) :- !.
falsify(A, [0|_]) :- falsify(A), !.
falsify(A, [1|_]) :- falsify(A).
*/
taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N).
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, taut(A, S, N), T = S.
% Second prover, more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.
quine:-
getFormula(_A,_T).
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
(time(taut(A, T, N)) -> /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.'),
nl,nl,nl,
quine
;
write('to prove that the formula is an antilogy.'),
nl,nl,nl,
quine
)
;
write('to prove that the formula is neither a tautology nor an antilogy.'),
nl,nl,nl,
quine
).
/*
Examples:
?- quine.
|: A => A.
A=>A
A=>A
------------------------------
0=>0
1
------------------------------
1=>1
1
------------------------------
% 45 inferences, 0.000 CPU in 0.000 seconds (98% CPU, 158510 Lips)
to prove that the formula is a tautology.
true.
?- quine.
|: A => B.
A=>B
A=>B
------------------------------
0=>B
1
------------------------------
1=>B
B
------------------------------
0
0
------------------------------
1
1
------------------------------
% 73 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 187048 Lips)
to prove that the formula is neither a tautology nor an antilogy.
true.
*/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:
https://swi-prolog.discourse.group/t/improving-wangs-algorithm-in-prolog/2872/2
Jan, I have a question about ‘plain.pl’. Can a syntactic change of definition of operator affect the performances of this prover?
Jan, I’m much impressed by plain.pl . Here are the stastics with a very big disjunction that is not valid and proved as being such by plain.pl :
% 447 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 3540510 Lips)
A11 = A21, A21 = A31, A31 = A41, A41 = A51, A51 = A12, A12 = A22, A22 = A32, A32 = A42, A42 = A52, A52 = A13, A13 = A23, A23 = A33, A33 = A43, A43 = A53, A53 = A14, A14 = A24, A24 = A34, A34 = A44, A44 = A54, A54 = A15, A15 = A25, A25 = A35, A35 = A45, A45 = A55, A55 = 0
Now the same formula submitted as input to boole-quine.pl , to the prover boole exactly:
% 2,866,876 inferences, 0.812 CPU in 0.813 seconds (100% CPU, 3529019 Lips)
to prove that the formula is not a tautology, i.e. that its truth value can be 0 .
and to the quine prover now:
% 6,277 inferences, 0.027 CPU in 0.047 seconds (59% CPU, 228329 Lips)
to prove that the formula is neither a tautology nor an antilogy.
But you said that in SAT there are no winner… 
But unfortunately, plain.pl does not succeed in giving an output for the big valid formula that your know:
time(falsify(((~ (( ~ 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) * ((~ + 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))
)).
Proved via boole:
?- boole.
|: (((( 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)).
|: |: |: |: |: |: |: |: |: |: |: |: |: |: |: |:
% 41,645 inferences, 0.032 CPU in 0.032 seconds (100% CPU, 1318876 Lips)
to prove that the formula is a tautology, i.e. that its truth value is always 1
and via quine:
% 34,421 inferences, 0.022 CPU in 0.555 seconds (4% CPU, 1564604 Lips) to prove that the formula is a tautology.
Finally Quine prover is a reasonable option, in my opinion.
Unfortunately, no. My first education was in Philosophy, and in France. I am interested in mathematical logic, but my students are often more afraid than interested by formal arguments.
Do not hesitate to write to Jen :
jeotten @ ifi.uio.no
All his programs are in Prolog and he will be certainly interested to have discussions with you.
Every work in Prolog that is related to theorems provers in first order logic (not necessarily classical) interests me. But I stress on the point that my endeavours are mainly to improve my skills, as far as I can.
I am almost quite certain that it is not. Dyckhoff masterly showed that the keypoint is rule L -> . Maybe you know well his famous paper where he defined sequent system LJT that is usually called now G4i. From Naoyuki classical sequent prover, I succeeded to implement G4i. It works pretty well in propositional logic, but meets difficulties in intuitionistic predicate calculus. Any improvements will be welcome. I email to you this paper and this fork.
I did it. The file I just sent to you is G4 in general: g4m, g4i, g4c for respectively, minimal, intuitionistic and classical logic.
Thanks for this interesting point on Prolog interpreter.
@j4n_bur53 . With your code:
taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N).
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, taut(A, T, N), throw(T)), T, true),
B = 1, taut(A, S, N), T = S.
% Second prover, more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.
quine:-
getFormula(_A,_T).
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
(time(taut(A, T, N)) -> /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.'),
nl,nl,nl,
quine
;
write('to prove that the formula is an antilogy.'),
nl,nl,nl,
quine
)
;
write('to prove that the formula is neither a tautology nor an antilogy.'),
nl,nl,nl,
quine
).
I wonder what I have to change in order to get the same result in a Quine prover working with atoms and not with Prolog variables. I tried different things with your atom provers based on judge/2, but all my tentatives failed.
Many thanks Jan for your help. I suspected that I was in a dead end, and I remember now that you told me that I needed subst/4. Sorry to be so slow.
I publish here the file variable-boole-quine-pl that provide a clear pretty-printing reflecting the work of the prover, here is the last version of this file:
/*
This prover is the work of Jan Burse. I changed only the symbols for operators, that's it.
See the web page : https://swi-prolog.discourse.group/t/implementing-quines-algorithm/2830
and also https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in?noredirect=1#comment112667699_63505466
the boole.pl original file is here: https://gist.github.com/jburse/4ab909be4406b0c960494c692fc7a37f#file-boole-pl
*/
:- use_module(library(statistics)).
:- op(700, xfy, <=>).
:- op(600, xfy, =>).
:- op(500, xfy, v).
:- op(400, xfy, &).
:- op(300, fy, ~).
eval(A, A) :- var(A), !.
eval(A => B, R) :- !, eval(A, X), eval(B, Y), simp(X => Y, R).
eval(A <=> B, R) :- !, eval(A, X), eval(B, Y), simp(X <=> Y, R).
eval(A v B, R) :- !, eval(A, X), eval(B, Y), simp(X v Y, R).
eval(A & B, R) :- !, eval(A, X), eval(B, Y), simp(X & Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).
simp(A, A) :- var(A), !.
simp(A => _, 1) :- A == 0, !.
simp(A => B, X) :- B == 0, !, simp(~A, X).
simp(A => B, B) :- A == 1, !.
simp(_ => B, 1) :- B == 1, !.
simp(A <=> B, X) :- A == 0, !, simp(~B, X).
simp(A <=> B, X) :- B == 0, !, simp(~A, X).
simp(A <=> B, B) :- A == 1, !.
simp(A <=> B, A) :- B == 1, !.
simp(A v B, B) :- A == 0, !.
simp(A v B, A) :- B == 0, !.
simp(A v _, 1) :- A == 1, !.
simp(_ v B, 1) :- B == 1, !.
simp(A & _, 0) :- A == 0, !.
simp(_ & B, 0) :- B == 0, !.
simp(A & B, B) :- A == 1, !.
simp(A & B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).
judge(A, [B|R]) :-
eval(A, B),
term_variables(B, L),
judge(B, L, R).
% Boole prover : boole/2
% First, write "boole" + Enter.
% Second, write your formula + Enter.
judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
copy_term(A-[B|L], C-[0|L]),
copy_term(A-[B|L], D-[1|L]),
judge(C & D, R).
boole :-
get_wff(_A,_L).
get_wff(A,L) :-
read_term(A, [variable_names(_N)]),
time(judge(A,L)),
last(L,R),
(
last(L,1) -> write('to prove that the formula is a tautology, i.e. that its truth value is always '),
write(R),write(' .'),nl,nl,nl,
boole
;
last(L,0) -> write('to prove that the formula is not a tautology, i.e. that its truth value can be '),
write(R),write(' .'),nl,nl,nl,
boole
).
/*
Examples:
?- true.
?- boole.
|: A => A.
% 22 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 758202 Lips)
to prove that the formula is a tautology, i.e. that its truth value is always 1 .
|: A => B.
% 30 inferences, 0.000 CPU in 0.000 seconds (93% CPU, 623662 Lips)
to prove that the formula is not a tautology, i.e. that its truth value can be 0 .
|: halt.
% 3 inferences, 0.000 CPU in 0.000 seconds (90% CPU, 53834 Lips)
false.
?-
*/
/*
falsify(A) :- eval(A, B), term_variables(B, L), falsify(B, L).
falsify(0,_) :- !.
falsify(A, [0|_]) :- falsify(A), !.
falsify(A, [1|_]) :- falsify(A).
*/
taut(A, T, N) :-
eval(A, B),
write_term(A, [variable_names(N)]),nl,
write_term(B, [variable_names(N)]),nl,
write('------------------------------'),nl,
term_variables(B, L), taut(B, L, T, N),nl.
taut(T, [], T, _) :- !.
taut(A, [B|_], T, N) :- catch((B = 0, write(N),nl, taut(A, T, N), throw(T)), T, true),
B = 1, write(N),nl, taut(A, S, N), T = S.
% Second prover, more practical and more verbose:
% First, write "quine" + Enter.
% Second, write only your formula + Enter.
quine:-
getFormula(_A,_T).
getFormula(A, T) :-
read_term(A, [variable_names(N)]),
(time(taut(A, T, N)) -> /* here is the missing outer if-then-else */
(T == 1 ->
write('to prove that the formula is a tautology.'),
nl,nl,nl,
quine
;
write('to prove that the formula is an antilogy.'),
nl,nl,nl,
quine
)
;
write('to prove that the formula is neither a tautology nor an antilogy.'),
nl,nl,nl,
quine
).
/*
Examples:
?- quine.
|: A => A.
A=>A
A=>A
------------------------------
0=>0
1
------------------------------
1=>1
1
------------------------------
% 45 inferences, 0.000 CPU in 0.000 seconds (98% CPU, 158510 Lips)
to prove that the formula is a tautology.
true.
?- quine.
|: A => B.
A=>B
A=>B
------------------------------
0=>B
1
------------------------------
1=>B
B
------------------------------
0
0
------------------------------
1
1
------------------------------
% 73 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 187048 Lips)
to prove that the formula is neither a tautology nor an antilogy.
true.
*/
Example of output with quine prover:
?- quine.
|: A => A.
A=>A
A=>A
------------------------------
[A=0]
0=>0
1
------------------------------
[A=1]
1=>1
1
------------------------------
% 53 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 509361 Lips)
to prove that the formula is a tautology.
|: ((A v B) => C) <=> ((A => C) & (B => C)).
A v B=>C<=>(A=>C)&(B=>C)
A v B=>C<=>(A=>C)&(B=>C)
------------------------------
[A=0,B=_4768,C=_4774]
0 v B=>C<=>(0=>C)&(B=>C)
B=>C<=>B=>C
------------------------------
[A=0,B=0,C=_4774]
0=>C<=>0=>C
1
------------------------------
[A=0,B=1,C=_4774]
1=>C<=>1=>C
C<=>C
------------------------------
[A=0,B=1,C=0]
0<=>0
1
------------------------------
[A=0,B=1,C=1]
1<=>1
1
------------------------------
[A=1,B=_4768,C=_4774]
1 v B=>C<=>(1=>C)&(B=>C)
C<=>C&(B=>C)
------------------------------
[A=1,B=_4768,C=0]
0<=>0&(B=>0)
1
------------------------------
[A=1,B=_4768,C=1]
1<=>1&(B=>1)
1
------------------------------
% 241 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 303785 Lips)
to prove that the formula is a tautology.
In my opinion, the reply should be yes, the four additional rules of G4 are all rules in minimal logic, and therefore must be derivable in any classical sequent system.
Dear Jan. You overestimate me. As you can see, I did not understand this homework.
To reply to your question on G4c, it is neither Dyckhoff’s nor Negri, I wanted only make the minimal adding to prove classical theorems inside a G4 system, i.e. with rule L -> -> only. Ax-c is classical by contrast with Ax of G4i in this prover: it accepts multi-conclusions.
Sorry for the delay of my reply Jan. These formulas are in the seqprover webpage. Naouki Tamura could certainly say more about them.
I add that I have indeed a github webpage, but I have not yet published the php program for G4i, program that is not written by me but by a good friend of mines.
Congrats Jan ! I am always working at the moment on my quine-wang.pl . The square-brackets problem is behind me, but there is still at least one user inconvenience that I would be glad to solve. I will be back soon.
Best,
Jo.
I do not know if there are provers for free logics. That’s an interesting question.
About your test case. g4-prover.pl finally succeeds to give the following reply:
G4 Prover: a Prolog Prover for Roy Dyckhoff's Sequent Calculus G4
This prover is a fork made by Joseph Vidal-Rosset (joseph.vidal-rosset@gmail.com),
from seqprover.pl, the sequent prover for CL-X, written by Naoyuki Tamura (tamura@kobe-u.ac.jp).
Type "help." if you need some help.
fol(g4i)> fol(g4i).
yes
fol(g4i)> output(pretty).
yes
fol(g4i)> _534#(~q(_534))->_534#q(_534)-->_534#q(_534).
Trying to prove with threshold = 0 1 2 3 4 5
Fail to prove _534#(~q(_534))->_534#q(_534) --> _534#q(_534) (232271 msec.)
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 232271 msec.
true
Fortunately, imogen confirms that it is correct:
joseph@mx:~$ imogen fol prove -i "(exists X.(~ q(X)) -> exists X.(q(X))) -> exists X.(q(X))"
Unprovable.
joseph@mx:~$ imogen fol prove -i "~ ~ ((exists X.(~ q(X)) -> exists X.(q(X))) -> exists X.(q(X)))"
Provable.
Your formula is provable, but only in classical FOL. It is proved by g4c as follows:
fol(g4c)> _534#(~q(_534))->_534#q(_534)-->_534#q(_534).
Trying to prove with threshold = 0 1 2
Succeed in proving _534#(~q(_534))->_534#q(_534) --> _534#q(_534) (41 msec.)
pretty:1 =
------------------------------------------------------ Ax-c
bot->X#q(X),q(X),X@(~q(X)->X#q(X)) --> bot,q(X),X#q(X)
------------------------------------------------------ R#-c ----------------------------------- Ax
bot->X#q(X),q(X),X@(~q(X)->X#q(X)) --> bot,X#q(X) X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
---------------------------------------------------------------------------------------------- L->->(4)
(q(X)->bot)->X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
------------------------------------------------ L~def
~q(X)->X#q(X),X@(~q(X)->X#q(X)) --> X#q(X)
------------------------------------------ L@
X@(~q(X)->X#q(X)) --> X#q(X)
---------------------------- L#->
X#(~q(X))->X#q(X) --> X#q(X)
yes
fol(g4c)> quit.
and via Naoyuki CL-X (seqprover.pl):
Trying to prove with threshold = 0 1 2
------------------------------ Ax
q(Y) --> X#(~q(X)),q(Y),X#q(X)
------------------------------ R#
q(Y) --> X#(~q(X)),X#q(X)
--------------------------- R~
--> ~q(Y),X#(~q(X)),X#q(X)
--------------------------- R# ----------------- Ax
--> X#(~q(X)),X#q(X) X#q(X) --> X#q(X)
---------------------------------------------- L->
X#(~q(X))->X#q(X) --> X#q(X)
To end on this point, I wonder if a logic that would use classical connective but non-classical quantifiers can be fully consistent: after all, exists X.f(X) is a kind of alternation, to speak like Quine.