The following files list move strings to positions where the proof tree
has a subtree of size N, but no child node has this size.

N=1000
easy12.lines (496)
e3c6.lines (840)
e3Nc6.lines (4333)
e3Nh6.lines (7318)
e3g5.lines (19982)
e3b5.lines (39388)
e3e6.lines (25570)
e3c5.lines (115334)
e3b6.lines (331507)

N=10000
easy12lines.10K (50)
e3c6lines.10K (89)
e3Nc6lines.10K (434)
e3Nh6lines.10K (809)
e3g5lines.10K (2155)
e3b5lines.10K (4113)
e3e6lines.10K (3005)
e3c5lines.10K (12177)
e3b6lines.10K (35915)

N=25000
easy12lines.25K (22)
e3c6lines.25K (36)
e3Nc6lines.25K (174)
e3Nh6lines.25K (310)
e3g5lines.25K (807)
e3b5lines.25K (1552)
e3e6lines.25K (1234)
e3c5lines.25K (4841)
e3b6lines.25K (14031)

These provide a low-overhead method (compared to parsing proof files)
of transferring information to other formats.