Since there is exactly one, well defined, unsatisfiable GT formula for a fixed parameter n, the approximate branching sequence given in Figure 5 below is straightforward. However, the fact that the same branching sequence works well for the satisfiable version of the GTn formulas, obtained by deleting a randomly chosen successor clause, is worth noting.