The Packing Chromatic Number of the Infinite Square Grid is 15

Bernardo Subercaseaux   0000-0003-2295-1299 Marijn J.H. Heule 0000-0002-5587-8801

B. Subercaseaux M.J.H. Heule

Carnegie Mellon University, Pittsburgh PA 15203, USA

{bsuberca<EMAIL_ADDRESS>
A packing $k$-coloring is a natural variation on the standard notion of graph $k$-coloring, where vertices are assigned numbers from $\{1, \ldots, k\}$, and any two vertices assigned a common color $c \in \{1, \ldots, k\}$ need to be at a distance greater than $c$  (as opposed to $1$, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15.
We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel, surprisingly effective propositional encoding for packing colorings. Additionally, we developed an alternative symmetry-breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding.

This work is supported by the U.S. National Science Foundation under grant CCF-2015445.
We thank the Pittsburgh Supercomputing Center for allowing us to use Bridges2 [4] in our experiments.
We thank as well the anonymous reviewers from TACAS2023 for their comments and suggestions. We also thank Donald Knuth for his thorough comments and suggestions. The first author thanks the Facebook group “actually good math problems”, from where he first learned about this problem, and in particular to Dylan Pizzo for his post about this problem.

§ INTRODUCTION

Automated reasoning techniques have been successfully applied to a variety of coloring problems ranging from the classical computer-assisted proof of the Four Color Theorem [1], to progress on the Hadwiger-Nelson problem [21], or improving the bounds on Ramsey-like numbers [19]. This article contributes a new success story to the area: we show the packing chromatic number of the infinite square grid to be 15, thus solving via automated reasoning techniques a combinatorial problem that had remained elusive for over 20 years.

The notion of packing coloring was introduced in the seminal work of Goddard et al. [10], and since then more than 70 articles have studied it [3], establishing it as an active area of research. Let us consider the following definition.

A packing $k$-coloring of a simple undirected graph $G = (V, E)$ is a function $f$ from $V$ to $\{1, \ldots, k\}$ such that for any two distinct vertices $u, v \in V$, and any color $c \in \{1, \ldots, k\}$, it holds that $f(u)=f(v)=c$ implies $d(u, v) > c$.

Note that by changing the last condition to $d(u, v) > 1$ we recover the standard notion of coloring, thus making packing colorings a natural variation of them. Intuitively, in a packing coloring, larger colors forbid being reused in a larger region of the graph around them. Indeed, packing colorings were originally presented under the name of broadcast coloring, motivated by the problem of assigning broadcast frequencies to radio stations in a non-conflicting way [10], where two radio stations that are assigned the same frequency need to be at distance greater than some function of the power of their broadcast signals. Therefore, a large color represents a powerful broadcast signal at a given frequency, that cannot be reused anywhere else within a large radius around it, to avoid interference. Minimizing the number of different colors assigned can then be interpreted as minimizing the radio spectrum pollution..
The literature has preferred the name packing coloring ever since [3].

Analogously to the case of standard colorings, we can naturally define the notion of packing chromatic number, and study its computation.

Given a graph $G = (V, E)$, define its packing chromatic number $\chi_{\rho}(G)$ as the minimum value $k$ such that $G$ admits a packing $k$-coloring.

Consider the infinite graph with vertex set $\mathbb{Z}$ and with edges between consecutive integers, which we denote as $\mathbb{Z}^1$. A packing $3$-coloring is illustrated in <Ref>. On the other hand, by examination one can observe that it is impossible to obtain a packing $2$-coloring for $\mathbb{Z}^1$.

[square/.style=regular polygon,regular polygon sides=4, minimum size=40]

at (-0.75,0) [] (h) $\cdots$;
at (4.25,0) [] (h) $\cdots$;

Illustration of a packing $3$-coloring for $\mathbb{Z}^1$.

While <Ref> shows that $\chi_\rho(\mathbb{Z}^1) = 3$, the question of computing $\chi_\rho(\mathbb{Z}^2)$, where $\mathbb{Z}^2$ is the graph with vertex set $\mathbb{Z} \times \mathbb{Z}$ and edges between orthogonally adjacent points (i.e., points whose $\ell_1$ distance equals $1$), has been open since the introduction of packing colorings by Goddard et al. [10]. On the other hand, it is known that $\chi_\rho(\mathbb{Z}^3) = \infty$ (again considering edges between points whose $\ell_1$ distance equals $1$) [9]. The problem of computing
$3 \leq \chi_\rho(\mathbb{Z}^2) \leq \infty$ has received significant attention, and it is described as “the most attractive [of the packing coloring problems over infinite graphs]” by Brešar et al. [3].
We can now state our main theorem, providing a final answer to this problem.

$\chi_\rho(\mathbb{Z}^2) = 15.$

An upper bound of $15$ had already been proved by Martin et al. [18], who found a packing $15$-coloring of a $72 \times 72$ grid that can be used for periodically tiling the entirety of $\mathbb{Z}^2$.

Therefore, the main contribution of our work consists of proving that $14$ colors are not enough for $\mathbb{Z}^2$. <Ref> presents a summary of the historical progress on computing $\chi_{\rho}(\mathbb{Z}^2)$. It is worth noting that amongst the computer-generated proofs (i.e., all since Soukal and Holub [22] in 2010), ours is the first one to be formally verified, see <Ref>.

Historical summary of the bounds known for $\chi_\rho(\mathbb{Z}^2)$.

Year     Citation     Approach     Lower bound     Upper bound
2002     Goddard et al. [10]     Manual     9     23

2002     Schwenk [20]     Unkown     9     22

2009     Fiala et al. [8]     Manual + Computer     10     23

2010     Soukal and Holub [22]     Simulated Annealing     10     17

2010     Ekstein et al. [7]     Brute Force Program     12     17

2015     Martin et al. [17]      SAT solver     13     16

2017     Martin et al. [18]     SAT solver     13     15

2022     Subercaseaux and Heule [23]     SAT solver     14     15

2022     This article      SAT solver     15     15

For any $k \geq 4$, the problem of determining whether a graph $G$ admits a packing $4$-coloring is known to be $\mathrm{NP}$-hard [10], and thus we do not  expect a polynomial time algorithm for computing $\chi_{\rho}(\cdot)$. This naturally motivates the use of satisfiability (SAT) solvers for studying the packing chromatic number of finite subgraphs of $\mathbb{Z}^2$. The rest of this article is thus devoted to proving <Ref> by using automated reasoning techniques, in a way that produces a proof that can be checked independently and that has been checked by verified software.

§ BACKGROUND

We start by recapitulating the components used to obtain a lower bound of 14 in our previous work [23].  Naturally, in order to prove a lower bound for $\mathbb{Z}^2$ one needs to prove a lower bound for a finite subgraph of it. As in earlier work, we consider disks (i.e., $2$-dimensional balls in the $\ell_1$-metric) as the finite subgraphs to study [23] . Concretely, let $D_r(v)$ be the subgraph induced by $\{ u \in V(\mathbb{Z}^2) \mid d(u, v) \leq r\}$. To simplify notation, we use $D_r$ as a shorthand for $D_r((0,0))$, and we let $D_{r, k}$ be the instance consisting of deciding whether $D_r$ admits a packing $k$-coloring. Moreover, let $D_{r, k, c}$ be the instance $D_{r, k}$ but enforcing that the central vertex $(0, 0)$ receives color $c$.

Illustration of satisfying assignments for $D_{3, 7, 3}$ and $D_{3, 6, 6}$. On the other hand, $D_{3, 6, 3}$ is not satisfiable.

For example, a simple lemma of Subercaseaux and Heule <cit.> proves that the unsatisfiability of $D_{3, 6, 3}$ is enough to deduce that $\chi_\rho(\mathbb{Z}^2) \geq 7$. We will prove a slight variation of it (<Ref>) later on in order to prove <Ref>, but for now let us summarize how they proved that $D_{12, 13, 12}$ is unsatisfiable.

The direct encoding for $D_{r, k, c}$ consists simply of variables $x_{v, t}$ stating that vertex $v$ gets color $t$, as well as the following clauses:

* (at-least-one-color clauses, aloc) \( \quad \quad
\bigvee_{t=1}^k x_{v, t}, \quad \forall v \in V,\)

* (at-most-one-distance clauses, amod)
\[
\overline{x_{u,t}} \lor \overline{x_{v,t}}, \quad \forall t \in \{1, \ldots, k\}, \forall u, v \in V \text{ s.t. } 0 < d(u, v) \leq t,
\]

* (center clause) \( \quad \quad
x_{(0, 0), c}.
\)

This amounts to $O(r^2 k^3)$ clauses [23]. The recursive encoding is significantly more involved, but it leads to only $O(r^2 k \log k)$ clauses asymptotically. Unfortunately, the constant involved in the asymptotic expression is large, and this encoding did not provide practical speed-ups [23].

Cube And Conquer.

Introduced by Heule et al. [13], the approach aims to split a SAT instance  $\varphi$ into multiple SAT instances $\varphi_1, \ldots, \varphi_m$ in such a way that $\varphi$ is satisfiable if, and only if, at least one of the instances $\varphi_i$ is satisfiable; thus allowing to work on the different instances $\varphi_i$  in parallel.
If $\psi = \left(c_1 \lor c_2 \lor \cdots \lor c_m\right)$ is a tautological DNF, then we have

\[
\mathrm{SAT}(\varphi) \iff \mathrm{SAT}(\varphi \land \psi) \iff \mathrm{SAT}\left( \bigvee_{i=1}^m (\varphi \land c_i)\right) \iff \mathrm{SAT}\left( \bigvee_{i=1}^m \varphi_i \right),
\]

where the different $\varphi_i \coloneqq (\varphi \land c_i)$ are the instances resulting from the split.

Intuitively, each cube $c_i$ represents a case, i.e., an assumption about a satisfying assignment to $\varphi$, and soundness comes from $\psi$ being a tautology, which means that the split into cases is exhaustive. If the split is well designed, then each $\varphi_i$ is a particular case that is substantially easier to solve than $\varphi$, and thus solving them all in parallel can give significant speed-ups, especially considering the sequential nature of CDCL, at the core of most solvers. Our previous work [23] proposed a concrete algorithm to generate a split, which already resulted in an almost linear speed-up, meaning that by using 128 cores, the performance gain was roughly a $\times 60$ factor.

Symmetry Breaking.

The idea of symmetry breaking [6] consists of exploiting the symmetries that are present in SAT instances to speed-up computation. In particular, $D_{r, k, c}$ instances have 3 axes of symmetry (i.e., vertical, horizontal and diagonal) which allowed for close to an $8$-fold improvement in performance for proving $D_{12,13,12}$ to be unsatisfiable. The particular use of symmetry breaking in our previous work [23] was happening at the level, where out of the sub-instances $\varphi_i, \ldots, \varphi_m$ produced by the split, only a $\nicefrac{1}{8}$-fraction of them had to be solved, as the rest were equivalent under isomorphism.

Arguably the biggest drawback of our previous approach to prove a lower bound of 14 is that it lacked the capability of generating a computer-checkable proof. To claim a full solution to the 20-year-old problem of computing $\chi_\rho(\mathbb{Z}^2)$ that is accepted by the mathematics community, we deem paramount a fully verifiable proof that can be scrutinized independently.

The most commonly-used proofs for SAT problems are expressed in the DRAT clausal proof system [11].
A DRAT proof of unsatisfiability is a list of clause addition and clause deletion steps.
Formally, a clausal proof is a list of pairs $\step{s_1}{C_1},\dots,\step{s_m}{C_m}$, where for each $i\in 1,\dots,m$, $s_i \in \{\mathsf{a}, \mathsf{d}\}$ and $C_i$ is a clause.
If $s_i = \mathsf{a}$, the pair is called an addition, and if $s_i = \mathsf{d}$, it is called a deletion.
For a given input formula $\varphi_0$, a clausal proof gives rise to a set of accumulated formulas $\varphi_i$ ($i \in \{1,\dots,m\}$) as follows:

\begin{align*}
\varphi_i =
\begin{cases}
\varphi_{i-1} \cup \{C_i\}	& \text{if $\mathsf{s}_i = \mathsf{a}$}\\
\varphi_{i-1} \setminus \{C_i\}	& \text{if $\mathsf{s}_i = \mathsf{d}$}\\
\end{cases}
\end{align*}

Each clause addition must preserve satisfiability, which is usually guaranteed by requiring the added clauses to fulfill some efficiently decidable syntactic criterion.
The main purpose of deletions is to speed up proof checking by keeping the accumulated formula small.
A valid proof of unsatisfiability must end with the addition of the empty clause.

§ OPTIMIZATIONS

Even with the best choice of parameters under the approach of Subercaseaux and Heule, solving the instance $D_{12,13,12}$ takes almost two days of computation with a $128$-core machine [23]. In order to prove <Ref>, we will require to solve an instance roughly 100 times harder, and thus several optimizations will be needed.
In fact, we improve on all aspects discussed in <Ref>; we present five different forms of optimization that are key to the success of our approach, which we summarize next.

* We present a new encoding, which we call the plus encoding that has conceptual similarities with the recursive encoding of Subercaseaux and Heule [23], while achieving a significant gain in practical efficiency.

* We present a new split algorithm that works substantially better than the previous split algorithm when coupled with the plus encoding.

* We improve on symmetry breaking by using multiple layers of symmetry-breaking clauses in a way that exploits the design of the split algorithm to increase performance.

* We study the choice of color to fix at the center, showing that one can gain significantly in performance by making instance-based choices; for example, $D_{12, 13, 6}$ can be solved more than three times as fast as $D_{12, 13, 12}$ (the instance used in our prior work [23]).

* We introduce a new and extremely simple kind of clauses called alod clauses, which improve performance when added to the other clauses of any encoding we have tested.

The following subsections present each of these components in detail.

§.§ “Plus”: a New Encoding

Despite the asymptotic improvement of the recursive encoding of Subercaseaux and Heule [23], its contribution is mostly of “theoretical interest” as it does not improve solution times. Nonetheless, that encoding suggests the possibility of finding one that is both more succinct than the direct encoding
and that speed-ups computation. Our path towards such an encoding starts with Bounded Variable Addition (BVA) [16], a technique to automatically re-encode CNF formulas by adding new variables, with the goal of minimizing their resulting size (measured as the sum of the number of variables and the number of clauses). BVA can significantly reduce the size of $D_{r, k, c}$ instances, even further than the recursive encoding. Moreover, BVA actually speeds-up computation when solving the resulting instances with a CDCL solver, see <Ref>. <Ref> compares the number of amod clauses between the direct encoding and the BVA encoding; for example in the direct encoding, for $D_{14}$ color $10$ would require roughly $30000$ clauses, whereas it requires roughly $3500$ in the BVA encoding. It can be observed as well in  <Ref> that the direct encoding grows in a very structured and predictable way, where color $c$ in $D_r$ requires roughly $r^2 c^2$ clauses. On the other hand, arguably because of its locally greedy nature, the results for BVA are far more erratic, and roughly follow a $4r^2 \lg c$ curve.

The encoding resulting from BVA does not perform particularly well when coupled with the split algorithm presented in our earlier work [23]. Indeed, <Ref> shows that while BVA heavily improves runtime under sequential CDCL, it does not provide a meaningful advantage when using . Furthermore, encodings resulting from BVA are hardly interpretable, as BVA uses a locally greedy strategy for introducing new variables. As a result, the design of a split algorithm that could work well with BVA is a very complicated task. Therefore, our approach consisted of reverse engineering what BVA was doing over some example instances, and using that insight to design a new encoding that produces instances of size comparable to those generated by BVA while being easily interpretable and thus compatible with natural split algorithms.

Comparison between the different encodings. experiments are realized with the approach of Subercaseaux and Heule [23] (parameters $F=5, d=2$) on a 128-core machine. Hardware details in Section <ref>.

2c|direct encoding     2c|bva encoding     2cplus encoding

$D_{5,10,5}$    $D_{6,11,6}$     $D_{5,10,5}$    $D_{6,11,6}$    $D_{5,10,5}$    $D_{6,11,6}$
Number of variables      00610     00935     0973      1559     0673     1039

Number of clauses     10688     21086     2313     3928      4063     7548
CDCL runtime (s)     0255.12     10774.79     39.88     2539.38     0015.90     811.66

Cube-and-conquer wall-clock (s)     0000.77     00026.20     00.78     017.97     0000.50     006.68

By manually inspecting BVA encodings one can deduce  that a fundamental part of their structure is what we call regional variables/clauses. A regional variable $r_{S, c}$ is associated to a set of vertices $S$ and a color $c$, meaning that at least one vertex in $S$ receives color $c$. Let us illustrate their use with an example.

Consider the instance $D_{6,11}$, and let us focus on the at-most-one-distance (amod) clauses for color $4$. <Ref> depicts two regional clauses: one in orange (vertices labeled with $\alpha$), and one in blue (vertices labeled with $\beta$), each consisting of $5$ vertices organized in a plus ($+$) shape. We thus introduce variables $r_{\text{orange}, 5}$ and $r_{\text{blue}, 5}$, defined by the following clauses:

* \(
\overline{r_{\text{orange}, 4}} \lor \bigvee_{v \text{ has label } \alpha} \;  x_{v, 4},\)

* \(
\overline{r_{\text{blue}, 4}} \lor \bigvee_{v \text{ has label } \beta} \; x_{v, 4},\)

* \(
r_{\text{orange}, 4} \lor \overline{x_{v,4}}, \; \text{ for each $v$ with label $\alpha$,}
\)

* \(
r_{\text{blue}, 4} \lor \overline{x_{v,4}}, \; \text{ for each $v$ with label $\beta$.}
\)

The benefit of introducing these two new variables and $2 + (5\cdot 2) = 12$ additional clauses will be shown now, when using them to forbid conflicts more compactly. Indeed, each vertex labeled with $\alpha$ or $\beta$ participates in $|D_4|-1 = 40$ amod clauses in the direct encoding, which equals a total of $10 \cdot 40 - \binom{10}{2} = 355$ clauses for all of them (subtracting the clauses counted twice). However, note that all $36$ vertices shaded in light orange are at distance at most $4$ from all vertices labeled with $\alpha$, and thus they are in conflict with $r_{\text{orange}, 4}$. This means that we can encode all conflicts between $\alpha$-vertices and orange-shaded vertices with $36$ clauses. The same can be done for $\beta$-vertices and the $36$ vertices shaded in light blue. Moreover, all pairs of vertices $(x, y)$ with $x$ being an $\alpha$-vertex and $y$ being a $\beta$-vertex are in conflict, which we can represent simply with the clause $(r_{\text{orange}, 4} \lor \,r_{\text{blue}, 4})$, instead of $5 \cdot 5 = 25$ pairwise clauses. We still need, however, to forbid that more than one $\alpha$-vertex receives color $4$, and the same for $\beta$-vertices, which can be done by simply adding all $2 \cdot \binom{5}{2} = 20$ amod clauses between all pairs. In total, the total number of clauses involving $\alpha$ or $\beta$ vertices has gone down to $12 + 2 \cdot 36 + 20 + 1= 105$ clauses, from the original $355$ clauses, by merely adding two new variables.

Illustration of regions interacting in $P_{6,11, 6}$, for color $4$.

[em/.style=draw, minimum width=3mm, minimum height=3mm]

Illustration of the placement of regions of the $13$ regions in $P_{6,11, 6}$.

Illustrations for $P_{6,11, 6}$.

As shown in <Ref>, the use of regional clauses can make encodings more compact, and this same idea scales even better for larger instances when the regions are larger. A key challenge for designing a regional encoding in this manner is that it requires a choice of regions (which can even be different for every color). After trying several different strategies for defining regions, we found one that works particularly well in practice (despite not yielding an optimal number for the metric $\# \text{variables} + \#\text{clauses}$),  which we denote the plus encoding. The plus encoding is based on simply using “+” shaped regions (i.e., $D_1$) for all colors greater than $3$, and to not introduce any changes for colors $1, 2$ and $3$ as they only amount to a very small fraction of the total size of the instances we consider. We denote with $P_{d,k,c}$ the plus encoding of the diamond of size $d$ with $k$ colors, and the centered being colored with $c$. <Ref> illustrates $P_{6,11,6}$. Interestingly, the BVA encoding opted for larger regions for the larger colors, using for example $D_2$'s or $D_3$'s as regions for color $14$. We have experimentally found this to be very ineffective when coupled with our split algorithms.
In terms of the locations of the “+” shaped regions, we have placed them manually through an interactive program, arriving to the conclusion that the best choice of locations consists of packing as many regions as possible and as densely around the center as possible. A more formal presentation of all the clauses involved in the plus encoding is shown in the appendix, but all its components have been illustrated in <Ref>.

The exact number of clauses resulting from the plus encoding is hard to analyze precisely, but it is clear that asymptotically it only improves from the direct encoding by a constant multiplicative factor. <Ref> and <Ref> illustrate the compactness of the plus encoding over particular instances, and its increase in efficiency both for CDCL solving as well as with the approach of Subercaseaux and Heule [23].

§.§ Symmetry Breaking

Another improvement of our approach is a static symmetry-breaking technique, while Subercaseaux and Heule [23] achieved symmetry breaking by discarding all but $\nicefrac{1}{8}$ of the cubes. We cannot do this easily since the plus encoding does not have an $8$-fold symmetry. Instead it has a $4$-fold symmetry (see <Ref>). We add symmetry breaking clauses directly on top of the direct encoding (i.e., instead of using it after a split), as $D_{r, k, c}$ has indeed an $8$-fold symmetry (see <Ref>). Concretely, if we consider a color $t$, it can only appear once in the $D_{\lfloor t/2\rfloor}$, as if appeared more than once said appearances would be at distance $\leq t$. Given this, we can assume without loss of generality that if there is one appearance of $t$ in $D_{\lfloor t/2\rfloor}$, then it appears with coordinates $(a, b)$ such that $a \geq 0 \land b \geq a$. We enforce this by adding negative units of the form $\overline{x_{(i, j), t}}$ for every pair $(i, j) \in D_{\lfloor t/2\rfloor}$ such that $i < 0 \lor j < i$. This is illustrated in <Ref> for $D_{5, 10}$.
Note however that this can only be applied to a single color $t$, as when a vertex in the north-north-east octant gets assigned color $t$, the $8$-fold symmetry is broken. However, if the symmetry breaking clauses have been added for color $t$, and yet $t$ does not appear in $D_{\lfloor t/2\rfloor}$, then there is still an $8$-fold symmetry in the encoding we can exploit by breaking symmetry on some other color $t'$. This way, our encoding uses $L = 5$ layers of symmetry breaking, for colors $k, k-1, \ldots, k-L+1$. At each layer $i$, where symmetry breaking is done over color $k-i$, except for the first (i.e., $i > 0$), we need to concatenate a clause

\[
{\rm SymmetryBroken}_i \coloneqq \bigvee_{t = k-i}^{k} \; \; \bigvee_{\substack{(a, b) \in D_{\lfloor t/2\rfloor} \\ 0 \leq a \leq b}} x_{(a, b), t}
\]

to each symmetry breaking clause, so that symmetry breaking is applied only when symmetry has not been broken already. <Ref> (page 14) illustrates the impact of this symmetry breaking approach, yielding close to a $\times 40$ speed-up for $D_{6,11, 6}$.

Illustration of the effect of adding alod clauses. The right figure, with alod clauses, presents a chessboard pattern.

at (-1,4) $\overline{10}$;
at (-1,3) $\overline{10}$;
at (-1,2) $\overline{10}$;
at (-1,1) $\overline{10}$;
at (-1,0) $\overline{10}$;
at (-1,-1) $\overline{10}$;
at (-1,-2) $\overline{10}$;
at (-1,-3) $\overline{10}$;
at (-1,-4) $\overline{10}$;
at (-2,3) $\overline{10}$;
at (-2,2) $\overline{10}$;
at (-2,1) $\overline{10}$;
at (-2,0) $\overline{10}$;
at (-2,-1) $\overline{10}$;
at (-2,-2) $\overline{10}$;
at (-2,-3) $\overline{10}$;
at (-3,2) $\overline{10}$;
at (-3,1) $\overline{10}$;
at (-3,0) $\overline{10}$;
at (-3,-1) $\overline{10}$;
at (-3,-2) $\overline{10}$;
at (-4,1) $\overline{10}$;
at (-4,0) $\overline{10}$;
at (-4,-1) $\overline{10}$;
at (-5,0) $\overline{10}$;

at (0,-1) $\overline{10}$;
at (0,-2) $\overline{10}$;
at (0,-3) $\overline{10}$;
at (0,-4) $\overline{10}$;
at (0,-5) $\overline{10}$;
at (1,0) $\overline{10}$;
at (1,-1) $\overline{10}$;
at (1,-2) $\overline{10}$;
at (1,-3) $\overline{10}$;
at (1,-4) $\overline{10}$;
at (2,1) $\overline{10}$;
at (2,0) $\overline{10}$;
at (2,-1) $\overline{10}$;
at (2,-2) $\overline{10}$;
at (2,-3) $\overline{10}$;
at (3,2) $\overline{10}$;
at (3,1) $\overline{10}$;
at (3,0) $\overline{10}$;
at (3,-1) $\overline{10}$;
at (3,-2) $\overline{10}$;
at (4,1) $\overline{10}$;
at (4,0) $\overline{10}$;
at (4,-1) $\overline{10}$;
at (5,0) $\overline{10}$;

Some symmetry-breaking unit clauses added to $D_{5,10}$.

The effect of adding alod clauses (left) and symmetry-breaking (right).

§.§ At-Least-One-Distance clauses

Yet another addition to our encoding is what we call At-Least-One-Distance (alod) clauses, which consist on stating that, for every vertex $v$, if we consider $D_1(v)$, then at least one vertex in $D_1(v)$ must get color $1$.  Concretely, the At-Least-One-Distance clause corresponding to a vertex $v = (i, j)$  is

\[
C_v = x_{(i, j), 1} \lor x_{(i+1, j), 1} \lor x_{(i-1, j), 1} \lor x_{(i, j+1), 1} \lor x_{(i, j-1), 1}.
\]

Note that these clauses are blocked [15] which implies that their addition preserves satisfiability. This can be seen as follows. If no vertex in $D_1(v)$ gets assigned color $1$, then we can simply assign $x_{v, 1}$, thus satisfying the new clause $C_v$.

The purpose of alod clauses can be described as incentives towards assigning color $1$ in a  chessboard pattern (see <Ref>), which seems to simplify the rest of the computation. Empirically, their addition improves runtimes; see <Ref>.

§.§ Cube And Conquer Using Auxiliary Variables

The split of Subercaseaux and Heule [23] is based on cases about the $x_{v, c}$ variables of the direct encoding, and specifically using vertices $v$ that are close to the center and colors $c$ that are in the top-$t$ colors for some parameter $t$.

Our algorithm is instead based on cases only around the new regional variables $r_{S, c}$, which appears to be key for exploiting their use in the encoding.

More concretely, our algorithm, which we call $\ptr$, is roughly based on splitting the instance into cases according to which out of the $R$ regions that are closest to the center get which of the $T$ highest colors (noting that a region can get multiple colors). A third parameter $P$ indicates the maximum number of positive literals in any cube of the split. More precisely, there are cubes with $i$ positive literals for $i \in \{0, 1, \ldots, P-1, P\}$, and the set of cubes with $i$ positive literals is constructed by $\ptr$ as follows:

* Let $\mathcal{R}$ be the set of $R$ regions that are the closest to the center, and $\mathcal{T}$ the set consisting of the $T$ highest colors (i.e., $\{k, k-1, \ldots, k-T+1 \}$).

* For each of the $R^i$ tuples $\vec{S}  \in \mathcal{R}^i$, we create $\binom{T}{i}$ cubes as described in the next step.

* For each subset $Q \subseteq \mathcal{T}$ with size $|Q| = i$, let $q_1, \ldots, q_i$ be its elements in increasing order, and then create
a cube with positive literals $r_{\vec{S}_j, q_j}$ for $j \in \{1, \ldots,  i\}$. Then, if $i < P$, add to the cube negative literals $\overline{r_{\vec{S}_j, q_\ell}}$ for $j \in \{1, \ldots, i\}$ and every $q_\ell \not \in Q$.

The cubes generated by the $\ptr$ algorithm form a tautology.

The proof of <Ref> is quite simple, and we refer the reader to the proof of Lemma 7 in Subercaseaux and Heule [23] for a very similar one. Moreover, because our goal is to have a verifiable proof, instead of relying on <Ref>, we test explicitly that the cubes generated by our algorithm form a tautology in all the instances mentioned in this paper.
Pseudo-code for $\ptr$ is presented in the appendix as Algorithm <ref>.

§.§ Optimizing the Center Color

Our previous work [23] argued that for an instance $D_{r, k}$, one should fix the color of the central vertex to $\min(r, k)$.
However, our experiments suggest otherwise. As the proof of <Ref> (in the appendix) implies, we are allowed to fix any color in the center, and as long as the resulting instance is unsatisfiable, that will allow us to establish the same lower bound.
It turns out that the choice of the center color can dramatically affect performance, as shown for instance $D_{12, 13}$ (the one used to prove $\chi_{\rho}(\mathbb{Z}^2) \geq 14$ [23]) in <Ref>. Interestingly, performance does not change monotonically with the value fixed in the center.
Intuitively, it appears that fixing smaller colors in the center is ineffective as they impose restrictions on a small region around the center, while fixing very large colors in the center does not constrain the center much; for example, on the one hand, fixing a $1$ or $2$ in the center does not seem to impose any serious constraints on solutions. On the other hand, when a $12$ is fixed in the center (as in our previous work [23]),
color $6$ can be used $5$ times in $D_6$, whereas if color $6$ is fixed in the center, it can only be used once in $D_6$. The apparent advantage of fixing $12$ in the center (that it cannot occur anywhere else in $D_{12, 13}$), is outweighed by the extra constraints around the center that fixing color $6$ imposes; Subercaseaux and Heule had already observed that most conflicts between colors occur around the center [23]), thus explaining why it makes sense to optimize in that area.

scale only axis,
ylabel near ticks, yticklabel pos=right,
legend style=at=(0.90,0.90),
ylabel=wallclock time (hours),
axis x line*=bottom]
[color=darkpurple, mark=diamond*] coordinates (1, 16.7111) (2, 11.644) (3, 1.56254)  (4, 1.10246)  (5, 0.347961) (6, 0.343833)  (7, 0.343433)  (8, 0.541108)  (9, 0.629939) (10, 0.795033)  (11, 0.869528)  (12, 0.870236) (13, 5.15691);

scale only axis,
legend style=at=(0.50,0.90),
axis y line*=left,
ylabel=average runtime (seconds),
axis x line*=bottom]
[color=redorange, mark=x] coordinates (1, 18.1142) (2, 7.53109) (3, 2.16696) (4, 1.20158) (5, 0.509671) (6, 0.439183) (7, 0.479794) (8, 0.697709) (9, 0.899855)      (10, 1.1596) (11, 1.23483) (12, 1.17986) (13,7.37375);

