----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Sun Feb 11 18:41:31 1996 ----> UNIT CONFLICT at 3.81 sec ----> 240 [binary,239.1,226.1] -> . Length of proof is 78. Level of proof is 26. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] A+ (B*C)= (A+B)* (A+C), (A*B)+B=B, B*B@ =A*A@ -> . 3 [] -> (x+y)*y=y. 5 [] -> x* (y+z)= (x*y)+ (x*z). 7,6 [copy,5,flip.1] -> (x*y)+ (x*z)=x* (y+z). 9,8 [] -> x+x@ =1. 11,10 [] -> p(x,y,z)= (x*y@ )+ ((x*z)+ (y@ *z)). 12 [] -> p(x,x,y)=y. 13 [copy,12,demod,11] -> (x*x@ )+ ((x*y)+ (x@ *y))=y. 15 [] -> p(x,y,y)=x. 17,16 [copy,15,demod,11] -> (x*y@ )+ ((x*y)+ (y@ *y))=x. 22,21 [para_from,8.1.1,3.1.1.1] -> 1*x@ =x@ . 23 [para_into,6.1.1.1,21.1.1] -> x@ + (1*y)=1* (x@ +y). 26,25 [para_into,6.1.1.1,3.1.1] -> x+ ((y+x)*z)= (y+x)* (x+z). 28,27 [para_into,6.1.1.2,3.1.1] -> ((x+y)*z)+y= (x+y)* (z+y). 29 [para_from,6.1.1,3.1.1.1] -> (x* (y+z))* (x*z)=x*z. 31 [para_into,23.1.1.2,21.1.1,flip.1] -> 1* (x@ +y@ )=x@ +y@ . 33 [para_into,25.1.1.2,3.1.1,flip.1] -> (x+y)* (y+y)=y+y. 35 [para_from,27.1.1,3.1.1.1] -> ((x+y)* (z+y))*y=y. 38,37 [para_into,31.1.1.2,8.1.1,demod,9] -> 1*1=1. 43 [para_into,35.1.1.1.2,8.1.1] -> ((x+y@ )*1)*y@ =y@ . 45 [para_from,37.1.1,23.1.1.2,flip.1] -> 1* (x@ +1)=x@ +1. 48,47 [para_from,37.1.1,29.1.1.2,demod,38] -> (1* (x+1))*1=1. 49 [para_from,37.1.1,6.1.1.2] -> (1*x)+1=1* (x+1). 52,51 [para_from,37.1.1,13.1.1.2.1,demod,22] -> 1@ + (1+ (1@ *1))=1. 55 [para_into,16.1.1.1,3.1.1] -> x@ + (((y+x@ )*x)+ (x@ *x))=y+x@ . 57 [para_into,16.1.1.2,6.1.1,demod,7] -> x@ * (x@ + (x+x))=x@ . 60,59 [para_from,16.1.1,27.1.1.1.1,demod,17] -> (x*y)+ ((x*z)+ (z@ *z))=x* (y+ ((x*z)+ (z@ *z))). 61 [para_from,16.1.1,3.1.1.1] -> x* ((x*y)+ (y@ *y))= (x*y)+ (y@ *y). 63 [back_demod,16,demod,60] -> x* (y@ + ((x*y)+ (y@ *y)))=x. 71 [para_from,49.1.1,33.1.1.1] -> (1* (x+1))* (1+1)=1+1. 74,73 [para_from,57.1.1,6.1.1.2] -> (x@ *y)+x@ =x@ * (y+ (x@ + (x+x))). 76,75 [para_into,63.1.1.2.2.1,47.1.1,demod,52,48,flip.1] -> 1* (x+1)=1. 78,77 [back_demod,71,demod,76,76,flip.1] -> 1+1=1. 82,81 [back_demod,45,demod,76,flip.1] -> x@ +1=1. 84,83 [para_from,77.1.1,57.1.1.2.2,demod,82] -> 1@ *1=1@ . 86,85 [para_from,83.1.1,55.1.1.2.2,demod,28,9,26,82] -> (x+1@ )*1=x+1@ . 87 [para_from,83.1.1,63.1.1.2.2.2] -> x* (1@ + ((x*1)+1@ ))=x. 90,89 [para_from,83.1.1,61.1.1.2.2,demod,84] -> x* ((x*1)+1@ )= (x*1)+1@ . 92,91 [para_from,83.1.1,73.1.1.1,demod,78,82,78,84] -> 1@ +1@ =1@ . 93 [para_from,83.1.1,59.1.1.2.1,demod,84,92,74,78,82,84,84,92,flip.1] -> 1@ * (x+1@ )=1@ * (x+1). 98,97 [para_from,85.1.1,25.1.1.2,demod,82,86] -> 1@ + (x+1@ )=x+1@ . 100,99 [back_demod,87,demod,98,90] -> (x*1)+1@ =x. 101 [back_demod,89,demod,100,100] -> x*x=x. 104,103 [para_into,99.1.1.1,3.1.1,demod,9,flip.1] -> x+1=1. 105 [back_demod,93,demod,104,84] -> 1@ * (x+1@ )=1@ . 108,107 [para_from,99.1.1,97.1.1.2,demod,100] -> 1@ +x=x. 110,109 [para_from,99.1.1,85.1.1.1,demod,100] -> x*1=x. 112,111 [para_from,99.1.1,43.1.1.1.1,demod,110] -> x*1@ =1@ . 114,113 [back_demod,99,demod,110] -> x+1@ =x. 116,115 [back_demod,105,demod,114] -> 1@ *x=1@ . 118,117 [para_from,101.1.1,6.1.1.2] -> (x*y)+x=x* (y+x). 120,119 [para_from,101.1.1,6.1.1.1] -> x+ (x*y)=x* (x+y). 126,125 [para_from,109.1.1,6.1.1.2,demod,118,104,110] -> x* (y+x)=x. 127 [para_from,109.1.1,6.1.1.1,demod,120] -> x* (x+y)=x* (1+y). 129,128 [back_demod,117,demod,126] -> (x*y)+x=x. 130 [para_from,111.1.1,13.1.1.2.2,demod,112,114,114] -> x*x@ =1@ . 133 [copy,130,flip.1] -> 1@ =x*x@ . 134 [para_into,115.1.1,61.1.1,demod,116,108] -> x@ *x=1@ . 138 [para_from,125.1.1,6.1.1.1,demod,120,flip.1] -> x* ((y+x)+z)=x* (x+z). 140 [para_into,127.1.1.2,8.1.1,demod,110,flip.1] -> x* (1+x@ )=x. 143,142 [para_from,130.1.1,13.1.1.2.2,demod,114,7,9,110,flip.1] -> x@ @ =x. 145,144 [para_from,130.1.1,13.1.1.1,demod,108] -> (x*y)+ (x@ *y)=y. 148 [para_into,133.1.1,133.1.1] -> x*x@ =y*y@ . 151 [para_from,134.1.1,6.1.1.2,demod,114,flip.1] -> x@ * (y+x)=x@ *y. 154,153 [para_from,134.1.1,6.1.1.1,demod,108,flip.1] -> x@ * (x+y)=x@ *y. 161 [para_into,144.1.1.1,127.1.1,demod,154] -> (x* (1+y))+ (x@ *y)=x+y. 167,166 [para_into,144.1.1.2,140.1.1,demod,143,126,9,143,flip.1] -> 1+x=1. 169,168 [back_demod,161,demod,167,110] -> x+ (x@ *y)=x+y. 171,170 [back_demod,127,demod,167,110] -> x* (x+y)=x. 173 [back_demod,138,demod,171] -> x* ((y+x)+z)=x. 176,175 [back_demod,119,demod,171] -> x+ (x*y)=x. 180,179 [para_from,151.1.1,6.1.1.1,demod,7,flip.1] -> x@ * ((y+x)+z)=x@ * (y+z). 189 [para_into,168.1.1.2,153.1.1,demod,169,flip.1] -> x+ (x+y)=x+y. 197 [para_from,173.1.1,144.1.1.1,demod,180,169,flip.1] -> (x+y)+z=y+ (x+z). 200,199 [para_into,189.1.1.2,144.1.1,demod,145] -> (x*y)+y=y. 201 [back_demod,2,demod,200,unit_del,1,148] A+ (B*C)= (A+B)* (A+C) -> . 206 [para_from,199.1.1,197.1.1.1,flip.1] -> x+ ((y*x)+z)=x+z. 213,212 [para_into,206.1.1.2,113.1.1,demod,114] -> x+ (y*x)=x. 216 [para_into,206.1.1.2,6.1.1] -> x+ (y* (x+z))=x+ (y*z). 218 [para_from,212.1.1,25.1.1.2.1,demod,213] -> (x*y)+ (y*z)=y* ((x*y)+z). 220 [para_from,212.1.1,27.1.1.1.1,demod,213] -> (x*y)+ (z*x)=x* (y+ (z*x)). 223,222 [para_into,218.1.1.1,170.1.1,demod,171] -> x+ ((x+y)*z)= (x+y)* (x+z). 226 [para_into,220.1.1,218.1.1,demod,129,176] -> x*y=y*x. 236,235 [para_from,226.1.1,216.1.1.2,demod,223,flip.1] -> x+ (y*z)= (x+z)* (x+y). 239 [back_demod,201,demod,236] (A+C)* (A+B)= (A+B)* (A+C) -> . 240 [binary,239.1,226.1] -> . ------------ end of proof -------------