Surprising. I have not the least error message. Could you give to me your output please?
I took an exact copy of from this post. I did not add any comments or such to your copy of the code.
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)
?- working_directory(_,'C:/Users/Eric/Documents').
true.
?- ['Wang''s Algorithm'].
ERROR: c:/users/eric/documents/wang's algorithm.pl:158:22: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:159:22: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:160:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:161:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:162:24: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:163:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:164:24: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:165:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:166:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:167:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:168:25: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:169:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:170:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:171:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:172:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:173:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:174:26: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:175:20: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:176:29: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:191:21: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:210:32: Syntax error: Operator expected
ERROR: c:/users/eric/documents/wang's algorithm.pl:216:55: Syntax error: Operator expected
true.
Line: 158
formula_simpler(~ ⊥, ⊤).
EDIT
The problem has to do with Windows.
When run on Ubuntu 18.04 via WSL 2 on Windows 10 it seems to work.
eric@WINDOWS-Something:~$ swipl
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.4)
?- working_directory(_,'/mnt/c/Users/Eric/Documents').
true.
?- ['Wang''s Algorithm'].
true.
?- qw.
|: p.
Quine:
T is substituted for p
⊤
⊤
⊥ is substituted for p
⊥
% 31,085 inferences, 0.008 CPU in 0.033 seconds (26% CPU, 3680572 Lips)
to prove that this formula is invalid.
|:
EDIT
The fix for Window is simple, just add
:- encoding(utf8).
in the code as the first executable line of code.
Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)
?- working_directory(_,'C:/Users/Eric/Documents').
true.
?- ['Wang''s Algorithm'].
true.
?- qw.
|: p.
Quine:
T is substituted for p
⊤
⊤
⊥ is substituted for p
⊥
% 29,566 inferences, 0.000 CPU in 0.105 seconds (0% CPU, Infinite Lips)
to prove that this formula is invalid.
|:
The change does not affect running on Linux.
1 Like
Tell me what I have to do, please. I wrote this file in emacs.
I note it on the file for Windows users.
Can I say that the best is to avoid using Windows ? 
Added ! Thanks !
Yes . Sorry to have made an allusion to a subject that is irrelevant here.
I just corrected my first post for this topic, because I was wrong to paste my first “work” on Hudson’s prover. These cuts are mines and of course it was nonsensical to add them on reduce/1 and not on prove/1 . I just pasted Ben Hudson’s original prover, and I apologize for not having done it from the start.
Jan, I am interested by your suggestion to get a kind of focusing. I understood that it is an important algorithmic tool, but I had difficulties to get it. That is a good occasion to finally understand this point.
I teach only what I understand easily, and on focusing, I have still to learn and understand completely. 
I just tested the big valid formula after having add cut just after del/2 on all prove/1 rules. It seems that the calculus speed has been improved, but not the number of inferences, but maybe there remains works to do on the order of the rules (I do not know):
% 183,434 inferences, 0.046 CPU in 0.500 seconds (9% CPU, 4021435 Lips)
to prove that []-->[(((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))] is a theorem in Classical Propositional Logic.
by comparison, without cuts:
% 183,434 inferences, 0.046 CPU in 0.768 seconds (6% CPU, 3966894 Lips)
to prove that []-->[(((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))] is a theorem in Classical Propositional Logic.
Thanks for this point. I nevertheless delete my previous version of quine-wang.pl because working on the order of rules, I get a very best result. I give in the file the new result. Here is the new quine-wang.pl:
% A Propositional Theorem Prover using Wang's Algorithm
% that makes use of Boole's method (Jan Burse work) for counter-models search.
% :- use_module(library(ordsets)).
% :- use_module(library(statistics)).
% :- use_module(library(dcg/basics)).
% :- use_module(library(clpfd)).
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, v). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
:- op(1200,xfy, -->). % implication (sequent)
%TYPE 'qw.' INTO THE CONSOLE TO START
help:-
write('-----------------------------------------------------------'),nl,
write('\nA Propositional Theorem Prover using both Quine\'s and Wang\'s Algorithms\n'),
write('by Joseph Vidal-Rosset from Ben Hudson\'s and Isabelle-Newbie\'s programs.\n\n'),
write('https://github.com/benhuds?tab=repositories \n\n'),
write('https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in\n\n'),
write('-----------------------------------------------------------'),nl,
write('To test the validity of your formula with Wang\'s algorithm:\n'),
write('- First, write "qw." and press Enter.\n'),
write('- Second, with this usual syntax: ~ a | a & b | a v b | a => b| a <=> b| \n'),
write('write your propositional formula and press Enter.\n'),
write('That\'s it. Have fun!').
qw :-
read(Formula),
getFormula(Formula).
getFormula(Formula):-
nl,
write('Quine:'),
time((nl,\+quine(Formula))),
write('to prove that this formula is invalid.'),nl,
qw
;
write('to prove that this formula is valid.'),nl,nl,
go([] --> [Formula]).
go(Formula):-
write('Wang:'),
nl,
write(' \t'),write(Formula),
time(prove(Formula)),
write('to prove that '),write(Formula), write(' is a theorem in Classical Propositional Logic.\n'),
qw.
%predicate to delete an element X from a list L.
del(X,[X|Tail],Tail).
del(X,[H|Tl1],[H|Tl2]):-
del(X,Tl1,Tl2),!.
%rule for id* (Ax.)
prove(L --> R):-
member(A,L),
member(B,R),
A == B,
nl,write(' \tDone (by id*)'),nl,nl.
%non-branching rules
prove(L --> R):-
member(A & B,L),
del(A & B,L,NewL),!,
nl,write(' \t'),write([A,B|NewL] --> R),
write(' \t (by and/left)'),
prove([A,B|NewL] --> R).
prove(L --> R):-
member(A v B,R),
del(A v B,R,NewR),!,
nl,write(' \t'),write(L --> [A,B|NewR]),
write(' \t (by or/right)'),
prove(L --> [A,B|NewR]).
prove(L --> R):-
member(A => B,R),!,
del(A => B,R,NewR),
nl,write(' \t'),write([A|L] --> [B|NewR]),
write(' \t (by arrow/right)'),
prove([A|L] --> [B|NewR]).
%branching rules
prove(L --> R):-
member(A => B,L),
del(A => B,L,NewL),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write([B|NewL] --> R),
write(' \t (by arrow/left)'),
prove([B|NewL] --> R),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write(NewL --> [A|R]),
write(' \t (by arrow/left)'),
prove(NewL --> [A|R]).
prove(L --> R):-
member(A & B,R),
del(A & B,R,NewR),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write(L --> [A|NewR]),
write(' \t (by and/right)'),
prove(L --> [A|NewR]),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write(L --> [B|NewR]),
write(' \t (by and/right)'),
prove(L --> [B|NewR]).
prove(L --> R):-
member(A v B,L),
del(A v B,L,NewL),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write([A|NewL] --> R),
write(' \t (by or/left)'),
prove([A|NewL] --> R),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write([B|NewL] --> R),
write(' \t (by or/left)'),
prove([B|NewL] --> R).
%negation
prove(L --> R):-
member(~X,L),
del(~X,L,NewL),!,
nl,write(' \t'),write(NewL --> [X|R]),
write(' \t (by negation/left)'),
prove(NewL --> [X|R]).
prove(L --> R):-
member(~X,R),
del(~X,R,NewR),!,
nl,write(' \t'),write([X|L] --> NewR),
write(' \t (by negation/right)'),
prove([X|L] --> NewR).
%rules for biconditional
prove(L --> R):-
member(A <=> B,L),
del(A <=> B,L,NewL),!,
nl,write(' \t'),write([(A => B),(B => A)|NewL] --> R),
write(' \t (by and/left)'),
prove([(A => B),(B => A)|NewL] --> R).
prove(L --> R):-
member(A <=> B,R),
del(A <=> B,R,NewR),!,
nl,write(' \t'),write(L --> [(A => B) & (B => A)|NewR]),
write(' \t (by and/right)'),
prove(L --> [(A => B) & (B => A)|NewR]).
% Quine
formula_simpler(~ ~ P , P).
formula_simpler(~ ⊥, ⊤).
formula_simpler(~ ⊤, ⊥).
formula_simpler(_P & ⊥, ⊥).
formula_simpler(⊥ & _P, ⊥).
formula_simpler(P & ⊤, P).
formula_simpler(⊤ & P, P).
formula_simpler(P v ⊥, P).
formula_simpler(⊥ v P, P).
formula_simpler(_P v ⊤, ⊤).
formula_simpler(⊤ v _P, ⊤).
formula_simpler(P => ⊥, ~ P).
formula_simpler(_P => ⊤, ⊤).
formula_simpler(⊥ => _P, ⊤).
formula_simpler(⊤ => P, P).
formula_simpler(P <=> ⊥, ~ P).
formula_simpler(⊥ <=> P, ~ P).
formula_simpler(P <=> ⊤, P).
formula_simpler(⊤ <=> P, P).
formula_simpler(P <=> P, ⊤).
formula_simple2(Formula, Simple) :-
Formula =.. [Operator | Args],
maplist(formula_simple2, Args, SimpleArgs),
SimplerFormula =.. [Operator | SimpleArgs],
formula_rootsimple(SimplerFormula, Simple).
formula_rootsimple(Formula, Simple) :-
( formula_simpler(Formula, Simpler)
-> formula_rootsimple(Simpler, Simple)
; Simple = Formula ).
formula_variable(Variable, Variable) :-
atom(Variable),
dif(Variable, ⊤),!,
atom(Variable),
dif(Variable, ⊥).
formula_variable(Formula, Variable) :-
Formula =.. [_Operator | Args],
member(Arg, Args),
formula_variable(Arg, Variable),!.
variable_replacement_formula_replaced(Variable, Replacement, Variable, Replacement).
variable_replacement_formula_replaced(Variable, _Replacement, Formula, Formula) :-
atom(Formula),
dif(Formula, Variable).
variable_replacement_formula_replaced(Variable, Replacement, Formula, Replaced) :-
Formula =.. [Operator | Args],
Args = [_ | _],
maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
Replaced =.. [Operator | ReplacedArgs].
quine(Formula) :-
formula_simple2(Formula, ⊤),
write(⊤),!.
quine(Formula) :-
formula_simple2(Formula, SimpleFormula),
formula_variable(SimpleFormula, Variable),
!,
variable_replacement_formula_replaced(Variable, ⊤, Formula, TopFormula),nl,
write(' \t'),write('T is substituted for '),write(Variable),nl,
write(' \t'),write(TopFormula),nl,
write(' \t'),quine(TopFormula),nl,
variable_replacement_formula_replaced(Variable, ⊥, Formula, BotFormula),nl,
write(' \t'),write('⊥ is substituted for '),write(Variable),nl,
write(' \t'),write(BotFormula),nl,
write(' \t'),quine(BotFormula).
/*
Examples:
?- qw.
|: p.
Quine:
T is substituted for p
⊤
⊤
⊥ is substituted for p
⊥
% 35,822 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 6215434 Lips)
to prove that this formula is invalid.
|: (~ p => p) <=> p.
Quine:
T is substituted for p
~ ⊤ => ⊤ <=> ⊤
⊤
⊥ is substituted for p
~ ⊥ => ⊥ <=> ⊥
⊤
% 25,057 inferences, 0.007 CPU in 0.007 seconds (100% CPU, 3777683 Lips)
to prove that this formula is valid.
Wang:
[]-->[(~p=>p<=>p)]
[]-->[(((~p=>p)=>p)&(p=> ~p=>p))] (by and/right)
First branch:
[]-->[((~p=>p)=>p)] (by and/right)
[(~p=>p)]-->[p] (by arrow/right)
First branch:
[p]-->[p] (by arrow/left)
Done (by id*)
Second branch:
[]-->[~p,p] (by arrow/left)
[p]-->[p] (by negation/right)
Done (by id*)
Second branch:
[]-->[(p=> ~p=>p)] (by and/right)
[p]-->[(~p=>p)] (by arrow/right)
[~p,p]-->[p] (by arrow/right)
Done (by id*)
% 172 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 1979150 Lips)
to prove that []-->[(~p=>p<=>p)] is a theorem in Classical Propositional Logic.
|: ((a => b) => a) => a.
Quine:
T is substituted for a
((⊤ => b)=> ⊤)=> ⊤
⊤
⊥ is substituted for a
((⊥ => b)=> ⊥)=> ⊥
⊤
% 426 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 1233306 Lips)
to prove that this formula is valid.
Wang:
[]-->[(((a=>b)=>a)=>a)]
[((a=>b)=>a)]-->[a] (by arrow/right)
First branch:
[a]-->[a] (by arrow/left)
Done (by id*)
Second branch:
[]-->[(a=>b),a] (by arrow/left)
[a]-->[b,a] (by arrow/right)
Done (by id*)
% 78 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 420648 Lips)
to prove that []-->[(((a=>b)=>a)=>a)] is a theorem in Classical Propositional Logic.
|:
Performances:
1. The valid formula:
(((( 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))
is proved by quine-wang.pl :
Quine:
% 1,013,782 inferences, 0.168 CPU in 0.922 seconds (18% CPU, 6023924 Lips)
to prove that this formula is valid.
Wang:
% 183,434 inferences, 0.046 CPU in 0.768 seconds (6% CPU, 3966894 Lips)
to prove that []-->[(((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))] is a theorem in Classical Propositional Logic.
with working on the order of rules and adding cut after del/1, as suggested by Jan Burse https://swi-prolog.discourse.group/t/improving-wangs-algorithm-in-prolog/2872/115 :
% 160,203 inferences, 0.034 CPU in 0.284 seconds (12% CPU, 4700335 Lips)
to prove that []-->[(((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))] is a theorem in Classical Propositional Logic.
2. The invalid disjunctive formula :
(( o11 & o21 ) v ( ( o11 & o31 ) v ( ( o11 & o41 ) v ( ( o11 & o51 ) v ( ( o11 & o61 ) v ( ( o21 & o31 ) v ( ( o21 & o41 ) v ( ( o21 & o51 ) v ( ( o21 & o61 ) v ( ( o31 & o41 ) v ( ( o31 & o51 ) v ( ( o31 & o61 ) v ( ( o41 & o51 ) v ( ( o41 & o61 ) v ( ( o51 & o61 ) v ( ( o12 & o22 ) v ( ( o12 & o32 ) v ( ( o12 & o42 ) v ( ( o12 & o52 ) v ( ( o12 & o62 ) v ( ( o22 & o32 ) v ( ( o22 & o42 ) v ( ( o22 & o52 ) v ( ( o22 & o62 ) v ( ( o32 & o42 ) v ( ( o32 & o52 ) v ( ( o32 & o62 ) v ( ( o42 & o52 ) v ( ( o42 & o62 ) v ( ( o52 & o62 ) v ( ( o13 & o23 ) v ( ( o13 & o33 ) v ( ( o13 & o43 ) v ( ( o13 & o53 ) v ( ( o13 & o63 ) v ( ( o23 & o33 ) v ( ( o23 & o43 ) v ( ( o23 & o53 ) v ( ( o23 & o63 ) v ( ( o33 & o43 ) v ( ( o33 & o53 ) v ( ( o33 & o63 ) v ( ( o43 & o53 ) v ( ( o43 & o63 ) v ( ( o53 & o63 ) v ( ( o14 & o24 ) v ( ( o14 & o34 ) v ( ( o14 & o44 ) v ( ( o14 & o54 ) v ( ( o14 & o64 ) v ( ( o24 & o34 ) v ( ( o24 & o44 ) v ( ( o24 & o54 ) v ( ( o24 & o64 ) v ( ( o34 & o44 ) v ( ( o34 & o54 ) v ( ( o34 & o64 ) v ( ( o44 & o54 ) v ( ( o44 & o64 ) v ( ( o54 & o64 ) v ( ( o15 & o25 ) v ( ( o15 & o35 ) v ( ( o15 & o45 ) v ( ( o15 & o55 ) v ( ( o15 & o65 ) v ( ( o25 & o35 ) v ( ( o25 & o45 ) v ( ( o25 & o55 ) v ( ( o25 & o65 ) v ( ( o35 & o45 ) v ( ( o35 & o55 ) v ( ( o35 & o65 ) v ( ( o45 & o55 ) v ( ( o45 & o65 ) v ( o55 & o65 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
is proved as being such via Quine:
% 403,094 inferences, 0.051 CPU in 0.230 seconds (22% CPU, 7922030 Lips)
to prove that this formula is invalid.
*/