# Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

Leroy Chew1, Alexis de Colnet1, Friedrich Slivovsky2, Stefan Szeider1

###### Abstract

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT
solvers. This has been observed even for simple formulas encoding two
contradictory parity constraints with different variable orders (Chew and
Heule 2020). We provide an analytical explanation for their hardness by
showing that they require exponential resolution refutations with high
probability when the variable order is chosen at random. We obtain this result
by proving that these formulas, which are known to be Tseitin formulas, have
Tseitin graphs of linear treewidth with high probability. Since such Tseitin
formulas require exponential resolution proofs, our result follows. We
generalize this argument to a new class of formulas that capture a basic form
of parity reasoning involving a sum of two random parity constraints with
random orders. Even when the variable order for the sum is chosen favorably,
these formulas remain hard for resolution. In contrast, we prove that they
have short DRAT refutations. We show experimentally that the running time of
CDCL SAT solvers on both classes of formulas grows exponentially with their
treewidth.

## Introduction

SAT solvers, including Conflict-Driven Clause-Learning (CDCL) solvers, can
solve practical problems with millions of variables (Marques-Silva, Lynce, and
Malik 2009; Fichte et al. 2023), but on the other hand, can struggle with
basic mathematical principles. The Handbook of Satisfiability (Biere et al.
2021, Section 9.6.1) lists one such example: the problem of XOR (exclusive-or)
constraints, which is equivalent to the parity problem of summation modulo 2.
XOR-constraints serve practical purposes, particularly around modern
cryptographical and cryptonanalytical problems. Provably hard XOR problems are
usually constructed over complex structures such as expander graphs (Urquhart
1987; Ben-Sasson and Wigderson 2001), but much simpler problems involving only
two constraints were found experimentally hard for CDCL (Chew and Heule 2020)
and, up until this paper, were not matched with a corresponding lower bound in
resolution.

Resolution is particularly important here because the relationship with CDCL
solving is two-way; CDCL runs of unsatisfiable instances can be output as
resolution proofs, but also every resolution refutation can be followed
completely by a CDCL algorithm (with a few non-deterministic choices) to
return UNSAT (Pipatsrisawat and Darwiche 2011). Lower bounds on the length of
resolution proof of unsatisfiability have been shown for pure XOR problems
structured by graphs and represented in CNF formulas called Tseitin formulas
(Tseitin 1968, 1983; Urquhart 1987). Finding a complete characterization of
hard Tseitin formulas for resolution is still an open problem. However,
exponential lower bounds for resolution are known under the suitable
condition: that their underlying graphs have high linear _treewidth_ (a graph
invariant that measures how close a graph is to being a tree). The
relationship between treewidth and resolution proof length has been
extensively studied for Tseitin formulas already (Ben-Sasson and Wigderson
2001; Galesi, Talebanfard, and Torán 2020; Itsykson, Riazanov, and Smirnov
2022; de Colnet and Mengel 2023).

Here, we look at some XOR-constraint problems that are strikingly simple to
define and whose hardness for resolution was observed empirically but yet to
be understood theoretically (Chew and Heule 2020). We prove that they are, in
fact, families of Tseitin formulas and that linear treewidth emerges for
almost all of them, thus showing asymptotic exponential lower bounds for
resolution. Furthermore, our experiments suggest that this is not just
theoretical and asymptotic for proof systems; treewidth indeed correlates to
the solving time of CDCL solvers on these families. In the rest of this
section, we present the problems and our results.

### Problem 1: Reordered Parity

The standard linear CNF encoding of an XOR-constraint over $n$ propositional
variables splits the constraint into a sequence of XORs of size 3 according to
an ordering of its variables (Biere et al. 2021, Section 2.2.5). The encoding
uses one auxiliary variable for every $k<n$ to store the parity of the first
$k$ variables. The simplest form of the XOR-constraint problem starts with two
opposite XOR-constraints and their standard linear CNF encodings where the $n$
variables appear in a different order given by the permutation $\sigma$. The
two CNF are saying the sum of the $n$ variables is both odd and even, so their
conjunction—denoted by $\mathsf{rPar}(n,\sigma)$—is a contradiction a SAT
solver should be able to recognize.

Chew and Heule (2020) showed that these problems could be proven false by
$O(n\log n)$-size DRAT proofs even without new variables (Buss and Thapen
2019). We show here that resolution proofs on their own are often unable to
handle even these restricted examples. For some $\sigma$, such as the identity
mapping, resolution proofs are short; in fact, the identity mapping gives the
Dubois family in the SAT library. However, the easiness is not seen with other
permutations. Chew and Heule (2020) conducted experiments that showed that
CDCL solvers struggle and time-out around $n=50$ for uniformly selected
permutations, although a theoretical lower bound was never proved. We show
that as $n$ increases, a random permutation $\sigma$ yields, with high
probability, a formula $\mathsf{rPar}(n,\sigma)$ whose resolution proof
requires exponentially many clauses.

######  Theorem 1.

There is a constant $\alpha>0$ such that, with probability tending to $1$ as
$n$ increases, the length of a smallest resolution refutation of the
unsatisfiable formula $\mathsf{rPar}(n,\sigma)$, where $\sigma$ is chosen
uniformly at random, is at least $2^{\alpha n}$.

A key observation here is that the $\mathsf{rPar}$ formulas are Tseitin
formulas. The fact that the $\mathsf{rPar}$ formulas come from standard CNF
encodings of very simple XOR-constraints problems makes them natural examples
of Tseitin formulas that are more likely to occur in practice than those that
appear in proofs of hardness that are often constructed from arbitrary
expander graphs (Urquhart 1987). Theorem 1 proves the context assumed by Chew
and Heule (2020) that a powerful proof system such as DRAT- was necessary for
the short proofs of $\mathsf{rPar}$, as we now have exponential resolution
lower bounds. Along with the evidence shown by our experiments, we now
conclude that high treewidth is the reason for the hardness in the experiments
of Chew and Heule (2020). We can also take this as clarification that order
matters in the encoding of parity constraints in general.

### Problem 2: Random Parity Addition

There are several effective strategies for dealing with XOR-constraints in
practice. One method that has succeeded is to employ Gaussian elimination (Han
and Jiang 2012; Soos 2012) techniques to simplify the problem. Two
contradictory parity constraints fall short of representing what happens in an
average step of Gaussian elimination. Instead, Gaussian elimination involves
many steps using the bitwise addition of two XOR-constraints to produce a new
constraint. In order to study such a step as an instance for resolution, we
have to write it as a contradiction. So here we modify $\mathsf{rPar}$ to use
three XOR-constraints, with the third containing the variables in the
symmetric difference of the first two constraints and then flip some literals
to create a contradiction. The input XOR-constraints are encoded in CNF
formulas $a$ and $b$ using the standard linear encoding. We then define a CNF
encoding $\mathsf{rAddPar}(a,b)$ of the contradiction similar to
$\mathsf{rPar}(n,\sigma)$, and we show their hardness for resolution.

######  Theorem 2.

With high probability, for any two random parity constraints over $n$
variables encoded randomly and independently in CNF formulas $a$ and $b$ using
the standard linear encoding, the length of the shortest resolution refutation
of $\mathsf{rAddPar}(a,b)$ is exponential in $n$, the length of a shortest
resolution refutation of $\mathsf{rAddPar}(a,b)$ is exponential in the number
of variables.

The $\mathsf{rAddPar}$ formulas turn out to also be Tseitin formulas, so this
again provides a new intuitive family that demonstrates the hardness of
Tseitin formulas—and yet again shows that order matters when encoding parity
constraints.

Adding Gaussian elimination to SAT-solving/preprocessing presents several
technical challenges. An example is verification—unsatisfiable instances in
CDCL SAT solvers can be readily verified in resolution proofs and thus
verified in the more powerful checking format standard DRAT (Järvisalo, Heule,
and Biere 2012). It was therefore pertinent to show that Gaussian elimination
techniques could also be verified efficiently in DRAT (Philipp and Rebola-
Pardo 2016). For the specific family of $\mathsf{rPar}(n,\sigma)$, it was
shown to have DRAT- refutations in $O(n\log n)$ many lines using a tool from
Chew and Heule (2020). Recently, a BDD-based SAT solver augmented with pseudo-
Boolean constraints (Bryant, Biere, and Heule 2022) was shown to have improved
the result experimentally. We can generalize Chew and Heule’s upper-bound
results to $\mathsf{rAddPar}(a,b)$.

######  Theorem 3.

For any two random parity constraints over $n$ variables encoded randomly and
independently in CNF formulas $a$ and $b$ using the standard linear encoding,
there are DRAT- refutations of $\mathsf{rAddPar}(a,b)$ with $O(n\log n)$ many
lines.

$O(n\log n)$ is already a good upper bound, and this can potentially be used
in verification. One of the advantages of DRAT- is that no extension variables
are added. This will speed up the proof checking.

######  Theorem 4.

For any two parity constraints over $n$ variables, and any standard linear
encodings $a$ and $b$ of theses constraints, there are Extended Resolution
refutations of $\mathsf{rAddPar}(a,b)$ that have $O(n\log n)$ many lines.

## Preliminaries

Boolean _variables_ take value in $\\{0,1\\}$. A _literal_ is either a
variable $x$ or its negation $\bar{x}$. _Clauses_ are disjunctions of literals
and _CNF formulas_ are conjunctions of clauses. The negation of clause $C$ can
be labelled $\bar{C}$ and is a CNF of clauses each containing one literal. The
symbols $\lor$, $\land$ denote disjunction and conjunction and we use $\oplus$
for exclusive disjunction, that is, $x\oplus y=x+y\text{ mod }2$. The
_canonical CNF representation_ of a _parity constraint_
$x_{1}\oplus\dots\oplus x_{k}=0$ is the CNF formula
$\mathsf{xor}(x_{1},\dots,x_{k})$ composed of all $2^{k-1}$ clauses of size
$k$ that contain an odd (resp. even) number of positive literals when $k$ is
odd (resp. even). For instance

$\mathsf{xor}(p,q,r):=(\bar{p}\vee\bar{q}\vee\bar{r})\wedge(\bar{p}\vee q\vee
r)\wedge(p\vee\bar{q}\vee r)\wedge(p\vee q\vee\bar{r}).$

The canonical representation of $x_{1}\oplus\dots\oplus x_{k}=1$ is just
$\mathsf{xor}(x_{1},\dots,x_{k})$ where we flip all literals for an arbitrary
variable, for instance $\mathsf{xor}(\bar{x}_{1},x_{2},\dots,x_{k})$.

### Proofs and Refutations

#### Resolution.

_Resolution_ is a refutational proof system that works by adding clauses based
on a single binary rule—the resolution rule (Robinson 1963). The resolution
rule’s new clause is a logical implication. Adding it to the formula preserves
not only satisfiability but also the models. A resolution proof that derives
the empty clause shows that the original formula is unsatisfiable.

$C_{1}\vee x$ $C_{2}\vee\neg x$ (Resolution) $C_{1}\vee C_{2}$

#### Extended Resolution.

_Extended resolution_ adds an extension rule, it creates extension clauses
that introduce a new variable with clauses that force that new variables to
follow a definition. If we treat the extension variables as new, the extension
rule does not change the satisfying assignments when considering only the
original variables. Therefore, when we reach the empty clause, we know that
the original formula must have been unsatisfiable.

######  Example 1.

We can add the following extension clauses that state that extension variable
$n$ is the exclusive or of $x$ with $y$: $(\bar{x}\vee y\vee
n),(x\vee\bar{y}\vee n),(x\vee y\vee\bar{n}),(\bar{x}\vee\bar{y}\vee\bar{n})$.

#### DRAT.

Unit propagation is an incomplete, model preserving, and polynomial-time
process.

######  Definition 1.

