Upper bound on proof tree size

Zenmastur · Post by **Zenmastur** » Fri Jul 11, 2014 8:54 pm

Can anyone point me to a paper that deals with proof-tree sizes. I'm looking for an upper bound for the number of nodes in proof-trees. The tighter the better.

I've spent some time on the problem and it seems that a good bound might be 2*b^(n/2) where b is the branching factor and n is the number of moves in the mate but I have no proof for it.

Regards,

Forrest

zullil · Post by **zullil** » Fri Jul 11, 2014 9:44 pm

Zenmastur wrote:Can anyone point me to a paper that deals with proof-tree sizes. I'm looking for an upper bound for the number of nodes in proof-trees. The tighter the better.

I've spent some time on the problem and it seems that a good bound might be 2*b^(n/2) where b is the branching factor and n is the number of moves in the mate but I have no proof for it.

Regards,

Forrest

To prove that the side-to-go has mate in at most n, it suffices to give one move for the side-to-go, and then for each reply by the opposing side, it suffices to prove that the side-to-go has mate in at most n-1. Assuming that there are at most b moves in any position, this leads to the recursive formula V[n] = 1 + b + b * V[n-1] = 1 + b * (1 + V[n-1]). Here V[n] denotes the number of nodes in a mate-in-at-most-n proof tree, with V[1] = 1.

From the recursion:

Code: Select all

V&#91;1&#93; = 1
V&#91;2&#93; = 1 + 2b
V&#91;3&#93; = 1 + 2b + 2b^2
V&#91;4&#93; = 1 + 2b + 2b^2 + 2b^3

so

V&#91;n&#93; = 1 + 2b + 2b^2 + 2b^3 + ... + 2b^&#40;n-1&#41;.

(Take this with a grain of salt, since

(a) I'm not sure this is what you're asking about, and

(b) I thought about this for only five minutes or so.)

AlvaroBegue · Post by **AlvaroBegue** » Sat Jul 12, 2014 1:28 am

To give a more closed form to the formula Louis posted:

Code: Select all

V&#91;n&#93; = 1 + 2*b + 2*b^2 + ... + 2*b^&#40;n-1&#41; =
     = -1 + 2 * &#40;1 + b + b^2 + ... + b^&#40;n-1&#41;)
     = -1 + 2 * &#40;b^n - 1&#41; / &#40;b - 1&#41;

zullil · Post by **zullil** » Sat Jul 12, 2014 2:02 am

AlvaroBegue wrote:To give a more closed form to the formula Louis posted:
Code: Select all
V&#91;n&#93; = 1 + 2*b + 2*b^2 + ... + 2*b^&#40;n-1&#41; =
     = -1 + 2 * &#40;1 + b + b^2 + ... + b^&#40;n-1&#41;)
     = -1 + 2 * &#40;b^n - 1&#41; / &#40;b - 1&#41;

Yes---geometric series. Thanks for the closed form.

Zenmastur · Post by **Zenmastur** » Sat Jul 12, 2014 2:25 am

zullil wrote:
Zenmastur wrote:Can anyone point me to a paper that deals with proof-tree sizes. I'm looking for an upper bound for the number of nodes in proof-trees. The tighter the better.

I've spent some time on the problem and it seems that a good bound might be 2*b^(n/2) where b is the branching factor and n is the number of moves in the mate but I have no proof for it.

Regards,

Forrest
To prove that the side-to-go has mate in at most n, it suffices to give one move for the side-to-go, and then for each reply by the opposing side, it suffices to prove that the side-to-go has mate in at most n-1. Assuming that there are at most b moves in any position, this leads to the recursive formula V[n] = 1 + b + b * V[n-1] = 1 + b * (1 + V[n-1]). Here V[n] denotes the number of nodes in a mate-in-at-most-n proof tree, with V[1] = 1.

From the recursion:
Code: Select all
V&#91;1&#93; = 1
V&#91;2&#93; = 1 + 2b
V&#91;3&#93; = 1 + 2b + 2b^2
V&#91;4&#93; = 1 + 2b + 2b^2 + 2b^3

so

