Contents of 6.2.1 Automatic Sequence Generation: GTnSeq1UIP

6.2.1 Automatic Sequence Generation: `GTnSeq1UIP`

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 GT_n formulas, obtained by deleting a randomly chosen successor clause, is worth noting.

**Figure 5:** Approximate branching sequence for *GTn* formulas. The sequence goes left to right along row 1, then along row 2, and so on. Entries marked `-' correspond to non-existent variables x_{i, i}.
$\begin{figure}\begin{displaymath} \begin{array}{llllll} - & x_{2,1} & x_{3,1} & ... ...,n} & x_{4,n} & \ldots & x_{n-1,n} \\ \end{array}\end{displaymath} \end{figure}$