----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 53.04 sec ----> 16772 [binary,16771.1,1.1] $Ans(Robbins_basis). Length of proof is 109. Level of proof is 37. ---------------- PROOF ---------------- 1 [] x=x. 2 [] B+A!=A+B| (A+B)+C!=A+ (B+C)| ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 3 [] ~(~(~(x+y)+z)+ ~(~(~z+ ~(u+z))+y))=z. 5 [para_into,3.1.1.1.1.1.1,3.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(~(~x+ ~(u+x))+v)))=y. 7 [para_into,5.1.1.1.2.1.2,5.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(u+x)))=y. 10,9 [para_into,5.1.1.1.2,5.1.1] ~(~(~(x+y)+y)+ ~(x+y))=y. 12,11 [para_into,9.1.1.1.1.1.1,9.1.1,demod,10] ~(~(x+ ~(y+x))+x)= ~(y+x). 15 [para_from,9.1.1,3.1.1.1.2.1.1.1.2] ~(~(~(x+y)+ ~(z+u))+ ~(~(~ ~(z+u)+u)+y))= ~(z+u). 19 [para_from,11.1.1,3.1.1.1.1] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ ~(x+y)))=y. 25 [para_into,7.1.1.1.2.1.2,3.1.1] ~(~(~(~(~x+ ~(y+x))+z)+u)+ ~(~(~u+ ~(v+u))+x))=u. 28,27 [para_into,7.1.1.1.2,7.1.1] ~(~(~(x+ ~y)+y)+ ~(z+y))=y. 31 [para_into,7.1.1.1.2,3.1.1] ~(~(x+ (y+x))+ ~(z+ (y+x)))=y+x. 38,37 [para_from,19.1.1,11.1.1.1.1,flip.1] ~(~(~x+ ~(y+x))+ ~(z+x))= ~(x+ ~(z+x)). 47 [back_demod,19,demod,38] ~(~(x+y)+ ~(y+ ~(x+y)))=y. 60,59 [para_into,47.1.1.1.1,27.1.1,demod,28] ~(x+ ~(~(y+x)+x))= ~(y+x). 75 [para_into,59.1.1,7.1.1,flip.1] ~(~x+ ~(x+x))=x. 105 [para_from,75.1.1,5.1.1.1.2.1.2] ~(~(x+y)+ ~(~(~y+ ~(z+y))+ (~x+ ~(u+x))))=y. 110,109 [para_from,75.1.1,7.1.1.1.2.1.1] ~(~(x+y)+ ~(y+ ~(z+x)))=y. 114,113 [para_from,75.1.1,3.1.1.1.2.1.1] ~(~(~(x+y)+z)+ ~(z+y))=z. 124,123 [para_into,15.1.1.1.1,27.1.1,demod,60] ~(~ ~(x+y)+y)= ~(x+y). 136,135 [para_into,123.1.1.1.1.1,27.1.1,demod,28] ~(~x+ ~(y+x))=x. 140,139 [para_into,123.1.1.1.1.1,7.1.1,demod,136,136,110] ~(~x+ ~(x+ ~(y+z)))=x. 141 [para_into,123.1.1.1.1.1,5.1.1,demod,136,136,140,136,136,flip.1] ~(~(x+y)+ ~(y+ ~(x+z)))=y. 144,143 [para_into,123.1.1.1.1.1,3.1.1,demod,136,136,114] ~(~x+ ~(x+y))=x. 149 [back_demod,105,demod,136] ~(~(x+y)+ ~(y+ (~x+ ~(z+x))))=y. 167 [back_demod,25,demod,136,136] ~(~(~(x+y)+z)+ ~(z+x))=z. 190,189 [para_into,143.1.1.1.2,143.1.1] ~(~ ~x+x)= ~x. 192,191 [para_into,143.1.1,31.1.1,flip.1] x+ (y+x)=y+x. 194,193 [para_into,143.1.1,27.1.1,flip.1] ~(x+ ~y)+y=y. 218,217 [para_from,189.1.1,135.1.1.1.2] ~(~x+ ~x)=x. 226,225 [para_into,217.1.1.1.1,217.1.1,demod,218] ~(x+x)= ~x+ ~x. 228,227 [para_into,217.1.1.1.1,189.1.1,demod,190,226] ~ ~x+ ~ ~x= ~ ~x+x. 229 [para_into,217.1.1.1.1,143.1.1,demod,144,226,flip.1] ~x+ ~(x+y)= ~x+ ~x. 232,231 [para_into,217.1.1.1.1,135.1.1,demod,136,226,flip.1] ~x+ ~(y+x)= ~x+ ~x. 234,233 [para_into,217.1.1.1.1,123.1.1,demod,124,226,228] ~ ~(x+y)+ (x+y)= ~ ~(x+y)+y. 235 [para_into,217.1.1.1.1,59.1.1,demod,60,226,228,234,flip.1] x+ ~(~(y+x)+x)= ~ ~(y+x)+x. 237 [para_into,217.1.1.1.1,11.1.1,demod,12,226,228,234,flip.1] ~(x+ ~(y+x))+x= ~ ~(y+x)+x. 239 [para_into,217.1.1.1.1,9.1.1,demod,10,226,flip.1] ~(~(x+y)+y)+ ~(x+y)= ~y+ ~y. 244,243 [back_demod,217,demod,226,228] ~ ~x+x=x. 253 [back_demod,149,demod,232] ~(~(x+y)+ ~(y+ (~x+ ~x)))=y. 260,259 [back_demod,233,demod,244,flip.1] ~ ~(x+y)+y=x+y. 261 [back_demod,227,demod,244] ~ ~x+ ~ ~x=x. 263 [back_demod,237,demod,260] ~(x+ ~(y+x))+x=y+x. 265 [back_demod,235,demod,260] x+ ~(~(y+x)+x)=y+x. 272,271 [para_into,191.1.1.2,243.1.1,demod,244] x+x=x. 274,273 [back_demod,261,demod,272] ~ ~x=x. 275 [back_demod,253,demod,272] ~(~(x+y)+ ~(y+ ~x))=y. 281 [back_demod,239,demod,272] ~(~(x+y)+y)+ ~(x+y)= ~y. 283 [back_demod,231,demod,272] ~x+ ~(y+x)= ~x. 286,285 [back_demod,229,demod,272] ~x+ ~(x+y)= ~x. 297 [para_into,283.1.1.1,273.1.1,demod,274] x+ ~(y+ ~x)=x. 315 [para_from,109.1.1,273.1.1.1,flip.1] ~(x+y)+ ~(y+ ~(z+x))= ~y. 318,317 [para_into,285.1.1.1,273.1.1,demod,274] x+ ~(~x+y)=x. 320,319 [para_from,285.1.1,297.1.1.2.1,demod,274] (x+y)+x=x+y. 323 [para_from,285.1.1,191.1.1.2,demod,286] ~(x+y)+ ~x= ~x. 325 [para_from,317.1.1,191.1.1.2,demod,318] ~(~x+y)+x=x. 327 [para_into,113.1.1.1.1.1.1.1,271.1.1] ~(~(~x+y)+ ~(y+x))=y. 344,343 [para_from,113.1.1,273.1.1.1,flip.1] ~(~(x+y)+z)+ ~(z+y)= ~z. 375 [para_from,141.1.1,263.1.1.1.1.2,demod,344,flip.1] ~(x+y)+ ~(y+ ~(x+z))= ~y. 382,381 [para_into,265.1.1.2.1.1.1,285.1.1,demod,274,286] ~(x+y)+ ~(x+ ~(x+y))= ~x. 384,383 [para_into,265.1.1.2.1,325.1.1,flip.1] ~x+x=x+ ~x. 391 [para_from,275.1.1,265.1.1.2.1.1,demod,382,flip.1] ~(x+y)+ ~(y+ ~x)= ~y. 403 [para_from,327.1.1,265.1.1.2.1.1,demod,382,flip.1] ~(~x+y)+ ~(y+x)= ~y. 431 [para_from,167.1.1,265.1.1.2.1.1,demod,382,flip.1] ~(~(x+y)+z)+ ~(z+x)= ~z. 435 [para_into,391.1.1.2.1,391.1.1,demod,274,274] ~((x+ ~y)+ ~(y+x))+x=y+x. 463 [para_into,315.1.1.1.1,319.1.1] ~(x+y)+ ~(x+ ~(z+ (x+y)))= ~x. 465 [para_into,315.1.1.1.1,317.1.1,demod,274] ~x+ ~(~(~x+y)+ ~(z+x))= ~x+y. 467 [para_into,315.1.1.1.1,315.1.1,demod,274,274] x+ ~(~(x+ ~(y+z))+ ~(u+ ~(z+x)))=x+ ~(y+z). 477 [para_into,315.1.1.1.1,283.1.1,demod,274,274] x+ ~(~(y+x)+ ~(z+ ~x))=y+x. 489 [para_from,315.1.1,403.1.1.1.1,demod,274,274] x+ ~(~(x+ ~(y+z))+ (z+x))=x+ ~(y+z). 491 [para_from,315.1.1,391.1.1.2.1,demod,274,274] ~((x+ ~(y+z))+ ~(z+x))+x=z+x. 507 [para_into,343.1.1.2.1,323.1.1,demod,274,274] ~(~(x+ ~y)+ ~(y+z))+y=y+z. 591 [para_into,431.1.1.1.1,431.1.1,demod,274,274] x+ ~(~(x+y)+ ~(y+z))=x+y. 593 [para_into,431.1.1.1.1,375.1.1,demod,274,274] x+ ~(~(x+ ~(y+z))+y)=x+ ~(y+z). 647 [para_into,435.1.1.1.1.1,391.1.1] ~(~x+ ~((x+ ~y)+ ~(y+x)))+ ~(y+x)= (x+ ~y)+ ~(y+x). 801 [para_from,591.1.1,343.1.1.2.1] ~(~(x+ ~(~(y+z)+ ~(z+u)))+y)+ ~(y+z)= ~y. 966,965 [para_into,477.1.1.2.1,325.1.1,demod,274,274,flip.1] (x+ ~y)+y=y+ (x+ ~y). 1010 [para_into,965.1.1.1,319.1.1,demod,320] (~x+y)+x=x+ (~x+y). 1151 [para_from,1010.1.1,315.1.1.1.1] ~(x+ (~x+y))+ ~(x+ ~(z+ (~x+y)))= ~x. 1190,1189 [para_into,507.1.1.1.1,463.1.1,demod,274,272,flip.1] x+ ~(y+ (x+ ~x))=x. 1208,1207 [para_into,1189.1.1.2.1.2.2,273.1.1,demod,384] ~x+ ~(y+ (x+ ~x))= ~x. 1262,1261 [para_from,1189.1.1,281.1.1.2.1,demod,1190,1208,274,274,flip.1] x+ (y+ ~y)=y+ ~y. 1285 [para_from,1261.1.1,465.1.1.2.1.1.1,demod,1262] ~x+ ~(~(y+ ~y)+ ~(z+x))=y+ ~y. 1288,1287 [para_from,1261.1.1,325.1.1.1.1] ~(x+ ~x)+y=y. 1290,1289 [para_from,1261.1.1,317.1.1.2.1] x+ ~(y+ ~y)=x. 1291 [para_from,1261.1.1,507.1.1.1.1.2.1,demod,1290,274,966,1262] x+ (y+ ~x)=z+ ~z. 1293 [back_demod,1285,demod,1288,274] ~x+ (y+x)=z+ ~z. 1299,1298 [para_from,1287.1.1,591.1.1.2.1,demod,274] x+ (~x+y)=x+ ~x. 1301 [para_from,1287.1.1,431.1.1.2.1,demod,1290,274,274] (x+y)+ ~x=z+ ~z. 1306,1305 [back_demod,1151,demod,1299,1288] ~(x+ ~(y+ (~x+z)))= ~x. 1319 [back_demod,1010,demod,1299] (~x+y)+x=x+ ~x. 1378,1377 [para_from,1291.1.1,375.1.1.1.1,demod,1288] ~((x+ ~y)+ ~(y+z))= ~(x+ ~y). 1419 [back_demod,647,demod,1378,286,274,flip.1] (x+ ~y)+ ~(y+x)=x+ ~(y+x). 1453,1452 [para_from,1293.1.1,343.1.1.2.1,demod,1290,274] ~(~(x+ (y+z))+ ~z)=z. 1647,1646 [para_from,1301.1.1,375.1.1.1.1,demod,1288,274] ~(~x+ ~((x+y)+z))=x. 1680 [para_from,1319.1.1,467.1.1.2.1.2.1.2.1,demod,1306,1290,318,flip.1] x+ ~(y+ (~x+z))=x. 1775 [para_from,489.1.1,391.1.1.1.1,demod,1453,274,flip.1] ~(x+ ~(y+z))+ (z+x)= ~(x+ ~(y+z))+x. 1841 [para_from,491.1.1,403.1.1.2.1,demod,1647,274,flip.1] (x+ ~(y+z))+ ~(z+x)=x+ ~(z+x). 1879 [para_into,1680.1.1.2.1,507.1.1] x+ ~((~x+y)+z)=x. 2073,2072 [para_into,1879.1.1.2.1.1,193.1.1] (x+ ~y)+ ~(y+z)=x+ ~y. 2081,2080 [back_demod,1419,demod,2073,flip.1] x+ ~(y+x)=x+ ~y. 2085,2084 [back_demod,1841,demod,2081] (x+ ~(y+z))+ ~(z+x)=x+ ~z. 2091,2090 [back_demod,263,demod,2081] ~(x+ ~y)+x=y+x. 2092 [back_demod,1775,demod,2091] ~(x+ ~(y+z))+ (z+x)= (y+z)+x. 14574 [para_from,2084.1.1,593.1.1.2.1.1.1,demod,194,2085] (x+ ~(y+z))+ ~z=x+ ~z. 14869,14868 [para_into,14574.1.1.1.2.1,801.1.1,demod,274,274,274] (x+y)+ (y+z)=x+ (y+z). 14991,14990 [para_into,14574.1.1.1,315.1.1,demod,274,274,flip.1] ~(x+y)+ (z+x)= ~y+ (z+x). 15093,15092 [back_demod,2092,demod,14991,274,14869,flip.1] (x+y)+z=x+ (y+z). 15935 [back_demod,319,demod,15093,192] x+y=y+x. 15936 [back_demod,2,demod,15093,unit_del,15935,1] ~(~(A+B)+ ~(~A+B))!=B|$Ans(Robbins_basis). 16666,16665 [para_from,15935.1.1,403.1.1.2.1] ~(~x+y)+ ~(x+y)= ~y. 16771 [para_from,15935.1.1,15936.1.1.1,demod,16666,274] B!=B|$Ans(Robbins_basis). 16772 [binary,16771.1,1.1] $Ans(Robbins_basis). ------------ end of proof -------------