V&#91;n&#93; = 1 + 2b + 2b^2 + 2b^3 + ... + 2b^&#40;n-1&#41;.
(Take this with a grain of salt, since

(a) I'm not sure this is what you're asking about, and

(b) I thought about this for only five minutes or so.)

That's what I originally thought as well. But it turns out to be a very bad estimate/ bound because it assumes (incorrectly I might add) that all the mates are "n" moves long. I'm not sure this is even possible if the mate is very long. e.g. 15-25 moves or more. In the mates that I have looked at about half the moves at each ply lead to very short mates (1-2 moves) due to being inferior replies. So while the side to move may have "b" replies few of them actually lead to a mate of full length. If we count the nodes at each ply over all possible lines of play the count goes up as we get deeper into the lines then at some point (around the middle) it begins to decline. This lead me to conclude that 2*b^(n/2) might be close.

But after thinking about it a little more maybe it should be :

Code: Select all

 V&#91;n&#93; = 2 * ( 1 + 2*b + 2*b^2 + ... + 2*b^&#40;n/2&#41;) =
                  = 2 + 4 * &#40;1 + b + b^2 + ... + b^&#40;n/2&#41;)

What I'm looking for is a "good" upper bound. By "good" I mean something that is accurate enough to give order of magnitude estimates of the trees size for storage purposes. To be used in a program to generate proof trees for long mates. e.g. in the 15 to 40+ move range.

Regards,

Zen

syzygy · Post by **syzygy** » Sat Jul 12, 2014 3:04 am

Zenmastur wrote:What I'm looking for is a "good" upper bound.

You're not going to get anything better as a general formula.

To get a general upper bound for the size of a proof tree of a mate in N, you'll just have to assume the worst case scenario: all lines need N moves. Certainly for each value of N games can be found (or constructed) where this worst case scenario applies for at least one position.

Even if you limit the game to chess (which you do not, see your original question... unless the use of the word "mate" excludes anything else than chess), it does not seem realistic to hope to be able to get a tighter bound by somehow making use of "chess specific" properties of proof trees.

By "good" I mean something that is accurate enough to give order of magnitude estimates of the trees size for storage purposes. To be used in a program to generate proof trees for long mates. e.g. in the 15 to 40+ move range.

Just pick a somewhat flexible data structure. You're not going to have a constant b, either.

zullil · Post by **zullil** » Sat Jul 12, 2014 3:59 am

syzygy wrote:
Zenmastur wrote:What I'm looking for is a "good" upper bound.
You're not going to get anything better as a general formula.

Right.

Here's perhaps an interesting question: What is the exact maximal number of nodes in a mate-in-3 proof tree (in traditional chess)?

ie, consider all possible mate-in-3 positions and all possible proof trees of such positions, and determine the number of nodes in the "largest" such tree.

[D]6k1/R7/5K2/8/8/8/8/8 w - - 0 1

Only needs 7 nodes to prove mate-in-3. Probably not maximal

zullil · Post by **zullil** » Sat Jul 12, 2014 4:03 am

Zenmastur wrote:
zullil wrote:
Zenmastur wrote:Can anyone point me to a paper that deals with proof-tree sizes. I'm looking for an upper bound for the number of nodes in proof-trees. The tighter the better.

I've spent some time on the problem and it seems that a good bound might be 2*b^(n/2) where b is the branching factor and n is the number of moves in the mate but I have no proof for it.

Regards,

Forrest
To prove that the side-to-go has mate in at most n, it suffices to give one move for the side-to-go, and then for each reply by the opposing side, it suffices to prove that the side-to-go has mate in at most n-1. Assuming that there are at most b moves in any position, this leads to the recursive formula V[n] = 1 + b + b * V[n-1] = 1 + b * (1 + V[n-1]). Here V[n] denotes the number of nodes in a mate-in-at-most-n proof tree, with V[1] = 1.

From the recursion:
Code: Select all
V&#91;1&#93; = 1
V&#91;2&#93; = 1 + 2b
V&#91;3&#93; = 1 + 2b + 2b^2
V&#91;4&#93; = 1 + 2b + 2b^2 + 2b^3

so

