----- Otter 3.1-b0, May 2000 ----- -----> EMPTY CLAUSE at 4.60 sec ----> 159 [hyper,158,2,95,147] $ANS("Sheffer"). Length of proof is 66. Level of proof is 42. ---------------- PROOF ---------------- 2 [] f(f(a,a),f(a,a))!=a|f(a,f(b,f(b,b)))!=f(a,a)|f(f(f(b,b),a),f(f(c,c),a))!=f(f(a,f(b,c)),f(a,f(b,c)))|$ANS("Sheffer"). 3 [] f(f(x,f(f(y,x),x)),f(y,f(z,x)))=y. 70 [para_into,3.1.1.1.2.1,3.1.1] f(f(f(x,f(y,z)),f(x,f(x,f(y,z)))),f(f(z,f(f(x,z),z)),f(u,f(x,f(y,z)))))=f(z,f(f(x,z),z)). 71 [para_into,3.1.1.2,3.1.1] f(f(f(x,y),f(f(f(y,f(f(z,y),y)),f(x,y)),f(x,y))),z)=f(y,f(f(z,y),y)). 72 [para_from,71.1.1,3.1.1.2.2] f(f(x,f(f(y,x),x)),f(y,f(z,f(f(x,z),z))))=y. 73 [para_from,72.1.1,70.1.1.1] f(x,f(f(x,f(f(x,x),x)),f(y,f(x,f(f(x,x),x)))))=f(x,f(f(x,x),x)). 74 [para_into,73.1.1.2,72.1.1,flip.1] f(x,f(f(x,x),x))=f(x,x). 75 [para_from,74.1.1,3.1.1.2] f(f(x,f(f(x,x),x)),f(x,x))=x. 76 [para_from,74.1.1,3.1.1.1] f(f(x,x),f(x,f(y,x)))=x. 77 [para_from,76.1.1,72.1.1.2] f(f(x,f(f(f(y,y),x),x)),y)=f(y,y). 78 [para_from,77.1.1,71.1.1.1.2.1] f(f(f(x,y),f(f(f(x,y),f(x,y)),f(x,y))),f(f(x,y),f(x,y)))=f(y,f(f(f(f(x,y),f(x,y)),y),y)). 79 [para_into,78.1.1,75.1.1,flip.1] f(x,f(f(f(f(y,x),f(y,x)),x),x))=f(y,x). 80 [para_from,79.1.1,76.1.1.2] f(f(x,x),f(y,x))=x. 83 [para_into,80.1.1.1,80.1.1] f(x,f(y,f(x,x)))=f(x,x). 84 [para_into,80.1.1.2,80.1.1] f(f(f(x,y),f(x,y)),y)=f(x,y). 85 [para_from,84.1.1,79.1.1.2.1] f(x,f(f(y,x),x))=f(y,x). 86 [para_from,85.1.1,3.1.1.1] f(f(x,y),f(x,f(z,y)))=x. 88 [para_into,86.1.1.2.2,80.1.1] f(f(x,f(y,z)),f(x,z))=x. 89 [para_into,88.1.1.1,86.1.1] f(x,f(f(x,y),f(z,y)))=f(x,y). 90 [para_from,88.1.1,86.1.1.2] f(f(f(x,f(y,z)),z),x)=f(x,f(y,z)). 91 [para_into,89.1.1.2,3.1.1,flip.1] f(x,f(f(y,x),x))=f(x,y). 93 [para_into,91.1.1,85.1.1] f(x,y)=f(y,x). 95 [para_from,91.1.1,88.1.1.1] f(f(x,y),f(x,x))=x. 97 [para_from,91.1.1,3.1.1.1] f(f(x,y),f(y,f(z,x)))=y. 101 [para_from,93.1.1,88.1.1.2] f(f(x,f(y,z)),f(z,x))=x. 104 [para_into,97.1.1.2.2,93.1.2] f(f(x,y),f(y,f(x,z)))=y. 105 [para_into,101.1.1.1.2,93.1.2] f(f(x,f(y,z)),f(y,x))=x. 106 [para_from,104.1.1,97.1.1.2] f(f(f(x,y),f(x,z)),z)=f(x,z). 108 [para_into,105.1.1.1,105.1.1] f(x,f(y,f(x,f(y,z))))=f(x,f(y,z)). 109 [para_from,105.1.1,104.1.1.2] f(f(x,f(y,f(x,z))),y)=f(y,f(x,z)). 110 [para_from,105.1.1,89.1.1.2.1] f(f(x,f(y,z)),f(x,f(u,f(y,x))))=f(f(x,f(y,z)),f(y,x)). 114 [para_into,109.1.2.2,93.1.2] f(f(x,f(y,f(x,z))),y)=f(y,f(z,x)). 115 [para_into,110.1.2,105.1.1] f(f(x,f(y,z)),f(x,f(u,f(y,x))))=x. 116 [para_into,114.1.1.1,86.1.1,flip.1] f(x,f(y,f(x,y)))=f(x,x). 117 [para_into,114.1.1,109.1.1] f(x,f(y,z))=f(x,f(z,y)). 118 [para_from,115.1.1,90.1.1.1,flip.1] f(x,f(y,f(x,f(z,f(y,x)))))=f(x,x). 119 [para_into,116.1.1.2.2,105.1.1] f(f(x,f(y,z)),f(f(y,x),x))=f(f(x,f(y,z)),f(x,f(y,z))). 120 [para_into,116.1.1,93.1.2] f(f(x,f(y,x)),y)=f(y,y). 121 [para_into,117.1.1,93.1.2] f(f(x,y),z)=f(z,f(y,x)). 122 [para_from,118.1.1,108.1.1.2,flip.1] f(x,f(y,f(z,f(x,y))))=f(x,f(y,y)). 123 [para_into,120.1.1.1.2,101.1.1] f(f(f(x,y),y),f(y,f(z,x)))=f(f(y,f(z,x)),f(y,f(z,x))). 125 [para_into,121.1.1,117.1.2] f(f(x,y),f(z,u))=f(f(u,z),f(y,x)). 126 [para_into,122.1.1.2.2,121.1.2] f(x,f(y,f(f(y,x),z)))=f(x,f(y,y)). 127 [para_into,122.1.1.2.2,88.1.1] f(x,f(y,x))=f(x,f(y,y)). 128 [para_into,127.1.1,93.1.2] f(f(x,y),y)=f(y,f(x,x)). 130 [para_from,127.1.1,117.1.1] f(x,f(y,y))=f(x,f(x,y)). 131 [para_from,128.1.1,123.1.1.1] f(f(x,f(y,y)),f(x,f(z,y)))=f(f(x,f(z,y)),f(x,f(z,y))). 132 [para_from,128.1.1,119.1.1.2] f(f(x,f(y,z)),f(x,f(y,y)))=f(f(x,f(y,z)),f(x,f(y,z))). 133 [para_from,130.1.1,122.1.1.2.2.2] f(x,f(f(y,y),f(z,f(x,f(x,y)))))=f(x,f(f(y,y),f(y,y))). 134 [para_from,132.1.1,106.1.1.1] f(f(f(x,f(y,z)),f(x,f(y,z))),f(y,y))=f(x,f(y,y)). 135 [para_into,133.1.2.2,95.1.1] f(x,f(f(y,y),f(z,f(x,f(x,y)))))=f(x,y). 136 [para_into,134.1.1.1.1,120.1.1] f(f(f(f(x,y),f(x,y)),f(f(z,f(f(x,y),z)),f(x,y))),f(x,x))=f(f(z,f(f(x,y),z)),f(x,x)). 137 [para_into,136.1.1.1,80.1.1,flip.1] f(f(x,f(f(y,z),x)),f(y,y))=f(f(y,z),f(y,y)). 138 [para_into,137.1.2,95.1.1] f(f(x,f(f(y,z),x)),f(y,y))=y. 141 [para_from,138.1.1,88.1.1.1] f(x,f(f(y,f(f(x,z),y)),x))=f(y,f(f(x,z),y)). 142 [para_into,141.1.1.2.1.2,114.1.1] f(x,f(f(y,f(y,f(z,x))),x))=f(y,f(f(x,f(y,f(x,z))),y)). 143 [para_into,142.1.2.2,114.1.1] f(x,f(f(y,f(y,f(z,x))),x))=f(y,f(y,f(z,x))). 144 [para_from,143.1.1,126.1.1.2.2] f(x,f(y,f(z,f(z,f(u,f(y,x))))))=f(x,f(y,y)). 145 [para_from,144.1.1,108.1.1.2,flip.1] f(x,f(y,f(y,f(z,f(x,y)))))=f(x,f(y,f(x,x))). 146 [para_into,145.1.2,83.1.1] f(x,f(y,f(y,f(z,f(x,y)))))=f(x,x). 147 [para_into,146.1.1.2.2.2,105.1.1] f(x,f(y,f(y,y)))=f(x,x). 149 [para_from,146.1.1,135.1.1.2.2] f(x,f(f(f(y,f(z,x)),f(y,f(z,x))),f(z,z)))=f(x,f(y,f(z,x))). 151 [para_into,149.1.1.2,134.1.1] f(x,f(y,f(z,z)))=f(x,f(y,f(z,x))). 152 [para_into,151.1.1.2.2,95.1.1,flip.1] f(x,f(y,f(f(z,z),x)))=f(x,f(y,z)). 155 [para_from,152.1.2,131.1.1.2] f(f(x,f(y,y)),f(x,f(z,f(f(y,y),x))))=f(f(x,f(z,y)),f(x,f(z,y))). 156 [para_into,155.1.1.2.2.2,121.1.1] f(f(x,f(y,y)),f(x,f(z,f(x,f(y,y)))))=f(f(x,f(z,y)),f(x,f(z,y))). 157 [para_into,156.1.1,151.1.2] f(f(x,f(y,y)),f(x,f(z,z)))=f(f(x,f(z,y)),f(x,f(z,y))). 158 [para_into,157.1.1,125.1.2] f(f(f(x,x),y),f(f(z,z),y))=f(f(y,f(x,z)),f(y,f(x,z))). 159 [hyper,158,2,95,147] $ANS("Sheffer"). ------------ end of proof -------------