The theorem states that the axioms of symmetry and associativity completely axiomatize
equivalential calculus; in particular, their use leads to the deduction of
e(e(e(x,y),e(z,x)),e(y,z)),
which, with symmetry, forms a complete axiomatization of the calculus.
The proof presented here (obtained June 21, 1995) has length 6.
Reference: For a detailed description of this theorem, see L. Wos, ``Meeting the Challenge of Fifty Years of Logic,'' Journal of Automated Reasoning, 6 (1990) 213-232.
You may simply take the input and start experimenting.
=========== start of search ===========
Starting on level 1, last kept clause of level 0 is 4.
given clause #1: (wt=-2147483647) 2 [] P(e(e(x,y),e(y,x))).
----> UNIT CONFLICT at 1.61 sec ----> 297 [binary,296.1,4.1] $F.
Length of proof is 6. Level of proof is 4.
---------------- PROOF ----------------
1 [] -P(e(x,y))| -P(x)|P(y).
2 [] P(e(e(x,y),e(y,x))).
3 [] P(e(e(e(x,y),z),e(x,e(y,z)))).
4 [] -P(e(e(e(a,b),e(c,a)),e(b,c))).
5 [hyper,1,3,3] P(e(e(x,y),e(z,e(x,e(y,z))))).
6 [hyper,1,2,3] P(e(e(x,e(y,z)),e(e(x,y),z))).
8 [hyper,1,5,5] P(e(x,e(e(y,z),e(e(u,e(y,e(z,u))),x)))).
14 [hyper,1,5,6] P(e(x,e(e(y,e(z,u)),e(e(e(y,z),u),x)))).
30 [hyper,1,2,8] P(e(e(e(x,y),e(e(z,e(x,e(y,z))),u)),u)).
296 [hyper,1,30,14] P(e(e(e(x,y),e(z,x)),e(y,z))).
297 [binary,296.1,4.1] $F.
----> UNIT CONFLICT at 8.91 sec ----> 850 [binary,849.1,4.1] $F.
Length of proof is 5. Level of proof is 4.
---------------- PROOF ----------------
1 [] -P(e(x,y))| -P(x)|P(y).
2 [] P(e(e(x,y),e(y,x))).
3 [] P(e(e(e(x,y),z),e(x,e(y,z)))).
4 [] -P(e(e(e(a,b),e(c,a)),e(b,c))).
5 [hyper,1,3,3] P(e(e(x,y),e(z,e(x,e(y,z))))).
6 [hyper,1,2,3] P(e(e(x,e(y,z)),e(e(x,y),z))).
14 [hyper,1,5,6] P(e(x,e(e(y,e(z,u)),e(e(e(y,z),u),x)))).
77 [hyper,1,6,14] P(e(e(x,e(y,e(z,u))),e(e(e(y,z),u),x))).
849 [hyper,1,77,5] P(e(e(e(x,y),e(z,x)),e(y,z))).
850 [binary,849.1,4.1] $F.
-------------- statistics -------------
clauses given 275
clauses generated 54943
hyper_res generated 54943
demod & eval rewrites 0
clauses wt,lit,sk delete 44953
tautologies deleted 0
clauses forward subsumed 5675
cl not subsumed due to ancestor_subsume 336
(subsumed by sos) 2073
unit deletions 0
factor simplifications 0
clauses kept 4315
new demodulators 0
empty clauses 2
clauses back demodulated 0
clauses back subsumed 351
usable size 276
sos size 3691
demodulators size 0
passive size 1
hot size 0
Kbytes malloced 2139
----------- times (seconds) -----------
user CPU time 96.51 (0 hr, 1 min, 36 sec)
system CPU time 20.19 (0 hr, 0 min, 20 sec)
wall-clock time 124 (0 hr, 2 min, 4 sec)
input time 0.02
clausify time 0.00
hyper_res time 23.09
pre_process time 60.94
renumber time 7.42
demod time 17.09
order equalities 0.00
unit deleletion 0.00
factor simplify 0.00
weigh cl time 8.10
hints keep time 0.00
sort lits time 0.00
forward subsume 6.11
delete cl time 7.50
keep cl time 4.15
hints time 0.00
print_cl time 6.38
conflict time 1.12
new demod time 0.00
post_process time 10.78
back demod time 0.00
back subsume 9.07
factor time 0.00
unindex time 1.53
The job finished Wed Jun 21 17:34:01 1995