The theorem is that the 10 input equations are a basis for Boolean algebra. By previous results, we know that it is sufficient to derive either of the absorption laws. This theorem leads to an independent self-dual 2-basis for Boolean algebra.
The original proof was 816 steps. The proof presented here (obtained on October 3, 1995) has length 99.
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.
------------> process usable: ** KEPT (pick-wt=3): 7 [] x=x. Following clause subsumed by 7 during input processing: 0 [copy,7,flip.1] x=x. ------------> process sos: ** KEPT (pick-wt=13): 9 [copy,8,flip.1] (x*y)+ (x*z)=x* (y+z). ---> New Demodulator: 10 [new_demod,9] (x*y)+ (x*z)=x* (y+z). ** KEPT (pick-wt=13): 11 [] x+ (y*z)= (x+y)* (x+z). ---> New Demodulator: 12 [new_demod,11] x+ (y*z)= (x+y)* (x+z). ** KEPT (pick-wt=6): 13 [] x+x@ =1. ---> New Demodulator: 14 [new_demod,13] x+x@ =1. ** KEPT (pick-wt=6): 15 [] x*x@ =0. ---> New Demodulator: 16 [new_demod,15] x*x@ =0. ** KEPT (pick-wt=24): 18 [copy,17,demod,12,12] ((x*y@ )+ ((x*x)+y@ ))* ((x*y@ )+ ((x*x)+x))=x. ---> New Demodulator: 19 [new_demod,18] ((x*y@ )+ ((x*x)+y@ ))* ((x*y@ )+ ((x*x)+x))=x. ** KEPT (pick-wt=18): 21 [copy,20,demod,16,12,12] (0+ ((x*y)+x@ ))* (0+ ((x*y)+y))=y. ---> New Demodulator: 22 [new_demod,21] (0+ ((x*y)+x@ ))* (0+ ((x*y)+y))=y. ** KEPT (pick-wt=24): 24 [copy,23,demod,12,12] ((x*y@ )+ ((x*y)+y@ ))* ((x*y@ )+ ((x*y)+y))=x. ---> New Demodulator: 25 [new_demod,24] ((x*y@ )+ ((x*y)+y@ ))* ((x*y@ )+ ((x*y)+y))=x. ** KEPT (pick-wt=15): 26 [] (x+y@ )* ((x+x)* (y@ +x))=x. ---> New Demodulator: 27 [new_demod,26] (x+y@ )* ((x+x)* (y@ +x))=x. ** KEPT (pick-wt=12): 29 [copy,28,demod,14] 1* ((x+y)* (x@ +y))=y. ---> New Demodulator: 30 [new_demod,29] 1* ((x+y)* (x@ +y))=y. ** KEPT (pick-wt=15): 31 [] (x+y@ )* ((x+y)* (y@ +y))=x. ---> New Demodulator: 32 [new_demod,31] (x+y@ )* ((x+y)* (y@ +y))=x. >>>> Starting back demodulation with 10. >>>> Starting back demodulation with 12. >> back demodulating 9 with 12. >>>> Starting back demodulation with 14. >>>> Starting back demodulation with 16. >>>> Starting back demodulation with 19. >>>> Starting back demodulation with 22. >>>> Starting back demodulation with 25. >>>> Starting back demodulation with 27. >>>> Starting back demodulation with 30. >>>> Starting back demodulation with 32. >>>> Starting back demodulation with 34. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=13) 11 [] x+ (y*z)= (x+y)* (x+z). ----> UNIT CONFLICT at 6.42 sec ----> 224 [binary,222.1,2.1] $Ans(A4). Length of proof is 99. Level of proof is 44. ---------------- PROOF ---------------- 2 [] (A+B)*B!=B|$Ans(A4). 3 [] x* (y+z)= (x*y)+ (x*z). 4 [] x+ (y*z)= (x+y)* (x+z). 5 [] x+x@ =1. 6 [] x*x@ =0. 8 [] x* (y+z)= (x*y)+ (x*z). 9 [copy,8,flip.1] (x*y)+ (x*z)=x* (y+z). 12,11 [] x+ (y*z)= (x+y)* (x+z). 14,13 [] x+x@ =1. 16,15 [] x*x@ =0. 17 [] (x*y@ )+ ((x*x)+ (y@ *x))=x. 18 [copy,17,demod,12,12] ((x*y@ )+ ((x*x)+y@ ))* ((x*y@ )+ ((x*x)+x))=x. 20 [] (x*x@ )+ ((x*y)+ (x@ *y))=y. 22,21 [copy,20,demod,16,12,12] (0+ ((x*y)+x@ ))* (0+ ((x*y)+y))=y. 23 [] (x*y@ )+ ((x*y)+ (y@ *y))=x. 24 [copy,23,demod,12,12] ((x*y@ )+ ((x*y)+y@ ))* ((x*y@ )+ ((x*y)+y))=x. 26 [] (x+y@ )* ((x+x)* (y@ +x))=x. 28 [] (x+x@ )* ((x+y)* (x@ +y))=y. 29 [copy,28,demod,14] 1* ((x+y)* (x@ +y))=y. 32,31 [] (x+y@ )* ((x+y)* (y@ +y))=x. 34,33 [back_demod,9,demod,12] ((x*y)+x)* ((x*y)+z)=x* (y+z). 36,35 [para_from,33.1.1,11.1.1.2,demod,12,flip.1] (x+ ((y*z)+y))* (x+ ((y*z)+u))= (x+y)* (x+ (z+u)). 38,37 (heat=1) [para_into,35.1.1.1.2.1,6.1.1,demod,16,flip.1] (x+y)* (x+ (y@ +z))= (x+ (0+y))* (x+ (0+z)). 39 [para_into,37.1.1,33.1.1] x* (y+ (x@ +z))= ((x*y)+ (0+x))* ((x*y)+ (0+z)). 41 [para_from,37.1.1,33.1.1] ((x*y)+ (0+x))* ((x*y)+ (0+z))=x* (y+ (x@ +z)). 43,42 [para_from,15.1.1,11.1.1.2,flip.1] (x+y)* (x+y@ )=x+0. 45,44 [para_from,15.1.1,33.1.1.2.1,demod,16,flip.1] x* (x@ +y)= (0+x)* (0+y). 46 (heat=1) [para_into,42.1.1.1,4.1.1] ((x+y)* (x+z))* (x+ (y*z)@ )=x+0. 48 (heat=1) [para_into,42.1.1.2,5.1.1] (x+x)*1=x+0. 49 (heat=1) [para_from,42.1.1,4.1.1.2,flip.1] (x+ (y+z))* (x+ (y+z@ ))=x+ (y+0). 52,51 (heat=2) [para_into,46.1.1.2,5.1.1,demod,34,flip.1] (x*y)+0= (x* (y+y))*1. 53 [copy,48,flip.1] x+0= (x+x)*1. 54 [para_into,42.1.1,33.1.1,demod,52] x* (y+x@ )= (x* (y+y))*1. 55 [copy,54,flip.1] (x* (y+y))*1=x* (y+x@ ). 57,56 (heat=1) [para_into,54.1.1.2,5.1.1,flip.1] (x* (x+x))*1=x*1. 58 (heat=1) [para_into,55.1.1.1.2,4.1.1,demod,34,flip.1] x* ((y*z)+x@ )= (x* (y* (z+z)))*1. 61 [para_into,49.1.1,41.1.1] x* (y+ (x@ +x@ ))= (x*y)+ (0+0). 62 (heat=1) [para_from,61.1.1,4.1.1.2] x+ ((y*z)+ (0+0))= (x+y)* (x+ (z+ (y@ +y@ ))). 64,63 (heat=2) [para_into,62.1.1.2.1,6.1.1,demod,38,flip.1] (x+ (0+y))* (x+ (0+ (y@ +y@ )))=x+ (0+ (0+0)). 65 [para_into,18.1.1,35.1.1,demod,34] x@ * (x@ + (x@ +x@ ))=x@ . 67 (heat=1) [para_from,65.1.1,4.1.1.2,flip.1] (x+y@ )* (x+ (y@ + (y@ +y@ )))=x+y@ . 69 (heat=2) [para_into,67.1.1.1,5.1.1,demod,14] 1* (x+ (x@ + (x@ +x@ )))=1. 72,71 [para_into,69.1.1,39.1.1,demod,64] (1*1)+ (0+ (0+0))=1. 73 [para_into,21.1.1.1.2.1,15.1.1,demod,16] (0+ (0+x@ ))* (0+ (0+x@ ))=x@ . 75 (heat=1) [para_into,73.1.1.1.2,5.1.1,demod,14,flip.1] 0@ = (0+1)* (0+1). 77 (heat=2) [para_from,75.1.1,6.1.1.2] 0* ((0+1)* (0+1))=0. 79 (heat=3) [para_from,77.1.1,4.1.1.2,demod,12,flip.1] (x+0)* ((x+ (0+1))* (x+ (0+1)))=x+0. 81 [para_from,21.1.1,11.1.1.2,flip.1] (x+ (0+ ((y*z)+y@ )))* (x+ (0+ ((y*z)+z)))=x+z. 84,83 [para_into,71.1.1.2.2,53.1.1,demod,12,12,72] 1* ((1*1)+ (0+1))=1. 85 (heat=1) [para_from,83.1.1,4.1.1.2,flip.1] (x+1)* (x+ ((1*1)+ (0+1)))=x+1. 87 [para_from,83.1.1,21.1.1.2.2.1,demod,84,14] (0+1)* (0+ (1+ ((1*1)+ (0+1))))= (1*1)+ (0+1). 89 [para_into,85.1.1,33.1.1] 1* (x+ ((1*1)+ (0+1)))= (1*x)+1. 90 (heat=1) [para_from,89.1.1,4.1.1.2] x+ ((1*y)+1)= (x+1)* (x+ (y+ ((1*1)+ (0+1)))). 91 [copy,90,flip.1] (x+1)* (x+ (y+ ((1*1)+ (0+1))))=x+ ((1*y)+1). 93,92 [para_into,91.1.1,87.1.1] (1*1)+ (0+1)=0+ ((1*1)+1). 94 [para_into,24.1.1,35.1.1,demod,34] x@ * (x@ + (x+x))=x@ . 96 (heat=1) [para_from,94.1.1,4.1.1.2,flip.1] (x+y@ )* (x+ (y@ + (y+y)))=x+y@ . 98 (heat=2) [para_into,96.1.1.1,5.1.1,demod,14] 1* (x+ (x@ + (x+x)))=1. 101,100 [para_from,92.1.1,79.1.1.2.2,demod,52,57,93,36,52,57] (1*1)* ((0+1)* (0+ (1+1)))=1*1. 103,102 [para_into,98.1.1,39.1.1,demod,93] (0+ ((1*1)+1))* ((1*1)+ (0+ (1+1)))=1. 104 [para_from,100.1.1,81.1.1.2.2.2.1,demod,101,14,12,93,103,12,flip.1] (x+ (0+1))* (x+ (0+ (1+1)))= (x+ (0+1))* (x+ (0+1)). 107,106 [para_from,100.1.1,21.1.1.2.2.1,demod,101,14,12,93,103,flip.1] (0+1)* (0+ (1+1))= (0+1)* (0+1). 109,108 [para_into,104.1.1.1,92.1.1,demod,103,93,93,36,107,flip.1] (0+1)* (0+1)=1. 110 [back_demod,106,demod,109] (0+1)* (0+ (1+1))=1. 113,112 [back_demod,77,demod,109] 0*1=0. 115,114 [back_demod,75,demod,109] 0@ =1. 116 (heat=1) [para_from,112.1.1,4.1.1.2,flip.1] (x+0)* (x+1)=x+0. 119,118 (heat=1) [para_from,114.1.1,5.1.1.2] 0+1=1. 120 [back_demod,110,demod,119] 1* (0+ (1+1))=1. 123,122 [back_demod,108,demod,119,119] 1*1=1. 125,124 [back_demod,92,demod,123,119,123,flip.1] 0+ (1+1)=1+1. 127,126 (heat=1) [para_from,120.1.1,4.1.1.2,demod,125,flip.1] (x+1)* (x+ (1+1))=x+1. 129,128 [back_demod,102,demod,123,125,123,125,127] 1+1=1. 130 [back_demod,71,demod,123] 1+ (0+ (0+0))=1. 133,132 [para_from,112.1.1,58.1.1.2.1,demod,129,113] x* (0+x@ )= (x*0)*1. 135,134 [para_from,112.1.1,51.1.1.1,demod,129,113,113] 0+0=0. 137,136 [back_demod,130,demod,135,135] 1+0=1. 138 [para_into,26.1.1.2.1,11.1.1,demod,34,12] ((x*y)+z@ )* ((x* (y+y))* ((z@ +x)* (z@ +y)))=x*y. 140 (heat=1) [para_into,138.1.1.1,5.1.1] 1* ((x* (y+y))* (((x*y)@ +x)* ((x*y)@ +y)))=x*y. 143,142 (heat=2) [para_into,140.1.1.2.2.1.1.1,6.1.1,demod,45,43,135,115,16,115,43,137,113,16] 1*0=0. 148 [para_into,29.1.1.2.1,13.1.1] 1* (1* (x@ +x@ ))=x@ . 151,150 [para_into,148.1.1.2,54.1.1,demod,45,119,133,143,113,113,143,flip.1] 1@ =0. 153,152 [para_into,31.1.1.1.2,150.1.1,demod,151,119] (x+0)* ((x+1)*1)=x. 155,154 [para_from,31.1.1,11.1.1.2,demod,12,flip.1] (x+ (y+z@ ))* ((x+ (y+z))* (x+ (z@ +z)))=x+y. 156 [para_from,31.1.1,140.1.1.2.2.2.1.1,demod,12,34,32,12,155,32] 1* (((x+y@ )* ((x+y)* ((y@ +y)+ (y@ +y))))* (x@ +x))=x. 158 [para_from,152.1.1,58.1.1.2.1,demod,12,34,129,153] x* (y+x@ )= (x*y)*1. 161,160 [para_from,152.1.1,51.1.1.1,demod,12,34,129,153] x+0=x*1. 163,162 (heat=1) [para_into,158.1.1.2,5.1.1,flip.1] (x*x)*1=x*1. 165,164 [back_demod,152,demod,161] (x*1)* ((x+1)*1)=x. 167,166 [back_demod,116,demod,161,161] (x*1)* (x+1)=x*1. 169,168 [back_demod,53,demod,161,flip.1] (x+x)*1=x*1. 171,170 [back_demod,42,demod,161] (x+y)* (x+y@ )=x*1. 172 [para_from,160.1.1,44.1.1.2,demod,161,113] x* (x@ *1)= (0+x)*0. 174 [para_from,166.1.1,33.1.1.2.1,demod,167,12,34,129,flip.1] (x*1)* ((x+1)+y)= (x*1)* ((x*1)+y). 177,176 [para_into,174.1.1.2,160.1.1,demod,165,161,flip.1] (x*1)* ((x*1)*1)=x. 179,178 [para_into,176.1.1.1,168.1.1,demod,169,177,flip.1] x+x=x. 181,180 [para_into,176.1.1.1,162.1.1,demod,163,177,flip.1] x*x=x. 183,182 [back_demod,156,demod,179,32,45,181] 1* (0+x)=x. 185,184 [back_demod,94,demod,179] x@ * (x@ +x)=x@ . 189,188 [para_into,180.1.1,33.1.1,flip.1] (x*y)+x=x* (y+x). 190 [para_from,184.1.1,21.1.1.2.2.1,demod,185,14,119,183] x@ + (x@ +x)=x@ +x. 193,192 [para_from,190.1.1,39.1.1.2,demod,45,181,16,16,181,flip.1] 0+ (0+x)=0+x. 195,194 [para_from,192.1.1,81.1.1.2,demod,193,22,flip.1] 0+x=x. 196 [para_from,192.1.1,81.1.1.1,demod,195,195,195,195] ((x*y)+x@ )* ((x*y)+y)=y. 199,198 [para_from,192.1.1,182.1.1.2,demod,195,195] 1*x=x. 202 [para_from,192.1.1,154.1.1.2.1.2,demod,195,195,195,195,195,38,195,195,181,161] (x+y@ )* (x+y)=x*1. 204 [back_demod,172,demod,195] x* (x@ *1)=x*0. 207,206 (heat=1) [para_into,202.1.1.1,5.1.1,demod,179,199,flip.1] x*1=x. 208 (heat=1) [para_from,204.1.1,4.1.1.2,demod,12,161,207,207,171,207] (x+y)*x=x. 210 (heat=2) [para_into,208.1.1.1,4.1.1] ((x+y)* (x+z))*x=x. 212 [para_into,196.1.1.1.1,206.1.1,demod,14,207,199] x+1=1. 215,214 (heat=1) [para_from,212.1.1,3.1.1.2,demod,207,207,189,flip.1] x* (y+x)=x. 220 [para_into,210.1.1.1,196.1.1] x* (y*x)=y*x. 222 [para_into,220.1.1.2,214.1.1,demod,215] (x+y)*y=y. 224 [binary,222.1,2.1] $Ans(A4). ----> UNIT CONFLICT at 6.59 sec ----> 227 [binary,225.1,1.1] $Ans(A2). Length of proof is 100. Level of proof is 44. ---------------- PROOF ---------------- 1 [] (A*B)+B!=B|$Ans(A2). 3 [] x* (y+z)= (x*y)+ (x*z). 4 [] x+ (y*z)= (x+y)* (x+z). 5 [] x+x@ =1. 6 [] x*x@ =0. 8 [] x* (y+z)= (x*y)+ (x*z). 9 [copy,8,flip.1] (x*y)+ (x*z)=x* (y+z). 12,11 [] x+ (y*z)= (x+y)* (x+z). 14,13 [] x+x@ =1. 16,15 [] x*x@ =0. 17 [] (x*y@ )+ ((x*x)+ (y@ *x))=x. 18 [copy,17,demod,12,12] ((x*y@ )+ ((x*x)+y@ ))* ((x*y@ )+ ((x*x)+x))=x. 20 [] (x*x@ )+ ((x*y)+ (x@ *y))=y. 22,21 [copy,20,demod,16,12,12] (0+ ((x*y)+x@ ))* (0+ ((x*y)+y))=y. 23 [] (x*y@ )+ ((x*y)+ (y@ *y))=x. 24 [copy,23,demod,12,12] ((x*y@ )+ ((x*y)+y@ ))* ((x*y@ )+ ((x*y)+y))=x. 26 [] (x+y@ )* ((x+x)* (y@ +x))=x. 28 [] (x+x@ )* ((x+y)* (x@ +y))=y. 29 [copy,28,demod,14] 1* ((x+y)* (x@ +y))=y. 32,31 [] (x+y@ )* ((x+y)* (y@ +y))=x. 34,33 [back_demod,9,demod,12] ((x*y)+x)* ((x*y)+z)=x* (y+z). 36,35 [para_from,33.1.1,11.1.1.2,demod,12,flip.1] (x+ ((y*z)+y))* (x+ ((y*z)+u))= (x+y)* (x+ (z+u)). 38,37 (heat=1) [para_into,35.1.1.1.2.1,6.1.1,demod,16,flip.1] (x+y)* (x+ (y@ +z))= (x+ (0+y))* (x+ (0+z)). 39 [para_into,37.1.1,33.1.1] x* (y+ (x@ +z))= ((x*y)+ (0+x))* ((x*y)+ (0+z)). 41 [para_from,37.1.1,33.1.1] ((x*y)+ (0+x))* ((x*y)+ (0+z))=x* (y+ (x@ +z)). 43,42 [para_from,15.1.1,11.1.1.2,flip.1] (x+y)* (x+y@ )=x+0. 45,44 [para_from,15.1.1,33.1.1.2.1,demod,16,flip.1] x* (x@ +y)= (0+x)* (0+y). 46 (heat=1) [para_into,42.1.1.1,4.1.1] ((x+y)* (x+z))* (x+ (y*z)@ )=x+0. 48 (heat=1) [para_into,42.1.1.2,5.1.1] (x+x)*1=x+0. 49 (heat=1) [para_from,42.1.1,4.1.1.2,flip.1] (x+ (y+z))* (x+ (y+z@ ))=x+ (y+0). 52,51 (heat=2) [para_into,46.1.1.2,5.1.1,demod,34,flip.1] (x*y)+0= (x* (y+y))*1. 53 [copy,48,flip.1] x+0= (x+x)*1. 54 [para_into,42.1.1,33.1.1,demod,52] x* (y+x@ )= (x* (y+y))*1. 55 [copy,54,flip.1] (x* (y+y))*1=x* (y+x@ ). 57,56 (heat=1) [para_into,54.1.1.2,5.1.1,flip.1] (x* (x+x))*1=x*1. 58 (heat=1) [para_into,55.1.1.1.2,4.1.1,demod,34,flip.1] x* ((y*z)+x@ )= (x* (y* (z+z)))*1. 61 [para_into,49.1.1,41.1.1] x* (y+ (x@ +x@ ))= (x*y)+ (0+0). 62 (heat=1) [para_from,61.1.1,4.1.1.2] x+ ((y*z)+ (0+0))= (x+y)* (x+ (z+ (y@ +y@ ))). 64,63 (heat=2) [para_into,62.1.1.2.1,6.1.1,demod,38,flip.1] (x+ (0+y))* (x+ (0+ (y@ +y@ )))=x+ (0+ (0+0)). 65 [para_into,18.1.1,35.1.1,demod,34] x@ * (x@ + (x@ +x@ ))=x@ . 67 (heat=1) [para_from,65.1.1,4.1.1.2,flip.1] (x+y@ )* (x+ (y@ + (y@ +y@ )))=x+y@ . 69 (heat=2) [para_into,67.1.1.1,5.1.1,demod,14] 1* (x+ (x@ + (x@ +x@ )))=1. 72,71 [para_into,69.1.1,39.1.1,demod,64] (1*1)+ (0+ (0+0))=1. 73 [para_into,21.1.1.1.2.1,15.1.1,demod,16] (0+ (0+x@ ))* (0+ (0+x@ ))=x@ . 75 (heat=1) [para_into,73.1.1.1.2,5.1.1,demod,14,flip.1] 0@ = (0+1)* (0+1). 77 (heat=2) [para_from,75.1.1,6.1.1.2] 0* ((0+1)* (0+1))=0. 79 (heat=3) [para_from,77.1.1,4.1.1.2,demod,12,flip.1] (x+0)* ((x+ (0+1))* (x+ (0+1)))=x+0. 81 [para_from,21.1.1,11.1.1.2,flip.1] (x+ (0+ ((y*z)+y@ )))* (x+ (0+ ((y*z)+z)))=x+z. 84,83 [para_into,71.1.1.2.2,53.1.1,demod,12,12,72] 1* ((1*1)+ (0+1))=1. 85 (heat=1) [para_from,83.1.1,4.1.1.2,flip.1] (x+1)* (x+ ((1*1)+ (0+1)))=x+1. 87 [para_from,83.1.1,21.1.1.2.2.1,demod,84,14] (0+1)* (0+ (1+ ((1*1)+ (0+1))))= (1*1)+ (0+1). 89 [para_into,85.1.1,33.1.1] 1* (x+ ((1*1)+ (0+1)))= (1*x)+1. 90 (heat=1) [para_from,89.1.1,4.1.1.2] x+ ((1*y)+1)= (x+1)* (x+ (y+ ((1*1)+ (0+1)))). 91 [copy,90,flip.1] (x+1)* (x+ (y+ ((1*1)+ (0+1))))=x+ ((1*y)+1). 93,92 [para_into,91.1.1,87.1.1] (1*1)+ (0+1)=0+ ((1*1)+1). 94 [para_into,24.1.1,35.1.1,demod,34] x@ * (x@ + (x+x))=x@ . 96 (heat=1) [para_from,94.1.1,4.1.1.2,flip.1] (x+y@ )* (x+ (y@ + (y+y)))=x+y@ . 98 (heat=2) [para_into,96.1.1.1,5.1.1,demod,14] 1* (x+ (x@ + (x+x)))=1. 101,100 [para_from,92.1.1,79.1.1.2.2,demod,52,57,93,36,52,57] (1*1)* ((0+1)* (0+ (1+1)))=1*1. 103,102 [para_into,98.1.1,39.1.1,demod,93] (0+ ((1*1)+1))* ((1*1)+ (0+ (1+1)))=1. 104 [para_from,100.1.1,81.1.1.2.2.2.1,demod,101,14,12,93,103,12,flip.1] (x+ (0+1))* (x+ (0+ (1+1)))= (x+ (0+1))* (x+ (0+1)). 107,106 [para_from,100.1.1,21.1.1.2.2.1,demod,101,14,12,93,103,flip.1] (0+1)* (0+ (1+1))= (0+1)* (0+1). 109,108 [para_into,104.1.1.1,92.1.1,demod,103,93,93,36,107,flip.1] (0+1)* (0+1)=1. 110 [back_demod,106,demod,109] (0+1)* (0+ (1+1))=1. 113,112 [back_demod,77,demod,109] 0*1=0. 115,114 [back_demod,75,demod,109] 0@ =1. 116 (heat=1) [para_from,112.1.1,4.1.1.2,flip.1] (x+0)* (x+1)=x+0. 119,118 (heat=1) [para_from,114.1.1,5.1.1.2] 0+1=1. 120 [back_demod,110,demod,119] 1* (0+ (1+1))=1. 123,122 [back_demod,108,demod,119,119] 1*1=1. 125,124 [back_demod,92,demod,123,119,123,flip.1] 0+ (1+1)=1+1. 127,126 (heat=1) [para_from,120.1.1,4.1.1.2,demod,125,flip.1] (x+1)* (x+ (1+1))=x+1. 129,128 [back_demod,102,demod,123,125,123,125,127] 1+1=1. 130 [back_demod,71,demod,123] 1+ (0+ (0+0))=1. 133,132 [para_from,112.1.1,58.1.1.2.1,demod,129,113] x* (0+x@ )= (x*0)*1. 135,134 [para_from,112.1.1,51.1.1.1,demod,129,113,113] 0+0=0. 137,136 [back_demod,130,demod,135,135] 1+0=1. 138 [para_into,26.1.1.2.1,11.1.1,demod,34,12] ((x*y)+z@ )* ((x* (y+y))* ((z@ +x)* (z@ +y)))=x*y. 140 (heat=1) [para_into,138.1.1.1,5.1.1] 1* ((x* (y+y))* (((x*y)@ +x)* ((x*y)@ +y)))=x*y. 143,142 (heat=2) [para_into,140.1.1.2.2.1.1.1,6.1.1,demod,45,43,135,115,16,115,43,137,113,16] 1*0=0. 148 [para_into,29.1.1.2.1,13.1.1] 1* (1* (x@ +x@ ))=x@ . 151,150 [para_into,148.1.1.2,54.1.1,demod,45,119,133,143,113,113,143,flip.1] 1@ =0. 153,152 [para_into,31.1.1.1.2,150.1.1,demod,151,119] (x+0)* ((x+1)*1)=x. 155,154 [para_from,31.1.1,11.1.1.2,demod,12,flip.1] (x+ (y+z@ ))* ((x+ (y+z))* (x+ (z@ +z)))=x+y. 156 [para_from,31.1.1,140.1.1.2.2.2.1.1,demod,12,34,32,12,155,32] 1* (((x+y@ )* ((x+y)* ((y@ +y)+ (y@ +y))))* (x@ +x))=x. 158 [para_from,152.1.1,58.1.1.2.1,demod,12,34,129,153] x* (y+x@ )= (x*y)*1. 161,160 [para_from,152.1.1,51.1.1.1,demod,12,34,129,153] x+0=x*1. 163,162 (heat=1) [para_into,158.1.1.2,5.1.1,flip.1] (x*x)*1=x*1. 165,164 [back_demod,152,demod,161] (x*1)* ((x+1)*1)=x. 167,166 [back_demod,116,demod,161,161] (x*1)* (x+1)=x*1. 169,168 [back_demod,53,demod,161,flip.1] (x+x)*1=x*1. 171,170 [back_demod,42,demod,161] (x+y)* (x+y@ )=x*1. 172 [para_from,160.1.1,44.1.1.2,demod,161,113] x* (x@ *1)= (0+x)*0. 174 [para_from,166.1.1,33.1.1.2.1,demod,167,12,34,129,flip.1] (x*1)* ((x+1)+y)= (x*1)* ((x*1)+y). 177,176 [para_into,174.1.1.2,160.1.1,demod,165,161,flip.1] (x*1)* ((x*1)*1)=x. 179,178 [para_into,176.1.1.1,168.1.1,demod,169,177,flip.1] x+x=x. 181,180 [para_into,176.1.1.1,162.1.1,demod,163,177,flip.1] x*x=x. 183,182 [back_demod,156,demod,179,32,45,181] 1* (0+x)=x. 185,184 [back_demod,94,demod,179] x@ * (x@ +x)=x@ . 189,188 [para_into,180.1.1,33.1.1,flip.1] (x*y)+x=x* (y+x). 190 [para_from,184.1.1,21.1.1.2.2.1,demod,185,14,119,183] x@ + (x@ +x)=x@ +x. 193,192 [para_from,190.1.1,39.1.1.2,demod,45,181,16,16,181,flip.1] 0+ (0+x)=0+x. 195,194 [para_from,192.1.1,81.1.1.2,demod,193,22,flip.1] 0+x=x. 196 [para_from,192.1.1,81.1.1.1,demod,195,195,195,195] ((x*y)+x@ )* ((x*y)+y)=y. 199,198 [para_from,192.1.1,182.1.1.2,demod,195,195] 1*x=x. 202 [para_from,192.1.1,154.1.1.2.1.2,demod,195,195,195,195,195,38,195,195,181,161] (x+y@ )* (x+y)=x*1. 204 [back_demod,172,demod,195] x* (x@ *1)=x*0. 207,206 (heat=1) [para_into,202.1.1.1,5.1.1,demod,179,199,flip.1] x*1=x. 208 (heat=1) [para_from,204.1.1,4.1.1.2,demod,12,161,207,207,171,207] (x+y)*x=x. 210 (heat=2) [para_into,208.1.1.1,4.1.1] ((x+y)* (x+z))*x=x. 212 [para_into,196.1.1.1.1,206.1.1,demod,14,207,199] x+1=1. 215,214 (heat=1) [para_from,212.1.1,3.1.1.2,demod,207,207,189,flip.1] x* (y+x)=x. 216 [back_demod,188,demod,215] (x*y)+x=x. 220 [para_into,210.1.1.1,196.1.1] x* (y*x)=y*x. 225 [para_from,220.1.1,216.1.1.1] (x*y)+y=y. 227 [binary,225.1,1.1] $Ans(A2). -------------- statistics ------------- clauses given 98 clauses generated 2929 (hot clauses generated) 388 para_from generated 1697 para_into generated 1232 demod & eval rewrites 5968 clauses wt,lit,sk delete 2523 tautologies deleted 0 clauses forward subsumed 403 cl not subsumed due to ancestor_subsume 2 (subsumed by sos) 17 unit deletions 0 factor simplifications 0 clauses kept 114 (hot clauses kept) 29 new demodulators 100 empty clauses 2 clauses back demodulated 86 clauses back subsumed 2 usable size 24 sos size 2 demodulators size 25 passive size 2 hot size 4 Kbytes malloced 351 ----------- times (seconds) ----------- user CPU time 6.66 (0 hr, 0 min, 6 sec) system CPU time 0.80 (0 hr, 0 min, 0 sec) wall-clock time 58 (0 hr, 0 min, 58 sec) input time 0.35 clausify time 0.00 process input 0.03 para_into time 0.42 para_from time 0.55 pre_process time 4.83 renumber time 0.19 demod time 1.13 order equalities 0.44 unit deleletion 0.00 factor simplify 0.00 weigh cl time 1.62 hints keep time 0.00 sort lits time 0.00 forward subsume 0.73 delete cl time 0.22 keep cl time 0.13 hints time 0.00 print_cl time 0.00 conflict time 0.11 new demod time 0.06 post_process time 0.11 back demod time 0.09 back subsume 0.02 factor time 0.00 hot list time 0.75 unindex time 0.05 The job finished Tue Oct 3 15:21:54 1995