The impact of the color in the center ($c$) on the performance for $P^\star_{12,13,c}$.

The main result of Subercaseaux and Heule [23] is the unsatisfiability of $D_{12,13,12}$, which required 45 CPU hours using the same SAT solver and similar hardware.
Let $P^\star_{d,k,c}$denote $P_{d,k,c}$ with alod clauses and symmetry-breaking predicates.
We show unsatisfiability of $P^\star_{12,13,12}$ in 1.18 CPU hours and of $P^\star_{12,13,6}$ in 0.34 CPU hours. So the combination
of the plus encoding and the improved center reduces the computational costs by two orders of magnitude.

§ VERIFICATION

Our pipeline proves that, in order to trust $\chi_\rho(\mathbb{Z}^2) = 15$ as a result, the only component that requires unverified trust is the direct encoding of $\dplain$. Indeed, let $P^\star_{15, 14, 6}$ be the instance $P_{15, 14, 6}$ with alod-clauses and $5$ layers of symmetry breaking clauses, and let $\psi = \{c_1, \ldots, c_m\}$ be the set of cubes generated by the $\ptr$ algorithm with parameters $P=6, T=7, R=9$. We then prove:

* that $D_{15, 14, 6}$ is satisfiability equivalent to $P^\star_{15, 14, 6}$.

* the DNF $\psi = c_1 \lor c_2 \lor \cdots \lor c_m$ is a tautology.

* each instance $(P^\star_{15, 14, 6} \land c_i)$, for $c_i \in \psi$ is unsatisfiable.

* hence the negation of each cube is implied by $P^\star_{15, 14, 6}$.

* since $\psi$ is a tautology, its negation $\taut$ is unsatisfiable.

As a result, <Ref> relies only on our implementation of $D_{15, 14, 6}$. Fortunately, this is quite simple, and the whole implementation is presented in Code <ref> in the appendix. <Ref> illustrates the verification pipeline, and the following paragraphs detail its different components.

\[
\mathrlap{\overbrace{\phantom{\dplain \equiv \dsbp}}^{\text{symmetry proof}}}
\dplain \equiv
\mathrlap{\underbrace{\phantom{\dsbp \equiv \psbp}}_{\text{re-encoding proof}}}
\dsbp \equiv
\mathrlap{\overbrace{\phantom{\psbp \vDash \taut}}^{\text{implication proof}}}
\psbp \vDash
\underbrace{\taut \vDash \bot}_{\text{tautology proof}}
\]

Illustration of the verification pipeline.

Symmetry Proof.

The first part of the proof consists in the addition of symmetry-breaking predicates to the formula.
This part needs to go before the re-encoding proof, because the plus encoding
does not have the 8-fold symmetry of the direct encoding. Each of the clauses in the symmetry-breaking predicates have the substitution redundancy (SR) property [5].
This is a very strong redundancy property and checking whether a clause $C$ has SR w.r.t. a formula $\varphi$ is NP-complete. However, since we know the symmetry, it is easy
to compute a SR certificate. There exists no SR proof checker. Instead, we implemented a prototype tool to convert SR proofs into DRAT for which formally verified checkers exists.
Our conversion is similar to the approach to converted propagation redundancy into DRAT [12]. The conversion can significantly increase the size of the proof, but
the other proof parts are typically larger for harder formulas, thus the size is acceptable.

Re-encoding Proof.

After symmetry breaking, the formula encoding is optimized by transforming the direct encoding into the plus encoding and adding the alod clauses.
This part of the proof is easy. All clauses in the plus encoding and all alod clauses have the RAT redundancy property w.r.t. the
direct encoding. This means that we can add all these clauses with a single addition step per clause.
Afterward, the clauses that occur in the direct encoding but not in the plus encoding are removed using deletion steps.

Implication Proof.

The third part of the proof expresses that the formula cannot be satisfied with any of the cubes from the split.
For easy problems, one can avoid splitting and just use the empty cube as tautological DNF. For harder problems, splitting is crucial.
We solve $D_{15,14,6}$ using a split with just over 5 million cubes. Using a SAT solver to show that the formula
with a cube is unsatisfiable shows that the negative of the cube is implied by the formula. We can derive all these
implied clauses in parallel. The proofs of unsatisfiability can be merged into a single implication proof.

Tautology Proof.
The final proof part needs to show that the negation of the clauses derived in the prior steps form a tautology.
In most cases, including ours, the cubes are constructed using a tree-based method. This makes the tautology check easy
as there exists a resolution proof from the derived clauses to the empty clause using $m - 1$ resolution steps with
$m$ denoting the number of cubes. This part can be generated  using a simple SAT call.

The final proof merges all the proof parts. In case the proof parts are all in the DRAT format, such as our proof parts,
then they can simply be merged by concatenating the proofs using the order presented above.

§ EXPERIMENTS

Experimental Setup.

In terms of software, all sequential experiments were ran on state-of-the-art solver CaDiCaL [2], while parallel experiments with were ran using a new implementation of parallel iCaDiCaL because it supports incremental solving [13] while being significantly faster than iLingeling.
In terms of hardware, all our experiments were run in the Bridges2 [4] cluster from the Pittsburgh Supercomputing Center with the following specifications: Two AMD EPYC 7742 CPUs, each with 64 cores, 256MB of L3 cache, and 512GB total RAM memory.

Evaluating the effectiveness of the optimizations on $D_{6,11,6}$.

sym     alod     plus     #var     #cls     runtime     derivation     proof     check
0935     21086     10741.69     0 b     11.99 Gb     31731.20

x      1039     07548     00809.65      149 Kb     01.29 Gb     01720.82

x         0935     21171     08422.38     1.6 Kb     08.11 Gb     21732.74

x     x     1039     07633     00389.71     151 Kb     01.29 Gb     01708.21

x               0935     21286     00273.19    436 Mb     00.63 Gb      01390.04

x         x     1039     07748     00066.74     436 Mb     00.14 Gb     01022.42

x     x         0935     21371     00252.71     436 Mb     00.68 Gb    01359.05

x     x     x     1039      07833     00055.56     436 Mb     00.10 Gb     00997.90

Effectiveness of the Optimizations.

We evaluated the optimizations to the direct encoding as proposed in Section <ref>:
the plus encoding, the addition of the alod clauses, and the new symmetry breaking.
The results are shown in Table <ref>. We picked $D_{6,11,6}$
for this evaluation since it is the largest diamond that can still be solved within a couple of
hours on a single core.

The main conclusion is that the optimizations significantly improve the runtime. A comparison
between the direct encoding without symmetry breaking and the plus encoding with
symmetry breaking and the alod clauses shows that the latter can be solved roughly
200x faster. <Ref> shows all 8 possible configurations. Turning on any of the optimizations
always improves performance. The effectiveness of the plus encoding and alod clauses
is somewhat surprising: the speed-up factor obtained by re-encoding typically does not exceed the
factor by which the formula size is reduced. In this case, the reduction factor in formula size is less than
$3$, while the speed-up is larger than $13$ (see the difference between the first and second row of <Ref>). Moreover, we are not aware of the effectiveness of
adding blocked clauses. Typically SAT solvers remove them.

We also constructed DRAT proofs of the optimizations (shown as derivation in the table)
and the solver runtime. We merged them into a single DRAT proof by concatenating the files.
The proofs were first checked with the drat-trim tool, which produced LRAT proofs. These LRAT
file were validated using the formally-verified cake-lpr checker. The size of the DRAT proofs
and the checking time
are shown in the table. Note that the checking time for the proofs
with symmetry breaking is always larger than the solving times. This is caused by expressing the
symmetry breaking in DRAT resulting in a 436 Mb proof part.

The Implication Proof.

The largest part of the computation consist of showing that $P^{\star}_{15,4,6}$ is unsatisfiable under each of the $5,217,031$
cubes produced by the cube generator. The results of the experiments are shown in Figure <ref> (left). The left plot shows that
roughly half of the cubes can be solved in a second or less. The average runtime of cubes was 3.35 seconds, while the hardest cube
required 1584.61 seconds.
The total runtime was 4851.38 CPU hours.

[height=150pt, width=250pt, ymode=log,legend style=at=(0.70,0.90), xmin=0, xmax=5307031]

