The theorem is that the six equations named L1, L3, B1, L2, L4, and B2 are a basis for Boolean algebra. From this result, one can construct an independent self-dual 2-basis for Boolean algebra.
The proof presented here (obtained December 13, 1995) has length 30.
You may simply take the input and start experimenting.
------------> process usable:
** KEPT (pick-wt=3): 1 [] -> x=x.
** KEPT (pick-wt=29): 2 [] (A*B)+ (A*C)=A* (B+C), (A+B)*B=B, B+B@ =A+A@ -> .
Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] -> x=x.
------------> process sos:
** KEPT (pick-wt=9): 3 [] -> x+ (y* (x*z))=x.
---> New Demodulator: 4 [new_demod,3] -> x+ (y* (x*z))=x.
** KEPT (pick-wt=11): 5 [] -> ((x*y)+ (y*z))+y=y.
---> New Demodulator: 6 [new_demod,5] -> ((x*y)+ (y*z))+y=y.
** KEPT (pick-wt=2): 7 [] -> (x+y)* (x+y@ )=x.
---> New Demodulator: 8 [new_demod,7] -> (x+y)* (x+y@ )=x.
** KEPT (pick-wt=2): 9 [] -> x* (y+ (x+z))=x.
---> New Demodulator: 10 [new_demod,9] -> x* (y+ (x+z))=x.
** KEPT (pick-wt=11): 11 [] -> ((x+y)* (y+z))*y=y.
---> New Demodulator: 12 [new_demod,11] -> ((x+y)* (y+z))*y=y.
** KEPT (pick-wt=2): 13 [] -> (x*y)+ (x*y@ )=x.
---> New Demodulator: 14 [new_demod,13] -> (x*y)+ (x*y@ )=x.
** KEPT (pick-wt=7): 15 [] -> x+y=y+x.
** KEPT (pick-wt=7): 16 [] -> x*y=y*x.
** KEPT (pick-wt=11): 17 [] -> (x+y)+z=x+ (y+z).
---> New Demodulator: 18 [new_demod,17] -> (x+y)+z=x+ (y+z).
** KEPT (pick-wt=11): 19 [] -> (x*y)*z=x* (y*z).
---> New Demodulator: 20 [new_demod,19] -> (x*y)*z=x* (y*z).
>>>> Starting back demodulation with 4.
>>>> Starting back demodulation with 6.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 10.
>>>> Starting back demodulation with 12.
>>>> Starting back demodulation with 14.
Following clause subsumed by 15 during input processing: 0 [copy,15,flip.1] -> x+y=y+x.
Following clause subsumed by 16 during input processing: 0 [copy,16,flip.1] -> x*y=y*x.
>>>> Starting back demodulation with 18.
>> back demodulating 5 with 18.
>>>> Starting back demodulation with 20.
>> back demodulating 11 with 20.
>>>> Starting back demodulation with 22.
>>>> Starting back demodulation with 24.
======= end of input processing =======
=========== start of search ===========
-----> EMPTY CLAUSE at 15.64 sec ----> 3783 [back_demod,239,demod,3735,unit_del,16,2643] -> .
Length of proof is 30. Level of proof is 6.
---------------- PROOF ----------------
1 [] -> x=x.
2 [] (A*B)+ (A*C)=A* (B+C), (A+B)*B=B, B+B@ =A+A@ -> .
3 [] -> x+ (y* (x*z))=x.
7 [] -> (x+y)* (x+y@ )=x.
9 [] -> x* (y+ (x+z))=x.
13 [] -> (x*y)+ (x*y@ )=x.
15 [] -> x+y=y+x.
16 [] -> x*y=y*x.
18,17 [] -> (x+y)+z=x+ (y+z).
20,19 [] -> (x*y)*z=x* (y*z).
27 [para_from,7.1.1,3.1.1.2.2,demod,18] -> x+ (y+ (z*x))=x+y.
29 [para_into,9.1.1.2.2,3.1.1] -> x* (y+x)=x.
31 [para_from,9.1.1,3.1.1.2.2] -> x+ (y*x)=x.
37 [para_from,13.1.1,9.1.1.2.2,demod,20] -> x* (y* (z+x))=x*y.
46,45 [para_into,27.1.1.2,13.1.1,flip.1] -> x@ + (y*x)=x@ +y.
87 [para_from,45.1.1,27.1.1.2] -> x+ (x@ +y)=x+x@ .
92 [para_into,15.1.1,31.1.1,flip.1] -> (x*y)+y=y.
108 [para_from,15.1.1,7.1.1.2] -> (x+y)* (y@ +x)=x.
110 [para_from,15.1.1,7.1.1.1] -> (x+y)* (y+x@ )=y.
161 [para_into,87.1.1.2,15.1.1] -> x+ (y+x@ )=x+x@ .
233,232 [para_into,16.1.1,29.1.1,flip.1] -> (x+y)*y=y.
234 [para_into,16.1.1,9.1.1,flip.1] -> (x+ (y+z))*y=y.
236 [para_into,16.1.1,7.1.1,flip.1] -> (x+y@ )* (x+y)=x.
239 [back_demod,2,demod,233,unit_del,1] (A*B)+ (A*C)=A* (B+C), B+B@ =A+A@ -> .
245 [para_from,16.1.1,45.1.1.2] -> x@ + (x*y)=x@ +y.
247 [para_from,16.1.1,31.1.1.2] -> x+ (x*y)=x.
249 [para_from,16.1.1,27.1.1.2.2] -> x+ (y+ (x*z))=x+y.
261 [para_from,16.1.1,13.1.1.1] -> (x*y)+ (y*x@ )=y.
338,337 [para_into,108.1.1.1,92.1.1,demod,46] -> x* (x@ +y)=y*x.
440 [para_into,17.1.1,15.1.1] -> x+ (y+z)=y+ (z+x).
604,603 [para_into,234.1.1.1,161.1.1] -> (x+x@ )*y=y.
701,700 [para_from,236.1.1,37.1.1.2,flip.1] -> x* (y+x@ )=x*y.
771 [para_from,245.1.1,17.1.1.1,demod,18,flip.1] -> x@ + ((x*y)+z)=x@ + (y+z).
810 [para_from,249.1.1,110.1.1.1,demod,18] -> (x+y)* (y+ ((x*z)+x@ ))=y+ (x*z).
1047,1046 [para_into,261.1.1.2,232.1.1,demod,701] -> (x*y)+x@ =y+x@ .
1054 [back_demod,810,demod,1047] -> (x+y)* (y+ (z+x@ ))=y+ (x*z).
1870,1869 [para_from,440.1.1,337.1.1.2] -> x* (y+ (z+x@ ))= (y+z)*x.
2643 [para_from,603.1.1,13.1.1.2,demod,604] -> x+x@ =y+y@ .
3256,3255 [para_from,771.1.1,337.1.1.2,demod,338,flip.1] -> ((x*y)+z)*x= (y+z)*x.
3735,3734 [para_into,1054.1.1.1,247.1.1,demod,1870,3256,flip.1] -> (x*y)+ (x*z)= (y+z)*x.
3783 [back_demod,239,demod,3735,unit_del,16,2643] -> .
-------------- statistics -------------
clauses given 102
clauses generated 7785
hyper_res generated 0
para_from generated 3451
para_into generated 4334
demod & eval rewrites 16016
clauses wt,lit,sk delete 177
tautologies deleted 0
clauses forward subsumed 6712
cl not subsumed due to ancestor_subsume 58
(subsumed by sos) 506
unit deletions 3
factor simplifications 0
clauses kept 2084
new demodulators 1698
empty clauses 1
clauses back demodulated 806
clauses back subsumed 67
usable size 88
sos size 1123
demodulators size 980
passive size 0
hot size 0
Kbytes malloced 2650
----------- times (seconds) -----------
user CPU time 15.73 (0 hr, 0 min, 15 sec)
system CPU time 2.41 (0 hr, 0 min, 2 sec)
wall-clock time 19 (0 hr, 0 min, 19 sec)
input time 0.36
clausify time 0.00
process input 0.04
hyper_res time 0.00
para_into time 0.37
para_from time 0.45
pre_process time 12.34
renumber time 0.38
demod time 2.18
order equalities 0.21
unit deleletion 0.00
factor simplify 0.00
weigh cl time 4.39
hints keep time 0.00
sort lits time 0.00
forward subsume 1.87
delete cl time 0.11
keep cl time 2.04
hints time 0.01
print_cl time 0.00
conflict time 0.22
new demod time 0.54
post_process time 1.96
back demod time 1.47
back subsume 0.47
factor time 0.00
unindex time 0.80
The job finished Wed Dec 13 07:50:41 1995