----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 21:56:45 1995 ----> UNIT CONFLICT at 24.59 sec ----> 4972 [binary,4971.1,134.1] -> . Length of proof is 103. Level of proof is 24. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] (A*B)+ (A*C)=A* (B+C), (A*B)+B=B -> . 3 [] -> (x*y)+ ((y*z)+ (z*x))= (x+y)* ((y+z)* (z+x)). 5 [] -> x+ (y* (x*z))=x. 7 [] -> ((x*y)+ (y*z))+y=y. 9 [] -> (x+x@ )*y=y. 11 [] -> x* (y+ (x+z))=x. 15 [] -> (x*x@ )+y=y. 18,17 [] -> x+x@ =1. 20,19 [] -> x*x@ =0. 22,21 [] -> (x+y)+z=x+ (y+z). 24,23 [] -> (x*y)*z=x* (y*z). 26,25 [back_demod,9,demod,18] -> 1*x=x. 28,27 [back_demod,15,demod,20] -> 0+x=x. 29 [back_demod,7,demod,22] -> (x*y)+ ((y*z)+y)=y. 35 [para_from,25.1.1,3.1.1.2.1] -> (x*1)+ (y+ (y*x))= (x+1)* ((1+y)* (y+x)). 39 [para_into,17.1.1,27.1.1] -> 0@ =1. 41 [para_into,5.1.1.2.2,25.1.1] -> 1+ (x*y)=1. 44,43 [para_into,5.1.1.2,25.1.1] -> x+ (x*y)=x. 45 [para_into,5.1.1,27.1.1] -> x* (0*y)=0. 47 [back_demod,35,demod,44] -> (x*1)+y= (x+1)* ((1+y)* (y+x)). 49 [para_into,19.1.1.2,39.1.1] -> 0*1=0. 51 [para_into,19.1.1,25.1.1] -> 1@ =0. 57 [para_from,19.1.1,3.1.1.2.1,demod,28,18,26] -> (x*y)+ (y@ *x)= (x+y)* (y@ +x). 58 [para_from,19.1.1,3.1.1.1,demod,28,18,26] -> (x@ *y)+ (y*x)= (x@ +y)* (y+x). 60 [copy,57,flip.1] -> (x+y)* (y@ +x)= (x*y)+ (y@ *x). 61 [para_from,51.1.1,17.1.1.2] -> 1+0=1. 67 [para_from,49.1.1,3.1.1.1,demod,26,44,28,28,26,flip.1] -> (1+x)* (x+0)=x. 70,69 [para_into,11.1.1.2.2,61.1.1,demod,26] -> x+1=1. 74,73 [para_into,11.1.1.2.2,17.1.1,demod,70] -> x*1=x. 75 [para_into,11.1.1.2.2,5.1.1] -> x* (y+x)=x. 80,79 [para_into,11.1.1.2,27.1.1] -> x* (x+y)=x. 86 [back_demod,47,demod,74,70,26] -> x+y= (1+y)* (y+x). 93 [para_from,11.1.1,5.1.1.2.2] -> x+ (y*x)=x. 96,95 [para_into,41.1.1.2,73.1.1] -> 1+x=1. 99 [back_demod,86,demod,96,26] -> x+y=y+x. 101,100 [back_demod,67,demod,96,26] -> x+0=x. 106 [para_into,21.1.1.1,5.1.1,flip.1] -> x+ ((y* (x*z))+u)=x+u. 117,116 [para_into,43.1.1.2,73.1.1] -> x+x=x. 119,118 [para_into,43.1.1,27.1.1] -> 0*x=0. 123,122 [back_demod,45,demod,119] -> x*0=0. 125,124 [para_from,43.1.1,21.1.1.1,flip.1] -> x+ ((x*y)+z)=x+z. 134 [para_from,118.1.1,3.1.1.2.1,demod,123,28,28,101,28,80] -> x*y=y*x. 137 [para_into,23.1.1.1,19.1.1,demod,119,flip.1] -> x* (x@ *y)=0. 152,151 [para_into,75.1.1.2,116.1.1] -> x*x=x. 160,159 [para_from,75.1.1,23.1.1.1,flip.1] -> x* ((y+x)*z)=x*z. 161 [para_from,151.1.1,3.1.1.2.2,demod,117] -> (x*y)+ ((y*x)+x)= (x+y)* ((y+x)*x). 164,163 [para_from,151.1.1,3.1.1.2.1,demod,44,117,80] -> (x*y)+y= (x+y)*y. 165 [para_from,151.1.1,23.1.1.1,flip.1] -> x* (x*y)=x*y. 169 [back_demod,161,demod,164] -> (x*y)+ ((y+x)*x)= (x+y)* ((y+x)*x). 171 [back_demod,2,demod,164] (A*B)+ (A*C)=A* (B+C), (A+B)*B=B -> . 174 [para_into,79.1.1.2,3.1.1,demod,24,160] -> x* (y* ((y+z)* (z+x)))=x*y. 181,180 [para_from,79.1.1,23.1.1.1,flip.1] -> x* ((x+y)*z)=x*z. 183,182 [back_demod,174,demod,181] -> x* (y* (z+x))=x*y. 185,184 [para_into,29.1.1.1,118.1.1,demod,28] -> (x*y)+x=x. 187,186 [para_into,29.1.1.1,75.1.1,demod,185] -> x+ (y+x)=y+x. 193,192 [para_into,29.1.1.2.1,151.1.1,demod,117,164] -> (x+y)*y=y. 196 [back_demod,171,demod,193,unit_del,1] (A*B)+ (A*C)=A* (B+C) -> . 197 [back_demod,169,demod,193,185,193,flip.1] -> (x+y)*x=x. 200,199 [back_demod,163,demod,193] -> (x*y)+y=y. 204 [para_into,93.1.1,21.1.1] -> x+ (y+ (z* (x+y)))=x+y. 206 [para_from,93.1.1,21.1.1.1,flip.1] -> x+ ((y*x)+z)=x+z. 208 [para_into,99.1.1,21.1.1] -> x+ (y+z)=z+ (x+y). 210,209 [para_into,99.1.1,17.1.1,flip.1] -> x@ +x=1. 211 [para_into,99.1.1,5.1.1,flip.1] -> (x* (y*z))+y=y. 214 [copy,208,flip.1] -> x+ (y+z)=y+ (z+x). 221 [para_into,134.1.1,23.1.1] -> x* (y*z)=z* (x*y). 224 [para_into,134.1.1,11.1.1,flip.1] -> (x+ (y+z))*y=y. 227 [para_from,134.1.1,3.1.1.2.2] -> (x*y)+ ((y*z)+ (x*z))= (x+y)* ((y+z)* (z+x)). 239 [para_into,57.1.1.1,19.1.1,demod,28,18,26,flip.1] -> x@ @ +x=x@ @ *x. 243 [para_into,57.1.1.2,134.1.1] -> (x*y)+ (x*y@ )= (x+y)* (y@ +x). 246 [para_into,57.1.1.2,75.1.1,demod,22,210,70,187,26] -> ((x+y@ )*y)+y@ =x+y@ . 249 [copy,243,flip.1] -> (x+y)* (y@ +x)= (x*y)+ (x*y@ ). 281,280 [para_from,192.1.1,3.1.1.1,demod,125,22,117,183] -> x+ (y* (z+x))= (z+x)* (x+y). 287,286 [back_demod,204,demod,281] -> x+ ((x+y)* (y+z))=x+y. 322 [para_into,58.1.1,99.1.1] -> (x*y)+ (y@ *x)= (y@ +x)* (x+y). 338 [para_into,137.1.1.2,134.1.1] -> x* (y*x@ )=0. 340 [para_into,137.1.1,134.1.1,demod,24] -> x@ * (y*x)=0. 376,375 [para_into,60.1.1.2,99.1.1,flip.1] -> (x*y)+ (y@ *x)= (x+y)* (x+y@ ). 386 [back_demod,322,demod,376] -> (x+y)* (x+y@ )= (y@ +x)* (x+y). 388 [back_demod,57,demod,376] -> (x+y)* (x+y@ )= (x+y)* (y@ +x). 491 [para_from,340.1.1,58.1.1.1,demod,24,152,28,200,flip.1] -> (x@ + (y*x))*x=y*x. 734 [para_from,165.1.1,3.1.1.1,demod,24,44,183] -> (x*y)+ ((x* (y*z))+ (z*x))=x* ((x*y)+z). 812,811 [para_into,224.1.1.1.2,211.1.1] -> (x+y)* (z* (y*u))=z* (y*u). 824,823 [para_into,224.1.1.1,106.1.1] -> (x+y)* (z* (x*u))=z* (x*u). 828,827 [para_into,224.1.1.1,3.1.1,demod,24,24,824,812] -> (x+y)* (z*x)=z*x. 1108,1107 [para_into,124.1.1.2.1,23.1.1] -> (x*y)+ ((x* (y*z))+u)= (x*y)+u. 1124,1123 [para_into,124.1.1.2,58.1.1,demod,287,flip.1] -> x@ + (y*x)=x@ +y. 1130,1129 [back_demod,734,demod,1108] -> (x*y)+ (z*x)=x* ((x*y)+z). 1133 [back_demod,491,demod,1124] -> (x@ +y)*x=y*x. 1139 [back_demod,375,demod,1130] -> x* ((x*y)+y@ )= (x+y)* (x+y@ ). 1796,1795 [para_into,1133.1.1.1,99.1.1] -> (x+y@ )*y=x*y. 1798,1797 [para_into,1133.1.1.1,17.1.1,demod,26,flip.1] -> x@ @ *x=x. 1806,1805 [back_demod,246,demod,1796] -> (x*y)+y@ =x+y@ . 1808,1807 [back_demod,239,demod,1798] -> x@ @ +x=x. 1810,1809 [back_demod,1139,demod,1806,80,flip.1] -> (x+y)* (x+y@ )=x. 1812,1811 [back_demod,388,demod,1810,flip.1] -> (x+y)* (y@ +x)=x. 1813 [back_demod,386,demod,1810,flip.1] -> (x@ +y)* (y+x)=y. 1819 [back_demod,249,demod,1812,flip.1] -> (x*y)+ (x*y@ )=x. 1973 [para_from,1797.1.1,43.1.1.2,demod,1808,flip.1] -> x@ @ =x. 1976,1975 [para_from,1973.1.1,1133.1.1.1.1] -> (x+y)*x@ =y*x@ . 2749 [para_into,1813.1.1.2,99.1.1] -> (x@ +y)* (x+y)=y. 2879,2878 [para_into,1819.1.1.1,197.1.1,demod,1976] -> x+ (y*x@ )=x+y. 3083 [para_into,196.1.1.2,134.1.1,demod,1130] A* ((A*B)+C)=A* (B+C) -> . 4371 [para_into,2749.1.1.1,206.1.1] -> (x@ +y)* (x+ ((z*x@ )+y))= (z*x@ )+y. 4412,4411 [para_into,2878.1.1.2,23.1.1] -> x+ (y* (z*x@ ))=x+ (y*z). 4429,4428 [para_from,2878.1.1,21.1.1.1,demod,22,flip.1] -> x+ ((y*x@ )+z)=x+ (y+z). 4432,4431 [back_demod,4371,demod,4429,flip.1] -> (x*y@ )+z= (y@ +z)* (y+ (x+z)). 4617,4616 [para_from,214.1.1,182.1.1.2.2] -> (x+y)* (z* (x+ (y+u)))= (x+y)*z. 4739,4738 [para_into,221.1.1.2,1813.1.1,flip.1] -> (x+y)* (z* (y@ +x))=z*x. 4862,4861 [para_into,227.1.1.1,165.1.1,demod,24,1108,44,183] -> (x*y)+ (x*z)=x* ((x*y)+z). 4885 [para_into,227.1.1.2.1,338.1.1,demod,28,4862,2879,4432,4617,4739] -> x* ((x*y)+ (z*y@ ))= (y+z)*x. 4908,4907 [para_into,227.1.1.2.2,165.1.1,demod,200,4862,185,828] -> x* ((x*y)+z)= (y+ (x*z))*x. 4968,4967 [back_demod,4885,demod,4908,4412] -> (x+ (y*z))*y= (x+z)*y. 4971 [back_demod,3083,demod,4908,4968] (B+C)*A=A* (B+C) -> . 4972 [binary,4971.1,134.1] -> . ------------ end of proof -------------