[color=blue, mark=none, thick] coordinates (31, 0.145) (1031, 0.173) (2031, 0.179) (3031, 0.182) (4031, 0.184) (5031, 0.185) (6031, 0.186) (7031, 0.187) (8031, 0.188) (9031, 0.189) (10031, 0.19) (11031, 0.19) (12031, 0.191) (13031, 0.192) (14031, 0.193) (15031, 0.193) (16031, 0.194) (17031, 0.195) (18031, 0.195) (19031, 0.196) (20031, 0.197) (21031, 0.197) (22031, 0.198) (23031, 0.199) (24031, 0.199) (25031, 0.2) (26031, 0.201) (27031, 0.201) (28031, 0.202) (29031, 0.202) (30031, 0.203) (31031, 0.204) (32031, 0.204) (33031, 0.205) (34031, 0.205) (35031, 0.206) (36031, 0.206) (37031, 0.207) (38031, 0.207) (39031, 0.208) (40031, 0.208) (41031, 0.208) (42031, 0.209) (43031, 0.209) (44031, 0.21) (45031, 0.21) (46031, 0.21) (47031, 0.211) (48031, 0.211) (49031, 0.211) (50031, 0.212) (51031, 0.212) (52031, 0.212) (53031, 0.213) (54031, 0.213) (55031, 0.213) (56031, 0.214) (57031, 0.214) (58031, 0.214) (59031, 0.214) (60031, 0.215) (61031, 0.215) (62031, 0.215) (63031, 0.215) (64031, 0.216) (65031, 0.216) (66031, 0.216) (67031, 0.216) (68031, 0.217) (69031, 0.217) (70031, 0.217) (71031, 0.217) (72031, 0.218) (73031, 0.218) (74031, 0.218) (75031, 0.218) (76031, 0.219) (77031, 0.219) (78031, 0.219) (79031, 0.219) (80031, 0.219) (81031, 0.22) (82031, 0.22) (83031, 0.22) (84031, 0.22) (85031, 0.22) (86031, 0.221) (87031, 0.221) (88031, 0.221) (89031, 0.221) (90031, 0.222) (91031, 0.222) (92031, 0.222) (93031, 0.222) (94031, 0.222) (95031, 0.223) (96031, 0.223) (97031, 0.223) (98031, 0.223) (99031, 0.223) (100031, 0.224) (101031, 0.224) (102031, 0.224) (103031, 0.224) (104031, 0.224) (105031, 0.224) (106031, 0.225) (107031, 0.225) (108031, 0.225) (109031, 0.225) (110031, 0.225) (111031, 0.226) (112031, 0.226) (113031, 0.226) (114031, 0.226) (115031, 0.226) (116031, 0.226) (117031, 0.227) (118031, 0.227) (119031, 0.227) (120031, 0.227) (121031, 0.227) (122031, 0.228) (123031, 0.228) (124031, 0.228) (125031, 0.228) (126031, 0.228) (127031, 0.228) (128031, 0.229) (129031, 0.229) (130031, 0.229) (131031, 0.229) (132031, 0.229) (133031, 0.229) (134031, 0.23) (135031, 0.23) (136031, 0.23) (137031, 0.23) (138031, 0.23) (139031, 0.23) (140031, 0.231) (141031, 0.231) (142031, 0.231) (143031, 0.231) (144031, 0.231) (145031, 0.231) (146031, 0.232) (147031, 0.232) (148031, 0.232) (149031, 0.232) (150031, 0.232) (151031, 0.232) (152031, 0.233) (153031, 0.233) (154031, 0.233) (155031, 0.233) (156031, 0.233) (157031, 0.233) (158031, 0.233) (159031, 0.234) (160031, 0.234) (161031, 0.234) (162031, 0.234) (163031, 0.234) (164031, 0.234) (165031, 0.234) (166031, 0.235) (167031, 0.235) (168031, 0.235) (169031, 0.235) (170031, 0.235) (171031, 0.235) (172031, 0.235) (173031, 0.236) (174031, 0.236) (175031, 0.236) (176031, 0.236) (177031, 0.236) (178031, 0.236) (179031, 0.236) (180031, 0.237) (181031, 0.237) (182031, 0.237) (183031, 0.237) (184031, 0.237) (185031, 0.237) (186031, 0.237) (187031, 0.238) (188031, 0.238) (189031, 0.238) (190031, 0.238) (191031, 0.238) (192031, 0.238) (193031, 0.238) (194031, 0.239) (195031, 0.239) (196031, 0.239) (197031, 0.239) (198031, 0.239) (199031, 0.239) (200031, 0.239) (201031, 0.24) (202031, 0.24) (203031, 0.24) (204031, 0.24) (205031, 0.24) (206031, 0.24) (207031, 0.24) (208031, 0.24) (209031, 0.241) (210031, 0.241) (211031, 0.241) (212031, 0.241) (213031, 0.241) (214031, 0.241) (215031, 0.241) (216031, 0.241) (217031, 0.242) (218031, 0.242) (219031, 0.242) (220031, 0.242) (221031, 0.242) (222031, 0.242) (223031, 0.242) (224031, 0.242) (225031, 0.243) (226031, 0.243) (227031, 0.243) (228031, 0.243) (229031, 0.243) (230031, 0.243) (231031, 0.243) (232031, 0.243) (233031, 0.244) (234031, 0.244) (235031, 0.244) (236031, 0.244) (237031, 0.244) (238031, 0.244) (239031, 0.244) (240031, 0.244) (241031, 0.245) (242031, 0.245) (243031, 0.245) (244031, 0.245) (245031, 0.245) (246031, 0.245) (247031, 0.245) (248031, 0.245) (249031, 0.246) (250031, 0.246) (251031, 0.246) (252031, 0.246) (253031, 0.246) (254031, 0.246) (255031, 0.246) (256031, 0.246) (257031, 0.247) (258031, 0.247) (259031, 0.247) (260031, 0.247) (261031, 0.247) (262031, 0.247) (263031, 0.247) (264031, 0.247) (265031, 0.247) (266031, 0.248) (267031, 0.248) (268031, 0.248) (269031, 0.248) (270031, 0.248) (271031, 0.248) (272031, 0.248) (273031, 0.248) (274031, 0.249) (275031, 0.249) (276031, 0.249) (277031, 0.249) (278031, 0.249) (279031, 0.249) (280031, 0.249) (281031, 0.249) (282031, 0.249) (283031, 0.25) (284031, 0.25) (285031, 0.25) (286031, 0.25) (287031, 0.25) (288031, 0.25) (289031, 0.25) (290031, 0.25) (291031, 0.251) (292031, 0.251) (293031, 0.251) (294031, 0.251) (295031, 0.251) (296031, 0.251) (297031, 0.251) (298031, 0.251) (299031, 0.252) (300031, 0.252) (301031, 0.252) (302031, 0.252) (303031, 0.252) (304031, 0.252) (305031, 0.252) (306031, 0.252) (307031, 0.252) (308031, 0.253) (309031, 0.253) (310031, 0.253) (311031, 0.253) (312031, 0.253) (313031, 0.253) (314031, 0.253) (315031, 0.253) (316031, 0.253) (317031, 0.254) (318031, 0.254) (319031, 0.254) (320031, 0.254) (321031, 0.254) (322031, 0.254) (323031, 0.254) (324031, 0.254) (325031, 0.255) (326031, 0.255) (327031, 0.255) (328031, 0.255) (329031, 0.255) (330031, 0.255) (331031, 0.255) (332031, 0.255) (333031, 0.255) (334031, 0.256) (335031, 0.256) (336031, 0.256) (337031, 0.256) (338031, 0.256) (339031, 0.256) (340031, 0.256) (341031, 0.256) (342031, 0.257) (343031, 0.257) (344031, 0.257) (345031, 0.257) (346031, 0.257) (347031, 0.257) (348031, 0.257) (349031, 0.257) (350031, 0.257) (351031, 0.258) (352031, 0.258) (353031, 0.258) (354031, 0.258) (355031, 0.258) (356031, 0.258) (357031, 0.258) (358031, 0.258) (359031, 0.258) (360031, 0.259) (361031, 0.259) (362031, 0.259) (363031, 0.259) (364031, 0.259) (365031, 0.259) (366031, 0.259) (367031, 0.259) (368031, 0.26) (369031, 0.26) (370031, 0.26) (371031, 0.26) (372031, 0.26) (373031, 0.26) (374031, 0.26) (375031, 0.26) (376031, 0.26) (377031, 0.261) (378031, 0.261) (379031, 0.261) (380031, 0.261) (381031, 0.261) (382031, 0.261) (383031, 0.261) (384031, 0.261) (385031, 0.262) (386031, 0.262) (387031, 0.262) (388031, 0.262) (389031, 0.262) (390031, 0.262) (391031, 0.262) (392031, 0.262) (393031, 0.262) (394031, 0.263) (395031, 0.263) (396031, 0.263) (397031, 0.263) (398031, 0.263) (399031, 0.263) (400031, 0.263) (401031, 0.263) (402031, 0.264) (403031, 0.264) (404031, 0.264) (405031, 0.264) (406031, 0.264) (407031, 0.264) (408031, 0.264) (409031, 0.264) (410031, 0.264) (411031, 0.265) (412031, 0.265) (413031, 0.265) (414031, 0.265) (415031, 0.265) (416031, 0.265) (417031, 0.265) (418031, 0.265) (419031, 0.266) (420031, 0.266) (421031, 0.266) (422031, 0.266) (423031, 0.266) (424031, 0.266) (425031, 0.266) (426031, 0.266) (427031, 0.266) (428031, 0.267) (429031, 0.267) (430031, 0.267) (431031, 0.267) (432031, 0.267) (433031, 0.267) (434031, 0.267) (435031, 0.267) (436031, 0.268) (437031, 0.268) (438031, 0.268) (439031, 0.268) (440031, 0.268) (441031, 0.268) (442031, 0.268) (443031, 0.268) (444031, 0.269) (445031, 0.269) (446031, 0.269) (447031, 0.269) (448031, 0.269) (449031, 0.269) (450031, 0.269) (451031, 0.269) (452031, 0.269) (453031, 0.27) (454031, 0.27) (455031, 0.27) (456031, 0.27) (457031, 0.27) (458031, 0.27) (459031, 0.27) (460031, 0.27) (461031, 0.271) (462031, 0.271) (463031, 0.271) (464031, 0.271) (465031, 0.271) (466031, 0.271) (467031, 0.271) (468031, 0.271) (469031, 0.272) (470031, 0.272) (471031, 0.272) (472031, 0.272) (473031, 0.272) (474031, 0.272) (475031, 0.272) (476031, 0.272) (477031, 0.273) (478031, 0.273) (479031, 0.273) (480031, 0.273) (481031, 0.273) (482031, 0.273) (483031, 0.273) (484031, 0.273) (485031, 0.273) (486031, 0.274) (487031, 0.274) (488031, 0.274) (489031, 0.274) (490031, 0.274) (491031, 0.274) (492031, 0.274) (493031, 0.274) (494031, 0.275) (495031, 0.275) (496031, 0.275) (497031, 0.275) (498031, 0.275) (499031, 0.275) (500031, 0.275) (501031, 0.275) (502031, 0.276) (503031, 0.276) (504031, 0.276) (505031, 0.276) (506031, 0.276) (507031, 0.276) (508031, 0.276) (509031, 0.276) (510031, 0.277) (511031, 0.277) (512031, 0.277) (513031, 0.277) (514031, 0.277) (515031, 0.277) (516031, 0.277) (517031, 0.277) (518031, 0.278) (519031, 0.278) (520031, 0.278) (521031, 0.278) (522031, 0.278) (523031, 0.278) (524031, 0.278) (525031, 0.278) (526031, 0.279) (527031, 0.279) (528031, 0.279) (529031, 0.279) (530031, 0.279) (531031, 0.279) (532031, 0.279) (533031, 0.279) (534031, 0.28) (535031, 0.28) (536031, 0.28) (537031, 0.28) (538031, 0.28) (539031, 0.28) (540031, 0.28) (541031, 0.28) (542031, 0.281) (543031, 0.281) (544031, 0.281) (545031, 0.281) (546031, 0.281) (547031, 0.281) (548031, 0.281) (549031, 0.281) (550031, 0.282) (551031, 0.282) (552031, 0.282) (553031, 0.282) (554031, 0.282) (555031, 0.282) (556031, 0.282) (557031, 0.282) (558031, 0.283) (559031, 0.283) (560031, 0.283) (561031, 0.283) (562031, 0.283) (563031, 0.283) (564031, 0.283) (565031, 0.283) (566031, 0.284) (567031, 0.284) (568031, 0.284) (569031, 0.284) (570031, 0.284) (571031, 0.284) (572031, 0.284) (573031, 0.285) (574031, 0.285) (575031, 0.285) (576031, 0.285) (577031, 0.285) (578031, 0.285) (579031, 0.285) (580031, 0.285) (581031, 0.286) (582031, 0.286) (583031, 0.286) (584031, 0.286) (585031, 0.286) (586031, 0.286) (587031, 0.286) (588031, 0.286) (589031, 0.287) (590031, 0.287) (591031, 0.287) (592031, 0.287) (593031, 0.287) (594031, 0.287) (595031, 0.287) (596031, 0.287) (597031, 0.288) (598031, 0.288) (599031, 0.288) (600031, 0.288) (601031, 0.288) (602031, 0.288) (603031, 0.288) (604031, 0.288) (605031, 0.289) (606031, 0.289) (607031, 0.289) (608031, 0.289) (609031, 0.289) (610031, 0.289) (611031, 0.289) (612031, 0.29) (613031, 0.29) (614031, 0.29) (615031, 0.29) (616031, 0.29) (617031, 0.29) (618031, 0.29) (619031, 0.29) (620031, 0.291) (621031, 0.291) (622031, 0.291) (623031, 0.291) (624031, 0.291) (625031, 0.291) (626031, 0.291) (627031, 0.292) (628031, 0.292) (629031, 0.292) (630031, 0.292) (631031, 0.292) (632031, 0.292) (633031, 0.292) (634031, 0.292) (635031, 0.293) (636031, 0.293) (637031, 0.293) (638031, 0.293) (639031, 0.293) (640031, 0.293) (641031, 0.293) (642031, 0.294) (643031, 0.294) (644031, 0.294) (645031, 0.294) (646031, 0.294) (647031, 0.294) (648031, 0.294) (649031, 0.294) (650031, 0.295) (651031, 0.295) (652031, 0.295) (653031, 0.295) (654031, 0.295) (655031, 0.295) (656031, 0.295) (657031, 0.296) (658031, 0.296) (659031, 0.296) (660031, 0.296) (661031, 0.296) (662031, 0.296) (663031, 0.296) (664031, 0.296) (665031, 0.297) (666031, 0.297) (667031, 0.297) (668031, 0.297) (669031, 0.297) (670031, 0.297) (671031, 0.297) (672031, 0.298) (673031, 0.298) (674031, 0.298) (675031, 0.298) (676031, 0.298) (677031, 0.298) (678031, 0.298) (679031, 0.299) (680031, 0.299) (681031, 0.299) (682031, 0.299) (683031, 0.299) (684031, 0.299) (685031, 0.299) (686031, 0.299) (687031, 0.3) (688031, 0.3) (689031, 0.3) (690031, 0.3) (691031, 0.3) (692031, 0.3) (693031, 0.3) (694031, 0.301) (695031, 0.301) (696031, 0.301) (697031, 0.301) (698031, 0.301) (699031, 0.301) (700031, 0.301) (701031, 0.302) (702031, 0.302) (703031, 0.302) (704031, 0.302) (705031, 0.302) (706031, 0.302) (707031, 0.302) (708031, 0.303) (709031, 0.303) (710031, 0.303) (711031, 0.303) (712031, 0.303) (713031, 0.303) (714031, 0.303) (715031, 0.304) (716031, 0.304) (717031, 0.304) (718031, 0.304) (719031, 0.304) (720031, 0.304) (721031, 0.304) (722031, 0.305) (723031, 0.305) (724031, 0.305) (725031, 0.305) (726031, 0.305) (727031, 0.305) (728031, 0.305) (729031, 0.306) (730031, 0.306) (731031, 0.306) (732031, 0.306) (733031, 0.306) (734031, 0.306) (735031, 0.306) (736031, 0.307) (737031, 0.307) (738031, 0.307) (739031, 0.307) (740031, 0.307) (741031, 0.307) (742031, 0.307) (743031, 0.308) (744031, 0.308) (745031, 0.308) (746031, 0.308) (747031, 0.308) (748031, 0.308) (749031, 0.308) (750031, 0.309) (751031, 0.309) (752031, 0.309) (753031, 0.309) (754031, 0.309) (755031, 0.309) (756031, 0.31) (757031, 0.31) (758031, 0.31) (759031, 0.31) (760031, 0.31) (761031, 0.31) (762031, 0.31) (763031, 0.311) (764031, 0.311) (765031, 0.311) (766031, 0.311) (767031, 0.311) (768031, 0.311) (769031, 0.311) (770031, 0.312) (771031, 0.312) (772031, 0.312) (773031, 0.312) (774031, 0.312) (775031, 0.312) (776031, 0.312) (777031, 0.313) (778031, 0.313) (779031, 0.313) (780031, 0.313) (781031, 0.313) (782031, 0.313) (783031, 0.314) (784031, 0.314) (785031, 0.314) (786031, 0.314) (787031, 0.314) (788031, 0.314) (789031, 0.314) (790031, 0.315) (791031, 0.315) (792031, 0.315) (793031, 0.315) (794031, 0.315) (795031, 0.315) (796031, 0.316) (797031, 0.316) (798031, 0.316) (799031, 0.316) (800031, 0.316) (801031, 0.316) (802031, 0.316) (803031, 0.317) (804031, 0.317) (805031, 0.317) (806031, 0.317) (807031, 0.317) (808031, 0.317) (809031, 0.318) (810031, 0.318) (811031, 0.318) (812031, 0.318) (813031, 0.318) (814031, 0.318) (815031, 0.318) (816031, 0.319) (817031, 0.319) (818031, 0.319) (819031, 0.319) (820031, 0.319) (821031, 0.319) (822031, 0.32) (823031, 0.32) (824031, 0.32) (825031, 0.32) (826031, 0.32) (827031, 0.32) (828031, 0.321) (829031, 0.321) (830031, 0.321) (831031, 0.321) (832031, 0.321) (833031, 0.321) (834031, 0.322) (835031, 0.322) (836031, 0.322) (837031, 0.322) (838031, 0.322) (839031, 0.322) (840031, 0.322) (841031, 0.323) (842031, 0.323) (843031, 0.323) (844031, 0.323) (845031, 0.323) (846031, 0.323) (847031, 0.324) (848031, 0.324) (849031, 0.324) (850031, 0.324) (851031, 0.324) (852031, 0.324) (853031, 0.325) (854031, 0.325) (855031, 0.325) (856031, 0.325) (857031, 0.325) (858031, 0.325) (859031, 0.326) (860031, 0.326) (861031, 0.326) (862031, 0.326) (863031, 0.326) (864031, 0.326) (865031, 0.327) (866031, 0.327) (867031, 0.327) (868031, 0.327) (869031, 0.327) (870031, 0.327) (871031, 0.328) (872031, 0.328) (873031, 0.328) (874031, 0.328) (875031, 0.328) (876031, 0.328) (877031, 0.329) (878031, 0.329) (879031, 0.329) (880031, 0.329) (881031, 0.329) (882031, 0.329) (883031, 0.33) (884031, 0.33) (885031, 0.33) (886031, 0.33) (887031, 0.33) (888031, 0.331) (889031, 0.331) (890031, 0.331) (891031, 0.331) (892031, 0.331) (893031, 0.331) (894031, 0.332) (895031, 0.332) (896031, 0.332) (897031, 0.332) (898031, 0.332) (899031, 0.332) (900031, 0.333) (901031, 0.333) (902031, 0.333) (903031, 0.333) (904031, 0.333) (905031, 0.333) (906031, 0.334) (907031, 0.334) (908031, 0.334) (909031, 0.334) (910031, 0.334) (911031, 0.335) (912031, 0.335) (913031, 0.335) (914031, 0.335) (915031, 0.335) (916031, 0.335) (917031, 0.336) (918031, 0.336) (919031, 0.336) (920031, 0.336) (921031, 0.336) (922031, 0.337) (923031, 0.337) (924031, 0.337) (925031, 0.337) (926031, 0.337) (927031, 0.337) (928031, 0.338) (929031, 0.338) (930031, 0.338) (931031, 0.338) (932031, 0.338) (933031, 0.339) (934031, 0.339) (935031, 0.339) (936031, 0.339) (937031, 0.339) (938031, 0.339) (939031, 0.34) (940031, 0.34) (941031, 0.34) (942031, 0.34) (943031, 0.34) (944031, 0.341) (945031, 0.341) (946031, 0.341) (947031, 0.341) (948031, 0.341) (949031, 0.341) (950031, 0.342) (951031, 0.342) (952031, 0.342) (953031, 0.342) (954031, 0.342) (955031, 0.343) (956031, 0.343) (957031, 0.343) (958031, 0.343) (959031, 0.343) (960031, 0.344) (961031, 0.344) (962031, 0.344) (963031, 0.344) (964031, 0.344) (965031, 0.345) (966031, 0.345) (967031, 0.345) (968031, 0.345) (969031, 0.345) (970031, 0.346) (971031, 0.346) (972031, 0.346) (973031, 0.346) (974031, 0.346) (975031, 0.346) (976031, 0.347) (977031, 0.347) (978031, 0.347) (979031, 0.347) (980031, 0.347) (981031, 0.348) (982031, 0.348) (983031, 0.348) (984031, 0.348) (985031, 0.348) (986031, 0.349) (987031, 0.349) (988031, 0.349) (989031, 0.349) (990031, 0.349) (991031, 0.35) (992031, 0.35) (993031, 0.35) (994031, 0.35) (995031, 0.35) (996031, 0.351) (997031, 0.351) (998031, 0.351) (999031, 0.351) (1000031, 0.351) (1001031, 0.352) (1002031, 0.352) (1003031, 0.352) (1004031, 0.352) (1005031, 0.352) (1006031, 0.353) (1007031, 0.353) (1008031, 0.353) (1009031, 0.353) (1010031, 0.353) (1011031, 0.354) (1012031, 0.354) (1013031, 0.354) (1014031, 0.354) (1015031, 0.354) (1016031, 0.355) (1017031, 0.355) (1018031, 0.355) (1019031, 0.355) (1020031, 0.356) (1021031, 0.356) (1022031, 0.356) (1023031, 0.356) (1024031, 0.356) (1025031, 0.357) (1026031, 0.357) (1027031, 0.357) (1028031, 0.357) (1029031, 0.357) (1030031, 0.358) (1031031, 0.358) (1032031, 0.358) (1033031, 0.358) (1034031, 0.358) (1035031, 0.359) (1036031, 0.359) (1037031, 0.359) (1038031, 0.359) (1039031, 0.36) (1040031, 0.36) (1041031, 0.36) (1042031, 0.36) (1043031, 0.36) (1044031, 0.361) (1045031, 0.361) (1046031, 0.361) (1047031, 0.361) (1048031, 0.361) (1049031, 0.362) (1050031, 0.362) (1051031, 0.362) (1052031, 0.362) (1053031, 0.363) (1054031, 0.363) (1055031, 0.363) (1056031, 0.363) (1057031, 0.363) (1058031, 0.364) (1059031, 0.364) (1060031, 0.364) (1061031, 0.364) (1062031, 0.365) (1063031, 0.365) (1064031, 0.365) (1065031, 0.365) (1066031, 0.365) (1067031, 0.366) (1068031, 0.366) (1069031, 0.366) (1070031, 0.366) (1071031, 0.367) (1072031, 0.367) (1073031, 0.367) (1074031, 0.367) (1075031, 0.367) (1076031, 0.368) (1077031, 0.368) (1078031, 0.368) (1079031, 0.368) (1080031, 0.369) (1081031, 0.369) (1082031, 0.369) (1083031, 0.369) (1084031, 0.369) (1085031, 0.37) (1086031, 0.37) (1087031, 0.37) (1088031, 0.37) (1089031, 0.371) (1090031, 0.371) (1091031, 0.371) (1092031, 0.371) (1093031, 0.372) (1094031, 0.372) (1095031, 0.372) (1096031, 0.372) (1097031, 0.373) (1098031, 0.373) (1099031, 0.373) (1100031, 0.373) (1101031, 0.373) (1102031, 0.374) (1103031, 0.374) (1104031, 0.374) (1105031, 0.374) (1106031, 0.375) (1107031, 0.375) (1108031, 0.375) (1109031, 0.375) (1110031, 0.376) (1111031, 0.376) (1112031, 0.376) (1113031, 0.376) (1114031, 0.377) (1115031, 0.377) (1116031, 0.377) (1117031, 0.377) (1118031, 0.378) (1119031, 0.378) (1120031, 0.378) (1121031, 0.378) (1122031, 0.379) (1123031, 0.379) (1124031, 0.379) (1125031, 0.379) (1126031, 0.379) (1127031, 0.38) (1128031, 0.38) (1129031, 0.38) (1130031, 0.38) (1131031, 0.381) (1132031, 0.381) (1133031, 0.381) (1134031, 0.381) (1135031, 0.382) (1136031, 0.382) (1137031, 0.382) (1138031, 0.382) (1139031, 0.383) (1140031, 0.383) (1141031, 0.383) (1142031, 0.383) (1143031, 0.384) (1144031, 0.384) (1145031, 0.384) (1146031, 0.384) (1147031, 0.385) (1148031, 0.385) (1149031, 0.385) (1150031, 0.385) (1151031, 0.386) (1152031, 0.386) (1153031, 0.386) (1154031, 0.386) (1155031, 0.387) (1156031, 0.387) (1157031, 0.387) (1158031, 0.387) (1159031, 0.388) (1160031, 0.388) (1161031, 0.388) (1162031, 0.388) (1163031, 0.389) (1164031, 0.389) (1165031, 0.389) (1166031, 0.389) (1167031, 0.39) (1168031, 0.39) (1169031, 0.39) (1170031, 0.39) (1171031, 0.391) (1172031, 0.391) (1173031, 0.391) (1174031, 0.391) (1175031, 0.392) (1176031, 0.392) (1177031, 0.392) (1178031, 0.392) (1179031, 0.393) (1180031, 0.393) (1181031, 0.393) (1182031, 0.393) (1183031, 0.394) (1184031, 0.394) (1185031, 0.394) (1186031, 0.394) (1187031, 0.395) (1188031, 0.395) (1189031, 0.395) (1190031, 0.395) (1191031, 0.396) (1192031, 0.396) (1193031, 0.396) (1194031, 0.396) (1195031, 0.397) (1196031, 0.397) (1197031, 0.397) (1198031, 0.398) (1199031, 0.398) (1200031, 0.398) (1201031, 0.398) (1202031, 0.399) (1203031, 0.399) (1204031, 0.399) (1205031, 0.399) (1206031, 0.4) (1207031, 0.4) (1208031, 0.4) (1209031, 0.4) (1210031, 0.401) (1211031, 0.401) (1212031, 0.401) (1213031, 0.401) (1214031, 0.402) (1215031, 0.402) (1216031, 0.402) (1217031, 0.402) (1218031, 0.403) (1219031, 0.403) (1220031, 0.403) (1221031, 0.403) (1222031, 0.404) (1223031, 0.404) (1224031, 0.404) (1225031, 0.405) (1226031, 0.405) (1227031, 0.405) (1228031, 0.405) (1229031, 0.406) (1230031, 0.406) (1231031, 0.406) (1232031, 0.406) (1233031, 0.407) (1234031, 0.407) (1235031, 0.407) (1236031, 0.407) (1237031, 0.408) (1238031, 0.408) (1239031, 0.408) (1240031, 0.408) (1241031, 0.409) (1242031, 0.409) (1243031, 0.409) (1244031, 0.409) (1245031, 0.41) (1246031, 0.41) (1247031, 0.41) (1248031, 0.41) (1249031, 0.411) (1250031, 0.411) (1251031, 0.411) (1252031, 0.412) (1253031, 0.412) (1254031, 0.412) (1255031, 0.412) (1256031, 0.413) (1257031, 0.413) (1258031, 0.413) (1259031, 0.413) (1260031, 0.414) (1261031, 0.414) (1262031, 0.414) (1263031, 0.414) (1264031, 0.415) (1265031, 0.415) (1266031, 0.415) (1267031, 0.415) (1268031, 0.416) (1269031, 0.416) (1270031, 0.416) (1271031, 0.417) (1272031, 0.417) (1273031, 0.417) (1274031, 0.417) (1275031, 0.418) (1276031, 0.418) (1277031, 0.418) (1278031, 0.418) (1279031, 0.419) (1280031, 0.419) (1281031, 0.419) (1282031, 0.419) (1283031, 0.42) (1284031, 0.42) (1285031, 0.42) (1286031, 0.421) (1287031, 0.421) (1288031, 0.421) (1289031, 0.421) (1290031, 0.422) (1291031, 0.422) (1292031, 0.422) (1293031, 0.422) (1294031, 0.423) (1295031, 0.423) (1296031, 0.423) (1297031, 0.423) (1298031, 0.424) (1299031, 0.424) (1300031, 0.424) (1301031, 0.424) (1302031, 0.425) (1303031, 0.425) (1304031, 0.425) (1305031, 0.426) (1306031, 0.426) (1307031, 0.426) (1308031, 0.426) (1309031, 0.427) (1310031, 0.427) (1311031, 0.427) (1312031, 0.427) (1313031, 0.428) (1314031, 0.428) (1315031, 0.428) (1316031, 0.428) (1317031, 0.429) (1318031, 0.429) (1319031, 0.429) (1320031, 0.43) (1321031, 0.43) (1322031, 0.43) (1323031, 0.43) (1324031, 0.431) (1325031, 0.431) (1326031, 0.431) (1327031, 0.431) (1328031, 0.432) (1329031, 0.432) (1330031, 0.432) (1331031, 0.432) (1332031, 0.433) (1333031, 0.433) (1334031, 0.433) (1335031, 0.433) (1336031, 0.434) (1337031, 0.434) (1338031, 0.434) (1339031, 0.435) (1340031, 0.435) (1341031, 0.435) (1342031, 0.435) (1343031, 0.436) (1344031, 0.436) (1345031, 0.436) (1346031, 0.436) (1347031, 0.437) (1348031, 0.437) (1349031, 0.437) (1350031, 0.437) (1351031, 0.438) (1352031, 0.438) (1353031, 0.438) (1354031, 0.439) (1355031, 0.439) (1356031, 0.439) (1357031, 0.439) (1358031, 0.44) (1359031, 0.44) (1360031, 0.44) (1361031, 0.44) (1362031, 0.441) (1363031, 0.441) (1364031, 0.441) (1365031, 0.441) (1366031, 0.442) (1367031, 0.442) (1368031, 0.442) (1369031, 0.442) (1370031, 0.443) (1371031, 0.443) (1372031, 0.443) (1373031, 0.443) (1374031, 0.444) (1375031, 0.444) (1376031, 0.444) (1377031, 0.445) (1378031, 0.445) (1379031, 0.445) (1380031, 0.445) (1381031, 0.446) (1382031, 0.446) (1383031, 0.446) (1384031, 0.446) (1385031, 0.447) (1386031, 0.447) (1387031, 0.447) (1388031, 0.447) (1389031, 0.448) (1390031, 0.448) (1391031, 0.448) (1392031, 0.448) (1393031, 0.449) (1394031, 0.449) (1395031, 0.449) (1396031, 0.45) (1397031, 0.45) (1398031, 0.45) (1399031, 0.45) (1400031, 0.451) (1401031, 0.451) (1402031, 0.451) (1403031, 0.451) (1404031, 0.452) (1405031, 0.452) (1406031, 0.452) (1407031, 0.452) (1408031, 0.453) (1409031, 0.453) (1410031, 0.453) (1411031, 0.453) (1412031, 0.454) (1413031, 0.454) (1414031, 0.454) (1415031, 0.454) (1416031, 0.455) (1417031, 0.455) (1418031, 0.455) (1419031, 0.456) (1420031, 0.456) (1421031, 0.456) (1422031, 0.456) (1423031, 0.457) (1424031, 0.457) (1425031, 0.457) (1426031, 0.457) (1427031, 0.458) (1428031, 0.458) (1429031, 0.458) (1430031, 0.458) (1431031, 0.459) (1432031, 0.459) (1433031, 0.459) (1434031, 0.459) (1435031, 0.46) (1436031, 0.46) (1437031, 0.46) (1438031, 0.46) (1439031, 0.461) (1440031, 0.461) (1441031, 0.461) (1442031, 0.461) (1443031, 0.462) (1444031, 0.462) (1445031, 0.462) (1446031, 0.463) (1447031, 0.463) (1448031, 0.463) (1449031, 0.463) (1450031, 0.464) (1451031, 0.464) (1452031, 0.464) (1453031, 0.464) (1454031, 0.465) (1455031, 0.465) (1456031, 0.465) (1457031, 0.465) (1458031, 0.466) (1459031, 0.466) (1460031, 0.466) (1461031, 0.466) (1462031, 0.467) (1463031, 0.467) (1464031, 0.467) (1465031, 0.467) (1466031, 0.468) (1467031, 0.468) (1468031, 0.468) (1469031, 0.468) (1470031, 0.469) (1471031, 0.469) (1472031, 0.469) (1473031, 0.47) (1474031, 0.47) (1475031, 0.47) (1476031, 0.47) (1477031, 0.471) (1478031, 0.471) (1479031, 0.471) (1480031, 0.471) (1481031, 0.472) (1482031, 0.472) (1483031, 0.472) (1484031, 0.472) (1485031, 0.473) (1486031, 0.473) (1487031, 0.473) (1488031, 0.473) (1489031, 0.474) (1490031, 0.474) (1491031, 0.474) (1492031, 0.474) (1493031, 0.475) (1494031, 0.475) (1495031, 0.475) (1496031, 0.475) (1497031, 0.476) (1498031, 0.476) (1499031, 0.476) (1500031, 0.477) (1501031, 0.477) (1502031, 0.477) (1503031, 0.477) (1504031, 0.478) (1505031, 0.478) (1506031, 0.478) (1507031, 0.478) (1508031, 0.479) (1509031, 0.479) (1510031, 0.479) (1511031, 0.479) (1512031, 0.48) (1513031, 0.48) (1514031, 0.48) (1515031, 0.48) (1516031, 0.481) (1517031, 0.481) (1518031, 0.481) (1519031, 0.481) (1520031, 0.482) (1521031, 0.482) (1522031, 0.482) (1523031, 0.482) (1524031, 0.483) (1525031, 0.483) (1526031, 0.483) (1527031, 0.484) (1528031, 0.484) (1529031, 0.484) (1530031, 0.484) (1531031, 0.485) (1532031, 0.485) (1533031, 0.485) (1534031, 0.485) (1535031, 0.486) (1536031, 0.486) (1537031, 0.486) (1538031, 0.486) (1539031, 0.487) (1540031, 0.487) (1541031, 0.487) (1542031, 0.487) (1543031, 0.488) (1544031, 0.488) (1545031, 0.488) (1546031, 0.488) (1547031, 0.489) (1548031, 0.489) (1549031, 0.489) (1550031, 0.49) (1551031, 0.49) (1552031, 0.49) (1553031, 0.49) (1554031, 0.491) (1555031, 0.491) (1556031, 0.491) (1557031, 0.491) (1558031, 0.492) (1559031, 0.492) (1560031, 0.492) (1561031, 0.492) (1562031, 0.493) (1563031, 0.493) (1564031, 0.493) (1565031, 0.493) (1566031, 0.494) (1567031, 0.494) (1568031, 0.494) (1569031, 0.494) (1570031, 0.495) (1571031, 0.495) (1572031, 0.495) (1573031, 0.496) (1574031, 0.496) (1575031, 0.496) (1576031, 0.496) (1577031, 0.497) (1578031, 0.497) (1579031, 0.497) (1580031, 0.497) (1581031, 0.498) (1582031, 0.498) (1583031, 0.498) (1584031, 0.498) (1585031, 0.499) (1586031, 0.499) (1587031, 0.499) (1588031, 0.499) (1589031, 0.5) (1590031, 0.5) (1591031, 0.5) (1592031, 0.501) (1593031, 0.501) (1594031, 0.501) (1595031, 0.501) (1596031, 0.502) (1597031, 0.502) (1598031, 0.502) (1599031, 0.502) (1600031, 0.503) (1601031, 0.503) (1602031, 0.503) (1603031, 0.503) (1604031, 0.504) (1605031, 0.504) (1606031, 0.504) (1607031, 0.504) (1608031, 0.505) (1609031, 0.505) (1610031, 0.505) (1611031, 0.505) (1612031, 0.506) (1613031, 0.506) (1614031, 0.506) (1615031, 0.507) (1616031, 0.507) (1617031, 0.507) (1618031, 0.507) (1619031, 0.508) (1620031, 0.508) (1621031, 0.508) (1622031, 0.508) (1623031, 0.509) (1624031, 0.509) (1625031, 0.509) (1626031, 0.509) (1627031, 0.51) (1628031, 0.51) (1629031, 0.51) (1630031, 0.51) (1631031, 0.511) (1632031, 0.511) (1633031, 0.511) (1634031, 0.512) (1635031, 0.512) (1636031, 0.512) (1637031, 0.512) (1638031, 0.513) (1639031, 0.513) (1640031, 0.513) (1641031, 0.513) (1642031, 0.514) (1643031, 0.514) (1644031, 0.514) (1645031, 0.514) (1646031, 0.515) (1647031, 0.515) (1648031, 0.515) (1649031, 0.515) (1650031, 0.516) (1651031, 0.516) (1652031, 0.516) (1653031, 0.517) (1654031, 0.517) (1655031, 0.517) (1656031, 0.517) (1657031, 0.518) (1658031, 0.518) (1659031, 0.518) (1660031, 0.518) (1661031, 0.519) (1662031, 0.519) (1663031, 0.519) (1664031, 0.519) (1665031, 0.52) (1666031, 0.52) (1667031, 0.52) (1668031, 0.521) (1669031, 0.521) (1670031, 0.521) (1671031, 0.521) (1672031, 0.522) (1673031, 0.522) (1674031, 0.522) (1675031, 0.522) (1676031, 0.523) (1677031, 0.523) (1678031, 0.523) (1679031, 0.523) (1680031, 0.524) (1681031, 0.524) (1682031, 0.524) (1683031, 0.525) (1684031, 0.525) (1685031, 0.525) (1686031, 0.525) (1687031, 0.526) (1688031, 0.526) (1689031, 0.526) (1690031, 0.526) (1691031, 0.527) (1692031, 0.527) (1693031, 0.527) (1694031, 0.528) (1695031, 0.528) (1696031, 0.528) (1697031, 0.528) (1698031, 0.529) (1699031, 0.529) (1700031, 0.529) (1701031, 0.529) (1702031, 0.53) (1703031, 0.53) (1704031, 0.53) (1705031, 0.53) (1706031, 0.531) (1707031, 0.531) (1708031, 0.531) (1709031, 0.531) (1710031, 0.532) (1711031, 0.532) (1712031, 0.532) (1713031, 0.533) (1714031, 0.533) (1715031, 0.533) (1716031, 0.533) (1717031, 0.534) (1718031, 0.534) (1719031, 0.534) (1720031, 0.534) (1721031, 0.535) (1722031, 0.535) (1723031, 0.535) (1724031, 0.536) (1725031, 0.536) (1726031, 0.536) (1727031, 0.536) (1728031, 0.537) (1729031, 0.537) (1730031, 0.537) (1731031, 0.537) (1732031, 0.538) (1733031, 0.538) (1734031, 0.538) (1735031, 0.539) (1736031, 0.539) (1737031, 0.539) (1738031, 0.539) (1739031, 0.54) (1740031, 0.54) (1741031, 0.54) (1742031, 0.54) (1743031, 0.541) (1744031, 0.541) (1745031, 0.541) (1746031, 0.542) (1747031, 0.542) (1748031, 0.542) (1749031, 0.542) (1750031, 0.543) (1751031, 0.543) (1752031, 0.543) (1753031, 0.543) (1754031, 0.544) (1755031, 0.544) (1756031, 0.544) (1757031, 0.545) (1758031, 0.545) (1759031, 0.545) (1760031, 0.545) (1761031, 0.546) (1762031, 0.546) (1763031, 0.546) (1764031, 0.546) (1765031, 0.547) (1766031, 0.547) (1767031, 0.547) (1768031, 0.548) (1769031, 0.548) (1770031, 0.548) (1771031, 0.548) (1772031, 0.549) (1773031, 0.549) (1774031, 0.549) (1775031, 0.549) (1776031, 0.55) (1777031, 0.55) (1778031, 0.55) (1779031, 0.551) (1780031, 0.551) (1781031, 0.551) (1782031, 0.551) (1783031, 0.552) (1784031, 0.552) (1785031, 0.552) (1786031, 0.552) (1787031, 0.553) (1788031, 0.553) (1789031, 0.553) (1790031, 0.554) (1791031, 0.554) (1792031, 0.554) (1793031, 0.554) (1794031, 0.555) (1795031, 0.555) (1796031, 0.555) (1797031, 0.556) (1798031, 0.556) (1799031, 0.556) (1800031, 0.556) (1801031, 0.557) (1802031, 0.557) (1803031, 0.557) (1804031, 0.557) (1805031, 0.558) (1806031, 0.558) (1807031, 0.558) (1808031, 0.559) (1809031, 0.559) (1810031, 0.559) (1811031, 0.559) (1812031, 0.56) (1813031, 0.56) (1814031, 0.56) (1815031, 0.561) (1816031, 0.561) (1817031, 0.561) (1818031, 0.561) (1819031, 0.562) (1820031, 0.562) (1821031, 0.562) (1822031, 0.563) (1823031, 0.563) (1824031, 0.563) (1825031, 0.563) (1826031, 0.564) (1827031, 0.564) (1828031, 0.564) (1829031, 0.564) (1830031, 0.565) (1831031, 0.565) (1832031, 0.565) (1833031, 0.566) (1834031, 0.566) (1835031, 0.566) (1836031, 0.566) (1837031, 0.567) (1838031, 0.567) (1839031, 0.567) (1840031, 0.568) (1841031, 0.568) (1842031, 0.568) (1843031, 0.568) (1844031, 0.569) (1845031, 0.569) (1846031, 0.569) (1847031, 0.57) (1848031, 0.57) (1849031, 0.57) (1850031, 0.57) (1851031, 0.571) (1852031, 0.571) (1853031, 0.571) (1854031, 0.572) (1855031, 0.572) (1856031, 0.572) (1857031, 0.572) (1858031, 0.573) (1859031, 0.573) (1860031, 0.573) (1861031, 0.574) (1862031, 0.574) (1863031, 0.574) (1864031, 0.574) (1865031, 0.575) (1866031, 0.575) (1867031, 0.575) (1868031, 0.576) (1869031, 0.576) (1870031, 0.576) (1871031, 0.576) (1872031, 0.577) (1873031, 0.577) (1874031, 0.577) (1875031, 0.578) (1876031, 0.578) (1877031, 0.578) (1878031, 0.578) (1879031, 0.579) (1880031, 0.579) (1881031, 0.579) (1882031, 0.58) (1883031, 0.58) (1884031, 0.58) (1885031, 0.581) (1886031, 0.581) (1887031, 0.581) (1888031, 0.581) (1889031, 0.582) (1890031, 0.582) (1891031, 0.582) (1892031, 0.583) (1893031, 0.583) (1894031, 0.583) (1895031, 0.583) (1896031, 0.584) (1897031, 0.584) (1898031, 0.584) (1899031, 0.585) (1900031, 0.585) (1901031, 0.585) (1902031, 0.585) (1903031, 0.586) (1904031, 0.586) (1905031, 0.586) (1906031, 0.587) (1907031, 0.587) (1908031, 0.587) (1909031, 0.588) (1910031, 0.588) (1911031, 0.588) (1912031, 0.588) (1913031, 0.589) (1914031, 0.589) (1915031, 0.589) (1916031, 0.59) (1917031, 0.59) (1918031, 0.59) (1919031, 0.59) (1920031, 0.591) (1921031, 0.591) (1922031, 0.591) (1923031, 0.592) (1924031, 0.592) (1925031, 0.592) (1926031, 0.593) (1927031, 0.593) (1928031, 0.593) (1929031, 0.593) (1930031, 0.594) (1931031, 0.594) (1932031, 0.594) (1933031, 0.595) (1934031, 0.595) (1935031, 0.595) (1936031, 0.596) (1937031, 0.596) (1938031, 0.596) (1939031, 0.596) (1940031, 0.597) (1941031, 0.597) (1942031, 0.597) (1943031, 0.598) (1944031, 0.598) (1945031, 0.598) (1946031, 0.598) (1947031, 0.599) (1948031, 0.599) (1949031, 0.599) (1950031, 0.6) (1951031, 0.6) (1952031, 0.6) (1953031, 0.601) (1954031, 0.601) (1955031, 0.601) (1956031, 0.601) (1957031, 0.602) (1958031, 0.602) (1959031, 0.602) (1960031, 0.603) (1961031, 0.603) (1962031, 0.603) (1963031, 0.604) (1964031, 0.604) (1965031, 0.604) (1966031, 0.604) (1967031, 0.605) (1968031, 0.605) (1969031, 0.605) (1970031, 0.606) (1971031, 0.606) (1972031, 0.606) (1973031, 0.607) (1974031, 0.607) (1975031, 0.607) (1976031, 0.607) (1977031, 0.608) (1978031, 0.608) (1979031, 0.608) (1980031, 0.609) (1981031, 0.609) (1982031, 0.609) (1983031, 0.61) (1984031, 0.61) (1985031, 0.61) (1986031, 0.61) (1987031, 0.611) (1988031, 0.611) (1989031, 0.611) (1990031, 0.612) (1991031, 0.612) (1992031, 0.612) (1993031, 0.613) (1994031, 0.613) (1995031, 0.613) (1996031, 0.614) (1997031, 0.614) (1998031, 0.614) (1999031, 0.614) (2000031, 0.615) (2001031, 0.615) (2002031, 0.615) (2003031, 0.616) (2004031, 0.616) (2005031, 0.616) (2006031, 0.617) (2007031, 0.617) (2008031, 0.617) (2009031, 0.618) (2010031, 0.618) (2011031, 0.618) (2012031, 0.618) (2013031, 0.619) (2014031, 0.619) (2015031, 0.619) (2016031, 0.62) (2017031, 0.62) (2018031, 0.62) (2019031, 0.621) (2020031, 0.621) (2021031, 0.621) (2022031, 0.621) (2023031, 0.622) (2024031, 0.622) (2025031, 0.622) (2026031, 0.623) (2027031, 0.623) (2028031, 0.623) (2029031, 0.624) (2030031, 0.624) (2031031, 0.624) (2032031, 0.625) (2033031, 0.625) (2034031, 0.625) (2035031, 0.626) (2036031, 0.626) (2037031, 0.626) (2038031, 0.627) (2039031, 0.627) (2040031, 0.627) (2041031, 0.627) (2042031, 0.628) (2043031, 0.628) (2044031, 0.628) (2045031, 0.629) (2046031, 0.629) (2047031, 0.629) (2048031, 0.63) (2049031, 0.63) (2050031, 0.63) (2051031, 0.631) (2052031, 0.631) (2053031, 0.631) (2054031, 0.632) (2055031, 0.632) (2056031, 0.632) (2057031, 0.633) (2058031, 0.633) (2059031, 0.633) (2060031, 0.634) (2061031, 0.634) (2062031, 0.634) (2063031, 0.634) (2064031, 0.635) (2065031, 0.635) (2066031, 0.635) (2067031, 0.636) (2068031, 0.636) (2069031, 0.636) (2070031, 0.637) (2071031, 0.637) (2072031, 0.637) (2073031, 0.638) (2074031, 0.638) (2075031, 0.638) (2076031, 0.639) (2077031, 0.639) (2078031, 0.639) (2079031, 0.64) (2080031, 0.64) (2081031, 0.64) (2082031, 0.641) (2083031, 0.641) (2084031, 0.641) (2085031, 0.642) (2086031, 0.642) (2087031, 0.642) (2088031, 0.643) (2089031, 0.643) (2090031, 0.643) (2091031, 0.644) (2092031, 0.644) (2093031, 0.644) (2094031, 0.644) (2095031, 0.645) (2096031, 0.645) (2097031, 0.645) (2098031, 0.646) (2099031, 0.646) (2100031, 0.646) (2101031, 0.647) (2102031, 0.647) (2103031, 0.647) (2104031, 0.648) (2105031, 0.648) (2106031, 0.648) (2107031, 0.649) (2108031, 0.649) (2109031, 0.649) (2110031, 0.65) (2111031, 0.65) (2112031, 0.65) (2113031, 0.651) (2114031, 0.651) (2115031, 0.651) (2116031, 0.652) (2117031, 0.652) (2118031, 0.652) (2119031, 0.653) (2120031, 0.653) (2121031, 0.653) (2122031, 0.654) (2123031, 0.654) (2124031, 0.654) (2125031, 0.655) (2126031, 0.655) (2127031, 0.655) (2128031, 0.656) (2129031, 0.656) (2130031, 0.656) (2131031, 0.657) (2132031, 0.657) (2133031, 0.657) (2134031, 0.658) (2135031, 0.658) (2136031, 0.658) (2137031, 0.659) (2138031, 0.659) (2139031, 0.659) (2140031, 0.66) (2141031, 0.66) (2142031, 0.66) (2143031, 0.661) (2144031, 0.661) (2145031, 0.661) (2146031, 0.662) (2147031, 0.662) (2148031, 0.662) (2149031, 0.663) (2150031, 0.663) (2151031, 0.663) (2152031, 0.664) (2153031, 0.664) (2154031, 0.664) (2155031, 0.665) (2156031, 0.665) (2157031, 0.665) (2158031, 0.666) (2159031, 0.666) (2160031, 0.666) (2161031, 0.667) (2162031, 0.667) (2163031, 0.667) (2164031, 0.668) (2165031, 0.668) (2166031, 0.668) (2167031, 0.669) (2168031, 0.669) (2169031, 0.669) (2170031, 0.67) (2171031, 0.67) (2172031, 0.67) (2173031, 0.671) (2174031, 0.671) (2175031, 0.671) (2176031, 0.672) (2177031, 0.672) (2178031, 0.672) (2179031, 0.673) (2180031, 0.673) (2181031, 0.673) (2182031, 0.674) (2183031, 0.674) (2184031, 0.674) (2185031, 0.675) (2186031, 0.675) (2187031, 0.675) (2188031, 0.676) (2189031, 0.676) (2190031, 0.676) (2191031, 0.677) (2192031, 0.677) (2193031, 0.677) (2194031, 0.678) (2195031, 0.678) (2196031, 0.678) (2197031, 0.679) (2198031, 0.679) (2199031, 0.68) (2200031, 0.68) (2201031, 0.68) (2202031, 0.681) (2203031, 0.681) (2204031, 0.681) (2205031, 0.682) (2206031, 0.682) (2207031, 0.682) (2208031, 0.683) (2209031, 0.683) (2210031, 0.683) (2211031, 0.684) (2212031, 0.684) (2213031, 0.684) (2214031, 0.685) (2215031, 0.685) (2216031, 0.685) (2217031, 0.686) (2218031, 0.686) (2219031, 0.686) (2220031, 0.687) (2221031, 0.687) (2222031, 0.687) (2223031, 0.688) (2224031, 0.688) (2225031, 0.688) (2226031, 0.689) (2227031, 0.689) (2228031, 0.69) (2229031, 0.69) (2230031, 0.69) (2231031, 0.691) (2232031, 0.691) (2233031, 0.691) (2234031, 0.692) (2235031, 0.692) (2236031, 0.692) (2237031, 0.693) (2238031, 0.693) (2239031, 0.693) (2240031, 0.694) (2241031, 0.694) (2242031, 0.695) (2243031, 0.695) (2244031, 0.695) (2245031, 0.696) (2246031, 0.696) (2247031, 0.696) (2248031, 0.697) (2249031, 0.697) (2250031, 0.697) (2251031, 0.698) (2252031, 0.698) (2253031, 0.698) (2254031, 0.699) (2255031, 0.699) (2256031, 0.7) (2257031, 0.7) (2258031, 0.7) (2259031, 0.701) (2260031, 0.701) (2261031, 0.701) (2262031, 0.702) (2263031, 0.702) (2264031, 0.702) (2265031, 0.703) (2266031, 0.703) (2267031, 0.703) (2268031, 0.704) (2269031, 0.704) (2270031, 0.705) (2271031, 0.705) (2272031, 0.705) (2273031, 0.706) (2274031, 0.706) (2275031, 0.706) (2276031, 0.707) (2277031, 0.707) (2278031, 0.707) (2279031, 0.708) (2280031, 0.708) (2281031, 0.709) (2282031, 0.709) (2283031, 0.709) (2284031, 0.71) (2285031, 0.71) (2286031, 0.71) (2287031, 0.711) (2288031, 0.711) (2289031, 0.711) (2290031, 0.712) (2291031, 0.712) (2292031, 0.713) (2293031, 0.713) (2294031, 0.713) (2295031, 0.714) (2296031, 0.714) (2297031, 0.714) (2298031, 0.715) (2299031, 0.715) (2300031, 0.715) (2301031, 0.716) (2302031, 0.716) (2303031, 0.717) (2304031, 0.717) (2305031, 0.717) (2306031, 0.718) (2307031, 0.718) (2308031, 0.718) (2309031, 0.719) (2310031, 0.719) (2311031, 0.72) (2312031, 0.72) (2313031, 0.72) (2314031, 0.721) (2315031, 0.721) (2316031, 0.721) (2317031, 0.722) (2318031, 0.722) (2319031, 0.722) (2320031, 0.723) (2321031, 0.723) (2322031, 0.724) (2323031, 0.724) (2324031, 0.724) (2325031, 0.725) (2326031, 0.725) (2327031, 0.725) (2328031, 0.726) (2329031, 0.726) (2330031, 0.727) (2331031, 0.727) (2332031, 0.727) (2333031, 0.728) (2334031, 0.728) (2335031, 0.728) (2336031, 0.729) (2337031, 0.729) (2338031, 0.73) (2339031, 0.73) (2340031, 0.73) (2341031, 0.731) (2342031, 0.731) (2343031, 0.732) (2344031, 0.732) (2345031, 0.732) (2346031, 0.733) (2347031, 0.733) (2348031, 0.734) (2349031, 0.734) (2350031, 0.734) (2351031, 0.735) (2352031, 0.735) (2353031, 0.735) (2354031, 0.736) (2355031, 0.736) (2356031, 0.737) (2357031, 0.737) (2358031, 0.737) (2359031, 0.738) (2360031, 0.738) (2361031, 0.738) (2362031, 0.739) (2363031, 0.739) (2364031, 0.74) (2365031, 0.74) (2366031, 0.74) (2367031, 0.741) (2368031, 0.741) (2369031, 0.742) (2370031, 0.742) (2371031, 0.742) (2372031, 0.743) (2373031, 0.743) (2374031, 0.743) (2375031, 0.744) (2376031, 0.744) (2377031, 0.745) (2378031, 0.745) (2379031, 0.745) (2380031, 0.746) (2381031, 0.746) (2382031, 0.747) (2383031, 0.747) (2384031, 0.747) (2385031, 0.748) (2386031, 0.748) (2387031, 0.749) (2388031, 0.749) (2389031, 0.749) (2390031, 0.75) (2391031, 0.75) (2392031, 0.751) (2393031, 0.751) (2394031, 0.751) (2395031, 0.752) (2396031, 0.752) (2397031, 0.753) (2398031, 0.753) (2399031, 0.753) (2400031, 0.754) (2401031, 0.754) (2402031, 0.755) (2403031, 0.755) (2404031, 0.755) (2405031, 0.756) (2406031, 0.756) (2407031, 0.757) (2408031, 0.757) (2409031, 0.757) (2410031, 0.758) (2411031, 0.758) (2412031, 0.759) (2413031, 0.759) (2414031, 0.759) (2415031, 0.76) (2416031, 0.76) (2417031, 0.761) (2418031, 0.761) (2419031, 0.761) (2420031, 0.762) (2421031, 0.762) (2422031, 0.763) (2423031, 0.763) (2424031, 0.763) (2425031, 0.764) (2426031, 0.764) (2427031, 0.765) (2428031, 0.765) (2429031, 0.765) (2430031, 0.766) (2431031, 0.766) (2432031, 0.767) (2433031, 0.767) (2434031, 0.767) (2435031, 0.768) (2436031, 0.768) (2437031, 0.769) (2438031, 0.769) (2439031, 0.769) (2440031, 0.77) (2441031, 0.77) (2442031, 0.771) (2443031, 0.771) (2444031, 0.772) (2445031, 0.772) (2446031, 0.772) (2447031, 0.773) (2448031, 0.773) (2449031, 0.774) (2450031, 0.774) (2451031, 0.774) (2452031, 0.775) (2453031, 0.775) (2454031, 0.776) (2455031, 0.776) (2456031, 0.777) (2457031, 0.777) (2458031, 0.777) (2459031, 0.778) (2460031, 0.778) (2461031, 0.779) (2462031, 0.779) (2463031, 0.779) (2464031, 0.78) (2465031, 0.78) (2466031, 0.781) (2467031, 0.781) (2468031, 0.781) (2469031, 0.782) (2470031, 0.782) (2471031, 0.783) (2472031, 0.783) (2473031, 0.784) (2474031, 0.784) (2475031, 0.784) (2476031, 0.785) (2477031, 0.785) (2478031, 0.786) (2479031, 0.786) (2480031, 0.787) (2481031, 0.787) (2482031, 0.787) (2483031, 0.788) (2484031, 0.788) (2485031, 0.789) (2486031, 0.789) (2487031, 0.79) (2488031, 0.79) (2489031, 0.79) (2490031, 0.791) (2491031, 0.791) (2492031, 0.792) (2493031, 0.792) (2494031, 0.793) (2495031, 0.793) (2496031, 0.793) (2497031, 0.794) (2498031, 0.794) (2499031, 0.795) (2500031, 0.795) (2501031, 0.796) (2502031, 0.796) (2503031, 0.796) (2504031, 0.797) (2505031, 0.797) (2506031, 0.798) (2507031, 0.798) (2508031, 0.799) (2509031, 0.799) (2510031, 0.799) (2511031, 0.8) (2512031, 0.8) (2513031, 0.801) (2514031, 0.801) (2515031, 0.802) (2516031, 0.802) (2517031, 0.803) (2518031, 0.803) (2519031, 0.803) (2520031, 0.804) (2521031, 0.804) (2522031, 0.805) (2523031, 0.805) (2524031, 0.806) (2525031, 0.806) (2526031, 0.806) (2527031, 0.807) (2528031, 0.807) (2529031, 0.808) (2530031, 0.808) (2531031, 0.809) (2532031, 0.809) (2533031, 0.81) (2534031, 0.81) (2535031, 0.811) (2536031, 0.811) (2537031, 0.811) (2538031, 0.812) (2539031, 0.812) (2540031, 0.813) (2541031, 0.813) (2542031, 0.814) (2543031, 0.814) (2544031, 0.815) (2545031, 0.815) (2546031, 0.815) (2547031, 0.816) (2548031, 0.816) (2549031, 0.817) (2550031, 0.817) (2551031, 0.818) (2552031, 0.818) (2553031, 0.819) (2554031, 0.819) (2555031, 0.82) (2556031, 0.82) (2557031, 0.82) (2558031, 0.821) (2559031, 0.821) (2560031, 0.822) (2561031, 0.822) (2562031, 0.823) (2563031, 0.823) (2564031, 0.824) (2565031, 0.824) (2566031, 0.824) (2567031, 0.825) (2568031, 0.825) (2569031, 0.826) (2570031, 0.826) (2571031, 0.827) (2572031, 0.827) (2573031, 0.828) (2574031, 0.828) (2575031, 0.829) (2576031, 0.829) (2577031, 0.83) (2578031, 0.83) (2579031, 0.83) (2580031, 0.831) (2581031, 0.831) (2582031, 0.832) (2583031, 0.832) (2584031, 0.833) (2585031, 0.833) (2586031, 0.834) (2587031, 0.834) (2588031, 0.834) (2589031, 0.835) (2590031, 0.835) (2591031, 0.836) (2592031, 0.836) (2593031, 0.837) (2594031, 0.837) (2595031, 0.838) (2596031, 0.838) (2597031, 0.839) (2598031, 0.839) (2599031, 0.84) (2600031, 0.84) (2601031, 0.841) (2602031, 0.841) (2603031, 0.842) (2604031, 0.842) (2605031, 0.842) (2606031, 0.843) (2607031, 0.843) (2608031, 0.844) (2609031, 0.844) (2610031, 0.845) (2611031, 0.845) (2612031, 0.846) (2613031, 0.846) (2614031, 0.847) (2615031, 0.847) (2616031, 0.848) (2617031, 0.848) (2618031, 0.849) (2619031, 0.849) (2620031, 0.85) (2621031, 0.85) (2622031, 0.85) (2623031, 0.851) (2624031, 0.851) (2625031, 0.852) (2626031, 0.852) (2627031, 0.853) (2628031, 0.853) (2629031, 0.854) (2630031, 0.854) (2631031, 0.855) (2632031, 0.855) (2633031, 0.856) (2634031, 0.856) (2635031, 0.857) (2636031, 0.857) (2637031, 0.858) (2638031, 0.858) (2639031, 0.859) (2640031, 0.859) (2641031, 0.86) (2642031, 0.86) (2643031, 0.861) (2644031, 0.861) (2645031, 0.861) (2646031, 0.862) (2647031, 0.862) (2648031, 0.863) (2649031, 0.863) (2650031, 0.864) (2651031, 0.864) (2652031, 0.865) (2653031, 0.865) (2654031, 0.866) (2655031, 0.866) (2656031, 0.867) (2657031, 0.867) (2658031, 0.868) (2659031, 0.868) (2660031, 0.869) (2661031, 0.869) (2662031, 0.87) (2663031, 0.87) (2664031, 0.871) (2665031, 0.871) (2666031, 0.872) (2667031, 0.872) (2668031, 0.873) (2669031, 0.873) (2670031, 0.874) (2671031, 0.874) (2672031, 0.875) (2673031, 0.875) (2674031, 0.876) (2675031, 0.876) (2676031, 0.877) (2677031, 0.877) (2678031, 0.878) (2679031, 0.878) (2680031, 0.879) (2681031, 0.879) (2682031, 0.88) (2683031, 0.88) (2684031, 0.881) (2685031, 0.881) (2686031, 0.882) (2687031, 0.882) (2688031, 0.883) (2689031, 0.883) (2690031, 0.884) (2691031, 0.884) (2692031, 0.885) (2693031, 0.885) (2694031, 0.886) (2695031, 0.886) (2696031, 0.887) (2697031, 0.887) (2698031, 0.888) (2699031, 0.888) (2700031, 0.889) (2701031, 0.889) (2702031, 0.89) (2703031, 0.89) (2704031, 0.891) (2705031, 0.891) (2706031, 0.892) (2707031, 0.892) (2708031, 0.893) (2709031, 0.893) (2710031, 0.894) (2711031, 0.894) (2712031, 0.895) (2713031, 0.896) (2714031, 0.896) (2715031, 0.897) (2716031, 0.897) (2717031, 0.898) (2718031, 0.898) (2719031, 0.899) (2720031, 0.899) (2721031, 0.9) (2722031, 0.9) (2723031, 0.901) (2724031, 0.901) (2725031, 0.902) (2726031, 0.902) (2727031, 0.903) (2728031, 0.903) (2729031, 0.904) (2730031, 0.905) (2731031, 0.905) (2732031, 0.906) (2733031, 0.906) (2734031, 0.907) (2735031, 0.907) (2736031, 0.908) (2737031, 0.908) (2738031, 0.909) (2739031, 0.909) (2740031, 0.91) (2741031, 0.91) (2742031, 0.911) (2743031, 0.911) (2744031, 0.912) (2745031, 0.913) (2746031, 0.913) (2747031, 0.914) (2748031, 0.914) (2749031, 0.915) (2750031, 0.915) (2751031, 0.916) (2752031, 0.916) (2753031, 0.917) (2754031, 0.917) (2755031, 0.918) (2756031, 0.919) (2757031, 0.919) (2758031, 0.92) (2759031, 0.92) (2760031, 0.921) (2761031, 0.921) (2762031, 0.922) (2763031, 0.922) (2764031, 0.923) (2765031, 0.923) (2766031, 0.924) (2767031, 0.925) (2768031, 0.925) (2769031, 0.926) (2770031, 0.926) (2771031, 0.927) (2772031, 0.927) (2773031, 0.928) (2774031, 0.928) (2775031, 0.929) (2776031, 0.929) (2777031, 0.93) (2778031, 0.931) (2779031, 0.931) (2780031, 0.932) (2781031, 0.932) (2782031, 0.933) (2783031, 0.933) (2784031, 0.934) (2785031, 0.934) (2786031, 0.935) (2787031, 0.936) (2788031, 0.936) (2789031, 0.937) (2790031, 0.937) (2791031, 0.938) (2792031, 0.938) (2793031, 0.939) (2794031, 0.94) (2795031, 0.94) (2796031, 0.941) (2797031, 0.941) (2798031, 0.942) (2799031, 0.942) (2800031, 0.943) (2801031, 0.944) (2802031, 0.944) (2803031, 0.945) (2804031, 0.945) (2805031, 0.946) (2806031, 0.946) (2807031, 0.947) (2808031, 0.948) (2809031, 0.948) (2810031, 0.949) (2811031, 0.949) (2812031, 0.95) (2813031, 0.95) (2814031, 0.951) (2815031, 0.952) (2816031, 0.952) (2817031, 0.953) (2818031, 0.953) (2819031, 0.954) (2820031, 0.955) (2821031, 0.955) (2822031, 0.956) (2823031, 0.956) (2824031, 0.957) (2825031, 0.958) (2826031, 0.958) (2827031, 0.959) (2828031, 0.959) (2829031, 0.96) (2830031, 0.96) (2831031, 0.961) (2832031, 0.962) (2833031, 0.962) (2834031, 0.963) (2835031, 0.963) (2836031, 0.964) (2837031, 0.965) (2838031, 0.965) (2839031, 0.966) (2840031, 0.966) (2841031, 0.967) (2842031, 0.968) (2843031, 0.968) (2844031, 0.969) (2845031, 0.969) (2846031, 0.97) (2847031, 0.971) (2848031, 0.971) (2849031, 0.972) (2850031, 0.972) (2851031, 0.973) (2852031, 0.974) (2853031, 0.974) (2854031, 0.975) (2855031, 0.976) (2856031, 0.976) (2857031, 0.977) (2858031, 0.977) (2859031, 0.978) (2860031, 0.979) (2861031, 0.979) (2862031, 0.98) (2863031, 0.98) (2864031, 0.981) (2865031, 0.982) (2866031, 0.982) (2867031, 0.983) (2868031, 0.984) (2869031, 0.984) (2870031, 0.985) (2871031, 0.985) (2872031, 0.986) (2873031, 0.987) (2874031, 0.987) (2875031, 0.988) (2876031, 0.989) (2877031, 0.989) (2878031, 0.99) (2879031, 0.99) (2880031, 0.991) (2881031, 0.992) (2882031, 0.992) (2883031, 0.993) (2884031, 0.993) (2885031, 0.994) (2886031, 0.995) (2887031, 0.995) (2888031, 0.996) (2889031, 0.997) (2890031, 0.997) (2891031, 0.998) (2892031, 0.999) (2893031, 0.999) (2894031, 1) (2895031, 1) (2896031, 1.001) (2897031, 1.002) (2898031, 1.002) (2899031, 1.003) (2900031, 1.004) (2901031, 1.004) (2902031, 1.005) (2903031, 1.006) (2904031, 1.006) (2905031, 1.007) (2906031, 1.008) (2907031, 1.008) (2908031, 1.009) (2909031, 1.01) (2910031, 1.01) (2911031, 1.011) (2912031, 1.011) (2913031, 1.012) (2914031, 1.013) (2915031, 1.013) (2916031, 1.014) (2917031, 1.015) (2918031, 1.015) (2919031, 1.016) (2920031, 1.017) (2921031, 1.017) (2922031, 1.018) (2923031, 1.019) (2924031, 1.019) (2925031, 1.02) (2926031, 1.021) (2927031, 1.021) (2928031, 1.022) (2929031, 1.023) (2930031, 1.023) (2931031, 1.024) (2932031, 1.025) (2933031, 1.025) (2934031, 1.026) (2935031, 1.027) (2936031, 1.027) (2937031, 1.028) (2938031, 1.029) (2939031, 1.029) (2940031, 1.03) (2941031, 1.031) (2942031, 1.031) (2943031, 1.032) (2944031, 1.033) (2945031, 1.033) (2946031, 1.034) (2947031, 1.035) (2948031, 1.035) (2949031, 1.036) (2950031, 1.037) (2951031, 1.037) (2952031, 1.038) (2953031, 1.039) (2954031, 1.039) (2955031, 1.04) (2956031, 1.041) (2957031, 1.041) (2958031, 1.042) (2959031, 1.043) (2960031, 1.043) (2961031, 1.044) (2962031, 1.045) (2963031, 1.045) (2964031, 1.046) (2965031, 1.047) (2966031, 1.047) (2967031, 1.048) (2968031, 1.049) (2969031, 1.05) (2970031, 1.05) (2971031, 1.051) (2972031, 1.052) (2973031, 1.052) (2974031, 1.053) (2975031, 1.054) (2976031, 1.054) (2977031, 1.055) (2978031, 1.056) (2979031, 1.057) (2980031, 1.057) (2981031, 1.058) (2982031, 1.059) (2983031, 1.059) (2984031, 1.06) (2985031, 1.061) (2986031, 1.061) (2987031, 1.062) (2988031, 1.063) (2989031, 1.064) (2990031, 1.064) (2991031, 1.065) (2992031, 1.066) (2993031, 1.066) (2994031, 1.067) (2995031, 1.068) (2996031, 1.069) (2997031, 1.069) (2998031, 1.07) (2999031, 1.071) (3000031, 1.071) (3001031, 1.072) (3002031, 1.073) (3003031, 1.074) (3004031, 1.074) (3005031, 1.075) (3006031, 1.076) (3007031, 1.076) (3008031, 1.077) (3009031, 1.078) (3010031, 1.079) (3011031, 1.079) (3012031, 1.08) (3013031, 1.081) (3014031, 1.082) (3015031, 1.082) (3016031, 1.083) (3017031, 1.084) (3018031, 1.085) (3019031, 1.085) (3020031, 1.086) (3021031, 1.087) (3022031, 1.088) (3023031, 1.088) (3024031, 1.089) (3025031, 1.09) (3026031, 1.091) (3027031, 1.091) (3028031, 1.092) (3029031, 1.093) (3030031, 1.093) (3031031, 1.094) (3032031, 1.095) (3033031, 1.096) (3034031, 1.096) (3035031, 1.097) (3036031, 1.098) (3037031, 1.099) (3038031, 1.1) (3039031, 1.1) (3040031, 1.101) (3041031, 1.102) (3042031, 1.103) (3043031, 1.103) (3044031, 1.104) (3045031, 1.105) (3046031, 1.106) (3047031, 1.106) (3048031, 1.107) (3049031, 1.108) (3050031, 1.109) (3051031, 1.109) (3052031, 1.11) (3053031, 1.111) (3054031, 1.112) (3055031, 1.112) (3056031, 1.113) (3057031, 1.114) (3058031, 1.115) (3059031, 1.116) (3060031, 1.116) (3061031, 1.117) (3062031, 1.118) (3063031, 1.119) (3064031, 1.12) (3065031, 1.12) (3066031, 1.121) (3067031, 1.122) (3068031, 1.123) (3069031, 1.124) (3070031, 1.124) (3071031, 1.125) (3072031, 1.126) (3073031, 1.127) (3074031, 1.127) (3075031, 1.128) (3076031, 1.129) (3077031, 1.13) (3078031, 1.131) (3079031, 1.131) (3080031, 1.132) (3081031, 1.133) (3082031, 1.134) (3083031, 1.135) (3084031, 1.135) (3085031, 1.136) (3086031, 1.137) (3087031, 1.138) (3088031, 1.139) (3089031, 1.139) (3090031, 1.14) (3091031, 1.141) (3092031, 1.142) (3093031, 1.143) (3094031, 1.143) (3095031, 1.144) (3096031, 1.145) (3097031, 1.146) (3098031, 1.147) (3099031, 1.148) (3100031, 1.148) (3101031, 1.149) (3102031, 1.15) (3103031, 1.151) (3104031, 1.152) (3105031, 1.153) (3106031, 1.153) (3107031, 1.154) (3108031, 1.155) (3109031, 1.156) (3110031, 1.157) (3111031, 1.158) (3112031, 1.158) (3113031, 1.159) (3114031, 1.16) (3115031, 1.161) (3116031, 1.162) (3117031, 1.163) (3118031, 1.164) (3119031, 1.164) (3120031, 1.165) (3121031, 1.166) (3122031, 1.167) (3123031, 1.168) (3124031, 1.169) (3125031, 1.169) (3126031, 1.17) (3127031, 1.171) (3128031, 1.172) (3129031, 1.173) (3130031, 1.174) (3131031, 1.175) (3132031, 1.175) (3133031, 1.176) (3134031, 1.177) (3135031, 1.178) (3136031, 1.179) (3137031, 1.18) (3138031, 1.181) (3139031, 1.181) (3140031, 1.182) (3141031, 1.183) (3142031, 1.184) (3143031, 1.185) (3144031, 1.186) (3145031, 1.187) (3146031, 1.187) (3147031, 1.188) (3148031, 1.189) (3149031, 1.19) (3150031, 1.191) (3151031, 1.192) (3152031, 1.193) (3153031, 1.194) (3154031, 1.194) (3155031, 1.195) (3156031, 1.196) (3157031, 1.197) (3158031, 1.198) (3159031, 1.199) (3160031, 1.2) (3161031, 1.2) (3162031, 1.201) (3163031, 1.202) (3164031, 1.203) (3165031, 1.204) (3166031, 1.205) (3167031, 1.206) (3168031, 1.207) (3169031, 1.208) (3170031, 1.208) (3171031, 1.209) (3172031, 1.21) (3173031, 1.211) (3174031, 1.212) (3175031, 1.213) (3176031, 1.214) (3177031, 1.215) (3178031, 1.216) (3179031, 1.216) (3180031, 1.217) (3181031, 1.218) (3182031, 1.219) (3183031, 1.22) (3184031, 1.221) (3185031, 1.222) (3186031, 1.223) (3187031, 1.224) (3188031, 1.225) (3189031, 1.225) (3190031, 1.226) (3191031, 1.227) (3192031, 1.228) (3193031, 1.229) (3194031, 1.23) (3195031, 1.231) (3196031, 1.232) (3197031, 1.233) (3198031, 1.234) (3199031, 1.235) (3200031, 1.235) (3201031, 1.236) (3202031, 1.237) (3203031, 1.238) (3204031, 1.239) (3205031, 1.24) (3206031, 1.241) (3207031, 1.242) (3208031, 1.243) (3209031, 1.244) (3210031, 1.245) (3211031, 1.246) (3212031, 1.247) (3213031, 1.248) (3214031, 1.248) (3215031, 1.249) (3216031, 1.25) (3217031, 1.251) (3218031, 1.252) (3219031, 1.253) (3220031, 1.254) (3221031, 1.255) (3222031, 1.256) (3223031, 1.257) (3224031, 1.258) (3225031, 1.259) (3226031, 1.26) (3227031, 1.261) (3228031, 1.262) (3229031, 1.263) (3230031, 1.263) (3231031, 1.264) (3232031, 1.265) (3233031, 1.266) (3234031, 1.267) (3235031, 1.268) (3236031, 1.269) (3237031, 1.27) (3238031, 1.271) (3239031, 1.272) (3240031, 1.273) (3241031, 1.274) (3242031, 1.275) (3243031, 1.276) (3244031, 1.277) (3245031, 1.278) (3246031, 1.278) (3247031, 1.279) (3248031, 1.28) (3249031, 1.281) (3250031, 1.282) (3251031, 1.283) (3252031, 1.284) (3253031, 1.285) (3254031, 1.286) (3255031, 1.287) (3256031, 1.288) (3257031, 1.289) (3258031, 1.29) (3259031, 1.291) (3260031, 1.292) (3261031, 1.293) (3262031, 1.294) (3263031, 1.295) (3264031, 1.296) (3265031, 1.297) (3266031, 1.298) (3267031, 1.299) (3268031, 1.3) (3269031, 1.301) (3270031, 1.302) (3271031, 1.303) (3272031, 1.304) (3273031, 1.305) (3274031, 1.306) (3275031, 1.307) (3276031, 1.308) (3277031, 1.309) (3278031, 1.31) (3279031, 1.311) (3280031, 1.312) (3281031, 1.313) (3282031, 1.314) (3283031, 1.315) (3284031, 1.316) (3285031, 1.317) (3286031, 1.318) (3287031, 1.319) (3288031, 1.32) (3289031, 1.321) (3290031, 1.322) (3291031, 1.323) (3292031, 1.324) (3293031, 1.325) (3294031, 1.326) (3295031, 1.327) (3296031, 1.328) (3297031, 1.329) (3298031, 1.33) (3299031, 1.331) (3300031, 1.332) (3301031, 1.333) (3302031, 1.334) (3303031, 1.335) (3304031, 1.336) (3305031, 1.337) (3306031, 1.338) (3307031, 1.339) (3308031, 1.34) (3309031, 1.341) (3310031, 1.343) (3311031, 1.344) (3312031, 1.345) (3313031, 1.346) (3314031, 1.347) (3315031, 1.348) (3316031, 1.349) (3317031, 1.35) (3318031, 1.351) (3319031, 1.352) (3320031, 1.353) (3321031, 1.354) (3322031, 1.355) (3323031, 1.356) (3324031, 1.357) (3325031, 1.358) (3326031, 1.359) (3327031, 1.36) (3328031, 1.361) (3329031, 1.362) (3330031, 1.364) (3331031, 1.365) (3332031, 1.366) (3333031, 1.367) (3334031, 1.368) (3335031, 1.369) (3336031, 1.37) (3337031, 1.371) (3338031, 1.372) (3339031, 1.373) (3340031, 1.375) (3341031, 1.376) (3342031, 1.377) (3343031, 1.378) (3344031, 1.379) (3345031, 1.38) (3346031, 1.381) (3347031, 1.382) (3348031, 1.383) (3349031, 1.384) (3350031, 1.385) (3351031, 1.387) (3352031, 1.388) (3353031, 1.389) (3354031, 1.39) (3355031, 1.391) (3356031, 1.392) (3357031, 1.393) (3358031, 1.394) (3359031, 1.395) (3360031, 1.396) (3361031, 1.397) (3362031, 1.399) (3363031, 1.4) (3364031, 1.401) (3365031, 1.402) (3366031, 1.403) (3367031, 1.404) (3368031, 1.405) (3369031, 1.406) (3370031, 1.408) (3371031, 1.409) (3372031, 1.41) (3373031, 1.411) (3374031, 1.412) (3375031, 1.413) (3376031, 1.414) (3377031, 1.415) (3378031, 1.417) (3379031, 1.418) (3380031, 1.419) (3381031, 1.42) (3382031, 1.421) (3383031, 1.422) (3384031, 1.423) (3385031, 1.425) (3386031, 1.426) (3387031, 1.427) (3388031, 1.428) (3389031, 1.429) (3390031, 1.43) (3391031, 1.431) (3392031, 1.433) (3393031, 1.434) (3394031, 1.435) (3395031, 1.436) (3396031, 1.437) (3397031, 1.438) (3398031, 1.44) (3399031, 1.441) (3400031, 1.442) (3401031, 1.443) (3402031, 1.444) (3403031, 1.445) (3404031, 1.447) (3405031, 1.448) (3406031, 1.449) (3407031, 1.45) (3408031, 1.451) (3409031, 1.452) (3410031, 1.453) (3411031, 1.454) (3412031, 1.456) (3413031, 1.457) (3414031, 1.458) (3415031, 1.459) (3416031, 1.46) (3417031, 1.461) (3418031, 1.463) (3419031, 1.464) (3420031, 1.465) (3421031, 1.466) (3422031, 1.467) (3423031, 1.469) (3424031, 1.47) (3425031, 1.471) (3426031, 1.472) (3427031, 1.473) (3428031, 1.474) (3429031, 1.476) (3430031, 1.477) (3431031, 1.478) (3432031, 1.479) (3433031, 1.481) (3434031, 1.482) (3435031, 1.483) (3436031, 1.484) (3437031, 1.485) (3438031, 1.487) (3439031, 1.488) (3440031, 1.489) (3441031, 1.49) (3442031, 1.492) (3443031, 1.493) (3444031, 1.494) (3445031, 1.495) (3446031, 1.496) (3447031, 1.497) (3448031, 1.499) (3449031, 1.5) (3450031, 1.501) (3451031, 1.503) (3452031, 1.504) (3453031, 1.505) (3454031, 1.506) (3455031, 1.508) (3456031, 1.509) (3457031, 1.51) (3458031, 1.511) (3459031, 1.512) (3460031, 1.514) (3461031, 1.515) (3462031, 1.516) (3463031, 1.517) (3464031, 1.519) (3465031, 1.52) (3466031, 1.521) (3467031, 1.522) (3468031, 1.523) (3469031, 1.525) (3470031, 1.526) (3471031, 1.527) (3472031, 1.529) (3473031, 1.53) (3474031, 1.531) (3475031, 1.532) (3476031, 1.534) (3477031, 1.535) (3478031, 1.536) (3479031, 1.538) (3480031, 1.539) (3481031, 1.54) (3482031, 1.541) (3483031, 1.543) (3484031, 1.544) (3485031, 1.545) (3486031, 1.547) (3487031, 1.548) (3488031, 1.549) (3489031, 1.55) (3490031, 1.552) (3491031, 1.553) (3492031, 1.554) (3493031, 1.556) (3494031, 1.557) (3495031, 1.558) (3496031, 1.56) (3497031, 1.561) (3498031, 1.562) (3499031, 1.563) (3500031, 1.565) (3501031, 1.566) (3502031, 1.567) (3503031, 1.569) (3504031, 1.57) (3505031, 1.571) (3506031, 1.573) (3507031, 1.574) (3508031, 1.575) (3509031, 1.577) (3510031, 1.578) (3511031, 1.579) (3512031, 1.581) (3513031, 1.582) (3514031, 1.583) (3515031, 1.585) (3516031, 1.586) (3517031, 1.587) (3518031, 1.589) (3519031, 1.59) (3520031, 1.592) (3521031, 1.593) (3522031, 1.594) (3523031, 1.596) (3524031, 1.597) (3525031, 1.598) (3526031, 1.599) (3527031, 1.601) (3528031, 1.602) (3529031, 1.604) (3530031, 1.605) (3531031, 1.606) (3532031, 1.608) (3533031, 1.609) (3534031, 1.61) (3535031, 1.612) (3536031, 1.613) (3537031, 1.615) (3538031, 1.616) (3539031, 1.617) (3540031, 1.619) (3541031, 1.62) (3542031, 1.621) (3543031, 1.623) (3544031, 1.624) (3545031, 1.626) (3546031, 1.627) (3547031, 1.628) (3548031, 1.63) (3549031, 1.631) (3550031, 1.632) (3551031, 1.634) (3552031, 1.635) (3553031, 1.637) (3554031, 1.638) (3555031, 1.639) (3556031, 1.641) (3557031, 1.642) (3558031, 1.644) (3559031, 1.645) (3560031, 1.647) (3561031, 1.648) (3562031, 1.65) (3563031, 1.651) (3564031, 1.652) (3565031, 1.654) (3566031, 1.655) (3567031, 1.657) (3568031, 1.658) (3569031, 1.659) (3570031, 1.661) (3571031, 1.662) (3572031, 1.664) (3573031, 1.665) (3574031, 1.667) (3575031, 1.668) (3576031, 1.67) (3577031, 1.671) (3578031, 1.673) (3579031, 1.674) (3580031, 1.675) (3581031, 1.677) (3582031, 1.678) (3583031, 1.68) (3584031, 1.681) (3585031, 1.683) (3586031, 1.684) (3587031, 1.685) (3588031, 1.687) (3589031, 1.688) (3590031, 1.69) (3591031, 1.691) (3592031, 1.693) (3593031, 1.694) (3594031, 1.696) (3595031, 1.697) (3596031, 1.698) (3597031, 1.7) (3598031, 1.701) (3599031, 1.703) (3600031, 1.704) (3601031, 1.706) (3602031, 1.707) (3603031, 1.709) (3604031, 1.71) (3605031, 1.712) (3606031, 1.714) (3607031, 1.715) (3608031, 1.717) (3609031, 1.718) (3610031, 1.72) (3611031, 1.721) (3612031, 1.723) (3613031, 1.724) (3614031, 1.726) (3615031, 1.727) (3616031, 1.729) (3617031, 1.73) (3618031, 1.732) (3619031, 1.733) (3620031, 1.735) (3621031, 1.736) (3622031, 1.738) (3623031, 1.739) (3624031, 1.741) (3625031, 1.742) (3626031, 1.744) (3627031, 1.745) (3628031, 1.747) (3629031, 1.748) (3630031, 1.75) (3631031, 1.751) (3632031, 1.753) (3633031, 1.754) (3634031, 1.756) (3635031, 1.758) (3636031, 1.759) (3637031, 1.761) (3638031, 1.762) (3639031, 1.764) (3640031, 1.765) (3641031, 1.767) (3642031, 1.768) (3643031, 1.77) (3644031, 1.771) (3645031, 1.773) (3646031, 1.775) (3647031, 1.776) (3648031, 1.778) (3649031, 1.779) (3650031, 1.781) (3651031, 1.783) (3652031, 1.784) (3653031, 1.786) (3654031, 1.787) (3655031, 1.789) (3656031, 1.791) (3657031, 1.792) (3658031, 1.794) (3659031, 1.795) (3660031, 1.797) (3661031, 1.799) (3662031, 1.8) (3663031, 1.802) (3664031, 1.803) (3665031, 1.805) (3666031, 1.807) (3667031, 1.808) (3668031, 1.81) (3669031, 1.812) (3670031, 1.813) (3671031, 1.815) (3672031, 1.816) (3673031, 1.818) (3674031, 1.82) (3675031, 1.821) (3676031, 1.823) (3677031, 1.824) (3678031, 1.826) (3679031, 1.828) (3680031, 1.829) (3681031, 1.831) (3682031, 1.833) (3683031, 1.834) (3684031, 1.836) (3685031, 1.837) (3686031, 1.839) (3687031, 1.841) (3688031, 1.842) (3689031, 1.844) (3690031, 1.846) (3691031, 1.847) (3692031, 1.849) (3693031, 1.851) (3694031, 1.852) (3695031, 1.854) (3696031, 1.856) (3697031, 1.857) (3698031, 1.859) (3699031, 1.861) (3700031, 1.862) (3701031, 1.864) (3702031, 1.866) (3703031, 1.867) (3704031, 1.869) (3705031, 1.871) (3706031, 1.872) (3707031, 1.874) (3708031, 1.876) (3709031, 1.878) (3710031, 1.879) (3711031, 1.881) (3712031, 1.883) (3713031, 1.884) (3714031, 1.886) (3715031, 1.888) (3716031, 1.889) (3717031, 1.891) (3718031, 1.893) (3719031, 1.894) (3720031, 1.896) (3721031, 1.898) (3722031, 1.9) (3723031, 1.901) (3724031, 1.903) (3725031, 1.905) (3726031, 1.907) (3727031, 1.908) (3728031, 1.91) (3729031, 1.912) (3730031, 1.914) (3731031, 1.915) (3732031, 1.917) (3733031, 1.919) (3734031, 1.921) (3735031, 1.922) (3736031, 1.924) (3737031, 1.926) (3738031, 1.928) (3739031, 1.929) (3740031, 1.931) (3741031, 1.933) (3742031, 1.935) (3743031, 1.936) (3744031, 1.938) (3745031, 1.94) (3746031, 1.942) (3747031, 1.944) (3748031, 1.945) (3749031, 1.947) (3750031, 1.949) (3751031, 1.951) (3752031, 1.952) (3753031, 1.954) (3754031, 1.956) (3755031, 1.958) (3756031, 1.96) (3757031, 1.961) (3758031, 1.963) (3759031, 1.965) (3760031, 1.967) (3761031, 1.969) (3762031, 1.97) (3763031, 1.972) (3764031, 1.974) (3765031, 1.976) (3766031, 1.978) (3767031, 1.98) (3768031, 1.981) (3769031, 1.983) (3770031, 1.985) (3771031, 1.987) (3772031, 1.989) (3773031, 1.991) (3774031, 1.993) (3775031, 1.994) (3776031, 1.996) (3777031, 1.998) (3778031, 2) (3779031, 2.002) (3780031, 2.004) (3781031, 2.006) (3782031, 2.007) (3783031, 2.009) (3784031, 2.011) (3785031, 2.013) (3786031, 2.015) (3787031, 2.017) (3788031, 2.019) (3789031, 2.021) (3790031, 2.023) (3791031, 2.025) (3792031, 2.027) (3793031, 2.029) (3794031, 2.031) (3795031, 2.033) (3796031, 2.034) (3797031, 2.036) (3798031, 2.038) (3799031, 2.04) (3800031, 2.042) (3801031, 2.044) (3802031, 2.046) (3803031, 2.048) (3804031, 2.05) (3805031, 2.052) (3806031, 2.054) (3807031, 2.056) (3808031, 2.058) (3809031, 2.06) (3810031, 2.061) (3811031, 2.063) (3812031, 2.065) (3813031, 2.067) (3814031, 2.069) (3815031, 2.071) (3816031, 2.073) (3817031, 2.075) (3818031, 2.077) (3819031, 2.079) (3820031, 2.081) (3821031, 2.083) (3822031, 2.085) (3823031, 2.087) (3824031, 2.089) (3825031, 2.091) (3826031, 2.093) (3827031, 2.095) (3828031, 2.097) (3829031, 2.099) (3830031, 2.101) (3831031, 2.103) (3832031, 2.105) (3833031, 2.107) (3834031, 2.109) (3835031, 2.111) (3836031, 2.113) (3837031, 2.115) (3838031, 2.117) (3839031, 2.119) (3840031, 2.121) (3841031, 2.123) (3842031, 2.125) (3843031, 2.127) (3844031, 2.129) (3845031, 2.132) (3846031, 2.134) (3847031, 2.136) (3848031, 2.138) (3849031, 2.14) (3850031, 2.142) (3851031, 2.144) (3852031, 2.146) (3853031, 2.148) (3854031, 2.15) (3855031, 2.153) (3856031, 2.155) (3857031, 2.157) (3858031, 2.159) (3859031, 2.161) (3860031, 2.163) (3861031, 2.165) (3862031, 2.167) (3863031, 2.169) (3864031, 2.171) (3865031, 2.174) (3866031, 2.176) (3867031, 2.178) (3868031, 2.18) (3869031, 2.182) (3870031, 2.184) (3871031, 2.186) (3872031, 2.188) (3873031, 2.19) (3874031, 2.192) (3875031, 2.195) (3876031, 2.197) (3877031, 2.199) (3878031, 2.201) (3879031, 2.203) (3880031, 2.205) (3881031, 2.208) (3882031, 2.21) (3883031, 2.212) (3884031, 2.214) (3885031, 2.217) (3886031, 2.219) (3887031, 2.221) (3888031, 2.223) (3889031, 2.226) (3890031, 2.228) (3891031, 2.23) (3892031, 2.232) (3893031, 2.234) (3894031, 2.236) (3895031, 2.239) (3896031, 2.241) (3897031, 2.243) (3898031, 2.245) (3899031, 2.248) (3900031, 2.25) (3901031, 2.252) (3902031, 2.254) (3903031, 2.256) (3904031, 2.259) (3905031, 2.261) (3906031, 2.263) (3907031, 2.265) (3908031, 2.268) (3909031, 2.27) (3910031, 2.272) (3911031, 2.275) (3912031, 2.277) (3913031, 2.279) (3914031, 2.281) (3915031, 2.284) (3916031, 2.286) (3917031, 2.288) (3918031, 2.291) (3919031, 2.293) (3920031, 2.295) (3921031, 2.298) (3922031, 2.3) (3923031, 2.302) (3924031, 2.305) (3925031, 2.307) (3926031, 2.31) (3927031, 2.312) (3928031, 2.314) (3929031, 2.317) (3930031, 2.319) (3931031, 2.321) (3932031, 2.324) (3933031, 2.326) (3934031, 2.328) (3935031, 2.331) (3936031, 2.333) (3937031, 2.335) (3938031, 2.338) (3939031, 2.34) (3940031, 2.343) (3941031, 2.345) (3942031, 2.347) (3943031, 2.35) (3944031, 2.352) (3945031, 2.354) (3946031, 2.357) (3947031, 2.359) (3948031, 2.361) (3949031, 2.364) (3950031, 2.366) (3951031, 2.369) (3952031, 2.371) (3953031, 2.373) (3954031, 2.376) (3955031, 2.378) (3956031, 2.381) (3957031, 2.383) (3958031, 2.386) (3959031, 2.388) (3960031, 2.39) (3961031, 2.393) (3962031, 2.395) (3963031, 2.398) (3964031, 2.4) (3965031, 2.403) (3966031, 2.405) (3967031, 2.407) (3968031, 2.41) (3969031, 2.412) (3970031, 2.415) (3971031, 2.418) (3972031, 2.42) (3973031, 2.422) (3974031, 2.425) (3975031, 2.427) (3976031, 2.43) (3977031, 2.432) (3978031, 2.435) (3979031, 2.437) (3980031, 2.44) (3981031, 2.442) (3982031, 2.445) (3983031, 2.447) (3984031, 2.45) (3985031, 2.452) (3986031, 2.455) (3987031, 2.458) (3988031, 2.46) (3989031, 2.463) (3990031, 2.465) (3991031, 2.468) (3992031, 2.471) (3993031, 2.473) (3994031, 2.476) (3995031, 2.478) (3996031, 2.481) (3997031, 2.483) (3998031, 2.486) (3999031, 2.488) (4000031, 2.491) (4001031, 2.494) (4002031, 2.496) (4003031, 2.499) (4004031, 2.502) (4005031, 2.504) (4006031, 2.507) (4007031, 2.509) (4008031, 2.512) (4009031, 2.515) (4010031, 2.517) (4011031, 2.52) (4012031, 2.523) (4013031, 2.525) (4014031, 2.528) (4015031, 2.531) (4016031, 2.533) (4017031, 2.536) (4018031, 2.539) (4019031, 2.541) (4020031, 2.544) (4021031, 2.547) (4022031, 2.549) (4023031, 2.552) (4024031, 2.555) (4025031, 2.557) (4026031, 2.56) (4027031, 2.563) (4028031, 2.565) (4029031, 2.568) (4030031, 2.571) (4031031, 2.573) (4032031, 2.576) (4033031, 2.579) (4034031, 2.582) (4035031, 2.584) (4036031, 2.587) (4037031, 2.59) (4038031, 2.593) (4039031, 2.595) (4040031, 2.598) (4041031, 2.601) (4042031, 2.603) (4043031, 2.606) (4044031, 2.609) (4045031, 2.612) (4046031, 2.614) (4047031, 2.617) (4048031, 2.62) (4049031, 2.622) (4050031, 2.625) (4051031, 2.628) (4052031, 2.631) (4053031, 2.634) (4054031, 2.636) (4055031, 2.639) (4056031, 2.642) (4057031, 2.645) (4058031, 2.648) (4059031, 2.651) (4060031, 2.653) (4061031, 2.656) (4062031, 2.659) (4063031, 2.662) (4064031, 2.665) (4065031, 2.667) (4066031, 2.67) (4067031, 2.673) (4068031, 2.676) (4069031, 2.679) (4070031, 2.682) (4071031, 2.684) (4072031, 2.687) (4073031, 2.69) (4074031, 2.693) (4075031, 2.696) (4076031, 2.699) (4077031, 2.702) (4078031, 2.705) (4079031, 2.707) (4080031, 2.71) (4081031, 2.713) (4082031, 2.716) (4083031, 2.719) (4084031, 2.722) (4085031, 2.725) (4086031, 2.727) (4087031, 2.73) (4088031, 2.733) (4089031, 2.736) (4090031, 2.739) (4091031, 2.742) (4092031, 2.745) (4093031, 2.748) (4094031, 2.751) (4095031, 2.754) (4096031, 2.757) (4097031, 2.76) (4098031, 2.763) (4099031, 2.766) (4100031, 2.769) (4101031, 2.772) (4102031, 2.775) (4103031, 2.778) (4104031, 2.781) (4105031, 2.784) (4106031, 2.787) (4107031, 2.79) (4108031, 2.793) (4109031, 2.796) (4110031, 2.799) (4111031, 2.802) (4112031, 2.805) (4113031, 2.808) (4114031, 2.811) (4115031, 2.814) (4116031, 2.817) (4117031, 2.82) (4118031, 2.823) (4119031, 2.826) (4120031, 2.83) (4121031, 2.833) (4122031, 2.836) (4123031, 2.839) (4124031, 2.842) (4125031, 2.845) (4126031, 2.849) (4127031, 2.852) (4128031, 2.855) (4129031, 2.858) (4130031, 2.861) (4131031, 2.864) (4132031, 2.867) (4133031, 2.87) (4134031, 2.873) (4135031, 2.877) (4136031, 2.88) (4137031, 2.882) (4138031, 2.886) (4139031, 2.889) (4140031, 2.892) (4141031, 2.895) (4142031, 2.899) (4143031, 2.902) (4144031, 2.905) (4145031, 2.908) (4146031, 2.911) (4147031, 2.914) (4148031, 2.917) (4149031, 2.92) (4150031, 2.923) (4151031, 2.927) (4152031, 2.93) (4153031, 2.933) (4154031, 2.937) (4155031, 2.94) (4156031, 2.943) (4157031, 2.946) (4158031, 2.95) (4159031, 2.953) (4160031, 2.956) (4161031, 2.96) (4162031, 2.963) (4163031, 2.966) (4164031, 2.969) (4165031, 2.973) (4166031, 2.976) (4167031, 2.979) (4168031, 2.982) (4169031, 2.986) (4170031, 2.989) (4171031, 2.992) (4172031, 2.995) (4173031, 2.999) (4174031, 3.002) (4175031, 3.005) (4176031, 3.009) (4177031, 3.012) (4178031, 3.015) (4179031, 3.019) (4180031, 3.022) (4181031, 3.026) (4182031, 3.029) (4183031, 3.033) (4184031, 3.036) (4185031, 3.039) (4186031, 3.043) (4187031, 3.046) (4188031, 3.05) (4189031, 3.053) (4190031, 3.057) (4191031, 3.06) (4192031, 3.063) (4193031, 3.067) (4194031, 3.071) (4195031, 3.074) (4196031, 3.077) (4197031, 3.081) (4198031, 3.084) (4199031, 3.088) (4200031, 3.091) (4201031, 3.095) (4202031, 3.099) (4203031, 3.102) (4204031, 3.106) (4205031, 3.109) (4206031, 3.113) (4207031, 3.116) (4208031, 3.12) (4209031, 3.123) (4210031, 3.127) (4211031, 3.13) (4212031, 3.134) (4213031, 3.137) (4214031, 3.141) (4215031, 3.144) (4216031, 3.148) (4217031, 3.151) (4218031, 3.155) (4219031, 3.158) (4220031, 3.162) (4221031, 3.166) (4222031, 3.169) (4223031, 3.173) (4224031, 3.176) (4225031, 3.18) (4226031, 3.184) (4227031, 3.188) (4228031, 3.191) (4229031, 3.195) (4230031, 3.198) (4231031, 3.202) (4232031, 3.206) (4233031, 3.21) (4234031, 3.213) (4235031, 3.217) (4236031, 3.221) (4237031, 3.225) (4238031, 3.228) (4239031, 3.232) (4240031, 3.236) (4241031, 3.24) (4242031, 3.243) (4243031, 3.247) (4244031, 3.251) (4245031, 3.255) (4246031, 3.258) (4247031, 3.262) (4248031, 3.266) (4249031, 3.27) (4250031, 3.274) (4251031, 3.277) (4252031, 3.281) (4253031, 3.285) (4254031, 3.289) (4255031, 3.293) (4256031, 3.296) (4257031, 3.301) (4258031, 3.304) (4259031, 3.308) (4260031, 3.312) (4261031, 3.316) (4262031, 3.32) (4263031, 3.323) (4264031, 3.327) (4265031, 3.331) (4266031, 3.335) (4267031, 3.339) (4268031, 3.343) (4269031, 3.347) (4270031, 3.351) (4271031, 3.354) (4272031, 3.358) (4273031, 3.362) (4274031, 3.366) (4275031, 3.37) (4276031, 3.374) (4277031, 3.378) (4278031, 3.382) (4279031, 3.386) (4280031, 3.39) (4281031, 3.394) (4282031, 3.398) (4283031, 3.402) (4284031, 3.405) (4285031, 3.409) (4286031, 3.414) (4287031, 3.418) (4288031, 3.422) (4289031, 3.426) (4290031, 3.43) (4291031, 3.434) (4292031, 3.438) (4293031, 3.443) (4294031, 3.446) (4295031, 3.45) (4296031, 3.454) (4297031, 3.458) (4298031, 3.463) (4299031, 3.467) (4300031, 3.471) (4301031, 3.475) (4302031, 3.48) (4303031, 3.484) (4304031, 3.488) (4305031, 3.492) (4306031, 3.496) (4307031, 3.501) (4308031, 3.505) (4309031, 3.509) (4310031, 3.513) (4311031, 3.517) (4312031, 3.522) (4313031, 3.526) (4314031, 3.53) (4315031, 3.534) (4316031, 3.538) (4317031, 3.542) (4318031, 3.546) (4319031, 3.551) (4320031, 3.555) (4321031, 3.559) (4322031, 3.563) (4323031, 3.567) (4324031, 3.572) (4325031, 3.576) (4326031, 3.58) (4327031, 3.585) (4328031, 3.589) (4329031, 3.594) (4330031, 3.598) (4331031, 3.602) (4332031, 3.606) (4333031, 3.611) (4334031, 3.615) (4335031, 3.62) (4336031, 3.624) (4337031, 3.629) (4338031, 3.633) (4339031, 3.638) (4340031, 3.642) (4341031, 3.647) (4342031, 3.651) (4343031, 3.656) (4344031, 3.66) (4345031, 3.665) (4346031, 3.669) (4347031, 3.673) (4348031, 3.678) (4349031, 3.682) (4350031, 3.687) (4351031, 3.691) (4352031, 3.696) (4353031, 3.7) (4354031, 3.705) (4355031, 3.709) (4356031, 3.714) (4357031, 3.719) (4358031, 3.723) (4359031, 3.728) (4360031, 3.732) (4361031, 3.737) (4362031, 3.741) (4363031, 3.746) (4364031, 3.751) (4365031, 3.755) (4366031, 3.76) (4367031, 3.765) (4368031, 3.77) (4369031, 3.774) (4370031, 3.779) (4371031, 3.783) (4372031, 3.788) (4373031, 3.793) (4374031, 3.797) (4375031, 3.802) (4376031, 3.807) (4377031, 3.812) (4378031, 3.817) (4379031, 3.821) (4380031, 3.826) (4381031, 3.831) (4382031, 3.835) (4383031, 3.84) (4384031, 3.845) (4385031, 3.85) (4386031, 3.854) (4387031, 3.859) (4388031, 3.864) (4389031, 3.869) (4390031, 3.874) (4391031, 3.879) (4392031, 3.884) (4393031, 3.889) (4394031, 3.894) (4395031, 3.899) (4396031, 3.904) (4397031, 3.909) (4398031, 3.914) (4399031, 3.919) (4400031, 3.923) (4401031, 3.929) (4402031, 3.934) (4403031, 3.939) (4404031, 3.944) (4405031, 3.949) (4406031, 3.954) (4407031, 3.96) (4408031, 3.965) (4409031, 3.97) (4410031, 3.975) (4411031, 3.98) (4412031, 3.985) (4413031, 3.99) (4414031, 3.996) (4415031, 4.001) (4416031, 4.005) (4417031, 4.011) (4418031, 4.016) (4419031, 4.021) (4420031, 4.027) (4421031, 4.032) (4422031, 4.038) (4423031, 4.043) (4424031, 4.048) (4425031, 4.054) (4426031, 4.059) (4427031, 4.065) (4428031, 4.07) (4429031, 4.075) (4430031, 4.081) (4431031, 4.087) (4432031, 4.092) (4433031, 4.098) (4434031, 4.104) (4435031, 4.109) (4436031, 4.114) (4437031, 4.119) (4438031, 4.125) (4439031, 4.13) (4440031, 4.136) (4441031, 4.141) (4442031, 4.147) (4443031, 4.152) (4444031, 4.158) (4445031, 4.163) (4446031, 4.168) (4447031, 4.174) (4448031, 4.18) (4449031, 4.186) (4450031, 4.191) (4451031, 4.197) (4452031, 4.203) (4453031, 4.208) (4454031, 4.214) (4455031, 4.219) (4456031, 4.225) (4457031, 4.231) (4458031, 4.236) (4459031, 4.242) (4460031, 4.247) (4461031, 4.253) (4462031, 4.259) (4463031, 4.265) (4464031, 4.271) (4465031, 4.276) (4466031, 4.282) (4467031, 4.288) (4468031, 4.294) (4469031, 4.3) (4470031, 4.306) (4471031, 4.312) (4472031, 4.318) (4473031, 4.324) (4474031, 4.33) (4475031, 4.336) (4476031, 4.342) (4477031, 4.348) (4478031, 4.354) (4479031, 4.359) (4480031, 4.366) (4481031, 4.372) (4482031, 4.377) (4483031, 4.384) (4484031, 4.39) (4485031, 4.396) (4486031, 4.402) (4487031, 4.408) (4488031, 4.414) (4489031, 4.421) (4490031, 4.427) (4491031, 4.434) (4492031, 4.44) (4493031, 4.446) (4494031, 4.452) (4495031, 4.458) (4496031, 4.465) (4497031, 4.471) (4498031, 4.477) (4499031, 4.483) (4500031, 4.49) (4501031, 4.496) (4502031, 4.502) (4503031, 4.508) (4504031, 4.514) (4505031, 4.521) (4506031, 4.527) (4507031, 4.534) (4508031, 4.54) (4509031, 4.546) (4510031, 4.553) (4511031, 4.56) (4512031, 4.566) (4513031, 4.573) (4514031, 4.579) (4515031, 4.585) (4516031, 4.591) (4517031, 4.598) (4518031, 4.605) (4519031, 4.611) (4520031, 4.618) (4521031, 4.624) (4522031, 4.631) (4523031, 4.637) (4524031, 4.644) (4525031, 4.651) (4526031, 4.658) (4527031, 4.665) (4528031, 4.672) (4529031, 4.679) (4530031, 4.686) (4531031, 4.693) (4532031, 4.7) (4533031, 4.707) (4534031, 4.714) (4535031, 4.721) (4536031, 4.728) (4537031, 4.735) (4538031, 4.742) (4539031, 4.75) (4540031, 4.756) (4541031, 4.763) (4542031, 4.77) (4543031, 4.777) (4544031, 4.785) (4545031, 4.792) (4546031, 4.799) (4547031, 4.806) (4548031, 4.813) (4549031, 4.82) (4550031, 4.827) (4551031, 4.835) (4552031, 4.842) (4553031, 4.849) (4554031, 4.856) (4555031, 4.864) (4556031, 4.871) (4557031, 4.879) (4558031, 4.886) (4559031, 4.894) (4560031, 4.902) (4561031, 4.909) (4562031, 4.917) (4563031, 4.924) (4564031, 4.932) (4565031, 4.939) (4566031, 4.947) (4567031, 4.955) (4568031, 4.962) (4569031, 4.97) (4570031, 4.977) (4571031, 4.985) (4572031, 4.993) (4573031, 5) (4574031, 5.007) (4575031, 5.015) (4576031, 5.023) (4577031, 5.031) (4578031, 5.038) (4579031, 5.047) (4580031, 5.054) (4581031, 5.062) (4582031, 5.07) (4583031, 5.079) (4584031, 5.087) (4585031, 5.095) (4586031, 5.103) (4587031, 5.11) (4588031, 5.119) (4589031, 5.127) (4590031, 5.135) (4591031, 5.143) (4592031, 5.151) (4593031, 5.159) (4594031, 5.167) (4595031, 5.175) (4596031, 5.183) (4597031, 5.192) (4598031, 5.2) (4599031, 5.208) (4600031, 5.217) (4601031, 5.225) (4602031, 5.233) (4603031, 5.242) (4604031, 5.25) (4605031, 5.259) (4606031, 5.267) (4607031, 5.275) (4608031, 5.284) (4609031, 5.293) (4610031, 5.302) (4611031, 5.311) (4612031, 5.319) (4613031, 5.328) (4614031, 5.336) (4615031, 5.345) (4616031, 5.353) (4617031, 5.362) (4618031, 5.372) (4619031, 5.38) (4620031, 5.389) (4621031, 5.398) (4622031, 5.407) (4623031, 5.416) (4624031, 5.425) (4625031, 5.434) (4626031, 5.444) (4627031, 5.452) (4628031, 5.461) (4629031, 5.47) (4630031, 5.48) (4631031, 5.489) (4632031, 5.498) (4633031, 5.507) (4634031, 5.516) (4635031, 5.526) (4636031, 5.535) (4637031, 5.545) (4638031, 5.555) (4639031, 5.564) (4640031, 5.574) (4641031, 5.583) (4642031, 5.593) (4643031, 5.602) (4644031, 5.612) (4645031, 5.622) (4646031, 5.631) (4647031, 5.641) (4648031, 5.651) (4649031, 5.66) (4650031, 5.669) (4651031, 5.68) (4652031, 5.689) (4653031, 5.699) (4654031, 5.709) (4655031, 5.719) (4656031, 5.729) (4657031, 5.739) (4658031, 5.749) (4659031, 5.76) (4660031, 5.77) (4661031, 5.78) (4662031, 5.79) (4663031, 5.8) (4664031, 5.811) (4665031, 5.821) (4666031, 5.831) (4667031, 5.841) (4668031, 5.851) (4669031, 5.862) (4670031, 5.872) (4671031, 5.882) (4672031, 5.892) (4673031, 5.903) (4674031, 5.914) (4675031, 5.925) (4676031, 5.934) (4677031, 5.945) (4678031, 5.956) (4679031, 5.967) (4680031, 5.978) (4681031, 5.989) (4682031, 6) (4683031, 6.011) (4684031, 6.022) (4685031, 6.033) (4686031, 6.043) (4687031, 6.054) (4688031, 6.065) (4689031, 6.076) (4690031, 6.088) (4691031, 6.099) (4692031, 6.109) (4693031, 6.12) (4694031, 6.132) (4695031, 6.144) (4696031, 6.155) (4697031, 6.167) (4698031, 6.179) (4699031, 6.191) (4700031, 6.202) (4701031, 6.214) (4702031, 6.225) (4703031, 6.237) (4704031, 6.248) (4705031, 6.26) (4706031, 6.271) (4707031, 6.283) (4708031, 6.296) (4709031, 6.308) (4710031, 6.319) (4711031, 6.331) (4712031, 6.343) (4713031, 6.355) (4714031, 6.367) (4715031, 6.38) (4716031, 6.392) (4717031, 6.404) (4718031, 6.417) (4719031, 6.43) (4720031, 6.442) (4721031, 6.454) (4722031, 6.467) (4723031, 6.48) (4724031, 6.492) (4725031, 6.504) (4726031, 6.516) (4727031, 6.529) (4728031, 6.542) (4729031, 6.555) (4730031, 6.567) (4731031, 6.58) (4732031, 6.594) (4733031, 6.607) (4734031, 6.62) (4735031, 6.633) (4736031, 6.646) (4737031, 6.659) (4738031, 6.672) (4739031, 6.686) (4740031, 6.7) (4741031, 6.713) (4742031, 6.726) (4743031, 6.74) (4744031, 6.754) (4745031, 6.767) (4746031, 6.781) (4747031, 6.794) (4748031, 6.808) (4749031, 6.822) (4750031, 6.836) (4751031, 6.849) (4752031, 6.864) (4753031, 6.878) (4754031, 6.891) (4755031, 6.906) (4756031, 6.92) (4757031, 6.935) (4758031, 6.949) (4759031, 6.963) (4760031, 6.977) (4761031, 6.991) (4762031, 7.006) (4763031, 7.02) (4764031, 7.034) (4765031, 7.048) (4766031, 7.062) (4767031, 7.077) (4768031, 7.092) (4769031, 7.108) (4770031, 7.122) (4771031, 7.137) (4772031, 7.152) (4773031, 7.167) (4774031, 7.182) (4775031, 7.196) (4776031, 7.211) (4777031, 7.226) (4778031, 7.241) (4779031, 7.257) (4780031, 7.273) (4781031, 7.288) (4782031, 7.304) (4783031, 7.319) (4784031, 7.335) (4785031, 7.351) (4786031, 7.367) (4787031, 7.383) (4788031, 7.399) (4789031, 7.415) (4790031, 7.431) (4791031, 7.447) (4792031, 7.464) (4793031, 7.48) (4794031, 7.496) (4795031, 7.512) (4796031, 7.529) (4797031, 7.545) (4798031, 7.561) (4799031, 7.578) (4800031, 7.595) (4801031, 7.611) (4802031, 7.628) (4803031, 7.644) (4804031, 7.661) (4805031, 7.678) (4806031, 7.695) (4807031, 7.712) (4808031, 7.729) (4809031, 7.746) (4810031, 7.764) (4811031, 7.781) (4812031, 7.798) (4813031, 7.816) (4814031, 7.834) (4815031, 7.853) (4816031, 7.87) (4817031, 7.888) (4818031, 7.906) (4819031, 7.924) (4820031, 7.942) (4821031, 7.96) (4822031, 7.977) (4823031, 7.997) (4824031, 8.015) (4825031, 8.034) (4826031, 8.052) (4827031, 8.071) (4828031, 8.09) (4829031, 8.11) (4830031, 8.129) (4831031, 8.148) (4832031, 8.168) (4833031, 8.188) (4834031, 8.208) (4835031, 8.226) (4836031, 8.246) (4837031, 8.267) (4838031, 8.286) (4839031, 8.306) (4840031, 8.327) (4841031, 8.347) (4842031, 8.367) (4843031, 8.388) (4844031, 8.409) (4845031, 8.43) (4846031, 8.452) (4847031, 8.471) (4848031, 8.492) (4849031, 8.514) (4850031, 8.535) (4851031, 8.555) (4852031, 8.576) (4853031, 8.599) (4854031, 8.62) (4855031, 8.642) (4856031, 8.664) (4857031, 8.687) (4858031, 8.709) (4859031, 8.729) (4860031, 8.751) (4861031, 8.773) (4862031, 8.794) (4863031, 8.817) (4864031, 8.838) (4865031, 8.861) (4866031, 8.883) (4867031, 8.906) (4868031, 8.929) (4869031, 8.951) (4870031, 8.976) (4871031, 9) (4872031, 9.023) (4873031, 9.047) (4874031, 9.07) (4875031, 9.093) (4876031, 9.119) (4877031, 9.142) (4878031, 9.167) (4879031, 9.191) (4880031, 9.215) (4881031, 9.238) (4882031, 9.264) (4883031, 9.289) (4884031, 9.314) (4885031, 9.339) (4886031, 9.364) (4887031, 9.39) (4888031, 9.414) (4889031, 9.44) (4890031, 9.468) (4891031, 9.493) (4892031, 9.52) (4893031, 9.544) (4894031, 9.571) (4895031, 9.599) (4896031, 9.626) (4897031, 9.653) (4898031, 9.681) (4899031, 9.709) (4900031, 9.736) (4901031, 9.764) (4902031, 9.792) (4903031, 9.819) (4904031, 9.847) (4905031, 9.875) (4906031, 9.904) (4907031, 9.934) (4908031, 9.962) (4909031, 9.993) (4910031, 10.022) (4911031, 10.052) (4912031, 10.081) (4913031, 10.11) (4914031, 10.139) (4915031, 10.17) (4916031, 10.199) (4917031, 10.23) (4918031, 10.26) (4919031, 10.289) (4920031, 10.32) (4921031, 10.35) (4922031, 10.381) (4923031, 10.412) (4924031, 10.443) (4925031, 10.474) (4926031, 10.505) (4927031, 10.536) (4928031, 10.567) (4929031, 10.599) (4930031, 10.631) (4931031, 10.664) (4932031, 10.698) (4933031, 10.732) (4934031, 10.764) (4935031, 10.798) (4936031, 10.831) (4937031, 10.864) (4938031, 10.899) (4939031, 10.931) (4940031, 10.966) (4941031, 11) (4942031, 11.037) (4943031, 11.074) (4944031, 11.108) (4945031, 11.144) (4946031, 11.18) (4947031, 11.217) (4948031, 11.252) (4949031, 11.29) (4950031, 11.328) (4951031, 11.365) (4952031, 11.4) (4953031, 11.44) (4954031, 11.478) (4955031, 11.515) (4956031, 11.555) (4957031, 11.594) (4958031, 11.633) (4959031, 11.672) (4960031, 11.71) (4961031, 11.752) (4962031, 11.792) (4963031, 11.834) (4964031, 11.875) (4965031, 11.915) (4966031, 11.954) (4967031, 11.994) (4968031, 12.035) (4969031, 12.079) (4970031, 12.121) (4971031, 12.162) (4972031, 12.207) (4973031, 12.25) (4974031, 12.29) (4975031, 12.334) (4976031, 12.377) (4977031, 12.42) (4978031, 12.463) (4979031, 12.51) (4980031, 12.555) (4981031, 12.601) (4982031, 12.647) (4983031, 12.693) (4984031, 12.738) (4985031, 12.784) (4986031, 12.831) (4987031, 12.88) (4988031, 12.928) (4989031, 12.976) (4990031, 13.027) (4991031, 13.075) (4992031, 13.124) (4993031, 13.173) (4994031, 13.223) (4995031, 13.273) (4996031, 13.324) (4997031, 13.374) (4998031, 13.428) (4999031, 13.478) (5000031, 13.528) (5001031, 13.578) (5002031, 13.629) (5003031, 13.684) (5004031, 13.736) (5005031, 13.794) (5006031, 13.845) (5007031, 13.901) (5008031, 13.952) (5009031, 14.007) (5010031, 14.063) (5011031, 14.118) (5012031, 14.172) (5013031, 14.228) (5014031, 14.281) (5015031, 14.338) (5016031, 14.394) (5017031, 14.453) (5018031, 14.511) (5019031, 14.573) (5020031, 14.631) (5021031, 14.687) (5022031, 14.744) (5023031, 14.804) (5024031, 14.86) (5025031, 14.922) (5026031, 14.984) (5027031, 15.045) (5028031, 15.109) (5029031, 15.172) (5030031, 15.235) (5031031, 15.3) (5032031, 15.361) (5033031, 15.426) (5034031, 15.489) (5035031, 15.555) (5036031, 15.619) (5037031, 15.685) (5038031, 15.752) (5039031, 15.817) (5040031, 15.884) (5041031, 15.95) (5042031, 16.019) (5043031, 16.087) (5044031, 16.157) (5045031, 16.225) (5046031, 16.295) (5047031, 16.364) (5048031, 16.435) (5049031, 16.506) (5050031, 16.58) (5051031, 16.647) (5052031, 16.717) (5053031, 16.787) (5054031, 16.861) (5055031, 16.934) (5056031, 17.005) (5057031, 17.08) (5058031, 17.156) (5059031, 17.231) (5060031, 17.303) (5061031, 17.377) (5062031, 17.454) (5063031, 17.533) (5064031, 17.612) (5065031, 17.686) (5066031, 17.761) (5067031, 17.842) (5068031, 17.916) (5069031, 17.996) (5070031, 18.073) (5071031, 18.155) (5072031, 18.241) (5073031, 18.324) (5074031, 18.406) (5075031, 18.492) (5076031, 18.576) (5077031, 18.657) (5078031, 18.739) (5079031, 18.824) (5080031, 18.914) (5081031, 19.004) (5082031, 19.095) (5083031, 19.188) (5084031, 19.278) (5085031, 19.368) (5086031, 19.458) (5087031, 19.551) (5088031, 19.641) (5089031, 19.744) (5090031, 19.837) (5091031, 19.938) (5092031, 20.039) (5093031, 20.142) (5094031, 20.245) (5095031, 20.348) (5096031, 20.451) (5097031, 20.56) (5098031, 20.668) (5099031, 20.786) (5100031, 20.901) (5101031, 21.018) (5102031, 21.129) (5103031, 21.243) (5104031, 21.359) (5105031, 21.48) (5106031, 21.598) (5107031, 21.716) (5108031, 21.84) (5109031, 21.973) (5110031, 22.1) (5111031, 22.233) (5112031, 22.363) (5113031, 22.503) (5114031, 22.633) (5115031, 22.772) (5116031, 22.914) (5117031, 23.049) (5118031, 23.194) (5119031, 23.336) (5120031, 23.485) (5121031, 23.629) (5122031, 23.784) (5123031, 23.933) (5124031, 24.102) (5125031, 24.26) (5126031, 24.42) (5127031, 24.581) (5128031, 24.756) (5129031, 24.919) (5130031, 25.096) (5131031, 25.269) (5132031, 25.446) (5133031, 25.638) (5134031, 25.827) (5135031, 26.032) (5136031, 26.228) (5137031, 26.424) (5138031, 26.614) (5139031, 26.813) (5140031, 27.025) (5141031, 27.251) (5142031, 27.456) (5143031, 27.695) (5144031, 27.951) (5145031, 28.175) (5146031, 28.407) (5147031, 28.643) (5148031, 28.876) (5149031, 29.121) (5150031, 29.377) (5151031, 29.635) (5152031, 29.91) (5153031, 30.206) (5154031, 30.499) (5155031, 30.799) (5156031, 31.095) (5157031, 31.412) (5158031, 31.708) (5159031, 32.05) (5160031, 32.372) (5161031, 32.737) (5162031, 33.106) (5163031, 33.471) (5164031, 33.847) (5165031, 34.253) (5166031, 34.677) (5167031, 35.098) (5168031, 35.538) (5169031, 35.993) (5170031, 36.47) (5171031, 36.929) (5172031, 37.418) (5173031, 37.94) (5174031, 38.478) (5175031, 39.05) (5176031, 39.602) (5177031, 40.205) (5178031, 40.801) (5179031, 41.441) (5180031, 42.068) (5181031, 42.779) (5182031, 43.499) (5183031, 44.225) (5184031, 44.963) (5185031, 45.74) (5186031, 46.559) (5187031, 47.415) (5188031, 48.307) (5189031, 49.256) (5190031, 50.246) (5191031, 51.325) (5192031, 52.45) (5193031, 53.576) (5194031, 54.838) (5195031, 56.212) (5196031, 57.615) (5197031, 59.074) (5198031, 60.679) (5199031, 62.401) (5200031, 64.34) (5201031, 66.469) (5202031, 68.87) (5203031, 71.381) (5204031, 74.123) (5205031, 77.21) (5206031, 80.489) (5207031, 84.187) (5208031, 88.323) (5209031, 92.905) (5210031, 97.906) (5211031, 104.381) (5212031, 112.196) (5213031, 124.086) (5214031, 140.812) (5215031, 168.852) (5216031, 236.829) (5217031, 2606.99);