Length of proof is 142. Level of proof is 70. ---------------- PROOF ---------------- 2 [] x+y=y+x # label("commutativity"). 3 [] (x+y)+z=x+y+z # label("associativity"). 4 [] n(n(n(x)+y)+n(x+y))=y # label("Robbins"). 5 [] n(n(A)+B)+n(n(A)+n(B))!=A # label("denial of Huntington"). 152 [para_into,3.1.1.1,2.1.2] (x+y)+z=y+x+z # label("Hint 5(153)"). 153 [para_into,3.1.2.2,3.1.1] (x+y+z)+u=x+y+z+u # label("Hint 6(155)"). 154 [para_from,3.1.1,2.1.1] x+y+z=z+x+y # label("Hint 7(156)"). 155 [para_into,4.1.1.1.1.1,2.1.2] n(n(x+n(y))+n(y+x))=x # label("Hint 8(157)"). 156 [para_into,4.1.1.1.2.1,3.1.1] n(n(n(x+y)+z)+n(x+y+z))=z # label("Hint 9(158)"). 157 [para_into,4.1.1.1.2.1,2.1.2] n(n(n(x)+y)+n(y+x))=y # label("Hint 10(159)"). 158 [para_into,4.1.1.1,2.1.2] n(n(x+y)+n(n(x)+y))=y # label("Hint 11(160)"). 159 [para_into,152.1.1,3.1.1] x+y+z=y+x+z # label("Hint 12(161)"). 160 [para_into,152.1.1,2.1.2] x+y+z=z+y+x # label("Hint 13(162)"). 161 [para_into,154.1.1.2,3.1.1] x+y+z+u=u+x+y+z # label("Hint 14(163)"). 162 [para_from,159.1.1,4.1.1.1.1.1] n(n(x+n(y)+z)+n(y+x+z))=x+z # label("Hint 15(164)"). 163 [para_into,155.1.1.1.2.1,159.1.2] n(n((x+y)+n(z))+n(x+z+y))=x+y # label("Hint 16(165)"). 164 [para_into,155.1.1.1.2.1,152.1.1] n(n(x+n(y+z))+n(z+y+x))=x # label("Hint 17(166)"). 165 [para_into,155.1.1.1.2.1,3.1.1] n(n(x+n(y+z))+n(y+z+x))=x # label("Hint 18(167)"). 166 [para_into,155.1.1.1.2.1,2.1.2] n(n(x+n(y))+n(x+y))=x # label("Hint 19(168)"). 167 [para_into,155.1.1.1,2.1.2] n(n(x+y)+n(y+n(x)))=y # label("Hint 20(169)"). 168 [para_into,157.1.1.1.1.1.1,4.1.1] n(n(x+y)+n(y+n(n(z)+x)+n(z+x)))=y # label("Hint 21(170)"). 169 [para_into,157.1.1.1,2.1.2] n(n(x+y)+n(n(y)+x))=x # label("Hint 22(171)"). 170 [para_into,158.1.1.1.1.1,3.1.1] n(n(x+y+z)+n(n(x+y)+z))=z # label("Hint 23(172)"). 171 [para_into,166.1.1.1.2.1,154.1.1] n(n(x+n(y+z))+n(z+x+y))=x # label("Hint 24(173)"). 172 [para_into,166.1.1.1,2.1.2] n(n(x+y)+n(x+n(y)))=x # label("Hint 25(174)"). 173 [para_into,167.1.1.1.1.1,160.1.2] n(n(x+y+z)+n((y+x)+n(z)))=y+x # label("Hint 26(175)"). 174 [para_into,169.1.1.1.2.1.1,167.1.1] n(n(x+n(y+z)+n(z+n(y)))+n(z+x))=x # label("Hint 27(176)"). 175 [para_into,169.1.1.1.2,169.1.1] n(n(n(n(x)+y)+y+x)+y)=n(n(x)+y) # label("Hint 28(177)"). 176 [para_into,169.1.1.1.2,158.1.1] n(n(n(n(x)+y)+x+y)+y)=n(n(x)+y) # label("Hint 29(178)"). 177 [para_into,172.1.1.1.2.1.2,172.1.1] n(n(x+n(y+z)+n(y+n(z)))+n(x+y))=x # label("Hint 30(179)"). 178 [para_from,172.1.1,166.1.1.1.1.1.2] n(n(x+y)+n(x+n(y+z)+n(y+n(z))))=x # label("Hint 31(180)"). 179 [para_from,153.1.1,4.1.1.1.2.1] n(n(n(x+y+z)+u)+n(x+y+z+u))=u # label("Hint 32(181)"). 180 [para_into,156.1.1.1.1,169.1.1] n(x+n(x+y+n(n(y)+x)))=n(n(y)+x) # label("Hint 33(182)"). 181 [para_into,156.1.1.1.1,158.1.1] n(x+n(y+x+n(n(y)+x)))=n(n(y)+x) # label("Hint 34(183)"). 182 [para_from,162.1.1,169.1.1.1.2] n(n(n(x+y+z)+y+n(x)+z)+y+z)=n(x+y+z) # label("Hint 35(184)"). 183 [para_into,163.1.1.1.1.1,3.1.1] n(n(x+y+n(z))+n(x+z+y))=x+y # label("Hint 36(185)"). 184 [para_into,173.1.1.1.2.1,3.1.1] n(n(x+y+z)+n(y+x+n(z)))=y+x # label("Hint 37(186)"). 185 [para_into,175.1.1.1.1.1.2,161.1.2] n(n(n(n(x+y+z)+u)+x+y+z+u)+u)=n(n(x+y+z)+u) # label("Hint 38(187)"). 186 [para_from,176.1.1,170.1.1.1.2] n(n(n(n(x)+y)+ (x+y)+y)+n(n(x)+y))=y # label("Hint 39(188)"). 187 [para_into,183.1.1.1.1.1,154.1.2] n(n(x+n(y)+z)+n(z+y+x))=z+x # label("Hint 40(189)"). 188 [para_into,168.1.1.1.2.1.2.1,175.1.1] n(n(x+y)+n(y+n(n(z)+x)+n((n(n(z)+x)+x+z)+x)))=y # label("Hint 41(190)"). 189 [para_into,178.1.1.1.2.1.2.2,155.1.1] n(n(x+n(y+n(z)))+n(x+n(n(y+n(z))+z+y)+y))=x # label("Hint 42(191)"). 190 [para_into,179.1.1.1.2.1.2.2,153.1.1] n(n(n(x+y+z+u+v)+w)+n(x+y+z+u+v+w))=w # label("Hint 43(192)"). 191 [para_into,186.1.1.1.1.1.2,3.1.1] n(n(n(n(x)+y)+x+y+y)+n(n(x)+y))=y # label("Hint 44(193)"). 192 [para_from,191.1.1,170.1.1.1.2.1.1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z)+n(y+z))=z # label("Hint 45(194)"). 193 [para_into,182.1.1.1.1.1.1.1,159.1.2] n(n(n(x+y+z)+x+n(y)+z)+x+z)=n(y+x+z) # label("Hint 46(195)"). 194 [para_into,193.1.1.1.2,2.1.2] n(n(n(x+y+z)+x+n(y)+z)+z+x)=n(y+x+z) # label("Hint 47(196)"). 195 [para_into,189.1.1.1.2.1.2.1.1,154.1.2] n(n(x+n(y+n(z)))+n(x+n(z+y+n(y+n(z)))+y))=x # label("Hint 48(197)"). 196 [para_into,195.1.1.1.2.1.2,2.1.2] n(n(x+n(y+n(z)))+n(x+y+n(z+y+n(y+n(z)))))=x # label("Hint 49(198)"). 197 [para_into,188.1.1.1.2.1.2.2.1,153.1.1] n(n(x+y)+n(y+n(n(z)+x)+n(n(n(z)+x)+x+z+x)))=y # label("Hint 50(199)"). 198 [para_from,192.1.1,170.1.1.1.2] n(n(n(n(n(x)+y)+x+y+y)+ (n(n(x)+y)+z)+n(y+z))+z)=n(y+z) # label("Hint 51(200)"). 199 [para_into,197.1.1.1.1.1,2.1.2] n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+z+y)))=x # label("Hint 52(201)"). 200 [para_into,199.1.1.1.2.1.2.2.1.2.2,2.1.2] n(n(x+y)+n(x+n(n(z)+y)+n(n(n(z)+y)+y+y+z)))=x # label("Hint 53(202)"). 201 [para_into,198.1.1.1.1.1.2,3.1.1] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+z+n(y+z))+z)=n(y+z) # label("Hint 54(203)"). 202 [para_into,201.1.1.1.1.1.2.2,2.1.2] n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z)=n(y+z) # label("Hint 55(204)"). 203 [para_from,202.1.1,170.1.1.1.2.1.1] n(n(n(n(n(n(x)+y)+x+y+y)+n(n(x)+y)+n(y+z)+z)+z+u)+n(n(y+z)+u))=u # label("Hint 56(205)"). 204 [para_into,203.1.1.1.1,194.1.1] n(n((x+x+x)+n(n(x+x+x)+x)+x+x)+n(n(x+x+x)+n(n(x+x+x)+x)))=n(n(x+x+x)+x) # label("Hint 57(206)"). 205 [para_into,204.1.1.1.1.1,153.1.1] n(n(x+x+x+n(n(x+x+x)+x)+x+x)+n(n(x+x+x)+n(n(x+x+x)+x)))=n(n(x+x+x)+x) # label("Hint 58(207)"). 206 [para_from,205.1.1,165.1.1.1.1] n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(x+x+x+n(n(x+x+x)+x)+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 59(208)"). 207 [para_into,206.1.1.1.2.1.2.2.1,161.1.1] n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n((n(n(x+x+x)+x)+x+x)+x+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 60(209)"). 208 [para_into,207.1.1.1.2.1.2.2.1,153.1.1] n(n(n(x+x+x)+x)+n(n(x+x+x)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+x+x+x+x+x)))=n(x+x+x+n(n(x+x+x)+x)+x+x) # label("Hint 61(210)"). 209 [para_into,208.1.1,200.1.1,flip.1] n(x+x+x+n(n(x+x+x)+x)+x+x)=n(x+x+x) # label("Hint 62(211)"). 210 [para_into,209.1.1.1,161.1.1] n((n(n(x+x+x)+x)+x+x)+x+x+x)=n(x+x+x) # label("Hint 63(212)"). 211 [para_from,209.1.1,179.1.1.1.2] n(n(n(x+x+x)+n(n(x+x+x)+x)+x+x)+n(x+x+x))=n(n(x+x+x)+x)+x+x # label("Hint 64(213)"). 212 [para_into,210.1.1.1,153.1.1] n(n(n(x+x+x)+x)+x+x+x+x+x)=n(x+x+x) # label("Hint 65(214)"). 213 [para_from,212.1.1,190.1.1.1.2] n(n(n(n(n(x+x+x)+x)+x+x+x+x)+x)+n(x+x+x))=x # label("Hint 66(215)"). 214 [para_into,213.1.1.1.1,185.1.1] n(n(n(x+x+x)+x)+n(x+x+x))=x # label("Hint 67(216)"). 215 [para_from,214.1.1,170.1.1.1.2.1.1] n(n(n(n(x+x+x)+x)+n(x+x+x)+y)+n(x+y))=y # label("Hint 68(217)"). 216 [para_into,215.1.1.1.1.1,159.1.2] n(n(n(x+x+x)+n(n(x+x+x)+x)+y)+n(x+y))=y # label("Hint 69(218)"). 217 [para_into,211.1.1,216.1.1,flip.1] n(n(x+x+x)+x)+x+x=x+x # label("Hint 70(219)"). 218 [para_into,217.1.1,2.1.2] (x+x)+n(n(x+x+x)+x)=x+x # label("Hint 71(220)"). 219 [para_from,217.1.1,164.1.1.1.2.1.2] n(n((x+x)+n(n(n(x+x+x)+x)+y))+n(y+x+x))=x+x # label("Hint 72(221)"). 220 [para_from,217.1.1,171.1.1.1.2.1.2] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x))=n(n(x+x+x)+x) # label("Hint 73(222)"). 221 [para_from,217.1.1,172.1.1.1.1.1] n(n(x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n(n(x+x+x)+x) # label("Hint 74(223)"). 222 [para_from,217.1.1,152.1.1.1,flip.1] (x+x)+n(n(x+x+x)+x)+y= (x+x)+y # label("Hint 75(224)"). 223 [para_from,217.1.1,3.1.1.1,flip.1] n(n(x+x+x)+x)+ (x+x)+y= (x+x)+y # label("Hint 76(225)"). 224 [para_from,218.1.1,174.1.1.1.2.1] n(n(n(n(x+x+x)+x)+n(y+x+x)+n((x+x)+n(y)))+n(x+x))=n(n(x+x+x)+x) # label("Hint 77(226)"). 225 [para_from,222.1.1,164.1.1.1.2.1.2] n(n((n(n(x+x+x)+x)+y)+n((x+x)+z))+n(z+ (x+x)+y))=n(n(x+x+x)+x)+y # label("Hint 78(227)"). 226 [para_from,223.1.1,172.1.1.1.1.1] n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y)))=n(n(x+x+x)+x) # label("Hint 79(228)"). 227 [para_from,221.1.1,4.1.1.1.1] n(n(n(x+x+x)+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x))))=n(n(n(x+x+x)+x)+n(x+x)) # label("Hint 80(229)"). 228 [para_from,220.1.1,167.1.1.1.2.1.2] n(n((n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x))+z)+n(z+n(n(x+x+x)+x)))=z # label("Hint 81(230)"). 229 [para_from,226.1.1,196.1.1.1.1] n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 82(231)"). 230 [para_from,226.1.1,180.1.1.1.2.1.2.2] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+ ((x+x)+y)+n(n(x+x+x)+x)))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 83(232)"). 231 [para_into,225.1.1.1.1.1,3.1.1] n(n(n(n(x+x+x)+x)+y+n((x+x)+z))+n(z+ (x+x)+y))=n(n(x+x+x)+x)+y # label("Hint 84(233)"). 232 [para_into,228.1.1.1.1.1,3.1.1] n(n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(y+x+x)+z)+n(z+n(n(x+x+x)+x)))=z # label("Hint 85(234)"). 233 [para_from,227.1.1,219.1.1.1.1.1.2] n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+x+x))=x+x # label("Hint 86(235)"). 234 [para_into,233.1.1.1.2.1,2.1.2] n(n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))+n((x+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))))=x+x # label("Hint 87(236)"). 235 [para_into,229.1.1.1.2.1.2.2.1,159.1.2] n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+ ((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 88(237)"). 236 [para_into,235.1.1.1.2.1.2.2.1.2,3.1.1] n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+ (x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 89(238)"). 237 [para_into,236.1.1.1.2.1.2.2.1,223.1.1] n(n(n(x+x+x)+x)+n(n((x+x)+y)+n(n(x+x+x)+x)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 90(239)"). 238 [para_into,237.1.1.1.2.1,159.1.2] n(n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y) # label("Hint 91(240)"). 239 [para_into,230.1.1.1.2.1.2,2.1.2] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(x+x+x)+x)+ (x+x)+y))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 92(241)"). 240 [para_into,239.1.1.1.2.1.2,223.1.1] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n(n(n(n(x+x+x)+x)+n((x+x)+y))+ (x+x)+y))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 93(242)"). 241 [para_into,240.1.1.1.2.1,154.1.2] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))))=n(n((x+x)+y)+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 94(243)"). 242 [para_into,241.1.2,226.1.1] n(n(n(n(x+x+x)+x)+n((x+x)+y))+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))))=n(n(x+x+x)+x) # label("Hint 95(244)"). 244 [para_from,242.1.1,156.1.1.1.1] n(n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n((x+x)+y)+n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))))=n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y))) # label("Hint 96(246)"). 245 [para_into,244.1.1,238.1.1,flip.1] n((x+x)+y+n(n(n(x+x+x)+x)+n((x+x)+y)))=n((x+x)+y) # label("Hint 97(247)"). 246 [para_into,245.1.1.1.2.2.1.2.1,218.1.1] n((x+x)+n(n(x+x+x)+x)+n(n(n(x+x+x)+x)+n(x+x)))=n((x+x)+n(n(x+x+x)+x)) # label("Hint 98(248)"). 247 [para_into,246.1.1.1,222.1.1] n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n((x+x)+n(n(x+x+x)+x)) # label("Hint 99(249)"). 248 [para_into,247.1.2.1,218.1.1] n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))=n(x+x) # label("Hint 100(250)"). 249 [para_from,248.1.1,234.1.1.1.1] n(n(x+x)+n((x+x)+n((x+x)+n(n(n(x+x+x)+x)+n(x+x)))))=x+x # label("Hint 101(251)"). 250 [para_into,249.1.1.1.2.1.2,248.1.1] n(n(x+x)+n((x+x)+n(x+x)))=x+x # label("Hint 102(252)"). 251 [para_from,250.1.1,196.1.1.1.1] n((x+x)+n(n(x+x)+ (x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n(x+x) # label("Hint 103(253)"). 252 [para_from,250.1.1,181.1.1.1.2.1.2.2] n(n((x+x)+n(x+x))+n((x+x)+n((x+x)+n(x+x))+x+x))=n(n(x+x)+n((x+x)+n(x+x))) # label("Hint 104(254)"). 253 [para_into,251.1.1.1.2.1,159.1.2] n((x+x)+n((x+x)+n(x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n(x+x) # label("Hint 105(255)"). 254 [para_into,252.1.1.1.2.1.2,2.1.2] n(n((x+x)+n(x+x))+n((x+x)+ (x+x)+n((x+x)+n(x+x))))=n(n(x+x)+n((x+x)+n(x+x))) # label("Hint 106(256)"). 255 [para_into,254.1.2,250.1.1] n(n((x+x)+n(x+x))+n((x+x)+ (x+x)+n((x+x)+n(x+x))))=x+x # label("Hint 107(257)"). 256 [para_from,255.1.1,156.1.1.1.1] n((x+x)+n((x+x)+n(x+x)+n((x+x)+ (x+x)+n((x+x)+n(x+x)))))=n((x+x)+ (x+x)+n((x+x)+n(x+x))) # label("Hint 108(258)"). 257 [para_into,256.1.1,253.1.1,flip.1] n((x+x)+ (x+x)+n((x+x)+n(x+x)))=n(x+x) # label("Hint 109(259)"). 258 [para_from,257.1.1,231.1.1.1.2] n(n(n(n(x+x+x)+x)+n((x+x)+n(x+x))+n((x+x)+x+x))+n(x+x))=n(n(x+x+x)+x)+n((x+x)+n(x+x)) # label("Hint 110(260)"). 259 [para_into,258.1.1.1.1.1.2,2.1.2] n(n(n(n(x+x+x)+x)+n((x+x)+x+x)+n((x+x)+n(x+x)))+n(x+x))=n(n(x+x+x)+x)+n((x+x)+n(x+x)) # label("Hint 111(261)"). 260 [para_into,259.1.1,224.1.1,flip.1] n(n(x+x+x)+x)+n((x+x)+n(x+x))=n(n(x+x+x)+x) # label("Hint 112(262)"). 262 [para_from,260.1.1,232.1.1.1.1.1.1.1] n(n(n(n(n(x+x+x)+x))+n(n(x+x)+x+x)+y)+n(y+n(n(x+x+x)+x)))=y # label("Hint 113(264)"). 263 [para_from,260.1.1,187.1.1.1.2.1.2] n(n(n((x+x)+n(x+x))+n(n(n(x+x+x)+x))+y)+n(y+n(n(x+x+x)+x)))=y+n((x+x)+n(x+x)) # label("Hint 114(265)"). 264 [para_into,262.1.1.1.1.1.2.1.1,2.1.2] n(n(n(n(n(x+x+x)+x))+n((x+x)+n(x+x))+y)+n(y+n(n(x+x+x)+x)))=y # label("Hint 115(266)"). 265 [para_into,263.1.1.1.1.1,159.1.2] n(n(n(n(n(x+x+x)+x))+n((x+x)+n(x+x))+y)+n(y+n(n(x+x+x)+x)))=y+n((x+x)+n(x+x)) # label("Hint 116(267)"). 266 [para_into,265.1.1,264.1.1,flip.1] x+n((y+y)+n(y+y))=x # label("Hint 112(262)"). 267 [para_into,266.1.1,2.1.2] n((x+x)+n(x+x))+y=y # label("Hint 118(269)"). 269 [para_from,266.1.1,155.1.1.1.2.1] n(n(n((x+x)+n(x+x))+n(y))+n(y))=n((x+x)+n(x+x)) # label("Hint 119(271)"). 270 [para_from,266.1.1,172.1.1.1.1.1] n(n(x)+n(x+n(n((y+y)+n(y+y)))))=x # label("Hint 120(272)"). 271 [para_from,267.1.1,183.1.1.1.2.1.2] n(n(x+y+n(n((z+z)+n(z+z))))+n(x+y))=x+y # label("Hint 121(273)"). 273 [para_from,270.1.1,171.1.1.1.1.1.2] n(n(x+y)+n(n(y+n(n((z+z)+n(z+z))))+x+n(y)))=x # label("Hint 122(275)"). 274 [para_from,270.1.1,164.1.1.1.1] n(x+n(n(n((y+y)+n(y+y)))+x+n(x)))=n(x) # label("Hint 123(276)"). 275 [para_from,274.1.1,165.1.1.1.1] n(n(x)+n(n(n((y+y)+n(y+y)))+ (x+n(x))+x))=x # label("Hint 124(277)"). 276 [para_from,274.1.1,4.1.1.1.2] n(n(n(x)+n(n(n((y+y)+n(y+y)))+x+n(x)))+n(x))=n(n(n((y+y)+n(y+y)))+x+n(x)) # label("Hint 125(278)"). 277 [para_into,275.1.1.1.2.1.2,266.1.1] n(n(n((x+x)+n(x+x)))+n(n(n((y+y)+n(y+y)))+n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))))=n((x+x)+n(x+x)) # label("Hint 126(279)"). 278 [para_from,269.1.1,172.1.1.1.2.1.2] n(n(x+n(n((y+y)+n(y+y))+n(z))+n(z))+n(x+n((y+y)+n(y+y))))=x # label("Hint 127(280)"). 279 [para_into,278.1.1.1.2.1,267.1.1] n(n(n((x+x)+n(x+x))+n(n((y+y)+n(y+y))+n(z))+n(z))+n(n((y+y)+n(y+y))))=n((x+x)+n(x+x)) # label("Hint 128(281)"). 280 [para_from,277.1.1,276.1.1.1.1,flip.1] n(n(n((x+x)+n(x+x)))+n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y)))) # label("Hint 129(282)"). 281 [para_from,280.1.1,274.1.1.1.2] n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))))=n(n((x+x)+n(x+x))) # label("Hint 130(283)"). 282 [para_from,281.1.1,271.1.1.1.2] n(n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+n(n((y+y)+n(y+y))))+n(n((x+x)+n(x+x))))=n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x)))) # label("Hint 131(284)"). 283 [para_into,282.1.1,279.1.1,flip.1] n((x+x)+n(x+x))+n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))=n((x+x)+n(x+x)) # label("Hint 132(285)"). 284 [para_into,283.1.1,2.1.2] n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+n((x+x)+n(x+x))=n((x+x)+n(x+x)) # label("Hint 133(286)"). 285 [para_from,284.1.1,184.1.1.1.1.1.2] n(n(x+n((y+y)+n(y+y)))+n(n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x+n(n((y+y)+n(y+y)))))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x # label("Hint 134(287)"). 286 [para_into,285.1.1,273.1.1,flip.1] n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))+y=y # label("Hint 133(286)"). 290 [para_from,286.1.1,177.1.1.1.1.1] n(n(n(x+y)+n(x+n(y)))+n(n(n((z+z)+n(z+z))+n(n((z+z)+n(z+z))))+x))=n(n((z+z)+n(z+z))+n(n((z+z)+n(z+z)))) # label("Hint 136(292)"). 292 [para_into,290.1.1.1.1,172.1.1] n(x+n(n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y))))+x))=n(n((y+y)+n(y+y))+n(n((y+y)+n(y+y)))) # label("Hint 137(294)"). 293 [para_into,292.1.1.1.2.1,286.1.1,flip.1] n(n((x+x)+n(x+x))+n(n((x+x)+n(x+x))))=n(y+n(y)) # label("Hint 138(295)"). 294 [para_into,293.1.1,293.1.1] n(x+n(x))=n(y+n(y)) # label("Hint 138(295)"). 345 [para_from,294.1.1,157.1.1.1.2] n(n(n(n(x))+x)+n(y+n(y)))=x # label("Hint 140(347)"). 347 [para_into,345.1.1,169.1.1] n(n(x))=x # label("Hint 141(349)"). 348 [para_into,347.1.1.1,4.1.1,flip.1] n(n(x)+y)+n(x+y)=n(y) # label("Hint 142(350)"). 349 [para_into,348.1.2,347.1.1] n(n(x)+n(y))+n(x+n(y))=y # label("Hint 143(351)"). 350 [para_into,349.1.1.1.1.1,347.1.1] n(x+n(y))+n(n(x)+n(y))=y # label("Hint 144(352)"). 351 [para_into,350.1.1.2.1,2.1.2] n(x+n(y))+n(n(y)+n(x))=y # label("Hint 145(353)"). 352 [para_into,351.1.1.1.1,2.1.2] n(n(x)+y)+n(n(x)+n(y))=x # label("Hint 146(354)"). 353 [binary,352.1,5.1] $F. ------------ end of proof / derivation -------------