V&#91;n&#93; = 1 + 2b + 2b^2 + 2b^3 + ... + 2b^&#40;n-1&#41;.
(Take this with a grain of salt, since

(a) I'm not sure this is what you're asking about, and

(b) I thought about this for only five minutes or so.)
That's what I originally thought as well. But it turns out to be a very bad estimate/ bound

Zen

Yes, it's very bad. But unless you add additional assumptions ...

AlvaroBegue · Post by **AlvaroBegue** » Sat Jul 12, 2014 6:16 am

For any position P that is mate in N, define M[P] as the minimum number of nodes in any proof tree for that fact. I think what you meant to ask is what is the maximum value of M[P] among all positions P that are mate in N.

Zenmastur · Post by **Zenmastur** » Sat Jul 12, 2014 10:24 am

AlvaroBegue wrote:For any position P that is mate in N, define M[P] as the minimum number of nodes in any proof tree for that fact. I think what you meant to ask is what is the maximum value of M[P] among all positions P that are mate in N.

The minimum number of nodes in any proof tree is 2b(n-1)+1 nodes where "n" is the number of moves in the mate and "b" is the branching factor. This is trivial.

You are right, I would like to know the maximum number of nodes in any mate in N moves. I know for a mate in 1 the maximum and minimum tree size are the same. Each is one node. For a mate in 2 the minimum is 3 nodes and the maximum is 2b+1 where b is the branching factor of the opponents response. I know that both the minimum and maximum are possible at least for small N. I'm not convinced that either is possible for large N.

When N becomes large the minimum becomes hard to obtain in a proof tree. The equation implies that all moves by the opponent except one at each ply result in an immediate mate. i.e. a mate-in-one if the opponent deviates from the best line of play. "Best" meaning the move that extends the mate the longest number of plies. This seems possible for long mates where the line is forcing all the way to mate. An example would be a long series of checks where if the opponent plays the slightest inaccuracy he gets mated, followed by his eventual mate. I don't see any problem with this occurring in a game or a constructed position.

