----- Otter 3.1-b0, May 2000 ----- ----> UNIT CONFLICT at 7.15 sec ----> 7708 [binary,7707.1,1121.1] $Ans(Robbins_basis). Length of proof is 122. Level of proof is 43. ---------------- 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)+ ~(x+ ~(~z+ ~(z+u))))=z. 5 [para_into,3.1.1.1.1.1.1,3.1.1] ~(~(x+y)+ ~(~(~(z+u)+x)+ ~(~y+ ~(y+v))))=y. 7 [para_into,3.1.1.1.2,3.1.1] ~(~(~(~(~(~ ~x+y)+x)+z)+ ~x)+x)= ~x. 10,9 [para_into,7.1.1.1.1.1.1,3.1.1] ~(~(x+ ~x)+x)= ~x. 11 [para_from,7.1.1,3.1.1.1.1] ~(~x+ ~(~(~(~(~ ~x+y)+x)+z)+ ~(~x+ ~(x+u))))=x. 15 [para_from,9.1.1,3.1.1.1.1] ~(~x+ ~(x+ ~(~x+ ~(x+y))))=x. 21 [para_into,15.1.1.1.2.1.2,15.1.1] ~(~x+ ~(x+x))=x. 27 [para_from,15.1.1,3.1.1.1.2.1.2] ~(~(~(x+y)+z)+ ~(x+z))=z. 43 [para_into,5.1.1.1.2,9.1.1] ~(~(~ ~(~x+ ~(x+y))+x)+ ~ ~(~x+ ~(x+y)))=x. 45 [para_into,21.1.1.1.1,21.1.1] ~(x+ ~((~x+ ~(x+x))+ (~x+ ~(x+x))))= ~x+ ~(x+x). 47 [para_into,21.1.1.1.1,9.1.1] ~(~x+ ~((~(x+ ~x)+x)+ (~(x+ ~x)+x)))= ~(x+ ~x)+x. 52,51 [para_into,27.1.1.1.1.1.1,21.1.1] ~(~(x+y)+ ~(~x+y))=y. 56,55 [para_into,27.1.1.1.1,27.1.1] ~(x+ ~(~(y+z)+ ~(y+x)))= ~(y+x). 61 [para_into,27.1.1.1.2,27.1.1] ~(~(~(~(~(x+y)+z)+u)+ ~(x+z))+z)= ~(x+z). 69 [back_demod,2,demod,52,unit_del,1] B+A!=A+B| (A+B)+C!=A+ (B+C)|$Ans(Robbins_basis). 70 [para_from,27.1.1,3.1.1.1.2] ~(~(~(~(~(~x+y)+ ~(x+z))+u)+x)+ ~(x+z))=x. 74 [para_into,11.1.1.1.2.1.1.1.1.1.1,21.1.1] ~(~x+ ~(~(~(~x+x)+y)+ ~(~x+ ~(x+z))))=x. 87,86 [para_into,51.1.1.1.1,9.1.1] ~(~x+ ~(~ ~(x+ ~x)+x))=x. 112 [para_into,51.1.1.1.2,9.1.1] ~(~((x+ ~x)+x)+ ~x)=x. 116 [para_from,51.1.1,27.1.1.1.2] ~(~(~(~(x+y)+z)+ ~(~x+y))+y)= ~(~x+y). 120 [para_from,51.1.1,3.1.1.1.2] ~(~(~(~(x+ ~(x+y))+z)+x)+ ~(x+y))=x. 125,124 [para_from,51.1.1,27.1.1.1.1] ~(x+ ~(y+ ~(~y+x)))= ~(~y+x). 131,130 [para_from,51.1.1,27.1.1.1.1.1.1] ~(~(x+y)+ ~(~(z+x)+y))=y. 142 [para_from,112.1.1,27.1.1.1.1] ~(x+ ~((x+ ~x)+ ~x))= ~x. 177,176 [para_from,142.1.1,15.1.1.1.2.1.2.1.2,demod,125] ~(~x+ ~x)=x. 179,178 [para_from,142.1.1,27.1.1.1.1.1.1] ~(~(~x+y)+ ~(x+y))=y. 183,182 [para_into,176.1.1.1.1,176.1.1,demod,177] ~(x+x)= ~x+ ~x. 189,188 [para_into,176.1.1.1.1,51.1.1,demod,52,183,flip.1] ~(x+y)+ ~(~x+y)= ~y+ ~y. 199,198 [para_into,176.1.1.1.1,9.1.1,demod,10,183,flip.1] ~(x+ ~x)+x= ~ ~x+ ~ ~x. 209,208 [back_demod,176,demod,183] ~ ~x+ ~ ~x=x. 225,224 [back_demod,47,demod,199,209,199,209,183,199,209] ~(~x+ (~x+ ~x))=x. 227,226 [back_demod,45,demod,183,183,183,225,225,183] ~(x+ (x+x))= ~x+ (~x+ ~x). 228 [back_demod,21,demod,183,227,209] ~ ~x+x=x. 239,238 [back_demod,198,demod,209] ~(x+ ~x)+x=x. 253,252 [para_from,182.1.1,228.1.1.1.1,demod,183,209] x+ (x+x)=x+x. 267,266 [para_into,178.1.1.1.1.1,228.1.1] ~(~x+ ~(~x+x))=x. 271,270 [para_into,178.1.1.1.1,182.1.1,demod,209] ~(x+ ~(x+ ~x))= ~x. 284 [para_into,178.1.1.1.2,182.1.1] ~(~(~x+x)+ (~x+ ~x))=x. 290 [para_from,178.1.1,208.1.1.2.1,demod,179,flip.1] ~(~x+y)+ ~(x+y)= ~y+ ~y. 302 [para_from,266.1.1,208.1.1.2.1,demod,267,flip.1] ~x+ ~(~x+x)= ~x+ ~x. 339,338 [para_from,270.1.1,208.1.1.2.1,demod,271,209,flip.1] x+ ~(x+ ~x)=x. 403,402 [para_into,284.1.1.1.2,208.1.1] ~(~(~ ~x+ ~x)+x)= ~x. 417,416 [para_from,402.1.1,208.1.1.2.1,demod,403,209,flip.1] ~(~ ~x+ ~x)+x=x. 432 [para_from,86.1.1,302.1.1.1,demod,87,87,87] x+ ~(x+ (~x+ ~(~ ~(x+ ~x)+x)))=x+x. 437,436 [para_from,86.1.1,208.1.1.2.1,demod,87,flip.1] ~x+ ~(~ ~(x+ ~x)+x)= ~x+ ~x. 439,438 [back_demod,432,demod,437] x+ ~(x+ (~x+ ~x))=x+x. 443,442 [para_into,43.1.1.1.1.1.1.1.1.2.1,438.1.1,demod,183,253,183,209,439,183,253,183,209] ~(~(~x+x)+ ~x)=x. 460 [para_from,442.1.1,208.1.1.2.1,demod,443,flip.1] ~(~x+x)+ ~x= ~x+ ~x. 498 [para_into,130.1.1.1.2.1.1.1,252.1.1,demod,183] ~(~((x+x)+y)+ ~((~x+ ~x)+y))=y. 514 [para_from,130.1.1,460.1.1.2,demod,131,131,131] ~(x+ (~(y+x)+ ~(~(z+y)+x)))+x=x+x. 521,520 [para_from,130.1.1,208.1.1.2.1,demod,131,flip.1] ~(x+y)+ ~(~(z+x)+y)= ~y+ ~y. 522 [back_demod,514,demod,521] ~(x+ (~x+ ~x))+x=x+x. 530 [para_into,55.1.1.1.2.1.1.1,338.1.1] ~(x+ ~(~y+ ~(y+x)))= ~(y+x). 562 [para_into,55.1.1.1.2,182.1.1,demod,209] ~(x+ (y+x))= ~(y+x). 576 [para_from,55.1.1,208.1.1.2.1,demod,56,209,flip.1] x+ ~(~(y+z)+ ~(y+x))=y+x. 579,578 [para_into,562.1.1.1.2,416.1.1,demod,183,417] ~x+ ~x= ~x. 589,588 [back_demod,522,demod,579,239,flip.1] x+x=x. 590 [back_demod,520,demod,589] ~(x+y)+ ~(~(z+x)+y)= ~y. 593,592 [back_demod,498,demod,589,589,189,589] ~ ~x=x. 613,612 [back_demod,290,demod,589] ~(~x+y)+ ~(x+y)= ~y. 626 [back_demod,188,demod,589] ~(x+y)+ ~(~x+y)= ~y. 684 [para_into,592.1.1.1,562.1.1,demod,593,flip.1] x+ (y+x)=y+x. 702 [para_into,61.1.1.1.1.1.2.1,338.1.1,demod,339] ~(~(~(~(~(x+y)+ ~(x+ ~x))+z)+ ~x)+ ~(x+ ~x))= ~x. 706 [para_into,61.1.1.1.1,61.1.1] ~(~(x+ ~(~(x+y)+z))+z)= ~(~(x+y)+z). 750 [para_into,70.1.1.1.1.1.1.1,684.1.1] ~(~(~(x+ ~(~(~y+z)+ ~(y+u)))+y)+ ~(y+u))=y. 792 [para_from,612.1.1,684.1.1.2,demod,613] ~(x+y)+ ~y= ~y. 794 [para_into,792.1.1.2,592.1.1,demod,593] ~(x+ ~y)+y=y. 808 [para_into,74.1.1.1.2.1,792.1.1,demod,593] ~(~x+ (~x+ ~(x+y)))=x. 826 [para_into,626.1.1.1.1,338.1.1,demod,593] ~x+ ~(~x+ ~(x+ ~x))=x+ ~x. 906 [para_from,808.1.1,592.1.1.1,flip.1] ~x+ (~x+ ~(x+y))= ~x. 944 [para_from,116.1.1,592.1.1.1,demod,593,flip.1] ~(~(~(x+y)+z)+ ~(~x+y))+y= ~x+y. 967,966 [para_into,120.1.1.1.1.1,794.1.1] ~(~x+ ~(x+y))=x. 977,976 [back_demod,826,demod,967] ~x+x=x+ ~x. 992 [back_demod,530,demod,967] ~(x+y)= ~(y+x). 1020,1019 [para_from,120.1.1,794.1.1.1] x+ (x+y)=x+y. 1029 [back_demod,906,demod,1020] ~x+ ~(x+y)= ~x. 1042,1041 [para_from,992.1.1,794.1.1.1] ~(~x+y)+x=x. 1043 [para_from,992.1.1,626.1.1.2] ~(x+y)+ ~(y+ ~x)= ~y. 1045 [para_from,992.1.1,612.1.1.1] ~(x+ ~y)+ ~(y+x)= ~x. 1056 [para_from,992.1.1,592.1.1.1,demod,593] x+y=y+x. 1073 [para_from,992.1.1,626.1.1.1] ~(x+y)+ ~(~y+x)= ~x. 1079,1078 [para_into,1056.1.1,794.1.1,flip.1] x+ ~(y+ ~x)=x. 1080 [para_into,1056.1.1,792.1.1,flip.1] ~x+ ~(y+x)= ~x. 1084 [para_from,1056.1.1,69.2.1,unit_del,1056] C+ (A+B)!=A+ (B+C)|$Ans(Robbins_basis). 1121 [para_into,1084.1.1.2,1056.1.1] C+ (B+A)!=A+ (B+C)|$Ans(Robbins_basis). 1130 [para_into,1019.1.1,1056.1.1] (x+y)+x=x+y. 1136 [para_into,1041.1.1,1056.1.1] x+ ~(~x+y)=x. 1166 [para_from,1078.1.1,612.1.1.1.1,demod,593,593,593,593] x+ ~(x+ ~(y+x))=y+x. 1246 [para_into,1043.1.1.1.1,1080.1.1,demod,593,593,593] x+ ~(~(y+x)+x)=y+x. 1248 [para_into,1043.1.1.1.1,1056.1.1] ~(x+y)+ ~(x+ ~y)= ~x. 1282 [para_into,1045.1.1.2.1,1043.1.1,demod,593,593,593] ~(~(x+ ~y)+ (y+x))+x=x+ ~y. 1476 [para_from,1248.1.1,1073.1.1.2.1,demod,593,593] ~(~(x+ ~y)+ (x+y))+x=x+ ~y. 1504 [para_into,702.1.1.1.1.1,1056.1.1] ~(~(~x+ ~(~(~(x+y)+ ~(x+ ~x))+z))+ ~(x+ ~x))= ~x. 1539 [para_into,706.1.1.1.1.1,590.1.1,demod,593,589,flip.1] ~(~(~(x+y)+x)+y)= ~y. 1607 [para_from,1539.1.1,1166.1.1.2.1.2,demod,1079,flip.1] ~(~(x+y)+x)+y=y. 1659 [para_into,1607.1.1.1.1.1.1,1056.1.1] ~(~(x+y)+y)+x=x. 1679 [para_into,1607.1.1,1056.1.1] x+ ~(~(y+x)+y)=x. 1691 [para_into,1659.1.1.1.1,1056.1.1] ~(x+ ~(y+x))+y=y. 1860,1859 [para_into,1679.1.1.2.1.1.1,1136.1.1,demod,977] ~(~x+y)+ ~(x+ ~x)= ~(~x+y). 1866,1865 [para_into,1679.1.1.2.1.1.1,1080.1.1,demod,593] ~(x+y)+ ~(y+ ~y)= ~(x+y). 1878,1877 [para_into,1679.1.1.2.1.1.1,1029.1.1,demod,593] ~(x+y)+ ~(x+ ~x)= ~(x+y). 1892,1891 [back_demod,1504,demod,1878,593,1860,593] ~x+ ~((x+y)+z)= ~x. 1919 [para_into,1691.1.1.1.1.2.1,576.1.1] ~(~(~(x+y)+ ~(x+z))+ ~(x+z))+z=z. 1921 [para_into,1691.1.1,1056.1.1] x+ ~(y+ ~(x+y))=x. 2101 [para_into,750.1.1.1.1.1.1.1.2.1,1921.1.1,demod,593,1042,1866,593] ~(x+ (~y+z))+y=y. 2164,2163 [para_into,2101.1.1.1.1.2,1248.1.1] ~(x+ ~y)+ (y+z)=y+z. 2165 [para_into,2101.1.1.1.1.2,1246.1.1] ~(x+ (y+ ~z))+z=z. 2174,2173 [para_into,2101.1.1.1.1.2,1043.1.1] ~(x+ ~y)+ (z+y)=z+y. 2184,2183 [back_demod,1282,demod,2164] ~(x+y)+y=y+ ~x. 2190,2189 [back_demod,1476,demod,2174] ~(x+y)+x=x+ ~y. 2215 [back_demod,1919,demod,2184,593] ~(~(x+y)+ (x+z))+y=y. 2267 [para_from,2101.1.1,1043.1.1.2.1,demod,593,593,2190,593,593,593] x+ (y+ (x+z))=y+ (x+z). 2397 [para_into,2165.1.1.1.1,1130.1.1] ~((x+ ~y)+z)+y=y. 2404,2403 [para_from,2165.1.1,1043.1.1.2.1,demod,593,593,2190,593,593,593] x+ (y+ (z+x))=y+ (z+x). 2912 [para_into,2397.1.1,1056.1.1] x+ ~((y+ ~x)+z)=x. 3137,3136 [para_into,2912.1.1.2.1.1.2,592.1.1] ~x+ ~((y+x)+z)= ~x. 3783 [para_into,2215.1.1.1.1.1.1,1056.1.1] ~(~(x+y)+ (y+z))+x=x. 3853 [para_from,2215.1.1,944.1.1.1.1.1.1,demod,593,3137,593,593,flip.1] (x+y)+ (x+z)=y+ (x+z). 3883 [para_into,2267.1.1.2.2,1056.1.1,demod,2404] x+ (y+z)=x+ (z+y). 3935 [para_into,3883.1.1,1056.1.1] (x+y)+z=z+ (y+x). 3949 [copy,3935,flip.1] x+ (y+z)= (z+y)+x. 7306,7305 [para_from,3783.1.1,944.1.1.1.1.1.1,demod,593,1892,593,593,flip.1] (x+y)+ (y+z)=x+ (y+z). 7707 [para_into,3853.1.1,3949.1.1,demod,7306] x+ (y+z)=z+ (y+x). 7708 [binary,7707.1,1121.1] $Ans(Robbins_basis). ------------ end of proof -------------