The proof presented here (obtained October 16, 1995) has length 8.
You may simply take the input and start experimenting.
------------> process usable:
** KEPT (pick-wt=3): 3 [] x=x.
Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] x=x.
------------> process sos:
** KEPT (pick-wt=5): 4 [] x^x=x.
---> New Demodulator: 5 [new_demod,4] x^x=x.
** KEPT (pick-wt=7): 6 [] x^y=y^x.
** KEPT (pick-wt=11): 7 [] (x^y)^z=x^ (y^z).
---> New Demodulator: 8 [new_demod,7] (x^y)^z=x^ (y^z).
** KEPT (pick-wt=5): 9 [] x v x=x.
---> New Demodulator: 10 [new_demod,9] x v x=x.
** KEPT (pick-wt=7): 11 [] x v y=y v x.
** KEPT (pick-wt=11): 12 [] (x v y) v z=x v (y v z).
---> New Demodulator: 13 [new_demod,12] (x v y) v z=x v (y v z).
** KEPT (pick-wt=2): 14 [] (x^ (y v z)) v (x^y)=x^ (y v z).
---> New Demodulator: 15 [new_demod,14] (x^ (y v z)) v (x^y)=x^ (y v z).
** KEPT (pick-wt=2): 16 [] (x v (y^z))^ (x v y)=x v (y^z).
---> New Demodulator: 17 [new_demod,16] (x v (y^z))^ (x v y)=x v (y^z).
** KEPT (pick-wt=13): 18 [] x^ (y v (x^z))=x^ (y v z).
---> New Demodulator: 19 [new_demod,18] x^ (y v (x^z))=x^ (y v z).
** KEPT (pick-wt=13): 21 [copy,20,flip.1] (A^B) v (A^C)!=A^ (B v C).
>>>> Starting back demodulation with 5.
Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] x^y=y^x.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 10.
Following clause subsumed by 11 during input processing: 0 [copy,11,flip.1] x v y=y v x.
>>>> Starting back demodulation with 13.
>>>> Starting back demodulation with 15.
>>>> Starting back demodulation with 17.
>>>> Starting back demodulation with 19.
======= end of input processing =======
=========== start of search ===========
given clause #1: (wt=5) 4 [] x^x=x.
----> UNIT CONFLICT at 2.10 sec ----> 316 [binary,314.1,21.1] $F.
Length of proof is 8. Level of proof is 4.
---------------- PROOF ----------------
6 [] x^y=y^x.
11 [] x v y=y v x.
13,12 [] (x v y) v z=x v (y v z).
14 [] (x^ (y v z)) v (x^y)=x^ (y v z).
16 [] (x v (y^z))^ (x v y)=x v (y^z).
19,18 [] x^ (y v (x^z))=x^ (y v z).
20 [] A^ (B v C)!= (A^B) v (A^C).
21 [copy,20,flip.1] (A^B) v (A^C)!=A^ (B v C).
41 [para_from,6.1.1,14.1.1.2] (x^ (y v z)) v (y^x)=x^ (y v z).
86 [para_into,11.1.1,14.1.1,flip.1] (x^y) v (x^ (y v z))=x^ (y v z).
99 [para_from,11.1.1,41.1.1.1.2] (x^ (y v z)) v (z^x)=x^ (z v y).
104,103 [para_from,11.1.1,16.1.1.2] (x v (y^z))^ (y v x)=x v (y^z).
167,166 [para_into,86.1.1.2.2,11.1.1] (x^y) v (x^ (z v y))=x^ (y v z).
199 [para_into,99.1.1.1,16.1.1,demod,19,13,167,104] x v (y^ (z v x))=x v (y^z).
314 [para_into,199.1.1.2,18.1.1,demod,167,flip.1] (x^y) v (x^z)=x^ (y v z).
316 [binary,314.1,21.1] $F.
-------------- statistics -------------
clauses given 40
clauses generated 1871
(hot clauses generated) 446
para_from generated 712
para_into generated 1159
demod & eval rewrites 3089
clauses wt,lit,sk delete 648
tautologies deleted 0
clauses forward subsumed 1169
(subsumed by sos) 231
unit deletions 0
factor simplifications 0
clauses kept 208
(hot clauses kept) 42
new demodulators 104
empty clauses 1
clauses back demodulated 44
clauses back subsumed 2
usable size 37
sos size 125
demodulators size 72
passive size 0
hot size 2
Kbytes malloced 383
----------- times (seconds) -----------
user CPU time 2.16 (0 hr, 0 min, 2 sec)
system CPU time 0.67 (0 hr, 0 min, 0 sec)
wall-clock time 3 (0 hr, 0 min, 3 sec)
input time 0.09
clausify time 0.00
process input 0.03
para_into time 0.27
para_from time 0.15
pre_process time 1.42
renumber time 0.08
demod time 0.54
order equalities 0.06
unit deleletion 0.00
factor simplify 0.00
weigh cl time 0.17
hints keep time 0.00
sort lits time 0.00
forward subsume 0.08
delete cl time 0.09
keep cl time 0.14
hints time 0.00
print_cl time 0.00
conflict time 0.07
new demod time 0.04
post_process time 0.07
back demod time 0.02
back subsume 0.04
factor time 0.00
hot list time 0.38
unindex time 0.00
The job finished Mon Oct 16 16:55:55 1995