----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 22:14:31 1995 ----> UNIT CONFLICT at 71.49 sec ----> 6572 [binary,6570.1,3692.1] -> . Length of proof is 76. Level of proof is 21. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B^A=A^B, (A^B)^C=A^ (B^C), A^ (A v B)=A, B v A=A v B, (A v B) v C=A v (B v C), A v (A^B)=A -> . 4,3 [] -> x^ (x v y)=x. 5 [] -> x^ (y v z)= (z^x) v (y^x). 6 [back_demod,2,demod,4,unit_del,1] B^A=A^B, (A^B)^C=A^ (B^C), B v A=A v B, (A v B) v C=A v (B v C), A v (A^B)=A -> . 7 [copy,5,flip.1] -> (x^y) v (z^y)=y^ (z v x). 8 [para_into,5.1.1,3.1.1,flip.1] -> (x^y) v (y^y)=y. 19,18 [para_from,8.1.1,3.1.1.2] -> (x^y)^y=x^y. 20 [para_into,18.1.1.1,5.1.1] -> ((x^y) v (z^y))^ (z v x)=y^ (z v x). 22 [para_into,7.1.1.1,18.1.1] -> (x^y) v (z^y)=y^ (z v (x^y)). 23 [para_into,7.1.1.1,3.1.1] -> x v (y^ (x v z))= (x v z)^ (y v x). 26,25 [para_into,7.1.1.2,3.1.1] -> (x^ (y v z)) v y= (y v z)^ (y v x). 33,32 [para_from,7.1.1,3.1.1.2] -> (x^y)^ (y^ (z v x))=x^y. 36 [para_into,32.1.1.1,32.1.1,demod,33] -> (x^y)^ ((y^ (z v x))^ (u v (x^y)))=x^y. 55 [para_into,22.1.1,7.1.1,flip.1] -> x^ (y v (z^x))=x^ (y v z). 61 [para_into,55.1.1.2,8.1.1,flip.1] -> x^ ((y^x) v x)=x^x. 67 [para_into,61.1.1,5.1.1,demod,19] -> (x^x) v (y^x)=x^x. 76,75 [para_into,67.1.1,8.1.1,flip.1] -> x^x=x. 78,77 [para_into,67.1.1,7.1.1,demod,76] -> x^ (y v x)=x. 81 [back_demod,67,demod,76,76] -> x v (y^x)=x. 95 [back_demod,8,demod,76] -> (x^y) v y=y. 97 [para_into,75.1.1,5.1.1,demod,78,4] -> x v y=y v x. 108 [para_from,77.1.1,7.1.1.2] -> (x^ (y v z)) v z= (y v z)^ (z v x). 119,118 [para_into,81.1.1.2,75.1.1] -> x v x=x. 120 [para_into,81.1.1.2,55.1.1] -> (x v (y^z)) v (z^ (x v y))=x v (y^z). 132 [para_from,81.1.1,32.1.1.2.2] -> ((x^y)^z)^ (z^y)= (x^y)^z. 138 [para_into,118.1.1,7.1.1,demod,119] -> x^y=y^x. 141 [para_from,118.1.1,20.1.1.1,demod,119,119] -> (x^y)^x=y^x. 158,157 [para_into,23.1.1.2,77.1.1,flip.1] -> (x v y)^ (y v x)=x v y. 164 [para_into,23.1.1.2,3.1.1,demod,119,119,flip.1] -> (x v y)^x=x. 171,170 [para_into,97.1.1,7.1.1,flip.1] -> (x^y) v (z^y)=y^ (x v z). 184 [back_demod,7,demod,171] -> x^ (y v z)=x^ (z v y). 190 [para_into,138.1.1,55.1.1,flip.1] -> (x v (y^z))^z=z^ (x v y). 194 [para_into,138.1.1,32.1.1,flip.1] -> (x^ (y v z))^ (z^x)=z^x. 196 [para_into,138.1.1,18.1.1,flip.1] -> x^ (y^x)=y^x. 206 [para_from,138.1.1,95.1.1.1] -> (x^y) v x=x. 208 [para_from,138.1.1,32.1.1.1] -> (x^y)^ (x^ (z v y))=y^x. 211,210 [para_from,138.1.1,81.1.1.2] -> x v (x^y)=x. 214 [back_demod,6,demod,211,unit_del,138,97,1] (A^B)^C=A^ (B^C), (A v B) v C=A v (B v C) -> . 219 [para_from,164.1.1,55.1.1.2.2,demod,78,flip.1] -> x^ (y v (x v z))=x. 224 [para_into,25.1.1.1,55.1.1,demod,26,flip.1] -> (x v (y^z))^ (x v z)= (x v y)^ (x v z). 249,248 [para_from,206.1.1,164.1.1.1] -> x^ (x^y)=x^y. 269 [para_into,36.1.1.2.2,210.1.1] -> (x^y)^ ((y^ (z v x))^x)=x^y. 282,281 [para_from,141.1.1,210.1.1.2] -> (x^y) v (y^x)=x^y. 315 [para_into,219.1.1.2.2,206.1.1] -> (x^y)^ (z v x)=x^y. 525 [para_into,184.1.1,138.1.1] -> (x v y)^z=z^ (y v x). 526 [copy,525,flip.1] -> x^ (y v z)= (z v y)^x. 671 [para_into,108.1.1.1,138.1.1] -> ((x v y)^z) v y= (x v y)^ (y v z). 713 [para_from,315.1.1,25.1.1.1] -> (x^y) v z= (z v x)^ (z v (x^y)). 724 [copy,713,flip.1] -> (x v y)^ (x v (y^z))= (y^z) v x. 798,797 [para_into,120.1.1.1.2,138.1.1] -> (x v (y^z)) v (y^ (x v z))=x v (z^y). 1260 [para_into,132.1.1,138.1.1] -> (x^y)^ ((z^y)^x)= (z^y)^x. 1284 [para_into,525.1.1.1,281.1.1,demod,282] -> (x^y)^z=z^ (y^x). 2656,2655 [para_into,194.1.1.1.2,210.1.1] -> (x^y)^ ((y^z)^x)= (y^z)^x. 2710,2709 [back_demod,269,demod,2656] -> (x^ (y v z))^z=z^x. 3035 [para_into,208.1.1.2,18.1.1,demod,2710,33,flip.1] -> x^ (y^ (z v x))=x^y. 3069 [para_into,2709.1.1.1,190.1.1,flip.1] -> x^ (y v (z^ (u v x)))= ((u v x)^ (y v z))^x. 3076,3075 [para_into,2709.1.1.1,138.1.1] -> ((x v y)^z)^y=y^z. 3098,3097 [back_demod,3069,demod,3076] -> x^ (y v (z^ (u v x)))=x^ (y v z). 3101 [para_from,2709.1.1,120.1.1.1.2,demod,3098,798,2710] -> x v (y^z)=x v (z^y). 3127,3126 [para_into,3035.1.1.2.2,210.1.1] -> (x^y)^ (z^x)= (x^y)^z. 3135,3134 [para_into,3035.1.1.2.2,81.1.1] -> (x^y)^ (z^y)= (x^y)^z. 3144 [back_demod,1260,demod,3127,3135] -> (x^y)^z= (z^y)^x. 3369 [para_into,3101.1.1.2,157.1.1,demod,158] -> x v (y v z)=x v (z v y). 3452,3451 [para_into,3144.1.1,1284.1.1,flip.1] -> (x^y)^z=x^ (y^z). 3685 [back_demod,214,demod,3452,unit_del,1] (A v B) v C=A v (B v C) -> . 3692 [para_into,3685.1.1.1,97.1.1] (B v A) v C=A v (B v C) -> . 3730,3729 [para_into,224.1.1.1.2,196.1.1,demod,76,flip.1] -> (x v y)^ (x v (z^y))=x v (z^y). 3733 [para_into,224.1.1.1.2,164.1.1,demod,76,flip.1] -> (x v (y v z))^ (x v y)=x v y. 3746,3745 [para_into,224.1.1,138.1.1,demod,3730] -> x v (y^z)= (x v y)^ (x v z). 3747 [back_demod,724,demod,3746,249] -> (x v y)^ (x v z)= (y^z) v x. 3801 [para_into,3369.1.1,97.1.1] -> (x v y) v z=z v (y v x). 5932,5931 [para_into,3733.1.1,526.1.1] -> (x v y)^ (y v (x v z))=y v x. 5957 [para_from,3733.1.1,671.1.1.1,demod,5932] -> (x v y) v (y v z)= (y v z) v x. 6203 [para_from,3747.1.1,671.1.1.1,demod,5932] -> ((x^y) v z) v x=x v z. 6252 [para_into,6203.1.1.1.1,164.1.1] -> (x v y) v (x v z)= (x v z) v y. 6290 [copy,6252,flip.1] -> (x v y) v z= (x v z) v (x v y). 6533,6532 [para_into,5957.1.1,3801.1.1] -> (x v y) v (x v z)= (x v y) v z. 6552 [back_demod,6290,demod,6533] -> (x v y) v z= (x v z) v y. 6570 [para_into,6552.1.1,97.1.1,flip.1] -> (x v y) v z=y v (x v z). 6572 [binary,6570.1,3692.1] -> . ------------ end of proof -------------