----- Otter 3.0.7, April 2000 ----- -----> EMPTY CLAUSE at 6.49 sec ----> 122 [hyper,121,2,89,66] $Ans(Robbins_basis). Length of proof is 57. Level of proof is 30. ---------------- PROOF ---------------- 2 [] B+A!=A+B| (A+B)+C!=A+ (B+C)| ((A+B)@ + (A@ +B)@ )@ !=B|$Ans(Robbins_basis). 3 [] (((x+y)@ +z)@ + (x+ (z@ + (z+u)@ )@ )@ )@ =z. 61 [para_into,3.1.1.1.1.1.1,3.1.1] ((x+y)@ + (((z+u)@ +x)@ + (y@ + (y+v)@ )@ )@ )@ =y. 62 [para_into,61.1.1.1.2.1.1.1.1,61.1.1] ((x+y)@ + ((z+x)@ + (y@ + (y+u)@ )@ )@ )@ =y. 63 [para_into,61.1.1.1.2,3.1.1] ((x+x@ )@ +x)@ =x@ . 64 [para_into,62.1.1.1.2.1.2.1.1,63.1.2] ((x+y)@ + ((z+x)@ + (((y+y@ )@ +y)@ + (y+u)@ )@ )@ )@ =y. 65 [para_into,64.1.1.1.2.1.2,3.1.1] ((x+y)@ + ((z+x)@ +y)@ )@ =y. 66 [para_into,65.1.1.1.2.1.1,63.1.1] ((x+y)@ + (x@ +y)@ )@ =y. 67 [para_from,65.1.1,64.1.1.1.2] (((x+y)@ +x)@ + (x+y)@ )@ =x. 68 [para_into,67.1.1.1.1,67.1.1] (x+ ((x+y)@ +x)@ )@ = (x+y)@ . 69 [para_from,67.1.1,65.1.1.1.2.1.1] (((x+y)@ +z)@ + (x+z)@ )@ =z. 70 [para_into,69.1.1.1.1,69.1.1] (x+ ((y+z)@ + (y+x)@ )@ )@ = (y+x)@ . 71 [para_into,69.1.1.1.2,66.1.1] ((((x+y)@ +z)@ + (x@ +y)@ )@ +y)@ = (x@ +y)@ . 72 [para_into,70.1.1.1.2.1.1,70.1.1] (x+ ((y+z)@ + (z+x)@ )@ )@ = (z+x)@ . 73 [para_from,70.1.1,62.1.1.1.2.1.2.1.2] ((x+y)@ + ((z+x)@ + (y@ + (u+y)@ )@ )@ )@ =y. 74 [para_into,72.1.1.1.2,67.1.1] (x+y)@ = (y+x)@ . 75 [para_into,74.1.1,72.1.1,flip.1] (((x+y)@ + (y+z)@ )@ +z)@ = (y+z)@ . 76 [para_into,75.1.1.1.1.1.1,67.1.1] ((x+ ((x+y)@ +z)@ )@ +z)@ = ((x+y)@ +z)@ . 77 [para_into,76.1.1.1.1,65.1.1,flip.1] (((x+y)@ +x)@ +y)@ = (y+y)@ . 78 [para_into,73.1.1,70.1.1] (x@ + (y+x)@ )@ =x. 79 [para_into,78.1.1,74.1.2] ((x+y)@ +y@ )@ =y. 80 [para_from,79.1.1,69.1.1.1.1] (x+ (y+x@ )@ )@ =x@ . 81 [para_into,80.1.1.1.2,79.1.1] (x+x)@ =x@ . 83 [para_into,81.1.1,77.1.2] (((x+y)@ +x)@ +y)@ =y@ . 85 [para_into,83.1.1,79.1.1,flip.1] x@ @ =x. 86 [para_into,85.1.1.1,83.1.1,flip.1] ((x+y)@ +x)@ +y=y@ @ . 87 [para_into,85.1.1.1,74.1.2] (x+y)@ @ =y+x. 88 [para_into,85.1.1.1,70.1.1,flip.1] x+ ((y+z)@ + (y+x)@ )@ = (y+x)@ @ . 89 [para_into,87.1.1,85.1.1] x+y=y+x. 90 [para_into,86.1.2,85.1.1] ((x+y)@ +x)@ +y=y. 91 [para_into,90.1.1.1.1.1.1,89.1.2] ((x+y)@ +y)@ +x=x. 92 [para_into,90.1.1,89.1.2] x+ ((y+x)@ +y)@ =x. 93 [para_into,92.1.1.2.1.1,80.1.1] (x+y@ )@ + (y@ +y)@ = (x+y@ )@ . 94 [para_into,92.1.1.2.1.1,78.1.1] (x+y)@ + (y+y@ )@ = (x+y)@ . 95 [para_into,94.1.1.2.1,89.1.2] (x+y)@ + (y@ +y)@ = (x+y)@ . 96 [para_from,93.1.1,75.1.1.1.1.1] ((x+y@ )@ @ +y)@ = (y@ +y)@ . 97 [para_into,96.1.1.1.1,85.1.1] ((x+y@ )+y)@ = (y@ +y)@ . 98 [para_from,97.1.1,69.1.1.1.2] ((((x+y@ )+z)@ +y)@ + (y@ +y)@ )@ =y. 99 [para_into,88.1.2,85.1.1] x+ ((y+z)@ + (y+x)@ )@ =y+x. 100 [para_into,99.1.1.2.1.1,79.1.1] x+ (y+ ((z+y)@ +x)@ )@ = (z+y)@ +x. 101 [para_into,99.1.1.2.1,89.1.2] x+ ((y+x)@ + (y+z)@ )@ =y+x. 102 [para_from,101.1.1,91.1.1.1.1.1.1] ((x+y)@ + ((x+y)@ + (x+z)@ )@ )@ +y=y. 103 [para_into,98.1.1.1,95.1.1] (((x+y@ )+z)@ +y)@ @ =y. 104 [para_into,103.1.1,87.1.1] x+ ((y+x@ )+z)@ =x. 105 [para_into,104.1.1.2.1.1.2,85.1.1] x@ + ((y+x)+z)@ =x@ . 107 [para_into,100.1.1.2.1,92.1.1,flip.1] (x+y)@ +x=x+y@ . 108 [para_from,107.1.1,68.1.1.1.2.1] (x+ (x+y@ )@ )@ = (x+y)@ . 109 [para_into,102.1.1.1,108.1.1] ((x+y)@ + (x+z))@ +y=y. 110 [para_from,71.1.1,85.1.1.1,flip.1] (((x+y)@ +z)@ + (x@ +y)@ )@ +y= (x@ +y)@ @ . 111 [para_into,110.1.2,85.1.1] (((x+y)@ +z)@ + (x@ +y)@ )@ +y=x@ +y. 112 [para_into,111.1.1.1.1.1.1,109.1.1] (x@ + ((y+x)@ @ + (y+z))@ )@ + (y+z)= (y+x)@ @ + (y+z). 113 [para_into,112.1.1.1.1.2.1.1,85.1.1] (x@ + ((y+x)+ (y+z))@ )@ + (y+z)= (y+x)@ @ + (y+z). 114 [para_into,113.1.2.1,85.1.1] (x@ + ((y+x)+ (y+z))@ )@ + (y+z)= (y+x)+ (y+z). 115 [para_into,114.1.1.1.1,105.1.1] x@ @ + (y+z)= (y+x)+ (y+z). 117 [para_into,115.1.1.1,85.1.1,flip.1] (x+y)+ (x+z)=y+ (x+z). 118 [para_into,117.1.1,89.1.2] (x+y)+ (x+z)=z+ (x+y). 119 [para_into,118.1.1,117.1.1] x+ (y+z)=z+ (y+x). 120 [para_into,119.1.1.2,89.1.2] x+ (y+z)=y+ (z+x). 121 [para_into,120.1.1,89.1.2] (x+y)+z=x+ (y+z). 122 [hyper,121,2,89,66] $Ans(Robbins_basis). ------------ end of proof -------------