----- Otter 3.0.4, August 1995 ----- The job was started by mccune on gyro, Wed Nov 1 22:02:17 1995 ----> UNIT CONFLICT at 0.66 sec ----> 257 [binary,255.1,254.1] -> . Length of proof is 49. Level of proof is 19. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] B@ *B=A@ *A, A@ * (A*B)=B, (A*B)*B@ =A -> . 4,3 [] -> beta=alpha. 6,5 [] -> x@ *x=1. 7 [] -> x* ((((x*y@ )*y)@ *z)* ((alpha*u)@ * (beta*u)))=z. 8 [copy,7,demod,4,6] -> x* ((((x*y@ )*y)@ *z)*1)=z. 10 [back_demod,2,demod,6,6,unit_del,1] A@ * (A*B)=B, (A*B)*B@ =A -> . 11 [para_into,8.1.1.2.1.1.1.1,5.1.1] -> x@ @ * (((1*x)@ *y)*1)=y. 13 [para_into,8.1.1.2.1,8.1.1,flip.1] -> (((((x*y@ )*y)@ *z@ )*z)@ *u)*1=x* (u*1). 16,15 [para_into,8.1.1.2.1,5.1.1,flip.1] -> (x*y@ )*y=x* (1*1). 18,17 [back_demod,13,demod,16,16] -> (((x* (1*1))@ * (1*1))@ *y)*1=x* (y*1). 19 [back_demod,8,demod,16] -> x* (((x* (1*1))@ *y)*1)=y. 24,23 [para_into,15.1.1.1,5.1.1,flip.1] -> x@ @ * (1*1)=1*x. 25 [para_into,11.1.1.2,15.1.1] -> x@ @ * ((1*x)@ * (1*1))=1@ . 29 [para_into,19.1.1.2.1.1.1,5.1.1] -> (1*1)@ * ((1@ *x)*1)=x. 37 [para_into,29.1.1.2.1,19.1.1,flip.1] -> ((1@ * (1*1))@ *x)*1= (1*1)@ * (x*1). 40,39 [para_into,29.1.1.2,15.1.1] -> (1*1)@ * (1@ * (1*1))=1@ . 41 [para_from,29.1.1,11.1.1.2.1] -> 1@ @ * (x*1)= (1@ *x)*1. 43 [para_from,39.1.1,11.1.1.2.1,demod,6] -> 1@ @ *1=1@ * (1*1). 45 [para_into,17.1.1.1.1.1.1.1,15.1.1,demod,18,flip.1] -> (x* (1*1)@ )* (y*1)=x* (y*1). 49 [para_from,17.1.1,19.1.1.2] -> (x* (1*1))@ * (x* (y*1))=y. 56 [para_into,41.1.1,19.1.1,demod,24,flip.1] -> (1@ * ((1*1)@ *x))*1=x. 73 [para_into,49.1.1.1.1,5.1.1] -> 1@ * ((1*1)@ * (x*1))=x. 76,75 [para_into,49.1.1.2.2,56.1.1] -> (x* (1*1))@ * (x*y)=1@ * ((1*1)@ *y). 78,77 [para_into,49.1.1.2.2,43.1.1,demod,76,40,flip.1] -> 1@ @ =1@ *1@ . 82 [para_into,49.1.1.2.2,15.1.1,demod,76] -> 1@ * ((1*1)@ * (x* (1*1)))=x*1@ . 89 [para_into,49.1.1.2,5.1.1] -> ((x*1)@ * (1*1))@ *1=x. 104 [copy,82,flip.1] -> x*1@ =1@ * ((1*1)@ * (x* (1*1))). 107 [para_from,77.1.1,23.1.1.1] -> (1@ *1@ )* (1*1)=1*1. 117 [para_from,77.1.1,11.1.1.1.1] -> (1@ *1@ )@ * (((1*1@ )@ *x)*1)=x. 124,123 [para_into,25.1.1.1,77.1.1,demod,6,16] -> 1@ * (1*1)=1@ . 127 [back_demod,39,demod,124] -> (1*1)@ *1@ =1@ . 129 [back_demod,37,demod,124,78] -> ((1@ *1@ )*x)*1= (1*1)@ * (x*1). 130 [copy,129,flip.1] -> (1*1)@ * (x*1)= ((1@ *1@ )*x)*1. 131 [para_from,123.1.1,29.1.1.2.1,demod,6] -> (1*1)@ *1=1*1. 142,141 [para_into,73.1.1.2.2,131.1.1,demod,6,6,flip.1] -> (1*1)@ =1. 149,148 [back_demod,130,demod,142,flip.1] -> ((1@ *1@ )*x)*1=1* (x*1). 151,150 [back_demod,127,demod,142] -> 1*1@ =1@ . 152 [back_demod,104,demod,142] -> x*1@ =1@ * (1* (x* (1*1))). 156 [back_demod,75,demod,142] -> (x* (1*1))@ * (x*y)=1@ * (1*y). 163,162 [back_demod,45,demod,142] -> (x*1)* (y*1)=x* (y*1). 171 [back_demod,117,demod,151,78,149] -> (1@ *1@ )@ * (1* (x*1))=x. 192,191 [para_from,141.1.1,23.1.1.1.1,demod,124] -> 1@ =1* (1*1). 196,195 [para_from,141.1.1,5.1.1.1] -> 1* (1*1)=1. 200,199 [back_demod,107,demod,192,196,192,196,163,196,flip.1] -> 1*1=1. 204,203 [back_demod,171,demod,192,200,200,192,200,200,200,192,200,200] -> 1* (1* (x*1))=x. 219 [back_demod,156,demod,200,192,200,200] -> (x*1)@ * (x*y)=1* (1*y). 223,222 [back_demod,152,demod,192,200,200,192,200,200,200,204] -> x*1=x. 237,236 [back_demod,89,demod,223,223,223,223] -> x@ @ =x. 247,246 [back_demod,23,demod,237,223,223,flip.1] -> 1*x=x. 250 [back_demod,15,demod,223,223] -> (x*y@ )*y=x. 253,252 [back_demod,219,demod,223,247,247] -> x@ * (x*y)=y. 254 [back_demod,10,demod,253,unit_del,1] (A*B)*B@ =A -> . 255 [para_into,250.1.1.1.2,236.1.1] -> (x*y)*y@ =x. 257 [binary,255.1,254.1] -> . ------------ end of proof -------------