The theorem is that the seven positive input clauses are an axiomatization of Boolean algebra. The denial (a negative 3-clause) corresponds to 3 equations, which when added to the first 3 equations (the ones not involving p), is a previously known basis for Boolean algebra. This theorem arose when showing that a self-dual 2-basis for Boolean algebra is dependent.
The proof presented here (obtained on January 8, 1996) has length 77.
Reference:
W. McCune and R. Padmanabhan, Automated Deduction in Equational Logic and Geometry, submitted for publication, 1995. See the online version of this monograph for additional information.
You may simply take the input and start experimenting.
----- Otter 3.0.4, August 1995 -----
The job was started by wos on bashful.mcs.anl.gov, Mon Jan 8 10:29:39 1996
The command was "/home/mccune/bin-rs6000/otter".
op(400,xfx,[*,+,^,v,/,\,#]).
op(300,yf,@).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
assign(pick_given_ratio,12).
assign(max_mem,24000).
assign(max_seconds,60).
set(knuth_bendix).
dependent: set(para_from).
dependent: set(para_into).
dependent: clear(para_from_right).
dependent: clear(para_into_right).
dependent: set(para_from_vars).
dependent: set(eq_units_both_ways).
dependent: set(dynamic_demod_all).
dependent: set(dynamic_demod).
dependent: set(order_eq).
dependent: set(back_demod).
dependent: set(process_input).
dependent: set(lrpo).
WARNING: set(eq_units_both_ways) flag already set.
set(eq_units_both_ways).
set(build_proof_object).
dependent: set(order_history).
set(hyper_res).
WARNING: set(order_history) flag already set.
set(order_history).
set(unit_deletion).
set(para_from_units_only).
set(para_into_units_only).
set(ancestor_subsume).
WARNING: set(back_sub) flag already set.
set(back_sub).
assign(max_weight,8).
WARNING: assign(heat,1) already has that value.
assign(heat,1).
lex([1,A,B,C,_*_,_+_,_@ ,p(_,_,_)]).
weight_list(pick_and_purge).
weight(A,0).
weight(B,0).
weight(C,0).
weight(1*x@ =x@ ,4).
weight(x@ + (1*y)=1* (x@ +y),4).
weight(x+ ((y+x)*z)= (y+x)* (x+z),4).
weight(((x+y)*z)+y= (x+y)* (z+y),4).
weight((x* (y+z))* (x*z)=x*z,4).
weight(1* (x@ +y@ )=x@ +y@ ,4).
weight(1*1=1,4).
weight((x+y)* (y+y)=y+y,4).
weight(((x+y)* (z+y))*y=y,4).
weight(((x+y@ )*1)*y@ =y@ ,4).
weight(1* (x@ +1)=x@ +1,4).
weight((1* (x+1))*1=1,4).
weight((1*x)+1=1* (x+1),4).
weight((1* (x+1))* (1+1)=1+1,4).
weight(1@ + (1+ (1@ *1))=1,4).
weight(x@ + (((y+x@ )*x)+ (x@ *x))=y+x@ ,4).
weight(x@ * (x@ + (x+x))=x@ ,4).
weight((x*y)+ ((x*z)+ (z@ *z))=x* (y+ ((x*z)+ (z@ *z))),4).
weight(x* ((x*y)+ (y@ *y))= (x*y)+ (y@ *y),4).
weight(x* (y@ + ((x*y)+ (y@ *y)))=x,4).
weight((x@ *y)+x@ =x@ * (y+ (x@ + (x+x))),4).
weight(1* (x+1)=1,4).
weight(1+1=1,4).
weight(x@ +1=1,4).
weight(1@ *1=1@ ,4).
weight((x+1@ )*1=x+1@ ,4).
weight(x* (1@ + ((x*1)+1@ ))=x,4).
weight(x* ((x*1)+1@ )= (x*1)+1@ ,4).
weight(1@ +1@ =1@ ,4).
weight(1@ * (x+1@ )=1@ * (x+1),4).
weight(1@ + (x+1@ )=x+1@ ,4).
weight((x*1)+1@ =x,4).
weight(x*x=x,4).
weight(x+1=1,4).
weight(1@ * (x+1@ )=1@ ,4).
weight(1@ +x=x,4).
weight(x*1=x,4).
weight(x*1@ =1@ ,4).
weight(x+1@ =x,4).
weight(1@ *x=1@ ,4).
weight((x*y)+x=x* (y+x),4).
weight(x+ (x*y)=x* (x+y),4).
weight(x* (y+x)=x,4).
weight(x* (x+y)=x* (1+y),4).
weight((x*y)+x=x,4).
weight(x* (1+x@ )=x,4).
weight(x*x@ =1@ ,4).
weight(x@ *x=1@ ,4).
weight(x* ((y+x)+z)=x* (x+z),4).
weight(x@ @ =x,4).
weight((x*y)+ (x@ *y)=y,4).
weight(1@ =x*x@ ,4).
weight(x@ * (y+x)=x@ *y,4).
weight(x@ * (x+y)=x@ *y,4).
weight((x* (1+y))+ (x@ *y)=x+y,4).
weight(x*x@ =y*y@ ,4).
weight(x@ * ((y+x)+z)=x@ * (y+z),4).
weight(1+x=1,4).
weight(x* (x+y)=x,4).
weight(x+ (x@ *y)=x+y,4).
weight(x* ((y+x)+z)=x,4).
weight(x+ (x*y)=x,4).
weight((x+y)+z=y+ (x+z),4).
weight(x+ (x+y)=x+y,4).
weight((x*y)+y=y,4).
weight(x+ ((y*x)+z)=x+z,4).
weight(x+ (y*x)=x,4).
weight(x+ (y* (x+z))=x+ (y*z),4).
weight((x*y)+ (y*z)=y* ((x*y)+z),4).
weight((x*y)+ (z*x)=x* (y+ (z*x)),4).
weight(x+ ((x+y)*z)= (x+y)* (x+z),4).
weight(x*y=y*x,4).
weight(x+ (y*z)= (x+z)* (x+y),4).
end_of_list.
list(usable).
0 [] x=x.
0 [] A+ (B*C)!= (A+B)* (A+C)| (A*B)+B!=B|B*B@ !=A*A@ .
end_of_list.
list(sos).
0 [] (x+y)*y=y.
0 [] x* (y+z)= (x*y)+ (x*z).
0 [] x+x@ =1.
0 [] p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)).
0 [] p(x,x,y)=y.
0 [] p(x,y,y)=x.
0 [] p(x,y,x)=x.
end_of_list.
list(hot).
1 [] x+x@ =1.
2 [] p(x,x,y)=y.
3 [] p(x,y,y)=x.
4 [] p(x,y,x)=x.
end_of_list.
------------> process usable:
** KEPT (pick-wt=3): 5 [] x=x.
** KEPT (pick-wt=14): 6 [] A+ (B*C)!= (A+B)* (A+C)| (A*B)+B!=B|B*B@ !=A*A@ .
Following clause subsumed by 5 during input processing: 0 [copy,5,flip.1] x=x.
------------> process sos:
** KEPT (pick-wt=7): 7 [] (x+y)*y=y.
---> New Demodulator: 8 [new_demod,7] (x+y)*y=y.
** KEPT (pick-wt=13): 10 [copy,9,flip.1] (x*y)+ (x*z)=x* (y+z).
---> New Demodulator: 11 [new_demod,10] (x*y)+ (x*z)=x* (y+z).
** KEPT (pick-wt=6): 12 [] x+x@ =1.
---> New Demodulator: 13 [new_demod,12] x+x@ =1.
** KEPT (pick-wt=18): 14 [] p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)).
---> New Demodulator: 15 [new_demod,14] p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)).
** KEPT (pick-wt=15): 17 [copy,16,demod,15] (x*x@ )+ ((x*y)+ (x@ *y))=y.
---> New Demodulator: 18 [new_demod,17] (x*x@ )+ ((x*y)+ (x@ *y))=y.
** KEPT (pick-wt=15): 20 [copy,19,demod,15] (x*y@ )+ ((x*y)+ (y@ *y))=x.
---> New Demodulator: 21 [new_demod,20] (x*y@ )+ ((x*y)+ (y@ *y))=x.
** KEPT (pick-wt=15): 23 [copy,22,demod,15] (x*y@ )+ ((x*x)+ (y@ *x))=x.
---> New Demodulator: 24 [new_demod,23] (x*y@ )+ ((x*x)+ (y@ *x))=x.
>>>> Starting back demodulation with 8.
>>>> Starting back demodulation with 11.
>>>> Starting back demodulation with 13.
>>>> Starting back demodulation with 15.
>>>> Starting back demodulation with 18.
>>>> Starting back demodulation with 21.
>>>> Starting back demodulation with 24.
======= end of input processing =======
=========== start of search ===========
----> UNIT CONFLICT at 3.48 sec ----> 251 [binary,250.1,237.1] $F.
Length of proof is 77. Level of proof is 27.
---------------- PROOF ----------------
1 [] x+x@ =1.
5 [] x=x.
6 [] A+ (B*C)!= (A+B)* (A+C)| (A*B)+B!=B|B*B@ !=A*A@ .
7 [] (x+y)*y=y.
9 [] x* (y+z)= (x*y)+ (x*z).
11,10 [copy,9,flip.1] (x*y)+ (x*z)=x* (y+z).
13,12 [] x+x@ =1.
15,14 [] p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)).
16 [] p(x,x,y)=y.
17 [copy,16,demod,15] (x*x@ )+ ((x*y)+ (x@ *y))=y.
19 [] p(x,y,y)=x.
21,20 [copy,19,demod,15] (x*y@ )+ ((x*y)+ (y@ *y))=x.
26,25 [para_from,12.1.1,7.1.1.1] 1*x@ =x@ .
27 [para_into,10.1.1.1,25.1.1] x@ + (1*y)=1* (x@ +y).
30,29 [para_into,10.1.1.1,7.1.1] x+ ((y+x)*z)= (y+x)* (x+z).
32,31 [para_into,10.1.1.2,7.1.1] ((x+y)*z)+y= (x+y)* (z+y).
33 [para_from,10.1.1,7.1.1.1] (x* (y+z))* (x*z)=x*z.
35 [para_into,27.1.1.2,25.1.1,flip.1] 1* (x@ +y@ )=x@ +y@ .
38,37 (heat=1) [para_into,35.1.1.2,1.1.1,demod,13] 1*1=1.
39 [para_into,29.1.1.2,7.1.1,flip.1] (x+y)* (y+y)=y+y.
41 [para_from,31.1.1,7.1.1.1] ((x+y)* (z+y))*y=y.
43 (heat=1) [para_into,41.1.1.1.2,1.1.1] ((x+y@ )*1)*y@ =y@ .
45 [para_from,37.1.1,27.1.1.2,flip.1] 1* (x@ +1)=x@ +1.
48,47 [para_from,37.1.1,33.1.1.2,demod,38] (1* (x+1))*1=1.
49 [para_from,37.1.1,10.1.1.2] (1*x)+1=1* (x+1).
51 [para_from,49.1.1,39.1.1.1] (1* (x+1))* (1+1)=1+1.
54,53 [para_into,17.1.1.2.1,37.1.1,demod,26] 1@ + (1+ (1@ *1))=1.
61 [para_into,20.1.1.1,7.1.1] x@ + (((y+x@ )*x)+ (x@ *x))=y+x@ .
63 [para_into,20.1.1.2,10.1.1,demod,11] x@ * (x@ + (x+x))=x@ .
66,65 [para_from,20.1.1,31.1.1.1.1,demod,21] (x*y)+ ((x*z)+ (z@ *z))=x* (y+ ((x*z)+ (z@ *z))).
67 [para_from,20.1.1,7.1.1.1] x* ((x*y)+ (y@ *y))= (x*y)+ (y@ *y).
69 [back_demod,20,demod,66] x* (y@ + ((x*y)+ (y@ *y)))=x.
72,71 [para_from,63.1.1,10.1.1.2] (x@ *y)+x@ =x@ * (y+ (x@ + (x+x))).
80,79 [para_into,69.1.1.2.2.1,47.1.1,demod,54,48,flip.1] 1* (x+1)=1.
82,81 [back_demod,51,demod,80,80,flip.1] 1+1=1.
86,85 [back_demod,45,demod,80,flip.1] x@ +1=1.
88,87 [para_from,81.1.1,63.1.1.2.2,demod,86] 1@ *1=1@ .
90,89 [para_from,87.1.1,61.1.1.2.2,demod,32,13,30,86] (x+1@ )*1=x+1@ .
91 [para_from,87.1.1,69.1.1.2.2.2] x* (1@ + ((x*1)+1@ ))=x.
94,93 [para_from,87.1.1,67.1.1.2.2,demod,88] x* ((x*1)+1@ )= (x*1)+1@ .
96,95 [para_from,87.1.1,71.1.1.1,demod,82,86,82,88] 1@ +1@ =1@ .
97 [para_from,87.1.1,65.1.1.2.1,demod,88,96,72,82,86,88,88,96,flip.1] 1@ * (x+1@ )=1@ * (x+1).
102,101 [para_from,89.1.1,29.1.1.2,demod,86,90] 1@ + (x+1@ )=x+1@ .
104,103 [back_demod,91,demod,102,94] (x*1)+1@ =x.
105 [back_demod,93,demod,104,104] x*x=x.
108,107 [para_into,103.1.1.1,7.1.1,demod,13,flip.1] x+1=1.
109 [back_demod,97,demod,108,88] 1@ * (x+1@ )=1@ .
112,111 [para_from,103.1.1,101.1.1.2,demod,104] 1@ +x=x.
114,113 [para_from,103.1.1,89.1.1.1,demod,104] x*1=x.
116,115 [para_from,103.1.1,43.1.1.1.1,demod,114] x*1@ =1@ .
120,119 [back_demod,103,demod,114] x+1@ =x.
122,121 [back_demod,109,demod,120] 1@ *x=1@ .
124,123 [para_from,105.1.1,10.1.1.2] (x*y)+x=x* (y+x).
126,125 [para_from,105.1.1,10.1.1.1] x+ (x*y)=x* (x+y).
130,129 [para_from,113.1.1,10.1.1.2,demod,124,108,114] x* (y+x)=x.
131 [para_from,113.1.1,10.1.1.1,demod,126] x* (x+y)=x* (1+y).
133,132 [back_demod,123,demod,130] (x*y)+x=x.
136 [para_from,115.1.1,17.1.1.2.2,demod,116,120,120] x*x@ =1@ .
139 [copy,136,flip.1] 1@ =x*x@ .
142 [para_into,121.1.1,67.1.1,demod,122,112] x@ *x=1@ .
149 [para_from,129.1.1,10.1.1.1,demod,126,flip.1] x* ((y+x)+z)=x* (x+z).
156,155 [para_from,136.1.1,17.1.1.1,demod,112] (x*y)+ (x@ *y)=y.
163 [para_into,139.1.1,139.1.1] x*x@ =y*y@ .
167,166 [para_from,142.1.1,10.1.1.2,demod,120,flip.1] x@ * (y+x)=x@ *y.
169,168 [para_from,142.1.1,10.1.1.1,demod,112,flip.1] x@ * (x+y)=x@ *y.
172 [para_into,155.1.1.1,131.1.1,demod,169] (x* (1+y))+ (x@ *y)=x+y.
174 [para_into,155.1.1.1,129.1.1,demod,167] x+ (x@ *y)=y+x.
179 [para_from,166.1.1,10.1.1.1,demod,11,flip.1] x@ * ((y+x)+z)=x@ * (y+z).
188,187 [para_into,174.1.1.2,113.1.1,demod,13,flip.1] 1+x=1.
190,189 [back_demod,172,demod,188,114] x+ (x@ *y)=x+y.
192,191 [back_demod,131,demod,188,114] x* (x+y)=x.
195,194 [back_demod,149,demod,192] x* ((y+x)+z)=x.
197,196 [back_demod,125,demod,192] x+ (x*y)=x.
198 [para_from,179.1.1,155.1.1.2,demod,195,190,flip.1] (x+y)+z=y+ (x+z).
204 [para_into,189.1.1.2,168.1.1,demod,190,flip.1] x+ (x+y)=x+y.
215,214 [para_into,204.1.1.2,155.1.1,demod,156] (x*y)+y=y.
216 [back_demod,6,demod,215,unit_del,5,163] A+ (B*C)!= (A+B)* (A+C).
219 [para_from,214.1.1,198.1.1.1,flip.1] x+ ((y*x)+z)=x+z.
226,225 [para_into,219.1.1.2,119.1.1,demod,120] x+ (y*x)=x.
227 [para_into,219.1.1.2,10.1.1] x+ (y* (x+z))=x+ (y*z).
229 [para_from,225.1.1,29.1.1.2.1,demod,226] (x*y)+ (y*z)=y* ((x*y)+z).
231 [para_from,225.1.1,31.1.1.1.1,demod,226] (x*y)+ (z*x)=x* (y+ (z*x)).
234,233 [para_into,229.1.1.1,191.1.1,demod,192] x+ ((x+y)*z)= (x+y)* (x+z).
237 [para_into,231.1.1,229.1.1,demod,133,197] x*y=y*x.
247,246 [para_from,237.1.1,227.1.1.2,demod,234,flip.1] x+ (y*z)= (x+z)* (x+y).
250 [back_demod,216,demod,247] (A+C)* (A+B)!= (A+B)* (A+C).
251 [binary,250.1,237.1] $F.
-------------- statistics -------------
clauses given 89
clauses generated 2420
(hot clauses generated) 63
hyper_res generated 0
para_from generated 1291
para_into generated 1129
demod & eval rewrites 3206
clauses wt,lit,sk delete 1334
tautologies deleted 0
clauses forward subsumed 1049
cl not subsumed due to ancestor_subsume 3
(subsumed by sos) 27
unit deletions 2
factor simplifications 0
clauses kept 129
(hot clauses kept) 11
new demodulators 113
empty clauses 1
clauses back demodulated 70
clauses back subsumed 3
usable size 38
sos size 18
demodulators size 47
passive size 0
hot size 4
Kbytes malloced 798
----------- times (seconds) -----------
user CPU time 3.79 (0 hr, 0 min, 3 sec)
system CPU time 0.78 (0 hr, 0 min, 0 sec)
wall-clock time 7 (0 hr, 0 min, 7 sec)
input time 0.23
clausify time 0.00
process input 0.02
hyper_res time 0.02
para_into time 0.10
para_from time 0.19
pre_process time 2.89
renumber time 0.05
demod time 0.50
order equalities 0.05
unit deleletion 0.00
factor simplify 0.00
weigh cl time 0.75
hints keep time 0.00
sort lits time 0.00
forward subsume 1.01
delete cl time 0.09
keep cl time 0.04
hints time 0.00
print_cl time 0.00
conflict time 0.32
new demod time 0.02
post_process time 0.07
back demod time 0.06
back subsume 0.01
factor time 0.00
hot list time 0.07
unindex time 0.05
The job finished Mon Jan 8 10:29:46 1996
<\pre>