A unit clause is a clause of one literal. _Unit propagation_ takes any unit
clause $(a)$ and resolves it with every clause which has an $\bar{a}$ in it
(possibly creating another unit clause). After all resolvents are found, the
clause $(a)$ is removed, and we repeat the process for another unit clause
until no unit clauses remain. We also terminate if we reach the empty clause,
and we can write $F\vdash_{1}\bot$ to denote that unit propagation of $F$
reaches the empty clause.

While unit propagation itself is incomplete, it terminates in polynomial time.
It therefore is a convenient tool for checking implication, we can use this in
the concept of an asymmetric tautology, which is a clause that must be true
assuming a CNF because its negation would cause a conflict via unit
propagation.

######  Definition 2 (Järvisalo, Heule, and Biere 2012).

Let $F$ be a CNF formula. A clause $C$ is an _asymmetric tautology_ (AT)
w.r.t. $F$ if $F\wedge\bar{C}\vdash_{1}\bot$.

A clause being an asymmetric tautology in $F$ is a generalization of being a
resolvent of some pair of clauses in $F$. We also want to be able to
generalize the creation of extension clauses. To do this, we first generalize
extension clauses to blocked clauses. Blocked clauses are clauses that have a
literal that cannot be resolved without causing a tautology, and so they are
non-threatening to the satisfiability of the formula. We generalize blocked
clauses to RAT clauses, where we widen the condition of tautology to
asymmetric tautology.

######  Definition 3 (Järvisalo, Heule, and Biere 2012).

Let $F$ be a CNF formula. A clause $C$ is a _resolution asymmetry tautology_
(RAT) w.r.t. $F$ if there exists a literal $l\in C$ such that for every clause
$\bar{l}\vee D\in F$ it holds that
$F\wedge\bar{D}\wedge\bar{C}\vdash_{1}\bot$.

DRAT is a generalized and application friendly version of extended resolution.
Each rule modifies a formula by either adding (removing) a clause while
preserving satisfiability (unsatisfiability), respectively. Unlike resolution,
clauses can be added (removed) with or without preserving the exact set of
satisfying models of a formula. The first set of DRAT rules show us how we can
add or remove clauses while preserving models by using asymmetric tautologies
when $C$ is AT w.r.t. $F$:  $F$ (ATA) $F\wedge C$ $F\wedge C$ (ATE) $F$

The second set of rules use resolution asymmetric tautologies ($C$ is RAT
w.r.t. $F$) and do not preserve models:  $F$ (RATA) $F\wedge C$ $F\wedge C$
(RATE) $F$

In all clause additions, we can add a new variable as long as it works with
the side conditions of the rules. However, an excess of new variables can
cause a proof checker to slow down, so there is a version of DRAT that forbids
new variables known as DRAT-.

### Treewidth

A tree decomposition $(T,\lambda)$ of $G$ consists of a tree $T$ equipped with
a mapping $\lambda:V(T)\rightarrow\mathcal{P}(V(G))$ such that

  * •

$\bigcup_{t\in V(T)}\lambda(t)=V(G)$,

  * •

for every $uv\in E(G)$, there is $t\in V(T)$ such that
$\\{u,v\\}\subseteq\lambda(t)$,

  * •

for every $v\in V(G)$, $T[\\{\,t\mid v\in\lambda(t)\,\\}]$ is a connected
subtree of $T$.

The _width_ of $(T,\lambda)$ is $\max_{t\in V(T)}|\lambda(t)|-1$. The
treewidth of $G$, denoted by $tw(G)$, is the smallest width over all tree
decompositions of $G$.

### Tseitin Formulas

A _Tseitin formula_ is a CNF formula that represents a system of parity
constraints where every variable appears in exactly two constraints. Such a
formula is determined by a graph $G$: each edge $e$ corresponds to a unique
Boolean variable $x_{e}$ and each vertex $v$ defines a constraint
$\bigoplus_{e\in E(v)}x_{e}=c(v)$, where $E(v)$ is the set of edges incident
to $v$ in $G$ and $c:V(G)\rightarrow\\{0,1\\}$ is the _charge function_. The
Tseitin formula $T(G,c)$ is the conjunction of the $\mathsf{xor}$
representations for the constraints for every $v\in V(G)$. We call $G$ the
_Tseitin graph_ of the formula. It is often assumed that the maximum degree of
all vertices in $G$ is bounded by a constant, so that the size of $T(G,c)$ is
linear in $|var(T(G,c))|=|E(G)|$.

######  Example 2.

Let $G$ be the following graph with $V(G)=\\{1,2,3,4\\}$. Let
$c:V(G)\rightarrow\\{0,1\\}$ such that gray vertices have charge $0$ and white
vertices have charge $1$.  $x_{12}\oplus x_{13}\oplus x_{14}=0$ $x_{12}\oplus
x_{23}=1$ $x_{13}\oplus x_{23}\oplus x_{34}=1$ $x_{14}\oplus x_{34}=0$
$1$$2$$3$$4$ The Tseitin formula for this graph and this charge $c$ is

$T(G,c)=\mathsf{xor}(x_{12},x_{13},x_{14})\land\mathsf{xor}(\bar{x}_{12},x_{23})\\\
\land\mathsf{xor}(\bar{x}_{13},x_{23},x_{34})\land\mathsf{xor}(x_{14},x_{34}).$

Tseitin formulas were introduced by Tseitin (1968, 1983) in the 1960s as hard
instances for proof systems, despite an easy criterion to decide their
satisfiability (Urquhart 1987, Lemma 4.1). Urquhart (1987) later showed that
when $G$ belongs to the family of bounded-degree expander graphs (whose
definition we omit), all resolution refutations of $T(G,c)$ require
exponentially many clauses. This was generalized by Ben-Sasson and Widgerson
who used their width-length relations on refutation proofs to derive
exponential lower bounds parameterized on the edge expansion of $G$ (Ben-
Sasson and Wigderson 2001). Beyond expansion, the key parameter to
characterize the hardness of Tseitin formulas for resolution could be the
treewidth of the graph. Treewidth is a very well-known graph parameter whose
definition we omit (see (Bodlaender 1998)). Intuitively the treewidth of $G$,
denoted by $tw(G)$, is an integer between $0$ and $|V(G)|$ that measures how
close $G$ is to a tree (trees having treewidth $1$). On the one hand, it was
shown (Alekhnovich and Razborov 2011) that unsatisfiable Tseitin formulas have
resolution refutations of length at most $2^{O(tw(G))}|E(G)|^{O(1)}$, thus a
logarithmic treewidth guarantees short refutations. On the other hand,
combining the width-length relation with Corollaries 8 and 16 of Galesi et
al.’s (2020) yields the following:

######  Theorem 5.

Let $G$ be an $n$-vertex graph whose maximum degree is bounded by a constant,
if $tw(G)=\Omega(n)$, then the length of a shortest resolution refutation of
an unsatisfiable Tseitin formula $T(G,c)$ is at least $2^{\Omega(n)}$.

###### Proof.

Using (Ben-Sasson and Wigderson 2001, Corollary 3.6), the length of the
shortest resolution refutation of any unsatisfiable CNF formula $F$ is at
least $\exp(\Omega((w(F,\vdash)-w(F))^{2}/n))$ where $w(F)$ is the length of
the longest clause in $F$, and $w(F,\vdash)$ is the largest $k$ such that
every refutation of $F$ by resolution contains a clause of length $k$. Now let
$\Delta=O(1)$ be the maximum degree of $G$. Then $w(T(G,c))=\Delta$ and the
length of the shortest resolution refutation of $T(G,c)$ is in
$\exp(\Omega(w(T(G,c),\vdash)^{2}/n))$.

By (Galesi, Talebanfard, and Torán 2020, Corollaries 8 and 16),
$w(T(G,c),\vdash)=\max(\Delta,tw(L(G)))$ where $L(G)$ is the _line graph_ of
$G$ (see (Galesi, Talebanfard, and Torán 2020, Definition 6) if needed). It is
well-known that $tw(L(G))\geq\frac{1}{2}(tw(G)+1)-1$, see for instance (Harvey
and Wood 2018). So $tw(G)=\Omega(n)$ implies $tw(L(G))=\Omega(n)$, which
implies $w(T(G,c),\vdash)=\Omega(n)$. And the theorem follows. ∎

Note that there is still a gray area for $tw(G)$ less than linear, but more
than logarithmic in $n$. Note also that Tseitin formulas are easily refutable
in proof systems different from resolution, regardless of high treewidth
(Itsykson et al. 2020; Bonacina, Bonet, and Levy 2023).

## Parity Problems

For a constraint $x_{1}\oplus\dots\oplus x_{n}=c$, the number of clauses in
the canonical representation is exponential in $n$. We can use the
$\mathsf{xor}$ notation to build larger parity constraints if we include
auxiliary variables called Tseitin variables:

######  Definition 4.

Let $\sigma$ be a permutation of $n$ elements and $X=\\{\,x_{i}\mid 1\leq
i\leq n\,\\}$ be an ordered set of literals. We define
$\mathsf{Parity}(X,T,\sigma)=\mathsf{xor}(x_{\sigma(1)},x_{\sigma(2)},t_{1})\land{\bigwedge_{j=1}^{n-4}\mathsf{xor}(t_{j},{x_{\sigma(j+2)}},t_{j+1})}\land\mathsf{xor}({t}_{n-3},x_{\sigma(n-1)},x_{\sigma(n)})$,
where $T=\\{\,t_{i}\mid i\leq n-3\,\\}$ are Tseitin variables.

Here $\mathsf{Parity}(X,T,\sigma)$ is satisfiable if and only if the total
parity of $X$ is $0$. If we wanted a constraint which is satisfiable if and
only if the parity was $1$, again we simply flip a literal. In our particular
Tseitin encoding, we structure the $\oplus$ linearly so that the formula for
$n=5,\sigma=\textit{id}$ looks like $((((x_{1}\oplus x_{2})\oplus x_{3})\oplus
x_{4})\oplus x_{5})$. Here the formula depth is linear, however the structure
does not affect the satisfiability as $\oplus$ is associative. Furthermore the
actual permutation $\sigma$ does not affect the satisfiability because
$\oplus$ is commutative.

### Problem 1: Reordered Parity

In our first problem we simply take two parity constraints that are in
contradiction. We simultaneously state that the variables of $X$ have $0$
parity and $1$ parity. This is obviously a contradiction. However in order to
make it difficult we use two different permutations to obscure the conflict.
We define

$\mathsf{rPar}(n,\sigma)=\mathsf{Parity}(X,S,\textit{id})\wedge\mathsf{Parity}(X^{\prime},T,\sigma)$

where $X=\\{\,x_{i}\mid 1\leq i\leq n\,\\}$, $X^{\prime}=\\{\,x_{i}\mid 1\leq
i<n\,\\}\cup\\{\bar{x}_{n}\\}$, $\sigma$ is a permutation of $n$ elements, and
id is the identity map. $S$, $T$, and $X$ are disjoint sets of variables. Note
that $\mathsf{rPar}(n,\sigma)$ is a Tseitin formula where each $\mathsf{xor}$
constraint corresponds to a vertex of the underlying graph. This is because
every variable appears in exactly two $\mathsf{xor}$ constraints. For $n$
fixed, its Tseitin graph depends only on $\sigma$ and its vertices all have
charge $0$, except for the vertex corresponding to
$\mathsf{xor}(t_{n-3},x_{\sigma(n-1)},\bar{x}_{\sigma_{n}})$.

######  Fact 1.

$\mathsf{rPar}(n,\sigma)$ is an unsatisfiable Tseitin formula.

