----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Sun Feb 11 18:47:32 1996 ----> UNIT CONFLICT at 23.51 sec ----> 4974 [binary,4972.1,39.1] $F. Length of proof is 35. Level of proof is 10. ---------------- PROOF ---------------- 4 [] x^y=y^x. 6,5 [] (x^y)^z=x^ (y^z). 9 [] x v y=y v x. 11,10 [] (x v y) v z=x v (y v z). 12 [] x^ (x v y)=x. 14 [] x v (x^y)=x. 17,16 [] 0^x=0. 19,18 [] 0 v x=x. 20 [] 1^x=x. 25,24 [] (x^y) v (x^z)=x^ (y v (x^z)). 28 [] C1^ (A v B)=0. 30 [] C2 v (A^B)=1. 32 [] C2^ (A^B)=0. 34 [] C1 v (A^C2)=D. 37,36 [] C1 v (B^C2)=E. 38 [] D^E!=C1. 39 [para_from,4.1.1,38.1.1] E^D!=C1. 40 [para_from,4.1.1,36.1.1.2] C1 v (C2^B)=E. 44 [para_into,28.1.1,4.1.1] (A v B)^C1=0. 46 [para_into,5.1.1.1,28.1.1,demod,17,flip.1] C1^ ((A v B)^x)=0. 51 [para_into,5.1.1,4.1.1] x^ (y^z)=y^ (z^x). 54 [copy,51,flip.1] x^ (y^z)=z^ (x^y). 55 [para_into,30.1.1.2,4.1.1] C2 v (B^A)=1. 60,59 [para_into,32.1.1,4.1.1,demod,6] A^ (B^C2)=0. 88,87 [para_into,9.1.1,34.1.1,flip.1] (A^C2) v C1=D. 156 [para_into,12.1.1.2,40.1.1] C1^E=C1. 166 [para_into,12.1.1,4.1.1] (x v y)^x=x. 168 [para_from,12.1.1,5.1.1.1,flip.1] x^ ((x v y)^z)=x^z. 175,174 [para_into,156.1.1,4.1.1] E^C1=C1. 196 [para_into,14.1.1.2,4.1.1] x v (y^x)=x. 201,200 [para_into,14.1.1,9.1.1] (x^y) v x=x. 217,216 [para_into,16.1.1,4.1.1] x^0=0. 219,218 [para_into,18.1.1,9.1.1] x v 0=x. 231,230 [para_into,20.1.1,4.1.1] x^1=x. 296 [para_into,24.1.1.1,44.1.1,demod,19,flip.1] (A v B)^ (C1 v ((A v B)^x))= (A v B)^x. 306 [para_into,24.1.1.2,174.1.1,demod,175] (E^x) v C1=E^ (x v C1). 312 [para_into,24.1.1,9.1.1,demod,25] x^ (y v (x^z))=x^ (z v (x^y)). 349 [para_into,46.1.1.2,4.1.1] C1^ (x^ (A v B))=0. 1295 [para_into,349.1.1.2,12.1.1] C1^A=0. 1300,1299 [para_into,1295.1.1,4.1.1] A^C1=0. 3663 [para_into,312.1.1.2,55.1.1,demod,231,flip.1] B^ (A v (B^C2))=B. 3671 [para_into,312.1.1.2,34.1.1,demod,1300,219] A^D=A^C2. 3801 [para_into,3671.1.1,4.1.1] D^A=A^C2. 3854 [para_from,3663.1.1,196.1.1.2,demod,11,201,flip.1] A v (B^C2)=A v B. 3916 [para_into,3854.1.1,9.1.1] (B^C2) v A=A v B. 4122,4121 [para_from,3916.1.1,166.1.1.1] (A v B)^ (B^C2)=B^C2. 4395 [para_from,4121.1.1,296.1.1.2.2,demod,37,4122] (A v B)^E=B^C2. 4420 [para_from,4395.1.1,168.1.1.2,demod,60,flip.1] A^E=0. 4468 [para_from,4420.1.1,54.1.1.2,demod,217,flip.1] E^ (x^A)=0. 4721 [para_from,4468.1.1,306.1.1.1,demod,19,flip.1] E^ ((x^A) v C1)=C1. 4972 [para_into,4721.1.1.2.1,3801.1.1,demod,88] E^D=C1. 4974 [binary,4972.1,39.1] $F. ------------ end of proof -------------