When N becomes large the maximum number of nodes in a proof tree is more problematic. The current bound (if that's what you want to call it) is useless. Example a mate in 549 (taken from the 7-man Lomonosov table bases) isn't possible if the current upper bound is to be believed. Even with a branching factor of 2 or less the size of the proof tree would be orders of magnitude larger than the total number of positions in chess. Black's branching factor in line of play is as high as the mid-thirties and probably averages around 15-20. If we use the formula given in other posts the number of nodes in this tree would be ~ 1.0E+701. There are only approximately 1.0E+43 possible positions in chess. No proof tree may contain all possible chess positions. So clearly this upper bound is completely worthless!

I conclude that there exists a better upper bound. i.e. something that is around 2*b^(n/2)or there abouts. The problem is finding it's exact form and then proving it. Even if no proof is found having a good estimate vice a bound for such a fundamental concept would be useful.

The mate in 549 follows and it does demonstrate the problem in such a way that it's hard to argue. I haven't gone through it move by move to record the branching factor at each of blacks moves yet but it's clear that black has a large number of moves in most positions. The average for the first part is probably around 19 or so.

[D]1n1k4/6Q1/5KP1/8/7b/1r6/8/8 w - - 0 1

1. Kf5 Rb5+ 2. Kg4 Rb4+ 3. Kf3 Nd7 4. Qh8+ Ke7 5. g7 Bf6 6. g8=N+ Ke6 7. Qh3+ Kd6 8. Kg2 Rb2+ 9. Kf1 Rb1+ 10. Ke2 Rb2+ 11. Kd1 Rb1+ 12. Kc2 Rb2+ 13. Kc1 Rb5 14. Qh6 Rc5+ 15. Kb1 Rb5+ 16. Ka2 Ra5+ 17. Kb3 Rf5 18. Ka3 Rf3+ 19. Ka2 Ke6 20. Qh7 Ne5 21. Nh6 Rf2+ 22. Kb1 Rf4 23. Qg8+ Kd6 24. Ka2 Nc6 25. Ng4 Bd4 26. Qg6+ Kd5 27. Qg5+ Ke4 28. Kb1 Nb4 29. Qe7+ Kd3 30. Qh7+ Ke2 31. Qh2+ Kf3 32. Qh3+ Ke4 33. Qg2+ Kd3 34. Qg3+ Ke4 35. Qe1+ Kd3 36. Qd1+ Ke4 37. Qe2+ Kd5 38. Kc1 Kd6 39. Qh2 Nd5 40. Kd2 Bc3+ 41. Ke2 Bd4 42. Qh6+ Kd7 43. Qh7+ Kc6 44. Qg8 Kc5 45. Kd3 Nb4+ 46. Kd2 Nd5 47. Qc8+ Kd6 48. Nh6 Bc3+ 49. Ke2 Re4+ 50. Kf2 Rf4+ 51. Kg1 Bd4+ 52. Kh2 Ne3 53. Qd8+ Kc6 54. Qe8+ Kc5 55. Nf7 Rf2+ 56. Kh3 Rf3+ 57. Kh4 Rf5 58. Nh6 Rf1 59. Qa8 Kb4 60. Kh5 Kc3 61. Qc8+ Kd3 62. Kg6 Rf2 63. Qa8 Rf1 64. Qb8 Kd2 65. Qb3 Ke2 66. Qb5+ Kd2 67. Qg5 Kc2 68. Kh7 Kd3 69. Qb5+ Kc3 70. Qa5+ Kd3 71. Qg5 Rf6 72. Qb5+ Ke4 73. Qb7+ Kd3 74. Qd7 Kc3 75. Qe8 Kd2 76. Qb5 Kc2 77. Qe2+ Kc3 78. Qh5 Rf1 79. Qg6 Rf6 80. Qe4 Kc4 81. Qe8 Kd3 82. Ng8 Rf1 83. Ne7 Rh1+ 84. Kg6 Rg1+ 85. Kf7 Rf1+ 86. Ke6 Rf6+ 87. Kd7 Bc5 88. Nc6 Nd5 89. Nd8 Rd6+ 90. Kc8 Ne7+ 91. Kc7 Nd5+ 92. Kb7 Rb6+ 93. Kc8 Ne7+ 94. Kd7 Nd5 95. Qe1 Rd6+ 96. Kc8 Be3 97. Qd1+ Ke4 98. Qc2+ Kd4 99. Qa4+ Ke5 100. Qh4 Kf5 101. Qh3+ Ke4 102. Nf7 Rc6+ 103. Kd8 Kd4 104. Ke8 Rc7 105. Kf8 Bf4 106. Qe6 Ra7 107. Qe2 Be3 108. Qg4+ Kc5 109. Qc8+ Kd4 110. Qb8 Kd3 111. Kg8 Rc7 112. Qb5+ Kd4 113. Qa4+ Kc5 114. Qa6 Kd4 115. Kf8 Bd2 116. Qf1 Bc3 117. Kg7 Rc6 118. Kg8 Nf6+ 119. Kf8 Rc8+ 120. Kg7 Ne4 121. Qb5 Ke3+ 122. Kh7 Rc7 123. Qb6+ Rc5 124. Qe6 Kf4 125. Qh6+ Kf3 126. Qh3+ Ke2 127. Kg8 Rc6 128. Kf8 Bb4+ 129. Kg7 Bc3+ 130. Kg8 Rf6 131. Qh4 Kd3 132. Nd8 Kd4 133. Qg4 Ke5 134. Qe2 Kf4 135. Qc4 Kf3 136. Qb3 Kf2 137. Ne6 Ke3 138. Qa2 Rf3 139. Qc2 Be5 140. Qd1 Bc3 141. Qc1+ Kd3 142. Nf4+ Kc4 143. Ng2 Rf2 144. Nh4 Nf6+ 145. Kg7 Ne4+ 146. Kg6 Rf6+ 147. Kh5 Kd4 148. Qd1+ Ke3 149. Qb1 Bd2 150. Ng6 Ng3+ 151. Kh6 Bc3 152. Qc1+ Kd3 153. Qg1 Ne4 154. Kh7 Rd6 155. Kg8 Rd8+ 156. Kf7 Rd7+ 157. Ke6 Rd6+ 158. Ke7 Bf6+ 159. Ke8 Rd8+ 160. Kf7 Rd7+ 161. Ke6 Rd6+ 162. Kf5 Rd5+ 163. Kf4 Bg5+ 164. Kg4 Ke2 165. Qa7 Bd2 166. Qe7 Rg5+ 167. Kh3 Ke3 168. Nh4 Rg3+ 169. Kh2 Rg4 170. Qa3+ Bc3 171. Qa7+ Ke2 172. Ng2 Be5+ 173. Kg1 Nd2 174. Qf2+ Kd1 175. Kh1 Bd4 176. Qe1+ Kc2 177. Qe2 Re4 178. Qh5 Nf1 179. Qd5 Nd2 180. Qf5 Kd1 181. Nf4 Be5 182. Qh5+ Kc2 183. Ng6 Bf6 184. Kg2 Bg5 185. Qh7 Kd1 186. Qh8 Be3 187. Qh5+ Kc2 188. Nh4 Bd4 189. Nf5 Be5 190. Qe8 Rg4+ 191. Kh3 Re4 192. Qc8+ Kd1 193. Qc5 Nc4 194. Nh6 Nd2 195. Ng4 Bd4 196. Qb5 Rf4 197. Kh4 Be3 198. Qd3 Bd4 199. Kh5 Re4 200. Qa3 Rf4 201. Qd6 Re4 202. Nh6 Bf2 203. Kg6 Rc4 204. Qe5 Bb6 205. Qg3 Rc6+ 206. Kg7 Rc4 207. Nf7 Bc7 208. Qg1+ Kc2 209. Nh6 Be5+ 210. Kg8 Re4 211. Nf5 Bf4 212. Qh1 Be5 213. Qh3 Kd1 214. Kf8 Bf4 215. Qg4+ Ke1 216. Qg2 Be5 217. Qh1+ Ke2 218. Ke8 Bg3+ 219. Kd7 Bf2 220. Ne7 Rd4+ 221. Nd5 Kd3 222. Kc6 Rh4 223. Qg2 Rc4+ 224. Kb5 Be3 225. Qh1 Bc5 226. Qh7+ Ke2 227. Qh5+ Ke1 228. Kc6 Bd4+ 229. Kd6 Bf2 230. Kd7 Rd4 231. Qh1+ Ke2 232. Ke6 Rh4 233. Qg2 Rc4 234. Ke7 Nf3 235. Qh3 Re4+ 236. Kd8 Rd4 237. Qh5 Bg3 238. Qe8+ Be5 239. Qb5+ Kf2 240. Kc8 Re4 241. Kb7 Bd4 242. Qc6 Rg4 243. Ka6 Rg7 244. Nb4 Re7 245. Nd3+ Ke3 246. Qc1+ Ke4 247. Nb4 Re5 248. Qb1+ Ke3 249. Qc2 Rc5 250. Qd3+ Kf4 251. Qe2 Kg3 252. Qe7 Rh5 253. Nd3 Rh6+ 254. Ka5 Rh4 255. Qe6 Bc3+ 256. Ka6 Bd4 257. Qc6 Be3 258. Qe8 Bd4 259. Qb8+ Kg2 260. Qg8+ Kh3 261. Qg6 Rg4 262. Qc6 Kg3 263. Qc7+ Kh3 264. Nf4+ Kh4 265. Qd6 Kg3 266. Ng6+ Kf2 267. Qe6 Rg1 268. Nf4 Ra1+ 269. Kb7 Ra7+ 270. Kb8 Ra3 271. Qe2+ Kg3 272. Nd3 Rb3+ 273. Kc8 Rb6 274. Qe4 Rf6 275. Kd7 Bc3 276. Nc5 Bd4 277. Ne6 Be5 278. Ng5 Bb2 279. Qe3 Kg4 280. Ne4 Rf7+ 281. Kc6 Rf5 282. Nf2+ Kg3 283. Nd3 Be5 284. Kd7 Rf7+ 285. Ke8 Rf5 286. Qc5 Kg4 287. Nf2+ Kg5 288. Qd5 Kg6 289. Nd3 Bg7 290. Qe4 Kg5 291. Ke7 Bd4 292. Kd7 Rf6 293. Kc8 Rf8+ 294. Kb7 Rf7+ 295. Ka6 Rf6+ 296. Ka5 Bc3+ 297. Ka4 Ra6+ 298. Kb5 Ra5+ 299. Kb6 Rf5 300. Qe7+ Kg6 301. Qe8+ Kg5 302. Kb7 Bd4 303. Qe7+ Kh5 304. Qe4 Rf7+ 305. Ka6 Rf6+ 306. Kb5 Kg5 307. Nb4 Be5 308. Nd5 Rf5 309. Qe3+ Kh5 310. Ka6 Rf7 311. Qf2 Ng5 312. Qc2 Nf3 313. Qc8 Kg5 314. Qe6 Rf5 315. Kb7 Bd4 316. Qe7+ Bf6 317. Qe3+ Kh5 318. Qe4 Kg5 319. Nc7 Nd4 320. Qg2+ Kh5 321. Nd5 Nf3 322. Ne3 Rf4 323. Qh3+ Nh4 324. Qe6 Kg5 325. Qd5+ Kg6 326. Qd6 Kg5 327. Qc5+ Kg6 328. Qc7 Kg5 329. Nd5 Rf3 330. Qc1+ Kg4 331. Ne3+ Kg5 332. Nc4+ Rf4 333. Nb6 Kg4 334. Qd1+ Kg3 335. Nd5 Rf3 336. Qd2 Kg4 337. Ne3+ Kh5 338. Nc4 Bg5 339. Qd1 Bf4 340. Nb6 Bg3 341. Nd7 Kg5 342. Qd5+ Rf5 343. Qe4 Rf4 344. Qe7+ Kg4 345. Qe6+ Kf3 346. Nf6 Kg2 347. Qd5+ Kh2 348. Ne4 Nf5 349. Ng5 Nd6+ 350. Kb6 Bf2+ 351. Kc7 Bg3 352. Kd7 Nf5 353. Qd2+ Rf2 354. Qd1 Rf4 355. Qe2+ Rf2 356. Qh5+ Kg2 357. Kc6 Rc2+ 358. Kd5 Rd2+ 359. Kc4 Rf2 360. Qh3+ Kg1 361. Kb4 Rf1 362. Ka5 Rf4 363. Ka6 Ra4+ 364. Kb5 Rf4 365. Ka5 Rf2 366. Qh8 Kg2 367. Qc3 Rf4 368. Qd2+ Kf1 369. Qd5 Nd4 370. Kb6 Bf2 371. Kc7 Rh4 372. Qe5 Kg2 373. Ne4 Kf3 374. Nd2+ Kg2 375. Qd5+ Kh2 376. Kb7 Rh7+ 377. Ka6 Rh6+ 378. Ka5 Rh4 379. Qd6+ Kh3 380. Qd7+ Kg2 381. Qb7+ Kg3 382. Qg7+ Rg4 383. Nf1+ Kh3 384. Qd7 Kh4 385. Qh7+ Kg5 386. Qg7+ Kf4 387. Qc7+ Kg5 388. Nd2 Rf4 389. Qg7+ Kf5 390. Nc4 Nf3 391. Nd6+ Ke6 392. Ne8 Kf5 393. Ka6 Bd4 394. Nd6+ Ke6 395. Qg8+ Kf6 396. Qh7 Ke6 397. Ne4 Kd5 398. Qb7+ Ke6 399. Ng3 Be5 400. Qb3+ Kd6 401. Qb6+ Ke7 402. Ne4 Kf7 403. Qh6 Kg8 404. Qe6+ Kh8 405. Qe7 Rf5 406. Kb6 Bg7 407. Ng3 Rf6+ 408. Kb5 Nd4+ 409. Kc4 Rc6+ 410. Kd3 Rc3+ 411. Ke4 Rc6 412. Qe8+ Kh7 413. Kd3 Rd6 414. Qh5+ Kg8 415. Ne4 Rd8 416. Ke3 Bh6+ 417. Kf2 Rf8+ 418. Kg2 Kh7 419. Ng3 Ne6 420. Qh4 Ng7 421. Qe4+ Kg8 422. Qd5+ Kh7 423. Qd6 Rf7 424. Qd3+ Kg8 425. Qd5 Bc1 426. Kh3 Ba3 427. Kg4 Be7 428. Qc4 Kf8 429. Qc8+ Ne8 430. Nf5 Rf6 431. Qd7 Rf7 432. Qd3 Bf6 433. Qe3 Be7 434. Qh6+ Kg8 435. Qh1 Rh7 436. Qd5+ Kf8 437. Kf3 Nf6 438. Qe5 Ne8 439. Ke2 Bf6 440. Qd5 Rf7 441. Kd2 Bg5+ 442. Kc2 Rc7+ 443. Kb2 Bf6+ 444. Kb1 Rh7 445. Qf3 Ra7 446. Qb3 Rc7 447. Qb4+ Kf7 448. Qb6 Rd7 449. Qb3+ Kf8 450. Nh6 Rg7 451. Qa3+ Be7 452. Qf3+ Bf6 453. Ng4 Ke7 454. Kc2 Rg5 455. Qe3+ Kf7 456. Qb3+ Kf8 457. Qe6 Bg7 458. Ne3 Re5 459. Qb6 Bf6 460. Ng4 Rf5 461. Qe6 Rf4 462. Qc8 Bd4 463. Qd7 Bg7 464. Ne3 Rf2+ 465. Kb1 Rf7 466. Qc8 Rc7 467. Qa6 Rd7 468. Qa3+ Kf7 469. Qb3+ Kf8 470. Qb4+ Nd6 471. Qf4+ Kg8 472. Nd5 Nf7 473. Qc4 Ra7 474. Nf4 Rb7+ 475. Kc2 Rb2+ 476. Kd1 Rb6 477. Qc8+ Kh7 478. Qc7 Rd6+ 479. Ke2 Kg8 480. Qe7 Bf8 481. Qe8 Ng5 482. Qc8 Rf6 483. Qg4 Bh6 484. Nh5 Re6+ 485. Kf1 Re5 486. Qc8+ Bf8 487. Qc2 Re6 488. Qa2 Kh7 489. Qg2 Kh6 490. Qh1 Rb6 491. Nf4+ Kg7 492. Qh5 Nh7 493. Qg4+ Kf7 494. Qd7+ Be7 495. Qd5+ Kf8 496. Ne6+ Ke8 497. Qh5+ Kd7 498. Ng7 Nf6 499. Qf5+ Kc7 500. Qe5+ Kd7 501. Qd4+ Kc7 502. Qe3 Nd5 503. Qe5+ Kc6 504. Nf5 Rb7 505. Qe4 Kc5 506. Qc2+ Kb6 507. Qb3+ Kc6 508. Nd4+ Kc5 509. Qxb7 Kxd4 510. Kf2 Ke4 511. Qb1+ Kd4 512. Qg6 Bf6 513. Kf3 Be7 514. Qg1+ Kc4 515. Qg4+ Kc5 516. Ke2 Nf6 517. Qf5+ Kd4 518. Qf4+ Kd5 519. Kf3 Ke6 520. Qc4+ Kf5 521. Qa6 Nd7 522. Qd3+ Ke6 523. Qe3+ Kd6 524. Kf4 Nc5 525. Kf5 Bf8 526. Qf3 Nd7 527. Qc3 Ke7 528. Qd4 Ke8 529. Ke6 Nc5+ 530. Kd5 Nd7 531. Kc6 Nb8+ 532. Kb6 Nd7+ 533. Kc7 Nc5 534. Qc4 Be7 535. Qg8+ Bf8 536. Kc6 Na6 537. Qe6+ Be7 538. Qc8+ Kf7 539. Qxa6 Ke6 540. Qd3 Bg5 541. Qe4+ Kf6 542. Kd6 Bd2 543. Qe5+ Kg6 544. Ke6 Bg5 545. Qf5+ Kh5 546. Qf3+ Kh6 547. Qf7 Bh4 548. Kf5 Bg5 549. Qg6# 1-0

Regards,

Zen

Upper bound on proof tree size

Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size

Re: Upper bound on proof tree size