The version where the identity map is used for $\sigma$ is the most natural,
and is easy to solve. However the random version can still appear from
equivalences (which themselves are xors) obfuscating the random parity. For
example: A system of equations containing $x_{1}\oplus x_{2}\oplus x_{3}\oplus
x_{4}=0$ and $x_{5}\oplus x_{6}\oplus x_{7}\oplus x_{8}=1$ and other binary
clauses implying: $x_{5}\leftrightarrow x_{4}$ and $x_{6}\leftrightarrow
x_{1}$ and $x_{7}\leftrightarrow x_{2}$ and $x_{8}\leftrightarrow x_{3}$. A
standard CNF encoding using the natural variable ordering
$x_{1}<x_{2}<x_{3}<x_{4}<x_{5}<x_{6}<x_{7}<x_{8}$ (as done in the Dubois
benchmark family) yields a non-trivial random parity problem after removing
binary clauses, namely: $x_{1}\oplus x_{2}\oplus x_{3}\oplus x_{4}=0$ encoded
in CNF using the ordering $x_{1}<x_{2}<x_{3}<x_{4}$, and $x_{4}\oplus
x_{1}\oplus x_{2}\oplus x_{3}=1$ encoded in CNF using the ordering
$x_{4}<x_{1}<x_{2}<x_{3}$.

### Problem 2: Random Parity Addition

Problem 1 is a simple special case. In general, solvers and preprocessors want
to deal with XOR-constraints by Gaussian elimination. In Gaussian elimination
we use multiple steps involving adding two parity constraints together to get
a third parity constraint. Since the parity constraints may have a large
number of input variables we would have to use Tseitin variables, including in
the sum constraint. We model the difficulty of an addition step by taking the
three parity constraints: the two summands and the negation of the sum, in
conjunction to get a contradiction.

Let $a=\mathsf{Parity}(A,S,\sigma_{a})$ and
$b=\mathsf{Parity}(B,T,\sigma_{b})$, where $A$ and $B$ are subsets of
$X=\\{\,x_{i}\mid 1\leq i\leq n\,\\}$ and $S$ and $T$ are disjoint sets of
Tseitin variables. We define

$\mathsf{rAddPar}(a,b,\sigma_{c})=\mathsf{Parity}(A,S,\sigma_{a})\\\
\land\mathsf{Parity}(B,T,\sigma_{b})\land\mathsf{Parity}(C,U,\sigma_{c})$

where $U$ is disjoint from $S$, $T$ and $X$. Here $C$ is the symmetric
difference of $A$ and $B$ but with a literal flipped. In a first scenario, the
variable ordering $\sigma_{c}$ for the sum constraint is independent of that
used in $a$ and $b$. This is modeled fixing $\sigma_{c}$ to be the identity
id. For convenience we write
$\mathsf{rAddPar}(a,b)=\mathsf{rAddPar}(a,b,\textit{id})$. A more clever
approach is to choose $\sigma_{c}$ favorably for $\sigma_{a}$ and
$\sigma_{b}$. We will precise what we mean by “choosing $\sigma_{c}$
favorably” later in the paper.

Again $\mathsf{rAddPar}(a,b,\sigma_{c})$ is a Tseitin formula since every
variable appears in two $\mathsf{xor}$ constraints. Every variable appearing
in $A$ and $B$ does not appear in the third constraint, and every variable in
the symmetric difference of $A$ and $B$ appears a second time the third
constraint. The Tseitin variables are disjoint so they also appear in exactly
two $\mathsf{xor}$.

######  Fact 2.

$\mathsf{rAddPar}(a,b,\sigma_{c})$ is an unsatisfiable Tseitin formula.

## The Graph Model and Lower Bounds

In this section we present our lower bounds on the length of resolution
refutations for $\mathsf{rPar}$ and $\mathsf{rAddPar}$ when they are
constructed in a random fashion.

### Lower Bounds for Reordered Parity

In the following, we denote the set $\\{1,\dots,n\\}$ by $[n]$ and we call
$\mathfrak{S}_{n}$ the set of permutations of $[n]$. Consider $2n$ vertices
labeled $1,\dots,n,1^{\prime},\dots,n^{\prime}$, a permutation
$\sigma\in\mathfrak{S}_{n}$, and let $G_{\sigma}$ be the graph over these
vertices whose edge set is $\\{\,(i,i+1)\mid
i<n\,\\}\cup\\{\,(\sigma(i)^{\prime},\sigma(i+1)^{\prime})\mid
i<n\,\\}\cup\\{\,(i,i^{\prime})\mid i\leq n\,\\}$. Let $G^{*}_{\sigma}$ be the
multigraph obtained by contracting the edges $(i,i^{\prime})$ for all
$i\in[n]$. That is, $V(G^{*}_{\sigma})=[n]$ and, for every edge $(i,j)$,
$(i^{\prime},j)$, $(i,j^{\prime})$ or $(i^{\prime},j^{\prime})$ in $E(G)$, we
add an edge $(i,j)$ to $E(G^{*}_{\sigma})$.

######  Example 3.

Let $n=5$ and $\sigma(1)=3$, $\sigma(2)=1$, $\sigma(3)=5$, $\sigma(4)=4$,
$\sigma(5)=2$. The graph $G_{\sigma}$ and $G^{*}_{\sigma}$ are:

