----- Otter 3.0.3c, Jan 1995 ----- The job was started by mccune on gyro, Tue Feb 14 09:35:13 1995 ----> UNIT CONFLICT at 404.66 sec ----> 6036 [binary,6034.1,16.1] $Ans(assoc_meet). Length of proof is 33. Level of proof is 10. ---------------- PROOF ---------------- 2 [] x^x=x. 4 [] x^y=y^x. 5 [] ((x v y)^ (z v y))^y=y. 8,7 [] x v x=x. 9 [] x v y=y v x. 10 [] ((x^y) v (z^y)) v y=y. 13,12 [] (x v y) v z=x v (y v z). 14 [] x^ (y v (x v z))=x. 16 [] (A^B)^C!=A^ (B^C)|$Ans(assoc_meet). 17 [back_demod,10,demod,13] (x^y) v ((z^y) v y)=y. 25 [para_into,14.1.1.2,7.1.1] x^ (x v y)=x. 29 [para_into,5.1.1.1.1,9.1.1] ((x v y)^ (z v x))^x=x. 35 [para_into,5.1.1.1,2.1.1] (x v y)^y=y. 37 [para_into,5.1.1,4.1.1] x^ ((y v x)^ (z v x))=x. 42 [para_into,12.1.1.1,7.1.1,flip.1] x v (x v y)=x v y. 56 [para_from,12.1.1,35.1.1.1] (x v (y v z))^z=z. 71,70 [para_into,42.1.1.2,9.1.1] x v (y v x)=x v y. 87,86 [para_into,17.1.1.1,56.1.1,demod,71] x v (y^x)=x. 92 [para_into,17.1.1.1,4.1.1] (x^y) v ((z^x) v x)=x. 95,94 [para_into,17.1.1.2.1,56.1.1,demod,8] (x^y) v y=y. 100 [back_demod,92,demod,95] (x^y) v x=x. 102 [para_into,86.1.1.2,4.1.1] x v (x^y)=x. 112 [para_from,86.1.1,5.1.1.1.2] ((x v (y^z))^z)^ (y^z)=y^z. 116 [para_from,86.1.1,12.1.1.1,flip.1] x v ((y^x) v z)=x v z. 122 [para_into,29.1.1.1.2,86.1.1] (((x^y) v z)^y)^ (x^y)=x^y. 142 [para_from,100.1.1,29.1.1.1.1] (x^ (y v (x^z)))^ (x^z)=x^z. 144 [para_from,100.1.1,25.1.1.2] (x^y)^x=x^y. 146 [para_from,100.1.1,12.1.1.1,flip.1] (x^y) v (x v z)=x v z. 174 [para_into,37.1.1.2.1,102.1.1] (x^y)^ (x^ (z v (x^y)))=x^y. 339 [para_into,116.1.1.2,102.1.1,demod,87,flip.1] x v ((y^x)^z)=x. 341 [para_into,116.1.1.2,86.1.1,demod,87,flip.1] x v (y^ (z^x))=x. 366 [para_into,339.1.1.2.1,144.1.1] x v ((x^y)^z)=x. 408 [para_into,341.1.1.2.2,144.1.1] x v (y^ (x^z))=x. 1248 [para_into,112.1.1.1.1,366.1.1] (x^y)^ ((x^z)^y)= (x^z)^y. 1511 [para_into,122.1.1.1.1,146.1.1] ((x v y)^z)^ (x^z)=x^z. 1717 [para_into,142.1.1.1.2,408.1.1] (x^y)^ (x^ (y^z))=x^ (y^z). 2583,2582 [para_into,174.1.1.2.2,341.1.1] (x^ (y^z))^ (x^z)=x^ (y^z). 3667,3666 [para_into,1511.1.1,4.1.1] (x^y)^ ((x v z)^y)=x^y. 5866 [para_into,1248.1.1.2,3666.1.1,demod,2583,3667] x^ ((x v y)^z)=x^z. 5985,5984 [para_into,5866.1.1.2.1,100.1.1] (x^y)^ (x^z)= (x^y)^z. 5987,5986 [para_into,5866.1.1.2.1,94.1.1] (x^y)^ (y^z)= (x^y)^z. 6034 [back_demod,1717,demod,5985,5987] (x^y)^z=x^ (y^z). 6036 [binary,6034.1,16.1] $Ans(assoc_meet). ------------ end of proof -------------