----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 22:01:56 1995 ----> UNIT CONFLICT at 0.66 sec ----> 246 [binary,244.1,239.1] -> . Length of proof is 48. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B@ *B=A@ *A, A@ * (A*B)=B, (A*B)*B@ =A -> . 3 [] -> x* ((((x*y@ )*y)@ *z)* (u@ *u))=z. 6,5 [] -> x@ *x=1. 7 [back_demod,3,demod,6] -> x* ((((x*y@ )*y)@ *z)*1)=z. 9 [back_demod,2,demod,6,6,unit_del,1] A@ * (A*B)=B, (A*B)*B@ =A -> . 10 [para_into,7.1.1.2.1.1.1.1,5.1.1] -> x@ @ * (((1*x)@ *y)*1)=y. 12 [para_into,7.1.1.2.1,7.1.1,flip.1] -> (((((x*y@ )*y)@ *z@ )*z)@ *u)*1=x* (u*1). 15,14 [para_into,7.1.1.2.1,5.1.1,flip.1] -> (x*y@ )*y=x* (1*1). 17,16 [back_demod,12,demod,15,15] -> (((x* (1*1))@ * (1*1))@ *y)*1=x* (y*1). 18 [back_demod,7,demod,15] -> x* (((x* (1*1))@ *y)*1)=y. 23,22 [para_into,14.1.1.1,5.1.1,flip.1] -> x@ @ * (1*1)=1*x. 24 [para_into,10.1.1.2,14.1.1] -> x@ @ * ((1*x)@ * (1*1))=1@ . 28 [para_into,18.1.1.2.1.1.1,5.1.1] -> (1*1)@ * ((1@ *x)*1)=x. 36 [para_into,28.1.1.2.1,18.1.1,flip.1] -> ((1@ * (1*1))@ *x)*1= (1*1)@ * (x*1). 39,38 [para_into,28.1.1.2,14.1.1] -> (1*1)@ * (1@ * (1*1))=1@ . 40 [para_from,28.1.1,10.1.1.2.1] -> 1@ @ * (x*1)= (1@ *x)*1. 42 [para_from,38.1.1,10.1.1.2.1,demod,6] -> 1@ @ *1=1@ * (1*1). 44 [para_into,16.1.1.1.1.1.1.1,14.1.1,demod,17,flip.1] -> (x* (1*1)@ )* (y*1)=x* (y*1). 48 [para_from,16.1.1,18.1.1.2] -> (x* (1*1))@ * (x* (y*1))=y. 55 [para_into,40.1.1,18.1.1,demod,23,flip.1] -> (1@ * ((1*1)@ *x))*1=x. 66 [para_into,48.1.1.1.1,5.1.1] -> 1@ * ((1*1)@ * (x*1))=x. 69,68 [para_into,48.1.1.2.2,55.1.1] -> (x* (1*1))@ * (x*y)=1@ * ((1*1)@ *y). 71,70 [para_into,48.1.1.2.2,42.1.1,demod,69,39,flip.1] -> 1@ @ =1@ *1@ . 75 [para_into,48.1.1.2.2,14.1.1,demod,69] -> 1@ * ((1*1)@ * (x* (1*1)))=x*1@ . 82 [para_into,48.1.1.2,5.1.1] -> ((x*1)@ * (1*1))@ *1=x. 104 [para_from,70.1.1,22.1.1.1] -> (1@ *1@ )* (1*1)=1*1. 110 [para_from,70.1.1,10.1.1.1.1] -> (1@ *1@ )@ * (((1*1@ )@ *x)*1)=x. 121,120 [para_into,24.1.1.1,70.1.1,demod,6,15] -> 1@ * (1*1)=1@ . 124 [back_demod,38,demod,121] -> (1*1)@ *1@ =1@ . 126 [back_demod,36,demod,121,71] -> ((1@ *1@ )*x)*1= (1*1)@ * (x*1). 127 [copy,126,flip.1] -> (1*1)@ * (x*1)= ((1@ *1@ )*x)*1. 128 [para_from,120.1.1,28.1.1.2.1,demod,6] -> (1*1)@ *1=1*1. 137,136 [para_from,128.1.1,66.1.1.2.2,demod,6,6,flip.1] -> (1*1)@ =1. 142,141 [back_demod,127,demod,137,flip.1] -> ((1@ *1@ )*x)*1=1* (x*1). 144,143 [back_demod,124,demod,137] -> 1*1@ =1@ . 149 [back_demod,75,demod,137] -> 1@ * (1* (x* (1*1)))=x*1@ . 151 [back_demod,68,demod,137] -> (x* (1*1))@ * (x*y)=1@ * (1*y). 158,157 [back_demod,44,demod,137] -> (x*1)* (y*1)=x* (y*1). 162 [back_demod,110,demod,144,71,142] -> (1@ *1@ )@ * (1* (x*1))=x. 173,172 [para_from,136.1.1,22.1.1.1.1,demod,121] -> 1@ =1* (1*1). 177,176 [para_from,136.1.1,5.1.1.1] -> 1* (1*1)=1. 187,186 [back_demod,162,demod,173,177,173,177,137] -> 1* (1* (x*1))=x. 195,194 [back_demod,104,demod,173,177,173,177,158,177,flip.1] -> 1*1=1. 202 [back_demod,151,demod,195,173,195,195] -> (x*1)@ * (x*y)=1* (1*y). 206,205 [back_demod,149,demod,173,195,195,195,187,173,195,195,flip.1] -> x*1=x. 226,225 [back_demod,82,demod,206,206,206,206] -> x@ @ =x. 232,231 [back_demod,22,demod,226,206,206,flip.1] -> 1*x=x. 235 [back_demod,14,demod,206,206] -> (x*y@ )*y=x. 238,237 [back_demod,202,demod,206,232,232] -> x@ * (x*y)=y. 239 [back_demod,9,demod,238,unit_del,1] (A*B)*B@ =A -> . 244 [para_into,235.1.1.1.2,225.1.1] -> (x*y)*y@ =x. 246 [binary,244.1,239.1] -> . ------------ end of proof -------------