$G_{\sigma}=\raisebox{-0.5pt}{ \leavevmode\hbox to55.09pt{\vbox
to76.93pt{\pgfpicture\makeatletter\hbox{\hskip
12.76848pt\lower-70.33437pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}} ; ; ; \par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{0.0pt}\pgfsys@curveto{1.90918pt}{1.05441pt}{1.05441pt}{1.90918pt}{0.0pt}{1.90918pt}\pgfsys@curveto{-1.05441pt}{1.90918pt}{-1.90918pt}{1.05441pt}{-1.90918pt}{0.0pt}\pgfsys@curveto{-1.90918pt}{-1.05441pt}{-1.05441pt}{-1.90918pt}{0.0pt}{-1.90918pt}\pgfsys@curveto{1.05441pt}{-1.90918pt}{1.90918pt}{-1.05441pt}{1.90918pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-2.89996pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-15.93352pt}\pgfsys@curveto{1.90918pt}{-14.8791pt}{1.05441pt}{-14.02434pt}{0.0pt}{-14.02434pt}\pgfsys@curveto{-1.05441pt}{-14.02434pt}{-1.90918pt}{-14.8791pt}{-1.90918pt}{-15.93352pt}\pgfsys@curveto{-1.90918pt}{-16.98793pt}{-1.05441pt}{-17.8427pt}{0.0pt}{-17.8427pt}\pgfsys@curveto{1.05441pt}{-17.8427pt}{1.90918pt}{-16.98793pt}{1.90918pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-18.83353pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-31.86705pt}\pgfsys@curveto{1.90918pt}{-30.81264pt}{1.05441pt}{-29.95787pt}{0.0pt}{-29.95787pt}\pgfsys@curveto{-1.05441pt}{-29.95787pt}{-1.90918pt}{-30.81264pt}{-1.90918pt}{-31.86705pt}\pgfsys@curveto{-1.90918pt}{-32.92146pt}{-1.05441pt}{-33.77623pt}{0.0pt}{-33.77623pt}\pgfsys@curveto{1.05441pt}{-33.77623pt}{1.90918pt}{-32.92146pt}{1.90918pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-34.76712pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-47.80095pt}\pgfsys@curveto{1.90918pt}{-46.74654pt}{1.05441pt}{-45.89177pt}{0.0pt}{-45.89177pt}\pgfsys@curveto{-1.05441pt}{-45.89177pt}{-1.90918pt}{-46.74654pt}{-1.90918pt}{-47.80095pt}\pgfsys@curveto{-1.90918pt}{-48.85536pt}{-1.05441pt}{-49.71013pt}{0.0pt}{-49.71013pt}\pgfsys@curveto{1.05441pt}{-49.71013pt}{1.90918pt}{-48.85536pt}{1.90918pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-50.70108pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-63.73448pt}\pgfsys@curveto{1.90918pt}{-62.68007pt}{1.05441pt}{-61.8253pt}{0.0pt}{-61.8253pt}\pgfsys@curveto{-1.05441pt}{-61.8253pt}{-1.90918pt}{-62.68007pt}{-1.90918pt}{-63.73448pt}\pgfsys@curveto{-1.90918pt}{-64.7889pt}{-1.05441pt}{-65.64366pt}{0.0pt}{-65.64366pt}\pgfsys@curveto{1.05441pt}{-65.64366pt}{1.90918pt}{-64.7889pt}{1.90918pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-66.63467pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{0.0pt}\pgfsys@curveto{30.07736pt}{1.05441pt}{29.2226pt}{1.90918pt}{28.16818pt}{1.90918pt}\pgfsys@curveto{27.11377pt}{1.90918pt}{26.259pt}{1.05441pt}{26.259pt}{0.0pt}\pgfsys@curveto{26.259pt}{-1.05441pt}{27.11377pt}{-1.90918pt}{28.16818pt}{-1.90918pt}\pgfsys@curveto{29.2226pt}{-1.90918pt}{30.07736pt}{-1.05441pt}{30.07736pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{33.4369pt}{-3.59998pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-15.93352pt}\pgfsys@curveto{30.07736pt}{-14.8791pt}{29.2226pt}{-14.02434pt}{28.16818pt}{-14.02434pt}\pgfsys@curveto{27.11377pt}{-14.02434pt}{26.259pt}{-14.8791pt}{26.259pt}{-15.93352pt}\pgfsys@curveto{26.259pt}{-16.98793pt}{27.11377pt}{-17.8427pt}{28.16818pt}{-17.8427pt}\pgfsys@curveto{29.2226pt}{-17.8427pt}{30.07736pt}{-16.98793pt}{30.07736pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{33.4369pt}{-19.53354pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-31.86705pt}\pgfsys@curveto{30.07736pt}{-30.81264pt}{29.2226pt}{-29.95787pt}{28.16818pt}{-29.95787pt}\pgfsys@curveto{27.11377pt}{-29.95787pt}{26.259pt}{-30.81264pt}{26.259pt}{-31.86705pt}\pgfsys@curveto{26.259pt}{-32.92146pt}{27.11377pt}{-33.77623pt}{28.16818pt}{-33.77623pt}\pgfsys@curveto{29.2226pt}{-33.77623pt}{30.07736pt}{-32.92146pt}{30.07736pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{33.4369pt}{-35.46713pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-47.80095pt}\pgfsys@curveto{30.07736pt}{-46.74654pt}{29.2226pt}{-45.89177pt}{28.16818pt}{-45.89177pt}\pgfsys@curveto{27.11377pt}{-45.89177pt}{26.259pt}{-46.74654pt}{26.259pt}{-47.80095pt}\pgfsys@curveto{26.259pt}{-48.85536pt}{27.11377pt}{-49.71013pt}{28.16818pt}{-49.71013pt}\pgfsys@curveto{29.2226pt}{-49.71013pt}{30.07736pt}{-48.85536pt}{30.07736pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{33.4369pt}{-51.4011pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-63.73448pt}\pgfsys@curveto{30.07736pt}{-62.68007pt}{29.2226pt}{-61.8253pt}{28.16818pt}{-61.8253pt}\pgfsys@curveto{27.11377pt}{-61.8253pt}{26.259pt}{-62.68007pt}{26.259pt}{-63.73448pt}\pgfsys@curveto{26.259pt}{-64.7889pt}{27.11377pt}{-65.64366pt}{28.16818pt}{-65.64366pt}\pgfsys@curveto{29.2226pt}{-65.64366pt}{30.07736pt}{-64.7889pt}{30.07736pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{33.4369pt}{-67.33469pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-2.08917pt}\pgfsys@lineto{0.0pt}{-13.84438pt}\pgfsys@moveto{0.0pt}{-18.02274pt}\pgfsys@lineto{0.0pt}{-29.77797pt}\pgfsys@moveto{0.0pt}{-33.95633pt}\pgfsys@lineto{0.0pt}{-45.71193pt}\pgfsys@moveto{0.0pt}{-49.89029pt}\pgfsys@lineto{0.0pt}{-61.64552pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{28.16805pt}{-2.08917pt}\pgfsys@lineto{28.16805pt}{-13.84438pt}\pgfsys@moveto{28.16805pt}{-18.02274pt}\pgfsys@lineto{28.16805pt}{-29.77797pt}\pgfsys@moveto{28.16805pt}{-33.95633pt}\pgfsys@lineto{28.16805pt}{-45.71193pt}\pgfsys@moveto{28.16805pt}{-49.89029pt}\pgfsys@lineto{28.16805pt}{-61.64552pt}\pgfsys@stroke\pgfsys@invoke{
} \par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.81839pt}{-1.0286pt}\pgfsys@lineto{26.34964pt}{-14.90495pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.06064pt}{-17.73349pt}\pgfsys@lineto{27.10742pt}{-61.9348pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.38359pt}{-30.30183pt}\pgfsys@lineto{26.78447pt}{-1.5653pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{-47.80113pt}\pgfsys@lineto{26.0789pt}{-47.80113pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.38359pt}{-62.16937pt}\pgfsys@lineto{26.78447pt}{-33.43251pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leavevmode\hbox to62.77pt{\vbox
to76.93pt{\pgfpicture\makeatletter\hbox{\hskip
12.76848pt\lower-70.33437pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}} ; ; ; \par\par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{0.0pt}\pgfsys@curveto{1.90918pt}{1.05441pt}{1.05441pt}{1.90918pt}{0.0pt}{1.90918pt}\pgfsys@curveto{-1.05441pt}{1.90918pt}{-1.90918pt}{1.05441pt}{-1.90918pt}{0.0pt}\pgfsys@curveto{-1.90918pt}{-1.05441pt}{-1.05441pt}{-1.90918pt}{0.0pt}{-1.90918pt}\pgfsys@curveto{1.05441pt}{-1.90918pt}{1.90918pt}{-1.05441pt}{1.90918pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-2.89996pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-15.93352pt}\pgfsys@curveto{1.90918pt}{-14.8791pt}{1.05441pt}{-14.02434pt}{0.0pt}{-14.02434pt}\pgfsys@curveto{-1.05441pt}{-14.02434pt}{-1.90918pt}{-14.8791pt}{-1.90918pt}{-15.93352pt}\pgfsys@curveto{-1.90918pt}{-16.98793pt}{-1.05441pt}{-17.8427pt}{0.0pt}{-17.8427pt}\pgfsys@curveto{1.05441pt}{-17.8427pt}{1.90918pt}{-16.98793pt}{1.90918pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-18.83353pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-31.86705pt}\pgfsys@curveto{1.90918pt}{-30.81264pt}{1.05441pt}{-29.95787pt}{0.0pt}{-29.95787pt}\pgfsys@curveto{-1.05441pt}{-29.95787pt}{-1.90918pt}{-30.81264pt}{-1.90918pt}{-31.86705pt}\pgfsys@curveto{-1.90918pt}{-32.92146pt}{-1.05441pt}{-33.77623pt}{0.0pt}{-33.77623pt}\pgfsys@curveto{1.05441pt}{-33.77623pt}{1.90918pt}{-32.92146pt}{1.90918pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-34.76712pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-47.80095pt}\pgfsys@curveto{1.90918pt}{-46.74654pt}{1.05441pt}{-45.89177pt}{0.0pt}{-45.89177pt}\pgfsys@curveto{-1.05441pt}{-45.89177pt}{-1.90918pt}{-46.74654pt}{-1.90918pt}{-47.80095pt}\pgfsys@curveto{-1.90918pt}{-48.85536pt}{-1.05441pt}{-49.71013pt}{0.0pt}{-49.71013pt}\pgfsys@curveto{1.05441pt}{-49.71013pt}{1.90918pt}{-48.85536pt}{1.90918pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-50.70108pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-63.73448pt}\pgfsys@curveto{1.90918pt}{-62.68007pt}{1.05441pt}{-61.8253pt}{0.0pt}{-61.8253pt}\pgfsys@curveto{-1.05441pt}{-61.8253pt}{-1.90918pt}{-62.68007pt}{-1.90918pt}{-63.73448pt}\pgfsys@curveto{-1.90918pt}{-64.7889pt}{-1.05441pt}{-65.64366pt}{0.0pt}{-65.64366pt}\pgfsys@curveto{1.05441pt}{-65.64366pt}{1.90918pt}{-64.7889pt}{1.90918pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-66.63467pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-31.86705pt}\pgfsys@curveto{30.07736pt}{-30.81264pt}{29.2226pt}{-29.95787pt}{28.16818pt}{-29.95787pt}\pgfsys@curveto{27.11377pt}{-29.95787pt}{26.259pt}{-30.81264pt}{26.259pt}{-31.86705pt}\pgfsys@curveto{26.259pt}{-32.92146pt}{27.11377pt}{-33.77623pt}{28.16818pt}{-33.77623pt}\pgfsys@curveto{29.2226pt}{-33.77623pt}{30.07736pt}{-32.92146pt}{30.07736pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{41.1191pt}{-35.46713pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{0.0pt}\pgfsys@curveto{30.07736pt}{1.05441pt}{29.2226pt}{1.90918pt}{28.16818pt}{1.90918pt}\pgfsys@curveto{27.11377pt}{1.90918pt}{26.259pt}{1.05441pt}{26.259pt}{0.0pt}\pgfsys@curveto{26.259pt}{-1.05441pt}{27.11377pt}{-1.90918pt}{28.16818pt}{-1.90918pt}\pgfsys@curveto{29.2226pt}{-1.90918pt}{30.07736pt}{-1.05441pt}{30.07736pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{41.1191pt}{-3.59998pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-63.73448pt}\pgfsys@curveto{30.07736pt}{-62.68007pt}{29.2226pt}{-61.8253pt}{28.16818pt}{-61.8253pt}\pgfsys@curveto{27.11377pt}{-61.8253pt}{26.259pt}{-62.68007pt}{26.259pt}{-63.73448pt}\pgfsys@curveto{26.259pt}{-64.7889pt}{27.11377pt}{-65.64366pt}{28.16818pt}{-65.64366pt}\pgfsys@curveto{29.2226pt}{-65.64366pt}{30.07736pt}{-64.7889pt}{30.07736pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{41.1191pt}{-67.33469pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-47.80095pt}\pgfsys@curveto{30.07736pt}{-46.74654pt}{29.2226pt}{-45.89177pt}{28.16818pt}{-45.89177pt}\pgfsys@curveto{27.11377pt}{-45.89177pt}{26.259pt}{-46.74654pt}{26.259pt}{-47.80095pt}\pgfsys@curveto{26.259pt}{-48.85536pt}{27.11377pt}{-49.71013pt}{28.16818pt}{-49.71013pt}\pgfsys@curveto{29.2226pt}{-49.71013pt}{30.07736pt}{-48.85536pt}{30.07736pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{41.1191pt}{-51.4011pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{30.07736pt}{-15.93352pt}\pgfsys@curveto{30.07736pt}{-14.8791pt}{29.2226pt}{-14.02434pt}{28.16818pt}{-14.02434pt}\pgfsys@curveto{27.11377pt}{-14.02434pt}{26.259pt}{-14.8791pt}{26.259pt}{-15.93352pt}\pgfsys@curveto{26.259pt}{-16.98793pt}{27.11377pt}{-17.8427pt}{28.16818pt}{-17.8427pt}\pgfsys@curveto{29.2226pt}{-17.8427pt}{30.07736pt}{-16.98793pt}{30.07736pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{28.16818pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{28.16818pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{41.1191pt}{-19.53354pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-2.08917pt}\pgfsys@lineto{0.0pt}{-13.84438pt}\pgfsys@moveto{0.0pt}{-18.02274pt}\pgfsys@lineto{0.0pt}{-29.77797pt}\pgfsys@moveto{0.0pt}{-33.95633pt}\pgfsys@lineto{0.0pt}{-45.71193pt}\pgfsys@moveto{0.0pt}{-49.89029pt}\pgfsys@lineto{0.0pt}{-61.64552pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{29.58875pt}{-30.3354pt}\pgfsys@curveto{37.59488pt}{-21.70323pt}{37.59488pt}{-10.16393pt}{29.58875pt}{-1.53177pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{27.20451pt}{-1.85367pt}\pgfsys@curveto{16.17023pt}{-23.08109pt}{16.17023pt}{-40.65361pt}{27.20451pt}{-61.88103pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{29.57661pt}{-62.19179pt}\pgfsys@curveto{33.10161pt}{-58.33064pt}{33.10161pt}{-53.20518pt}{29.57655pt}{-49.34409pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{29.58875pt}{-46.26936pt}\pgfsys@curveto{37.59499pt}{-37.63707pt}{37.59499pt}{-26.09763pt}{29.5887pt}{-17.46535pt}\pgfsys@stroke\pgfsys@invoke{
} \par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{0.0pt}\pgfsys@lineto{26.0789pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{-15.93356pt}\pgfsys@lineto{26.0789pt}{-15.93356pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{-31.86716pt}\pgfsys@lineto{26.0789pt}{-31.86716pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{-47.80113pt}\pgfsys@lineto{26.0789pt}{-47.80113pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.08916pt}{-63.73473pt}\pgfsys@lineto{26.0789pt}{-63.73473pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad
G^{*}_{\sigma}=\raisebox{-0.5pt}{ \leavevmode\hbox to30.08pt{\vbox
to75.53pt{\pgfpicture\makeatletter\hbox{\hskip-235.62144pt\lower-69.63435pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}} ; ; ; {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{257.98227pt}{0.0pt}\pgfsys@curveto{257.98227pt}{1.05441pt}{257.1275pt}{1.90918pt}{256.07309pt}{1.90918pt}\pgfsys@curveto{255.01868pt}{1.90918pt}{254.16391pt}{1.05441pt}{254.16391pt}{0.0pt}\pgfsys@curveto{254.16391pt}{-1.05441pt}{255.01868pt}{-1.90918pt}{256.07309pt}{-1.90918pt}\pgfsys@curveto{257.1275pt}{-1.90918pt}{257.98227pt}{-1.05441pt}{257.98227pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{256.07309pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{256.07309pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{238.62112pt}{-2.89996pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{257.98227pt}{-15.93352pt}\pgfsys@curveto{257.98227pt}{-14.8791pt}{257.1275pt}{-14.02434pt}{256.07309pt}{-14.02434pt}\pgfsys@curveto{255.01868pt}{-14.02434pt}{254.16391pt}{-14.8791pt}{254.16391pt}{-15.93352pt}\pgfsys@curveto{254.16391pt}{-16.98793pt}{255.01868pt}{-17.8427pt}{256.07309pt}{-17.8427pt}\pgfsys@curveto{257.1275pt}{-17.8427pt}{257.98227pt}{-16.98793pt}{257.98227pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{256.07309pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{256.07309pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{238.62112pt}{-18.83353pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{257.98227pt}{-31.86705pt}\pgfsys@curveto{257.98227pt}{-30.81264pt}{257.1275pt}{-29.95787pt}{256.07309pt}{-29.95787pt}\pgfsys@curveto{255.01868pt}{-29.95787pt}{254.16391pt}{-30.81264pt}{254.16391pt}{-31.86705pt}\pgfsys@curveto{254.16391pt}{-32.92146pt}{255.01868pt}{-33.77623pt}{256.07309pt}{-33.77623pt}\pgfsys@curveto{257.1275pt}{-33.77623pt}{257.98227pt}{-32.92146pt}{257.98227pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{256.07309pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{256.07309pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{238.62112pt}{-34.76712pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{257.98227pt}{-47.80095pt}\pgfsys@curveto{257.98227pt}{-46.74654pt}{257.1275pt}{-45.89177pt}{256.07309pt}{-45.89177pt}\pgfsys@curveto{255.01868pt}{-45.89177pt}{254.16391pt}{-46.74654pt}{254.16391pt}{-47.80095pt}\pgfsys@curveto{254.16391pt}{-48.85536pt}{255.01868pt}{-49.71013pt}{256.07309pt}{-49.71013pt}\pgfsys@curveto{257.1275pt}{-49.71013pt}{257.98227pt}{-48.85536pt}{257.98227pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{256.07309pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{256.07309pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{238.62112pt}{-50.70108pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{257.98227pt}{-63.73448pt}\pgfsys@curveto{257.98227pt}{-62.68007pt}{257.1275pt}{-61.8253pt}{256.07309pt}{-61.8253pt}\pgfsys@curveto{255.01868pt}{-61.8253pt}{254.16391pt}{-62.68007pt}{254.16391pt}{-63.73448pt}\pgfsys@curveto{254.16391pt}{-64.7889pt}{255.01868pt}{-65.64366pt}{256.07309pt}{-65.64366pt}\pgfsys@curveto{257.1275pt}{-65.64366pt}{257.98227pt}{-64.7889pt}{257.98227pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{256.07309pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{256.07309pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{238.62112pt}{-66.63467pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par\par\par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{256.07199pt}{-2.08917pt}\pgfsys@lineto{256.072pt}{-13.84438pt}\pgfsys@moveto{256.07199pt}{-18.02274pt}\pgfsys@lineto{256.072pt}{-29.77797pt}\pgfsys@moveto{256.07199pt}{-33.95633pt}\pgfsys@lineto{256.072pt}{-45.71193pt}\pgfsys@moveto{256.07199pt}{-49.89029pt}\pgfsys@lineto{256.072pt}{-61.64552pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{257.49272pt}{-30.33534pt}\pgfsys@curveto{265.49895pt}{-21.70323pt}{265.49895pt}{-10.16393pt}{257.49269pt}{-1.53183pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{255.10852pt}{-1.85365pt}\pgfsys@curveto{244.07428pt}{-23.08109pt}{244.07428pt}{-40.65361pt}{255.10852pt}{-61.88106pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{257.48056pt}{-62.19167pt}\pgfsys@curveto{261.00566pt}{-58.33064pt}{261.00566pt}{-53.20518pt}{257.48048pt}{-49.3442pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{257.49272pt}{-46.2693pt}\pgfsys@curveto{265.49905pt}{-37.63707pt}{265.49905pt}{-26.09763pt}{257.49269pt}{-17.46541pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$

The maximum degree of a vertex of $G_{\sigma}$ (resp. $G^{*}_{\sigma}$) is $3$
(resp. $4$). Since $G^{*}_{\sigma}$ is a minor of $G_{\sigma}$ after merging
of the parallel edges, we have that $tw(G^{*}_{\sigma})\leq tw(G_{\sigma})$.
We also have a bound in the other direction which may be useful when
$tw(G_{\sigma})$ is harder to compute than $tw(G^{*}_{\sigma})$ in practice.

######  Lemma 1.

We have that $\frac{1}{2}tw(G_{\sigma})\leq tw(G^{*}_{\sigma})\leq
tw(G_{\sigma})$.

###### Proof.

We only have to show that $tw(G_{\sigma})\leq 2\cdot tw(G^{*}_{\sigma})$. Let
$(T,\lambda^{*})$ be a tree decomposition of $G^{*}_{\sigma}$ and let
$\lambda$ be defined by, $\forall t\in T$, $\lambda(t)=\\{\,i\mid
i\in\lambda^{*}(t)\,\\}\cup\\{\,i^{\prime}\mid i\in\lambda^{*}(t)\,\\}$. We
show that $(T,\lambda)$ is a tree decomposition of $G_{\sigma}$. First it is
clear that $\bigcup_{t\in T}\lambda(t)=V(G_{\sigma})$. Second, for every
$(i,j)$, $(i,j^{\prime})$, $(i^{\prime},j)$ or $(i^{\prime},j^{\prime})$ in
$G_{\sigma}$ there is a $t\in T$ such that $\lambda^{*}(t)$ contains $(i,j)$
so the four aforementioned edges belong to $\lambda(t)$. Finally, for every
$i\in[n]$ we have that $T[\\{\,t\mid i\in\lambda(t)\,\\}]=T[\\{\,t\mid
i^{\prime}\in\lambda(t)\,\\}]=T[\\{\,t\mid i\in\lambda^{*}(t)\,\\}]$ and we
know that $T[\\{\,t\mid i\in\lambda^{*}(t)\,\\}]$ is connected. The width of
$(T,\lambda)$ is twice that of $(T,\lambda^{*})$, so $tw(G_{\sigma})\leq
2\cdot tw(G^{*}_{\sigma})$. ∎

The Tseitin graph of $\mathsf{rPar}(n,\sigma)$ is not exactly $G_{\sigma}$.
The two graphs would be the same if we were to slightly modify the first and
last constraints of $\mathsf{Parity}(X,S,\textit{id})$ and
$\mathsf{Parity}(X^{\prime},T,\sigma)$ by replacing
$\mathsf{xor}(x_{1},x_{2},s_{1})$ by
$\mathsf{xor}(x_{1},\bar{s}_{0})\land\mathsf{xor}(s_{0},x_{2},s_{1})$ etc.

######  Lemma 2.

The Tseitin graph of $\mathsf{rPar}(n,\sigma)$ is obtained by contracting four
edges of $G_{\sigma}$.

###### Proof sketch.

Contract the edges $(1,2)$, $(n-1,n)$,
$(\sigma(1)^{\prime},\sigma(2)^{\prime})$ and
$(\sigma(n-1)^{\prime},\sigma(n)^{\prime})$ of $G_{\sigma}$. ∎

Since an edge contraction can only decrease the treewidth by one, it follows
that the treewidth of the Tseitin graph of $\mathsf{rPar}(n,\sigma)$ is at
least $tw(G_{\sigma})-4$. But then we show that when $\sigma$ is sampled
uniformly at random from $\mathfrak{S}_{n}$, with high probability (i.e., with
probability tending to $1$ as $n$ increases) both $G_{\sigma}$ and
$\mathsf{rPar}(n,\sigma)$ have linear treewidth.

######  Lemma 3.

There is a constant $\alpha>0$ such that $\textup{Pr}(tw(G_{\sigma})<\alpha
n)$ vanishes to $0$ as $n$ increases when $\sigma$ is chosen uniformly at
random in $\mathfrak{S}_{n}$.

###### Proof.

Kim and Wormald (2001) have studied the graph distribution
$\mathcal{H}_{n}\oplus\mathcal{H}_{n}$ where each graph over $n$ vertices is
the superposition of two independent hamiltonian cycles over these vertices
(merging parallel edges). They call $\mathcal{G}_{4,n}$ the uniform
distribution over all 4-regular graphs over $n$ vertices. They show that any
sequence of events is true asymptotically almost surely (a.a.s.) in
$\mathcal{H}_{n}\oplus\mathcal{H}_{n}$ if and only if it is true a.a.s. in
$\mathcal{G}_{4,n}$ (Kim and Wormald 2001, Theorem 2).

The treewidth of a random 4-regular graph from $\mathcal{G}_{4,n}$ is linear
in $n$ with high probability (Chandran and Subramanian 2003). On the one hand,
Chandran and Subramanian (2003) have shown that the treewidth of a $d$-regular
graph $G$ is at least
$\lfloor\frac{3n}{4}\frac{(d-\lambda_{2}(G))}{(3d-2\lambda_{2}(G))}\rfloor-1$
where $\lambda_{2}(G)$ is the second largest eigenvalue of the adjacency
matrix of $G$. On the other hand, Friedman has shown that, for any fixed
$\varepsilon>0$ and any $d\geq 2$, $|\lambda_{2}(G)|\leq
2\sqrt{d-1}+\varepsilon$ holds with high probability when
$G\in\mathcal{G}_{d,n}$ (Friedman 2003, Corollary 1.4)111Note that our
$\mathcal{G}_{d,n}$ is Friedman’s $\mathcal{K}_{d,n}$. The combination of the
two results yields that, with high probability when $G\in\mathcal{G}_{4,n}$,
$tw(G)\geq\Omega(n)$.

Thus, with high probability, a random graph
$G\in\mathcal{H}_{n}\oplus\mathcal{H}_{n}$ has linear treewidth. Now
$G^{*}_{\sigma}$ is not the superposition of two independent hamiltonian
cycles but the superposition of two independent paths. But if we close both
paths before superposition, then we obtain a graph in
$\mathcal{H}_{n}\oplus\mathcal{H}_{n}$ whose treewidth is at least
$tw(G^{*}_{\sigma})-2$. So with high probability $tw(G_{\sigma})\geq
tw(G^{*}_{\sigma})\geq\Omega(n)$ holds. ∎

$\mathsf{rPar}(n,\sigma)$’s graph has degree at most $4$ and linear treewidth
with high probability so, by Theorem 5 we immediately have that, with high
probability, the Tseitin formula is hard for resolution.

######  Theorem 1.

There is a constant $\alpha>0$ such that, with probability tending to $1$ as
$n$ increases, the length of a shortest resolution refutation of
$\mathsf{rPar}(n,\sigma)$ where $\sigma$ is chosen uniformly at random in
$\mathfrak{S}_{n}$, is least $2^{\alpha n}$.

### Lower Bounds for Random Parity Addition

The symmetric difference of two subsets $A$ and $B$ of
$X=\\{x_{1},\dots,x_{n}\\}$ is denoted by $A\triangle B:=(A\cup
B)\setminus(A\cap B)$. Recall that for $a=\mathsf{Parity}(A,S,\sigma_{a})$ and
$b=\mathsf{Parity}(B,T,\sigma_{b})$, the formula $\mathsf{rAddPar}(a,b)=a\land
b\land\mathsf{Parity}(C,U,\textit{id})$ is a Tseitin formula (where $U\cap
S=U\cap T=\emptyset$ and $C$ is $A\triangle B$ with one literal flipped). Let
us describe $\mathsf{rAddPar}(a,b)$’s Tseitin graph. We call $H$ the graph
whose vertices are split into three sets $V=\\{\,i\mid x_{i}\in A\,\\}$,
$V^{\prime}=\\{\,i^{\prime}\mid x_{i}\in B\,\\}$ and
$V^{\prime\prime}=\\{\,i^{\prime\prime}\mid x_{i}\in A\triangle B\,\\}$. The
edge set of $H$ contains $(i,i^{\prime})$ for all $x_{i}\in A\cap B$, and
$(i,i^{\prime\prime})$ for all $x_{i}\in A\cap(A\triangle B)$, and
$(i^{\prime},i^{\prime\prime})$ for all $x_{i}\in B\cap(A\triangle B)$. The
vertices in $V$ (resp. $V^{\prime}$ and $V^{\prime\prime}$) are also connected
in a path following the order $\sigma_{a}$ (resp. $\sigma_{b}$ and id). $H$ is
not exactly the Tseitin graph of $\mathsf{rAddPar}$, but is close enough and
easier to analyze.

######  Lemma 4.

For $a=\mathsf{Parity}(A,S,\sigma_{a})$ and $b=\mathsf{Parity}(B,T,$
$\sigma_{b})$ the Tseitin graph of $\mathsf{rAddPar}(a,b)$ is obtained by
contracting six edges of the graph $H$.

At this point it is worth giving an example of such a graph $H$.

######  Example 4.

Let $n=6$, $A=\\{x_{1},x_{2},x_{4},x_{5},x_{6}\\}$ and
$B=\\{x_{1},x_{2},x_{3},x_{5}\\}$. So $A\triangle B=\\{x_{3},x_{4},x_{6}\\}$.
The constraints encoded in CNF with $\mathsf{Parity}$ are $x_{1}\oplus
x_{2}\oplus x_{4}\oplus x_{5}\oplus x_{6}=0$, $x_{1}\oplus x_{2}\oplus
x_{3}\oplus x_{5}=0$ and $x_{3}\oplus x_{4}\oplus x_{6}=1$. Let
$\sigma_{a}(1)=4$, $\sigma_{a}(2)=5$, $\sigma_{a}(4)=1$, $\sigma_{a}(5)=6$,
$\sigma_{a}(6)=2$ and $\sigma_{b}(1)=1$, $\sigma_{b}(2)=5$, $\sigma_{b}(3)=2$,
$\sigma_{b}(5)=3$. Then the graph $H$ is:

$H=\raisebox{-0.5pt}{ \leavevmode\hbox to130.74pt{\vbox
to80.57pt{\pgfpicture\makeatletter\hbox{\hskip
12.76848pt\lower-74.66765pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}} ; ; ; \par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{0.0pt}\pgfsys@curveto{1.90918pt}{1.05441pt}{1.05441pt}{1.90918pt}{0.0pt}{1.90918pt}\pgfsys@curveto{-1.05441pt}{1.90918pt}{-1.90918pt}{1.05441pt}{-1.90918pt}{0.0pt}\pgfsys@curveto{-1.90918pt}{-1.05441pt}{-1.05441pt}{-1.90918pt}{0.0pt}{-1.90918pt}\pgfsys@curveto{1.05441pt}{-1.90918pt}{1.90918pt}{-1.05441pt}{1.90918pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-2.89996pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-15.93352pt}\pgfsys@curveto{1.90918pt}{-14.8791pt}{1.05441pt}{-14.02434pt}{0.0pt}{-14.02434pt}\pgfsys@curveto{-1.05441pt}{-14.02434pt}{-1.90918pt}{-14.8791pt}{-1.90918pt}{-15.93352pt}\pgfsys@curveto{-1.90918pt}{-16.98793pt}{-1.05441pt}{-17.8427pt}{0.0pt}{-17.8427pt}\pgfsys@curveto{1.05441pt}{-17.8427pt}{1.90918pt}{-16.98793pt}{1.90918pt}{-15.93352pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-15.93352pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-15.93352pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-18.83353pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-31.86705pt}\pgfsys@curveto{1.90918pt}{-30.81264pt}{1.05441pt}{-29.95787pt}{0.0pt}{-29.95787pt}\pgfsys@curveto{-1.05441pt}{-29.95787pt}{-1.90918pt}{-30.81264pt}{-1.90918pt}{-31.86705pt}\pgfsys@curveto{-1.90918pt}{-32.92146pt}{-1.05441pt}{-33.77623pt}{0.0pt}{-33.77623pt}\pgfsys@curveto{1.05441pt}{-33.77623pt}{1.90918pt}{-32.92146pt}{1.90918pt}{-31.86705pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-31.86705pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-31.86705pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-34.76712pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-47.80095pt}\pgfsys@curveto{1.90918pt}{-46.74654pt}{1.05441pt}{-45.89177pt}{0.0pt}{-45.89177pt}\pgfsys@curveto{-1.05441pt}{-45.89177pt}{-1.90918pt}{-46.74654pt}{-1.90918pt}{-47.80095pt}\pgfsys@curveto{-1.90918pt}{-48.85536pt}{-1.05441pt}{-49.71013pt}{0.0pt}{-49.71013pt}\pgfsys@curveto{1.05441pt}{-49.71013pt}{1.90918pt}{-48.85536pt}{1.90918pt}{-47.80095pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-47.80095pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-47.80095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-50.70108pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$6$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{1.90918pt}{-63.73448pt}\pgfsys@curveto{1.90918pt}{-62.68007pt}{1.05441pt}{-61.8253pt}{0.0pt}{-61.8253pt}\pgfsys@curveto{-1.05441pt}{-61.8253pt}{-1.90918pt}{-62.68007pt}{-1.90918pt}{-63.73448pt}\pgfsys@curveto{-1.90918pt}{-64.7889pt}{-1.05441pt}{-65.64366pt}{0.0pt}{-65.64366pt}\pgfsys@curveto{1.05441pt}{-65.64366pt}{1.90918pt}{-64.7889pt}{1.90918pt}{-63.73448pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{-63.73448pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{0.0pt}{-63.73448pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{{}{}}}{{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{-9.7688pt}{-66.63467pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par\par\par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{104.33841pt}{-7.96693pt}\pgfsys@curveto{104.33841pt}{-6.91252pt}{103.48364pt}{-6.05775pt}{102.42923pt}{-6.05775pt}\pgfsys@curveto{101.37482pt}{-6.05775pt}{100.52005pt}{-6.91252pt}{100.52005pt}{-7.96693pt}\pgfsys@curveto{100.52005pt}{-9.02135pt}{101.37482pt}{-9.87611pt}{102.42923pt}{-9.87611pt}\pgfsys@curveto{103.48364pt}{-9.87611pt}{104.33841pt}{-9.02135pt}{104.33841pt}{-7.96693pt}\pgfsys@closepath\pgfsys@moveto{102.42923pt}{-7.96693pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{102.42923pt}{-7.96693pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{107.69768pt}{-11.56693pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3^{\prime\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{104.33841pt}{-23.90047pt}\pgfsys@curveto{104.33841pt}{-22.84605pt}{103.48364pt}{-21.99129pt}{102.42923pt}{-21.99129pt}\pgfsys@curveto{101.37482pt}{-21.99129pt}{100.52005pt}{-22.84605pt}{100.52005pt}{-23.90047pt}\pgfsys@curveto{100.52005pt}{-24.95488pt}{101.37482pt}{-25.80965pt}{102.42923pt}{-25.80965pt}\pgfsys@curveto{103.48364pt}{-25.80965pt}{104.33841pt}{-24.95488pt}{104.33841pt}{-23.90047pt}\pgfsys@closepath\pgfsys@moveto{102.42923pt}{-23.90047pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{102.42923pt}{-23.90047pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{107.69768pt}{-27.50052pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$4^{\prime\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{104.33841pt}{-39.834pt}\pgfsys@curveto{104.33841pt}{-38.77959pt}{103.48364pt}{-37.92482pt}{102.42923pt}{-37.92482pt}\pgfsys@curveto{101.37482pt}{-37.92482pt}{100.52005pt}{-38.77959pt}{100.52005pt}{-39.834pt}\pgfsys@curveto{100.52005pt}{-40.88841pt}{101.37482pt}{-41.74318pt}{102.42923pt}{-41.74318pt}\pgfsys@curveto{103.48364pt}{-41.74318pt}{104.33841pt}{-40.88841pt}{104.33841pt}{-39.834pt}\pgfsys@closepath\pgfsys@moveto{102.42923pt}{-39.834pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{102.42923pt}{-39.834pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{107.69768pt}{-43.43411pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$6^{\prime\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{53.1238pt}{-7.96693pt}\pgfsys@curveto{53.1238pt}{-6.91252pt}{52.26903pt}{-6.05775pt}{51.21461pt}{-6.05775pt}\pgfsys@curveto{50.1602pt}{-6.05775pt}{49.30544pt}{-6.91252pt}{49.30544pt}{-7.96693pt}\pgfsys@curveto{49.30544pt}{-9.02135pt}{50.1602pt}{-9.87611pt}{51.21461pt}{-9.87611pt}\pgfsys@curveto{52.26903pt}{-9.87611pt}{53.1238pt}{-9.02135pt}{53.1238pt}{-7.96693pt}\pgfsys@closepath\pgfsys@moveto{51.21461pt}{-7.96693pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{51.21461pt}{-7.96693pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{56.48325pt}{-11.56693pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$1^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{53.1238pt}{-23.90047pt}\pgfsys@curveto{53.1238pt}{-22.84605pt}{52.26903pt}{-21.99129pt}{51.21461pt}{-21.99129pt}\pgfsys@curveto{50.1602pt}{-21.99129pt}{49.30544pt}{-22.84605pt}{49.30544pt}{-23.90047pt}\pgfsys@curveto{49.30544pt}{-24.95488pt}{50.1602pt}{-25.80965pt}{51.21461pt}{-25.80965pt}\pgfsys@curveto{52.26903pt}{-25.80965pt}{53.1238pt}{-24.95488pt}{53.1238pt}{-23.90047pt}\pgfsys@closepath\pgfsys@moveto{51.21461pt}{-23.90047pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{51.21461pt}{-23.90047pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{56.48325pt}{-27.50052pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$5^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{53.1238pt}{-39.834pt}\pgfsys@curveto{53.1238pt}{-38.77959pt}{52.26903pt}{-37.92482pt}{51.21461pt}{-37.92482pt}\pgfsys@curveto{50.1602pt}{-37.92482pt}{49.30544pt}{-38.77959pt}{49.30544pt}{-39.834pt}\pgfsys@curveto{49.30544pt}{-40.88841pt}{50.1602pt}{-41.74318pt}{51.21461pt}{-41.74318pt}\pgfsys@curveto{52.26903pt}{-41.74318pt}{53.1238pt}{-40.88841pt}{53.1238pt}{-39.834pt}\pgfsys@closepath\pgfsys@moveto{51.21461pt}{-39.834pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{51.21461pt}{-39.834pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{56.48325pt}{-43.43411pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$2^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{}}
{{{}{}{{}}{}}}{{{}}}{{{{}}{{}}}}{{}}{{}}{{{
}}}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\pgfsys@moveto{53.1238pt}{-55.76753pt}\pgfsys@curveto{53.1238pt}{-54.71312pt}{52.26903pt}{-53.85835pt}{51.21461pt}{-53.85835pt}\pgfsys@curveto{50.1602pt}{-53.85835pt}{49.30544pt}{-54.71312pt}{49.30544pt}{-55.76753pt}\pgfsys@curveto{49.30544pt}{-56.82195pt}{50.1602pt}{-57.67671pt}{51.21461pt}{-57.67671pt}\pgfsys@curveto{52.26903pt}{-57.67671pt}{53.1238pt}{-56.82195pt}{53.1238pt}{-55.76753pt}\pgfsys@closepath\pgfsys@moveto{51.21461pt}{-55.76753pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{51.21461pt}{-55.76753pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.9}{0.0}{0.0}{0.9}{56.48325pt}{-59.3677pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$3^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.89313pt}{-30.98366pt}\pgfsys@lineto{49.32126pt}{-8.85045pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{2.06432pt}{-16.2547pt}\pgfsys@lineto{49.15009pt}{-23.5794pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{1.89313pt}{-62.85121pt}\pgfsys@lineto{49.32126pt}{-40.71764pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{52.74168pt}{-54.34221pt}\pgfsys@lineto{100.90155pt}{-9.39246pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{1.85623pt}{-48.75978pt}\pgfsys@curveto{35.68158pt}{-66.22913pt}{88.3369pt}{-74.46765pt}{101.64145pt}{-41.76926pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{} {{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{2.08916pt}{0.0pt}\pgfsys@curveto{41.93538pt}{0.0pt}{75.47313pt}{4.83226pt}{100.99942pt}{-22.37692pt}\pgfsys@stroke\pgfsys@invoke{
} \par{{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{0.0pt}{-2.08917pt}\pgfsys@lineto{0.0pt}{-13.84438pt}\pgfsys@moveto{0.0pt}{-18.02274pt}\pgfsys@lineto{0.0pt}{-29.77797pt}\pgfsys@moveto{0.0pt}{-33.95633pt}\pgfsys@lineto{0.0pt}{-45.71193pt}\pgfsys@moveto{0.0pt}{-49.89029pt}\pgfsys@lineto{0.0pt}{-61.64552pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{51.21439pt}{-10.05614pt}\pgfsys@lineto{51.21439pt}{-21.81137pt}\pgfsys@moveto{51.21439pt}{-25.98973pt}\pgfsys@lineto{51.21439pt}{-37.74496pt}\pgfsys@moveto{51.21439pt}{-41.92332pt}\pgfsys@lineto{51.21439pt}{-53.67856pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}{{}} {{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}\pgfsys@moveto{102.42879pt}{-10.05614pt}\pgfsys@lineto{102.42882pt}{-21.81137pt}\pgfsys@moveto{102.42879pt}{-25.98973pt}\pgfsys@lineto{102.42882pt}{-37.74496pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }$

The Tseitin graph of $\mathsf{rAddPar}(a,b)$ is the graph $H$ above after
contraction of the edges $(4,5)$, $(6,2)$, $(1^{\prime},5^{\prime})$,
$(2^{\prime},3^{\prime})$, $(3^{\prime\prime},4^{\prime\prime})$ and
$(4^{\prime\prime},6^{\prime\prime})$.

Let $n^{\prime}=|A\cup B|$. Since $A\cap B$, $A\cap(A\triangle B)$ and
$B\cap(A\triangle B)$ are pairwise disjoint and form a partition of $A\cup B$,
we have that $\max(|A\cap B|,|A\cap(A\triangle B)|,|B\cap(A\triangle
B)|)\geq\frac{n^{\prime}}{3}$. We assume, without loss of generality, that
$|A\cap B|\geq\frac{n^{\prime}}{3}$. When both $A$ and $B$ are chosen
uniformly at random from $X$ then, with high probability, we have that
$n^{\prime}\geq\frac{n}{2}$ and thus $|A\cap B|\geq\frac{n}{6}$. We now show
that when $|A\cap B|>0$ we can find a minor of $H$ that is isomorphic to a
graph $G_{\sigma}$ with $\sigma\in\mathfrak{S}_{|A\cap B|}$. The minor, that
we call $m(H)$, is obtained as follows:

  * 1.

remove all edges incident to a vertex of $V^{\prime\prime}$, then remove
$V^{\prime\prime}$

  * 2.

contract every vertex $i\in V$ not connected to any $j^{\prime}\in V^{\prime}$
with one of its neighbors, repeat until $V$ contains only vertices connected
to some vertex in $V^{\prime}$

  * 3.

contract every vertex $i^{\prime}\in V^{\prime}$ not connected to any $j\in V$
with one of its neighbors, repeat until $V^{\prime}$ contains only vertices
connected to some vertex in $V$

The construction is illustrated by Figure 1 for the graph $H$ of Example 4.
The construction gives the same minor regardless of the neighbors chosen for
the contractions in steps 2 and 3.

$4$$5$$1$$6$$2$$1^{\prime}$$5^{\prime}$$2^{\prime}$$3^{\prime}$Step
1$5$$1$$2$$1^{\prime}$$5^{\prime}$$2^{\prime}$$3^{\prime}$Step
2$5$$1$$2$$1^{\prime}$$5^{\prime}$$2^{\prime}$Step 3 Figure 1: Construction of
$m(H)$

######  Lemma 5.

When $A$, $B$, $\sigma_{a}$ and $\sigma_{b}$ are chosen independently and
uniformly at random then, conditioned on $|A\cap B|=k$, the minor $m(H)$
follows the same distribution as $G_{\sigma}$ when $\sigma$ is sampled
uniformly at random in $\mathfrak{S}_{k}$.

###### Proof.

Consider the event “$m(H)$ is isomorphic to $G_{\sigma}$”, which we just
denote by $m(H)=G_{\sigma}$. Fix $A$ and $B$. For every $\sigma_{a}$ there is
a unique bijection $\rho_{a}:A\cap B\rightarrow[k]$ such that
$\rho_{a}^{-1}\circ\sigma_{a}\circ\rho_{a}=\textit{id}\in\mathfrak{S}_{k}$
($\rho_{a}$ is just a renaming of the vertices). Let
$\sigma\in\mathfrak{S}_{k}$ be the unique permutation such that $m(H)$ is
isomorphic to $G_{\sigma}$, then
$\sigma=\rho_{a}\circ\sigma_{b}\circ\sigma_{a}^{-1}\circ\rho_{a}^{-1}$. For
every $\sigma\in\mathfrak{S}_{k}$, there exists the same number of pairs
$(\sigma_{a},\sigma_{b})$ such that
$\sigma=\rho_{a}\circ\sigma_{b}\circ\sigma_{a}^{-1}\circ\rho_{a}^{-1}$, so
when $A$ and $B$ are fixed, the probability that $m(H)=G_{\sigma}$ is the same
for all $\sigma$. This probability is independent of $A$ and $B$ as long as
$|A\cap B|=k$, so the result follows. ∎

######  Lemma 6.

There is a constant $\alpha>0$ such that, when $A$, $B$, $\sigma_{a}$ and
$\sigma_{b}$ are chosen independently and uniformly at random, the probability
that $tw(H)<\alpha n$ vanishes to $0$ as $n$ goes to infinity.

###### Proof.

Suppose, without loss of generality, that we always have $\max(|A\cap
B|,|A\cap(A\triangle B)|,|B\cap(A\triangle B)|)=|A\cap B|$. Fix
$k\in\mathbb{N}$. By Lemmas 3 and 5, there is a constant $\beta$ such that
$\textup{Pr}(tw(m(H))<\beta k\mid|A\cap B|=k)$ tends to $0$ as $k$ increases.
Since $m(H)$ is a minor of $H$, we have that $tw(m(H))\leq tw(H)$, thus
$\textup{Pr}(tw(H)<\beta k\mid|A\cap B|=k)$ also tends to $0$ as $k$
increases. It follows that $\textup{Pr}(tw(H)<\frac{\beta n}{6}\mid|A\cap
B|\geq\frac{n}{6})$ vanishes to $0$ as $n$ increases, and since
$\textup{Pr}(|A\cap B|\geq\frac{n}{6})$ tends to $1$ as $n$ increases, we
finally obtain that $\textup{Pr}(tw(H)<\frac{\beta n}{6})$ goes to $0$ as $n$
increases. ∎

The graphs $H$ have degree at most $3$ and by Lemma 6 they have linear
treewidth with high probability, so using Theorem 5 we immediately have that,
with high probability, Tseitin formulas over $H$ are hard for resolution
refutation. Given the relation between $H$ and $\mathsf{rAddPar}(a,b)$’s
Tseitin graphs described in Lemma 4, we conclude that almost all formulas
$\mathsf{rAddPar}(a,b)$ are hard for resolution.

######  Theorem 2.

There is a constant $\alpha>0$ such that, with probability tending to $1$ as
$n$ increases, when $A$, $B$, $\sigma_{a}$ and $\sigma_{b}$ are chosen
independently and uniformly at random, the length of a shortest resolution
refutation of $\mathsf{rAddPar}(a,b)$ is least $2^{\alpha n}$.

###### Proof.

$\mathsf{rAddPar}(a,b)$ is Tseitin graph whose graph $G$ has maximum degree at
most $4$. By Lemma LABEL:lemma:rAddPar_and_H we have $tw(G)\geq tw(H)-6$ so,
by Lemma 6, $tw(G)=\Omega(n)$ with high probability when $A$, $B$,
$\sigma_{a}$ and $\sigma_{b}$ are chosen independently and uniformly. The
statement of the theorem then follows from Theorem 5. ∎

Notice here that $\sigma_{a}$, $\sigma_{b}$ and id are relative to each other
shuffled randomly. This is the most chaotic scenario which is likely to
contribute to its difficulty. Let us instead briefly discuss an example that
favors shorter proofs. We are given $a$ and $b$ in their random orders but, in
an addition step, we may be the ones creating the encoding for the sum
constraint and so we can choose the permutation $\sigma_{c}$ favorably by
ensuring that $\sigma_{c}(i)<\sigma_{c}(j)$ if and only if either:

  * •

$x_{i}\in A\setminus B$ and $x_{j}\in B\setminus A$

  * •

$x_{i},x_{j}\in A\setminus B$ and $\sigma_{a}(i)<\sigma_{a}(j)$

  * •

$x_{i},x_{j}\in B\setminus A$ and $\sigma_{b}(i)<\sigma_{b}(j)$

Even in this case, the encoding $\mathsf{rAddPar}(a,b,\sigma_{c})=a\land
b\land\mathsf{Parity}(C,U,\sigma_{c})$ will be hard w.h.p. when $|A\cap
B|=\Omega(n)$ since then we can find the minor $G_{\sigma}$ evoked above by
only looking in $H[V\cup V^{\prime}]$. The condition $|A\cap B|=\Omega(n)$ is
fulfilled almost surely when $A$ and $B$ are chosen uniformly.

## Sorting and Upper Bounds

Philipp and Rebola-Pardo (2016) showed that XOR-reasoning such as in Gaussian
elimination can have short proofs; a BDD approach can find polynomial-size
extended resolution proofs (Sinz and Biere 2006). For these particular
formulas we can do even better, reducing the complexity and the number of
extra variables needed.

######  Lemma 7 (Chew and Heule 2020).

Suppose we have a CNF $F$ and two sets of XOR clauses $\mathsf{xor}(x,y,p)$
and $\mathsf{xor}(p,z,q)$, where variable $p$ appears nowhere in $F$. We can
infer: $F\wedge\mathsf{xor}(x,y,p)\wedge\mathsf{xor}(p,z,q)$
$F\wedge\mathsf{xor}(y,z,p)\wedge\mathsf{xor}(p,x,q)$ in 32 of DRAT steps
without adding new variables.

###### Proof.

We can do this in 32 steps as in Figure 2.

ATA $\bar{q}\vee x\vee y\vee z$ $\bar{q}\vee\bar{x}\vee\bar{y}\vee z$
$\bar{q}\vee x\vee\bar{y}\vee\bar{z}$ $\bar{q}\vee\bar{x}\vee y\vee\bar{z}$
$q\vee\bar{x}\vee y\vee z$ $q\vee x\vee\bar{y}\vee z$ $q\vee x\vee
y\vee\bar{z}$ $q\vee\bar{x}\vee\bar{y}\vee\bar{z}$ RATE
$\mathtt{d}\quad\bar{p}\vee x\vee y$
$\mathtt{d}\quad\bar{p}\vee\bar{x}\vee\bar{y}$ $\mathtt{d}\quad p\vee
x\vee\bar{y}$ $\mathtt{d}\quad p\vee\bar{x}\vee y$ $\mathtt{d}\quad\bar{p}\vee
q\vee z$ $\mathtt{d}\quad\bar{p}\vee\bar{q}\vee\bar{z}$ $\mathtt{d}\quad p\vee
q\vee\bar{z}$ $\mathtt{d}\quad p\vee\bar{q}\vee z$ RATA $\bar{p}\vee z\vee y$
$\bar{p}\vee\bar{z}\vee\bar{y}$ $p\vee z\vee\bar{y}$ $p\vee\bar{z}\vee y$
$\bar{p}\vee q\vee x$ $\bar{p}\vee\bar{q}\vee\bar{x}$ $p\vee q\vee\bar{x}$
$p\vee\bar{q}\vee x$

ATE

$\mathtt{d}\quad\bar{q}\vee x\vee y\vee z\\\
\quad\mathtt{d}\quad\bar{q}\vee\bar{x}\vee\bar{y}\vee z$
$\mathtt{d}\quad\bar{q}\vee x\vee\bar{y}\vee\bar{z}\\\
\quad\mathtt{d}\quad\bar{q}\vee\bar{x}\vee b\vee\bar{z}$ $\mathtt{d}\quad
q\vee\bar{x}\vee y\vee z\\\ \quad\mathtt{d}\quad q\vee x\vee\bar{y}\vee z$
$\mathtt{d}\quad q\vee x\vee y\vee\bar{z}\\\ \quad\mathtt{d}\quad
q\vee\bar{x}\vee\bar{y}\vee\bar{z}$

Figure 2: DRAT steps required for Lemma 7, d denotes a deletion step.

∎

######  Lemma 8 (Chew and Heule 2020).

Suppose we have a CNF $F$ and two sets of XOR clauses $\mathsf{xor}(x,y,p)$
and $\mathsf{xor}(p,z,q)$, where variable $p$ appears nowhere in $F$. We can
start with $F\wedge\mathsf{xor}(x,y,p)\wedge\mathsf{xor}(p,z,q)$ and by
introducing a new variable $p^{\prime}$ infer all clauses from
$\mathsf{xor}(y,z,p^{\prime})$ and $\mathsf{xor}(p^{\prime},x,q)$ in a
constant number of Extended Resolution steps.

###### Proof.

We emulate the DRAT proof except we remove all deletion steps, derive the ATA
clauses by resolution, and the $\mathsf{xor}(y,z,p^{\prime})$ clauses can be
introduced as extension clauses on $p^{\prime}$. Then the
$\mathsf{xor}(p^{\prime},x,q)$ clauses can be derived by resolution with the
ATA clauses. ∎

######  Lemma 9 (Chew and Heule 2020).

Given two permutations $\sigma_{1}$ and $\sigma_{2}$, $X$, $S$ and $T$ are
disjoint sets of variables where both $S$ variables and $T$ variables do not
appear in CNF $F$, $F\wedge\mathsf{Parity}(X,S,\sigma_{1})$ can be transformed
into $F\wedge\mathsf{Parity}(X,T,\sigma_{2})$ in $O(n\log n)$ many DRAT steps
where $|X|=n$.

###### Sketch Proof.

  1. 1.

In $O(n\log n)$ applications of Lemma 7 we can take the linear structure of
the Tseitin variables and reorganize it into a balanced binary tree, using a
divide-and-conquer approach.

  2. 2.

In $O(n\log n)$ applications of Lemma 7 we can make any permutation of the
leaf edges. By first swapping any two leaves takes $O(\log n)$ applications of
Lemma 7 and then $n-1$ swaps are required (in the worst case) and sufficient
to place every variable in place.

  3. 3.

In $O(n\log n)$ applications of Lemma 7 we can take our balanced binary tree
and return it to a linear structure. ∎

######  Theorem 3 (Chew and Heule 2020).

For any permutation $\sigma\in\mathfrak{S}_{n}$, there are DRAT- refutations
of $\mathsf{rPar}(n,\sigma)$ that have $O(n\log n)$ many lines with no new
variables.

###### Sketch Proof.

  1. 1.

Using Lemma 9, we can rearrange the two parity constraints to be in the same
ordering.

  2. 2.

With this ordering, the treewidth of the Tseitin graph shrinks, and a linear
induction proof showing the equivalence of the Tseitin variables in resolution
can be performed.

∎

######  Theorem 4 ((Chew and Heule 2020)).

For any permutation $\sigma\in\mathfrak{S}_{n}$, there are Extended Resolution
refutations of $\mathsf{rPar}(n,\sigma)$ that have $O(n\log n)$ many lines
with no new variables.

###### Proof.

This is a corollary of Theorem 3. Lemma 9 can be done entirely in Extended
Resolution using Lemma 8. The remainder of the proof is a resolution proof so
is unaffected by that change from DRAT to Extended Resolution. ∎

######  Theorem 5.

For any parity constraints $a,b$ over $n$ input variables $X$, there are DRAT-
refutations of $\mathsf{rAddPar}(a,b)$ that have $O(n\log n)$ many lines.

###### Proof.

If both $a$ and $b$ have the same variable set either this reduces to a case
in Theorem 3, or it trivially includes the empty clause as the final
constraint.

Otherwise, without loss of generality, assume both $a$ and $b$ express even
parities, we can flip a literal to achieve this. $c$ is the third constraint
in $\mathsf{rAddPar}(a,b)$. Let $X$ be the set $\\{\,x_{i}\mid 0<i\leq
n\,\\}$, without loss of generality assume each $x_{i}$ appears in at least
one of $a$ or $b$.

$a=\mathsf{xor}(x_{\sigma_{a}(1)},x_{\sigma_{a}(2)},t^{a}_{1})\wedge{\bigwedge_{j=1}^{n_{a}-4}\mathsf{xor}(t^{a}_{j},{x_{\sigma_{a}(j+2)}},t^{a}_{j+1})}$
$\wedge\mathsf{xor}({t}^{a}_{n_{a}-3},x_{\sigma_{a}(n_{a}-1)},x_{\sigma_{a}(n_{a})})$
$b=\mathsf{xor}(x_{\sigma_{b}(1)},x_{\sigma_{b}(2)},t^{b}_{1})\wedge{\bigwedge_{j=1}^{n_{b}-4}\mathsf{xor}(t^{b}_{j},{x_{\sigma_{b}(j+2)}},t^{b}_{j+1})}$
$\wedge\mathsf{xor}({t}^{b}_{n_{b}-3},x_{\sigma_{b}(n_{b}-1)},x_{\sigma_{b}(n_{b})})$
$c=\mathsf{xor}(x_{\sigma_{c}(1)},x_{\sigma_{c}(2)},t^{c}_{1})\wedge{\bigwedge_{j=1}^{n_{c}-4}\mathsf{xor}(t^{c}_{j},{x_{\sigma_{c}(j+2)}},t^{c}_{j+1})}$
$\wedge\mathsf{xor}(\neg{t}^{c}_{n_{c}-3},x_{\sigma_{c}(n_{c}-1)},x_{\sigma_{c}(n_{c})})$

We first consider the ordered special case when
$\sigma_{a},\sigma_{b},\sigma_{c}$ all preserve order. E.g.
$\sigma_{l}(i)<\sigma_{l}(j)$ for $i<j$ and $l\in\\{a,b,c\\}$. For
$l\in\\{a,b,c\\}$ and $1<j\leq n-4$, we find the highest $i\leq j+1$ such that
there is some $k$ so that $i=\sigma_{l}(k)$, since $\sigma_{l}$ is injective,
$\tau_{l}(j)$ is defined as $k-1$. The purpose of $\tau_{l}$, is that
$t^{l}_{\tau_{l}(j)}$ is defined as parity of all the variables in $l$ up to
$x_{j+1}$ by index, this way we can talk about comparable $t$-variables from
$a,b$ and $c$ together.

Induction Hypothesis: Suppose

$\max(\sigma_{a}(2),\sigma_{b}(2),\sigma_{c}(2))-1<j\\\
<\min(\sigma_{a}(n_{a}-1),\sigma_{b}(n_{b}-1),\sigma_{c}(n_{c}-1))-1$

then all clauses of
$\mathsf{xor}(t^{a}_{\tau_{a}(j)},t^{b}_{\tau_{b}(j)},t^{c}_{\tau_{c}(j)})$
can be proven in an $O(j)$ size resolution proof.

Inductive Step: Starting with the four clauses from
$\mathsf{xor}(t^{a}_{\tau_{a}(j)},t^{b}_{\tau_{b}(j)},t^{c}_{\tau_{c}(j)})$,
we introduce $x_{j+2}$ and eliminate it. Because each $x$ appears in two
constraints. There are $u,v\in\\{a,b,c\\}$ such that $u\neq v$ and
$\mathsf{xor}(t^{u}_{\tau_{u}(j)},x_{j+2},t^{u}_{\tau_{u}(j)+1})$ and
$\mathsf{xor}(t^{v}_{\tau_{v}(j)},x_{j+2},t^{v}_{\tau_{v}(j)+1})$ are part of
$\mathsf{rAddPar}(a,b)$. Assume without loss of generality $u=a$, $v=b$

First we can eliminate $t^{a}_{\tau_{a}(j)}$, we get 8 clauses, then for each
of the eight clauses there is a unique clause in
$\mathsf{xor}(t^{b}_{\tau_{b}(j)},x_{j+2},t^{b}_{\tau_{b}(j)+1})$ for which it
can resolve without a tautological resolvent.

$\bar{t}^{b}_{\tau_{b}(j)}\vee t^{c}_{\tau_{c}(j)}\vee x_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$
$\bar{t}^{b}_{\tau_{b}(j)}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$ $\bar{t}^{b}_{\tau_{b}(j)}\vee
t^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$\bar{t}^{b}_{\tau_{b}(j)}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee
x_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee x_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$ $t^{b}_{\tau_{b}(j)}\vee
t^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee t^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)}\vee t^{c}_{\tau_{c}(j)}\vee
x_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$

$\bar{t}^{b}_{\tau_{b}(j)+1}\vee t^{c}_{\tau_{c}(j)}\vee x_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$ $t^{b}_{\tau_{b}(j)+1}\vee
t^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$\bar{t}^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee
x_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee x_{j+2}\vee
t^{a}_{\tau_{a}(j)+1}$ $\bar{t}^{b}_{\tau_{b}(j)+1}\vee
t^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee t^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)+1}\vee t^{c}_{\tau_{c}(j)}\vee
x_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$
$\bar{t}^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee\bar{x}_{j+2}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$

The next 8 clauses can resolve in pairs over $x_{j+2}$ to produce the four
clauses of
$\mathsf{xor}(t^{a}_{\tau_{a}(j)+1},t^{b}_{\tau_{b}(j)+1},t^{c}_{\tau_{c}(j)})$:

$\bar{t}^{b}_{\tau_{b}(j)+1}\vee t^{c}_{\tau_{c}(j)}\vee
t^{a}_{\tau_{a}(j)+1}\qquad
t^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee t^{a}_{\tau_{a}(j)+1}$
$t^{b}_{\tau_{b}(j)+1}\vee
t^{c}_{\tau_{c}(j)}\vee\bar{t}^{a}_{\tau_{a}(j)+1}\qquad\bar{t}^{b}_{\tau_{b}(j)+1}\vee\bar{t}^{c}_{\tau_{c}(j)}\vee\bar{t}^{a}_{\tau_{a}(j)+1}$

${\tau_{a}(j)+1}=\tau_{a}(j+1)$, $\tau_{b}(j)+1=\tau_{b}(j+1)$, and
$\tau_{c}(j)=\tau_{c}(j+1)$. So we are done in $+20$ steps ($+48$ if we want
to include deletions) and incremented $j$ by 1.

Reordered ParityRandom Parity
Addition6810121416246810121416181105025010003600Time (s)SolvedTimeout Figure
3: Treewidth (x-axis) vs. solving time (y-axis) for reordered parity (left)
and random parity addition (right).

Base Case: In the inductive step we proceeded by eliminating two $t$ variables
then resolving an $x$ variable. We can do the same with the base case, however
we do not start with a clause with three $t$ variables, but the 12 clauses of
$\mathsf{xor}(x_{\sigma_{a}(1)},x_{\sigma_{a}(2)},t^{a}_{1})$,
$\mathsf{xor}(x_{\sigma_{b}(1)},x_{\sigma_{b}(2)},t^{b}_{1})$,
$\mathsf{xor}(x_{\sigma_{c}(1)},x_{\sigma_{c}(2)},t^{c}_{1})$. We would start
by resolving any pair of $x$ that appear across these constraints, after that
we introduce new $x$ variables by eliminating a pair of $t$ variables and then
resolving away the $x$ variables. We want to eliminate all $x_{i}$ for $i\leq
j+1$ in increasing order.

Immediately before eliminating $x_{i}$ we eliminate all of
$t^{a}_{\tau_{a}(i-2)},t^{b}_{\tau_{b}(i-2)},t^{c}_{\tau_{c}(i-2)}$ if any of
them exist have not been eliminated prior. In other words we eliminate the
smallest index $t$ variables for clauses that include $x_{i}$. There will be