----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on gyro, Tue Feb 28 12:51:43 1995 ----> UNIT CONFLICT at 3.33 sec ----> 679 [binary,677.1,111.1] -> . Length of proof is 17. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B v (A^ (B^C))=B, ((A v B)^ (B v C))^B=B -> . 3 [] -> x^ (y v (x v z))=x. 5 [] -> ((x^y) v (y^z)) v y=y. 8,7 [] -> ((x v y)^ (x v z))^x=x. 9 [para_into,5.1.1.1.2,3.1.1] -> ((x^y) v y) v y=y. 11 [para_from,5.1.1,3.1.1.2] -> x^ (x v y)=x. 13 [para_into,11.1.1.2,5.1.1] -> ((x^y) v (y^z))^y= (x^y) v (y^z). 24,23 [para_into,7.1.1.1,3.1.1] -> (x v y)^x=x. 27 [para_from,7.1.1,5.1.1.1.1] -> (x v (x^y)) v x=x. 30,29 [para_into,13.1.1.1.1,7.1.1,demod,24,8,flip.1] -> x v (x^y)=x. 31 [back_demod,27,demod,30] -> x v x=x. 38,37 [para_from,31.1.1,3.1.1.2.2] -> x^ (y v x)=x. 40,39 [para_into,23.1.1.1,9.1.1,demod,38,flip.1] -> (x^y) v y=y. 45 [para_into,29.1.1.2,23.1.1] -> (x v y) v x=x v y. 55 [para_into,39.1.1.1,37.1.1] -> x v (y v x)=y v x. 67 [para_from,39.1.1,3.1.1.2.2] -> (x^y)^ (z v y)=x^y. 69 [para_into,45.1.1.1,39.1.1,demod,40] -> x v (y^x)=x. 106,105 [para_from,55.1.1,7.1.1.1.1] -> ((x v y)^ (y v z))^y=y. 111 [back_demod,2,demod,106,unit_del,1] B v (A^ (B^C))=B -> . 224 [para_from,67.1.1,69.1.1.2] -> (x v y) v (z^y)=x v y. 677 [para_into,224.1.1.1,29.1.1,demod,30] -> x v (y^ (x^z))=x. 679 [binary,677.1,111.1] -> . ------------ end of proof -------------