(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION *)
(* *)
(* Lemma: OXLZLEZ *)
(* Chapter: Packing *)
(* Author: Thomas C. Hales *)
(* Date: 2010-02-09 *)
(* ========================================================================== *)
(* This file contains the inequalities for the hard case of the cluster inequality,
consisting of 4 blades, 3 quarters, and one half-weight. *)
type irecord = {
caseno : int;
coef1 : term * term * term * term;
coef2 : term*term*term*term;
coef3 : term*term*term*term;
coef4 : term*term*term*term;
branch1 : int list;
branch2 : int list;
branch3 : int list;
branch4 : int list;
branch5 : int list;
eps : float;
numerical1 : float list;
numerical2 : float list;
numerical3 : float list;
numerical4 : float list;
};;
module Ineqdata3q1h :
sig
val records : irecord list
val mk_ineq : int -> irecord -> term
val domain_cover_calculation: bool
val combine : (int list*int list*int list*int list*int list)*
(int list*int list*int list*int list*int list) ->
(bool*int)*(int list*int list*int list*int list*int list)
end
= struct
(*
FOUR BLADE INEQUALITIES
Each record corresponds to 5 different formal inequalities obtained by
mk_ineq i, for i=0,1,2,3,4.
Data nonlindata automatically generated by Mathematica sphereBook.nb,
*process* function .
There is a nonlinear optimization problem of 4blades, 3quarters,
1halfwt along a common spine. This is a 13-dimensional problem.
A Mathematica calculation has broken it into a collection of 6-dimensional
nonlinear optimizations. The data describing these 6-dimensional
problems appears below.
Each list entry corresponds to four nonlinear optimization problems
(for the four different simplices around the spine.
Each list entry has the following format.
[[caseno];lindata;b1;b2;b3;b4;b5;d1;d2;d3;d4]
caseno : 1, 2,3,4
This gives information about what the lengths of the spine and
edge#4 on the 1halfwt are:
case spine edge#4
1 2h0 to 2hplus 2hminus to 2h0
2 2h0 to 2hplus 2h0 to 2hplus
3 2hminus to 2h0 2hminus to 2h0
4 2hminus to 2h0 2h0 to 2hplus
****
lindata is a list of length 14.
[eps,a, b1,c1,d1, b2,c2,d2, b3,c3,d3, b4,c4,d4]
These are the inequalities:
gamma + a dih + bi y1 + ci (y2+y3+y5+y6) + di >= 0.
-eps gives the margin by which it holds.
The first group is for the 4-cell of wt 0.5. The indices 2,3,4 are for the quarters.
****
b1,b2,b3,b4,b5 branch data
each of these is a sequence of 0s and 1s.
b1 <-> domain of y1 (the spine)
b2 <-> domain of y4 (on the (halfwt)
b3 <-> domain of the y4 variable on quarter 2
b4 <-> domain of the y4 variable on quarter 3
b5 <-> domain of the y4 variable on quarter 4
each entry in bi cuts the domain in half, 0 takes the LHS, 1 takes
the RHS.
The first in the sequence is the first subdivision performed.
****
d1,d2,d3,d4 data on the numerical optimization of the 4 nonlinear
inequalities
di = [value;y1,y2,y3,y4,y5,y6] minimizer(numerical) and optimal point.
*)
(*
produced from /tmp/ineqdata3q1h.ml (from Mathematica) with the
following edits:
s/{/[ /g
s/}/ ]/g
s/,/ ;/g
s/. /.0 /g
The formal version has the additional edits
s/-/-- /g
\([0-9]\)-> #\1
s/ //g
*)
open Sphere;;
let do_betas x = all_forall (snd(dest_eq(concl(BETAS_CONV x))));;
let dest_decimal x = match strip_comb x with
| (dec,[a;b]) -> div_num (dest_numeral a) (dest_numeral b)
| _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'");;
let dest_signed_decimal x = match strip_comb x with
| (dec,[a;b]) -> dest_decimal x
| (neg,[a]) -> Num.minus_num(dest_decimal a)
| _ -> failwith ("dest_decimal: '" ^ string_of_term x ^ "'");;
let int_of_dec u =
Num.int_of_num (dest_signed_decimal u);;
let float_of_dec u = Num.float_of_num (dest_signed_decimal u);;
let mk_irecord oni =
let fd t = map float_of_dec t in
let i t = map int_of_dec t in
let g = function
[eps;a;b1;c1;d1;b2;c2;d2;b3;c3;d3;b4;c4;d4] ->
(float_of_dec eps,(a,b1,c1,d1),(a,b2,c2,d2),(a,b3,c3,d3),(a,b4,c4,d4))
| _ -> failwith "parse error g" in
let f = function
[[case];lindata;b1;b2;b3;b4;b5;d1;d2;d3;d4]
-> (int_of_dec case,g lindata,i b1,i b2, i b3,i b4,i b5,fd d1,fd d2,fd d3,fd d4)
| _ -> failwith "parse error f" in
let (i,(e,c1,c2,c3,c4),b1,b2,b3,b4,b5,n1,n2,n3,n4) = f oni in
{
caseno = i;
coef1 = c1;
coef2 = c2;
coef3 = c3;
coef4 = c4;
branch1 = b1;
branch2 = b2;
branch3 = b3;
branch4 = b4;
branch5 = b5;
eps = e;
numerical1 = n1;
numerical2 = n2;
numerical3 = n3;
numerical4 = n4;
};;
let y1domain d =
List.nth [`&2 * h0,&2 * hplus`;`&2 * h0,&2 * hplus`;
`&2 * hminus,&2 * h0`; `&2 * hminus,&2 * h0`] (d.caseno -1);;
let y4domain d =
List.nth [`&2 * hminus,&2 * h0`; `&2 * h0,&2 * hplus`;
`&2 * hminus,&2 * h0`; `&2 * h0,&2 * hplus` ] (d.caseno-1);;
(* in sphere.hl:
let pathL = new_definition `pathL (a,b) = (a,(a+b)/ &2)`;;
let pathR = new_definition `pathR (a,b) = ((a+b)/ &2,b)`;;
*)
let rec mkpath r = function
[] -> r
| x::xs -> let t = if (x=0) then `pathL` else `pathR` in
mkpath (mk_comb (t,r)) xs;;
let template = `\ y1d y2d y3d y4d y5d y6d
a b c d w m. ineq
[(FST y1d, y1, SND y1d);
(FST y2d ,y2, SND y2d);
(FST y3d,y3,SND y3d);
(FST y4d,y4,SND y4d);
(FST y5d,y5,SND y5d);
(FST y6d,y6,SND y6d)]
(gamma4fgcy y1 y2 y3 y4 y5 y6 lmfun / &w + &m *beta_bump_force_y y1 y2 y3 y4 y5 y6
+ a * dih_y y1 y2 y3 y4 y5 y6
+ b * y1
+ c * (y2 + y3 + y5 + y6)
+ d > &0)`;;
let mk_ineq1 i d = (* i=1,2,3,4, d reconstructs the formal statement of the ineq *)
let nth = List.nth in
let halfwt i = (i=1) in
let mk = mk_small_numeral in
let y1d = (y1domain d) in
let yd = `(&2, &2 * hminus)` in
let y4d = if halfwt i then (y4domain d) else yd in
let y j = nth [y1d;yd;yd;y4d;yd;yd] (j-1) in
let w = if halfwt i then 2 else 1 in
let m = w - 1 in
let (a,b,c,e) = nth [d.coef1;d.coef2;d.coef3;d.coef4] (i-1) in
let p1 = d.branch1 in
let p4 = nth [d.branch2;d.branch3;d.branch4;d.branch5] (i-1) in
let p j = nth [p1;[];[];p4;[];[]] (j-1) in
let x j = mkpath (y j) (p j) in
do_betas(list_mk_comb (template,
[x 1;x 2;x 3;x 4;x 5;x 6;a;b;c;e;mk w; mk m]));;
(* NB:
In each simplex ineq, there are four products ci * yj. When we sum,
we get 16 products, each (ci + ci') is paired with y(i,i') and z(i,i'),
where y is the edge at the origin and z is the edge on top.
We combine y(i,i')+z(i,i') into a single variable &2 *y...
*)
let templateB = `\ a b1 b2 b3 b4 c1 c2 c3 c4 d1 d2 d3 d4 y1d.
ineq
[(FST y1d, y1, SND y1d);
(&2 ,y12, &2 * hminus);
(&2,y23, &2 * hminus);
(&2,y34, &2 * hminus);
(&2,y41, &2 * hminus)]
(&2 * pi * a + (b1+b2+b3+b4)* y1
+ &2 * (c1+c2) * y12 + &2 *(c2 + c3) * y23 + &2 *(c3 + c4) * y34 + &2 *
(c4+c1)* y41
+ d1 + d2 + d3 + d4 < &0)`;;
let mk_ineq0 d = (* test constant compatibility for the 4 simplices around the spine *)
let (a,b1,c1,d1) = d.coef1 in
let (_,b2,c2,d2) = d.coef2 in
let (_,b3,c3,d3) = d.coef3 in
let (_,b4,c4,d4) = d.coef4 in
let y1d = mkpath (y1domain d) d.branch1 in
do_betas(list_mk_comb(templateB,
[a; b1; b2; b3; b4; c1; c2; c3; c4; d1; d2; d3; d4; y1d]));;
let mk_ineq case d =
let _ = (case >= 0) or failwith "mk_ineq domain error" in
let _ = (case <= 4) or failwith "mk_ineq domain error" in
if (case=0) then mk_ineq0 d else mk_ineq1 case d;;
(* formal version.
We take the floating point numbers to be exact rational numbers given by their
decimal expansions: *)
let raw_nonlindatah = [ [ [ `#4.0` ] ; [ `-- #0.00289` ; `#0.129913` ; `-- #0.060416` ; `#0.002372` ; `-- #0.113134` ; `#0.01764` ;
`-- #0.002372` ; `-- #0.198777` ; `#0.045166` ; `#0.002372` ; `-- #0.306092` ; `#0.021777` ; `-- #0.002372` ;
`-- #0.259166` ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.003326` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ;
`#2.0` ] ; [ `#0.00289` ; `#2.463514` ; `#2.0` ; `#2.463508` ; `#2.0` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.003534` ; `#2.463509` ; `#2.000001` ; `#2.463508` ; `#2.0` ; `#2.0` ; `#2.000001` ] ;
[ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#4.0` ] ; [ `-- #0.002889` ; `#0.129699` ; `-- #0.060316` ; `#0.002264` ; `-- #0.112116` ; `#0.019214` ;
`-- #0.002264` ; `-- #0.203309` ; `#0.021887` ; `#0.002264` ; `-- #0.29619` ; `#0.019214` ; `-- #0.002264` ;
`-- #0.203309` ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.003328` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ;
`#2.0` ] ; [ `#0.00289` ; `#2.463513` ; `#2.0` ; `#2.463508` ; `#2.0` ; `#2.000001` ; `#2.0` ] ;
[ `#0.002889` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.002998` ; `#2.519915` ; `#2.000025` ; `#2.000038` ; `#2.000022` ; `#2.463485` ; `#2.000022` ] ] ;
[ [ `#4.0` ] ; [ `-- #0.00289` ; `#0.129913` ; `-- #0.060416` ; `#0.002372` ; `-- #0.113134` ; `#0.021777` ;
`-- #0.002372` ; `-- #0.259166` ; `#0.045166` ; `#0.002372` ; `-- #0.306092` ; `#0.01764` ; `-- #0.002372` ;
`-- #0.198777` ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.003326` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.52` ;
`#2.0` ; `#2.0` ] ; [ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.003534` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463508` ; `#2.0` ] ;
[ `#0.002915` ; `#2.519935` ; `#2.000027` ; `#2.00004` ; `#2.000024` ; `#2.463484` ; `#2.000025` ] ] ;
[ [ `#4.0` ] ; [ `-- #0.000426` ; `-- #0.114872` ; `#0.133539` ; `-- #0.080919` ; `#0.532524` ; `#0.148605` ;
`#0.080919` ; `-- #0.855148` ; `#0.08743` ; `-- #0.080919` ; `#0.593722` ; `#0.148605` ; `#0.080919` ;
`-- #0.855148` ] ; [ ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.000426` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.6508` ;
`#2.0` ; `#2.0` ] ; [ `#0.000435` ; `#2.463511` ; `#2.000001` ; `#2.000001` ; `#2.000002` ; `#2.000002` ;
`#2.000002` ] ; [ `#0.004824` ; `#2.46351` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.000435` ; `#2.463511` ; `#2.000001` ; `#2.000001` ; `#2.000002` ; `#2.000002` ; `#2.000002` ] ] ;
[ [ `#3.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.008732` ; `-- #0.024884` ; `#0.097156` ; `#0.072591` ;
`#0.024884` ; `-- #0.464803` ; `#0.042651` ; `-- #0.024884` ; `#0.008797` ; `#0.055356` ; `#0.024884` ;
`-- #0.458108` ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.002594` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.491729` ; `#2.0` ;
`#2.0` ] ; [ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#3.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.029778` ; `-- #0.027449` ; `#0.170713` ; `#0.072591` ;
`#0.027449` ; `-- #0.485323` ; `#0.055356` ; `-- #0.027449` ; `-- #0.039438` ; `#0.072591` ; `#0.027449` ;
`-- #0.485323` ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.002594` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.491998` ; `#2.0` ;
`#2.0` ] ; [ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#3.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.008732` ; `#0.025458` ; `-- #0.30558` ; `#0.055356` ;
`-- #0.025458` ; `-- #0.055371` ; `#0.072591` ; `#0.025458` ; `-- #0.469389` ; `#0.037947` ; `-- #0.025458` ;
`#0.025236` ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.002612` ; `#2.463509` ; `#2.0` ; `#2.0` ;
`#2.489061` ; `#2.0` ; `#2.0` ] ; [ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.00272` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ] ; [ [ `#3.0` ] ; [ `-- #0.00225` ; `-- #0.114872` ; `#0.116669` ; `#0.080919` ;
`-- #0.7251449999999999` ; `#0.08743` ; `-- #0.080919` ; `#0.595546` ; `#0.148605` ; `#0.080919` ;
`-- #0.853324` ; `#0.08743` ; `-- #0.080919` ; `#0.595546` ] ; [ ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ;
[ `#0.00225` ; `#2.519989` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.006648` ; `#2.46351` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ; [ `#0.002259` ; `#2.463511` ; `#2.000001` ; `#2.000001` ; `#2.000002` ;
`#2.000002` ; `#2.000002` ] ; [ `#0.006648` ; `#2.46351` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.00289` ; `#0.129913` ; `-- #0.09152` ; `#0.002372` ; `-- #0.034749` ; `#0.347659` ;
`-- #0.002372` ; `-- #1.030425` ; `-- #0.105208` ; `#0.002372` ; `#0.072849` ; `-- #0.150931` ; `-- #0.002372` ;
`#0.176057` ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ;
[ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.005089` ; `#2.52` ; `#2.0` ; `#2.463509` ;
`#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.00289` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.00289` ; `#0.129913` ; `#0.340765` ; `#0.002372` ; `-- #1.124108` ; `-- #0.094917` ;
`-- #0.002372` ; `#0.084866` ; `-- #0.150931` ; `#0.002372` ; `#0.138108` ; `-- #0.094917` ; `-- #0.002372` ;
`#0.084866` ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ;
[ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.463509` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.00289` ; `#2.6508` ; `#2.0` ; `#2.0` ;
`#2.231754` ; `#2.0` ; `#2.0` ] ; [ `#0.00289` ; `#2.520001` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.00289` ; `#0.129913` ; `-- #0.09152` ; `#0.002372` ; `-- #0.034749` ; `#0.291645` ;
`-- #0.002372` ; `-- #0.939234` ; `-- #0.105208` ; `#0.002372` ; `#0.072849` ; `-- #0.094917` ; `-- #0.002372` ;
`#0.084866` ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ;
`#2.0` ] ; [ `#0.00289` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.005089` ; `#2.520002` ; `#2.000001` ; `#2.000001` ; `#2.000001` ; `#2.463507` ; `#2.000001` ] ;
[ `#0.00289` ; `#2.520001` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.005361` ; `#0.128506` ; `#0.290371` ; `#0.003287` ; `-- #1.026581` ; `-- #0.070878` ;
`-- #0.003287` ; `#0.033394` ; `-- #0.097658` ; `#0.003287` ; `#0.050047` ; `-- #0.121835` ; `-- #0.003287` ;
`#0.13571` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.005361` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.52` ;
`#2.0` ; `#2.0` ] ; [ `#0.005361` ; `#2.585401` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.008408` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.005361` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.115877` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.005361` ; `#0.128506` ; `#0.263591` ; `#0.003287` ; `-- #0.957343` ; `-- #0.070878` ;
`-- #0.003287` ; `#0.033394` ; `-- #0.121835` ; `#0.003287` ; `#0.083125` ; `-- #0.070878` ; `-- #0.003287` ;
`#0.033394` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.005361` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.005361` ; `#2.585401` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ; [ `#0.005361` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.115877` ; `#2.0` ; `#2.0` ] ;
[ `#0.005362` ; `#2.585403` ; `#2.0` ; `#2.000001` ; `#2.0` ; `#2.463508` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.005361` ; `#0.128506` ; `-- #0.066254` ; `#0.003287` ; `-- #0.104563` ; `#0.234791` ;
`-- #0.003287` ; `-- #0.786309` ; `-- #0.097658` ; `#0.003287` ; `#0.050047` ; `-- #0.070878` ; `-- #0.003287` ;
`#0.033394` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.005361` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.005361` ; `#2.5854` ; `#2.0` ; `#2.0` ;
`#2.115877` ; `#2.0` ; `#2.0` ] ; [ `#0.008409` ; `#2.585403` ; `#2.000001` ; `#2.000001` ; `#2.000001` ;
`#2.463508` ; `#2.000001` ] ; [ `#0.005362` ; `#2.585403` ; `#2.0` ; `#2.000001` ; `#2.0` ; `#2.463508` ;
`#2.0` ] ] ; [ [ `#2.0` ] ; [ `-- #0.001637` ; `#0.127166` ; `-- #0.07331` ; `#0.003788` ; `-- #0.105909` ; `#0.23984` ;
`-- #0.003788` ; `-- #0.767737` ; `-- #0.096981` ; `#0.003788` ; `#0.04248` ; `-- #0.069548` ; `-- #0.003788` ;
`#0.032155` ] ; [ `#1.0` ] ; [ `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.001637` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.5854` ; `#2.0` ; `#2.0` ] ; [ `#0.001637` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.005148` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001637` ; `#2.585403` ; `#2.0` ; `#2.000001` ; `#2.0` ; `#2.463508` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.00125` ; `#0.126777` ; `-- #0.053069` ; `#0.003525` ; `-- #0.142652` ; `#0.196466` ;
`-- #0.003525` ; `-- #0.667227` ; `-- #0.093532` ; `#0.003525` ; `#0.035622` ; `-- #0.049865` ; `-- #0.003525` ;
`-- #0.022307` ] ; [ `#1.0` ; `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.00125` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001388` ; `#2.6181` ; `#2.000001` ; `#2.000001` ; `#2.0` ; `#2.463508` ; `#2.0` ] ;
[ `#0.004482` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001388` ; `#2.618101` ; `#2.000001` ; `#2.000002` ; `#2.0` ; `#2.463508` ; `#2.000001` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `#0.060747` ; `-- #0.530637` ; `-- #0.014413` ;
`-- #0.060747` ; `#0.594377` ; `-- #0.014413` ; `#0.060747` ; `-- #0.377571` ; `-- #0.02241` ; `-- #0.060747` ;
`#0.608509` ] ; [ `#1.0` ; `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ;
[ `#0.001974` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.520037` ; `#2.0` ; `#2.0` ] ;
[ `#0.005733` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001976` ; `#2.618027` ; `#2.000001` ; `#2.000001` ; `#2.000002` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `#0.060747` ; `-- #0.530636` ; `-- #0.014413` ;
`-- #0.060747` ; `#0.594377` ; `-- #0.02241` ; `#0.060747` ; `-- #0.36344` ; `-- #0.014413` ; `-- #0.060747` ;
`#0.594377` ] ; [ `#1.0` ; `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.001974` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.520037` ; `#2.0` ; `#2.0` ] ;
[ `#0.005733` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001975` ; `#2.585404` ; `#2.000001` ; `#2.000001` ; `#2.05794` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `#0.060747` ; `-- #0.530637` ; `-- #0.02241` ;
`-- #0.060747` ; `#0.608509` ; `-- #0.014413` ; `#0.060747` ; `-- #0.377571` ; `-- #0.014413` ; `-- #0.060747` ;
`#0.594377` ] ; [ `#1.0` ; `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.001974` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.520037` ; `#2.0` ; `#2.0` ] ;
[ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.0` ; `#2.0` ] ;
[ `#0.001975` ; `#2.585402` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ] ; [ [ `#2.0` ] ; [ `-- #0.00033` ; `-- #0.036939` ; `#0.050064` ; `-- #0.057593` ; `#0.397884` ;
`-- #0.016688` ; `#0.057593` ; `-- #0.362427` ; `-- #0.016688` ; `-- #0.057593` ; `#0.559062` ; `-- #0.016688` ;
`-- #0.057593` ; `#0.559062` ] ; [ `#1.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.00033` ; `#2.618094` ; `#2.000003` ; `#2.000003` ; `#2.520014` ; `#2.000003` ;
`#2.000003` ] ; [ `#0.00033` ; `#2.601753` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.00033` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.00033` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ] ] ; [ [ `#2.0` ] ; [ `-- #0.000417` ; `-- #0.049823` ; `#0.047052` ; `-- #0.061687` ; `#0.463622` ;
`-- #0.015684` ; `#0.061687` ; `-- #0.379191` ; `-- #0.015684` ; `-- #0.061687` ; `#0.607807` ; `-- #0.015684` ;
`#0.061687` ; `-- #0.379191` ] ; [ `#1.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.000417` ; `#2.60175` ; `#2.0` ; `#2.0` ; `#2.5527` ; `#2.0` ; `#2.0` ] ;
[ `#0.000418` ; `#2.601748` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.000417` ; `#2.60175` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.000418` ; `#2.601748` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000396` ; `-- #0.053582` ; `#0.049452` ; `-- #0.06302` ; `#0.475514` ; `-- #0.013853` ;
`#0.06302` ; `-- #0.389234` ; `-- #0.020791` ; `-- #0.06302` ; `#0.637132` ; `-- #0.013853` ; `-- #0.062897` ;
`#0.618101` ] ; [ `#1.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.000359` ; `#2.601749` ; `#2.0` ; `#2.0` ; `#2.536279` ; `#2.0` ; `#2.0` ] ;
[ `#0.000396` ; `#2.601748` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.000396` ; `#2.60175` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.000396` ; `#2.60175` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.002012` ; `-- #0.066935` ; `#0.079693` ; `#0.066241` ; `-- #0.605497` ; `-- #0.021495` ;
`-- #0.066241` ; `#0.685308` ; `-- #0.021495` ; `#0.066241` ; `-- #0.374549` ; `-- #0.036704` ; `-- #0.066241` ;
`#0.715304` ] ; [ `#0.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.00141` ; `#2.52` ; `#2.0` ; `#2.0` ;
`#2.584895` ; `#2.0` ; `#2.0` ] ; [ `#0.004908` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.002012` ; `#2.585399` ; `#2.000001` ; `#2.000001` ; `#2.000001` ; `#2.000001` ; `#2.0` ] ;
[ `#0.002012` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.115877` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.002012` ; `-- #0.066935` ; `#0.028887` ; `#0.066241` ; `-- #0.477466` ; `-- #0.021495` ;
`-- #0.066241` ; `#0.685308` ; `#0.014102` ; `#0.066241` ; `-- #0.472584` ; `-- #0.021495` ; `-- #0.066241` ;
`#0.685308` ] ; [ `#0.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.001651` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.596115` ; `#2.0` ; `#2.0` ] ;
[ `#0.004908` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ; [ `#0.002012` ; `#2.52` ; `#2.0` ; `#2.0` ;
`#2.115878` ; `#2.0` ; `#2.0` ] ; [ `#0.004908` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.002012` ; `-- #0.066935` ; `#0.028887` ; `-- #0.066241` ; `#0.582391` ; `#0.014102` ;
`#0.066241` ; `-- #0.472584` ; `-- #0.021495` ; `-- #0.066241` ; `#0.685308` ; `-- #0.021495` ; `#0.066241` ;
`-- #0.374549` ] ; [ `#0.0` ] ; [ ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.00141` ; `#2.520001` ; `#2.000001` ; `#2.000001` ; `#2.58489` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.002012` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.115878` ; `#2.0` ; `#2.0` ] ; [ `#0.004908` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ; [ `#0.002012` ; `#2.520001` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000405` ; `-- #0.070081` ; `#0.043025` ; `#0.06775` ; `-- #0.520998` ; `-- #0.014342` ;
`-- #0.06775` ; `#0.681778` ; `-- #0.014342` ; `#0.06775` ; `-- #0.402228` ; `-- #0.014342` ; `-- #0.06775` ;
`#0.681778` ] ; [ `#0.0` ; `#1.0` ] ; [ `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.000317` ; `#2.585399` ; `#2.0` ; `#2.0` ; `#2.612413` ; `#2.0` ; `#2.0` ] ;
[ `#0.004048` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.000405` ; `#2.585391` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.004048` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ] ; [ [ `#2.0` ] ; [ `-- #0.001161` ; `-- #0.074623` ; `#0.079355` ; `#0.068595` ;
`-- #0.608613` ; `-- #0.023711` ; `-- #0.068595` ; `#0.719631` ; `-- #0.023711` ; `#0.068595` ; `-- #0.37789` ;
`-- #0.031932` ; `-- #0.068595` ; `#0.735738` ] ; [ `#0.0` ; `#0.0` ] ; [ `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.001019` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.61793` ; `#2.0` ; `#2.0` ] ;
[ `#0.004236` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ; [ `#0.001162` ; `#2.520001` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.001161` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.001161` ; `-- #0.074623` ; `#0.019702` ; `-- #0.081204` ; `#0.740105` ; `-- #0.023711` ;
`#0.081204` ; `-- #0.47876` ; `-- #0.031932` ; `-- #0.081204` ; `#0.836608` ; `#0.035942` ; `#0.081204` ;
`-- #0.629086` ] ; [ `#0.0` ; `#0.0` ] ; [ `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.001084` ; `#2.552699` ; `#2.000001` ; `#2.000001` ; `#2.625659` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.001161` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.002657` ; `#2.52` ; `#2.0` ; `#2.463509` ;
`#2.057939` ; `#2.0` ; `#2.0` ] ; [ `#0.001162` ; `#2.52` ; `#2.000001` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.001161` ; `-- #0.074623` ; `#0.019702` ; `-- #0.068595` ; `#0.639237` ; `-- #0.031932` ;
`#0.068595` ; `-- #0.361784` ; `-- #0.023711` ; `-- #0.068595` ; `#0.719631` ; `#0.035942` ; `#0.068595` ;
`-- #0.528217` ] ; [ `#0.0` ; `#0.0` ] ; [ `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.001084` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.625659` ; `#2.0` ; `#2.0` ] ;
[ `#0.001161` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.0` ; `#2.0` ] ; [ `#0.004236` ; `#2.52` ; `#2.0` ; `#2.463509` ;
`#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.001161` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000308` ; `-- #0.090009` ; `#0.04151` ; `#0.073665` ; `-- #0.523458` ; `-- #0.013837` ;
`-- #0.073665` ; `#0.755879` ; `-- #0.013837` ; `#0.073665` ; `-- #0.422755` ; `-- #0.013837` ; `-- #0.073665` ;
`#0.755879` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#1.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.000308` ; `#2.53635` ; `#2.0` ; `#2.0` ; `#2.650799` ; `#2.0` ; `#2.0` ] ;
[ `#0.000308` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.000308` ; `#2.536357` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.000308` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000418` ; `-- #0.17025` ; `#0.094709` ; `#0.098535` ; `-- #0.692034` ; `-- #0.021455` ;
`-- #0.098535` ; `#1.087114` ; `#0.009749` ; `#0.098535` ; `-- #0.568591` ; `-- #0.021455` ; `-- #0.098535` ;
`#1.087114` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#1.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.000418` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.6508` ; `#2.0` ; `#2.0` ] ;
[ `#0.000418` ; `#2.53635` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.000418` ; `#2.536343` ; `#2.0` ; `#2.0` ;
`#2.000004` ; `#2.0` ; `#2.0` ] ; [ `#0.000418` ; `#2.53635` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000644` ; `-- #0.172166` ; `#0.09973` ; `-- #0.099785` ; `#0.882284` ; `#0.014169` ;
`#0.099785` ; `-- #0.586728` ; `-- #0.017353` ; `-- #0.099785` ; `#1.0903` ; `#0.014169` ; `#0.099785` ;
`-- #0.586728` ] ; [ `#0.0` ; `#0.0` ] ; [ `#1.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.000644` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.6181` ; `#2.0` ; `#2.0` ] ; [ `#0.000644` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.000644` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.000644` ; `#2.5527` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#2.0` ] ; [ `-- #0.000313` ; `-- #0.084789` ; `#0.039845` ; `-- #0.071708` ; `#0.632521` ; `-- #0.013282` ;
`-- #0.071708` ; `#0.731624` ; `-- #0.013282` ; `-- #0.071708` ; `#0.731624` ; `-- #0.013282` ; `#0.071708` ;
`-- #0.415701` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.000313` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.5854` ; `#2.0` ; `#2.0` ] ; [ `#0.003624` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ; [ `#0.003624` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.000314` ; `#2.520002` ; `#2.000002` ; `#2.000001` ; `#2.000001` ; `#2.000001` ; `#2.000001` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.052337` ; `-- #0.02292` ; `#0.191326` ; `#0.23854` ; `#0.02292` ;
`-- #0.867278` ; `-- #0.073933` ; `-- #0.02292` ; `#0.286871` ; `-- #0.11227` ; `#0.02292` ; `-- #0.019974` ] ;
[ ] ; [ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.002703` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.474335` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.004959` ; `#2.6508` ; `#2.0` ; `#2.463509` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.002721` ; `#2.650799` ; `#2.0` ; `#2.0` ; `#2.231755` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.052337` ; `#0.02292` ; `-- #0.17539` ; `#0.23854` ; `-- #0.02292` ;
`-- #0.500562` ; `-- #0.11227` ; `#0.02292` ; `-- #0.019974` ; `-- #0.073933` ; `-- #0.02292` ; `#0.286871` ] ;
[ ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.002703` ; `#2.650799` ; `#2.0` ; `#2.000001` ; `#2.474442` ;
`#2.000001` ; `#2.0` ] ; [ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.002721` ; `#2.650799` ; `#2.0` ; `#2.0` ; `#2.231755` ; `#2.0` ; `#2.0` ] ;
[ `#0.003897` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.00272` ; `#0.065103` ; `-- #0.052337` ; `#0.02292` ; `-- #0.175391` ; `-- #0.11227` ;
`-- #0.02292` ; `#0.346743` ; `#0.23854` ; `#0.02292` ; `-- #0.867278` ; `-- #0.073933` ; `-- #0.02292` ;
`#0.286871` ] ; [ ] ; [ ] ; [ `#1.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.002703` ; `#2.650799` ; `#2.0` ; `#2.000001` ;
`#2.474442` ; `#2.000001` ; `#2.0` ] ; [ `#0.00272` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.231754` ; `#2.0` ; `#2.0` ] ;
[ `#0.00272` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.003897` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ;
`#2.0` ] ] ; [ [ `#1.0` ] ; [ `-- #0.004545` ; `#0.062681` ; `-- #0.026929` ; `#0.023742` ; `-- #0.242815` ;
`-- #0.06441` ; `-- #0.023742` ; `#0.273568` ; `#0.176245` ; `#0.023742` ; `-- #0.72849` ; `-- #0.084906` ;
`-- #0.023742` ; `#0.3039` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ;
[ `#0.004424` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.491903` ; `#2.0` ; `#2.0` ] ;
[ `#0.006469` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.004545` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.004545` ; `#2.6508` ; `#2.0` ; `#2.0` ;
`#2.115877` ; `#2.0` ; `#2.0` ] ] ; [ [ `#1.0` ] ; [ `-- #0.004545` ; `#0.062681` ; `-- #0.026929` ; `#0.023742` ;
`-- #0.242815` ; `#0.176245` ; `-- #0.023742` ; `-- #0.348621` ; `-- #0.084906` ; `#0.023742` ; `-- #0.075969` ;
`-- #0.06441` ; `-- #0.023742` ; `#0.273568` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.004424` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.491903` ; `#2.0` ; `#2.0` ] ;
[ `#0.004545` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.004545` ; `#2.6508` ; `#2.0` ; `#2.0` ;
`#2.115877` ; `#2.0` ; `#2.0` ] ; [ `#0.006469` ; `#2.585401` ; `#2.0` ; `#2.000001` ; `#2.0` ; `#2.463508` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.004545` ; `#0.062681` ; `-- #0.026929` ; `#0.023742` ; `-- #0.242815` ; `-- #0.084906` ;
`-- #0.023742` ; `#0.3039` ; `#0.176245` ; `#0.023742` ; `-- #0.72849` ; `-- #0.06441` ; `-- #0.023742` ;
`#0.273568` ] ; [ `#1.0` ] ; [ ] ; [ `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.004424` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.491903` ; `#2.0` ; `#2.0` ] ;
[ `#0.004545` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.115877` ; `#2.0` ; `#2.0` ] ;
[ `#0.004545` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.006469` ; `#2.585401` ; `#2.0` ; `#2.000001` ;
`#2.0` ; `#2.463508` ; `#2.0` ] ] ; [ [ `#1.0` ] ; [ `-- #0.000884` ; `#0.061714` ; `-- #0.014502` ; `-- #0.02407` ;
`#0.104941` ; `#0.134266` ; `#0.02407` ; `-- #0.631477` ; `-- #0.059882` ; `-- #0.02407` ; `#0.261947` ;
`-- #0.059882` ; `-- #0.02407` ; `#0.261947` ] ; [ `#1.0` ; `#1.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ] ; [ `#0.000796` ; `#2.6508` ; `#2.0` ; `#2.0` ; `#2.488246` ; `#2.0` ; `#2.0` ] ;
[ `#0.000884` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.003066` ; `#2.618101` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.463509` ; `#2.0` ] ; [ `#0.003066` ; `#2.618101` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `#0.060747` ; `-- #0.530637` ; `-- #0.014413` ;
`-- #0.060747` ; `#0.594377` ; `-- #0.014413` ; `#0.060747` ; `-- #0.377571` ; `-- #0.02241` ; `-- #0.060747` ;
`#0.608509` ] ; [ `#1.0` ; `#0.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ;
[ `#0.002084` ; `#2.585663` ; `#2.000116` ; `#2.000116` ; `#2.519822` ; `#2.000113` ; `#2.000116` ] ;
[ `#0.005733` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001976` ; `#2.618027` ; `#2.000001` ; `#2.000001` ; `#2.000002` ; `#2.000001` ; `#2.000001` ] ;
[ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `-- #0.073427` ; `#0.542756` ; `-- #0.014413` ;
`#0.073427` ; `-- #0.479016` ; `-- #0.02241` ; `-- #0.073427` ; `#0.709954` ; `-- #0.014413` ; `#0.073427` ;
`-- #0.479016` ] ; [ `#1.0` ; `#0.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.001974` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ; `#2.0` ] ; [ `#0.004138` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.057939` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001974` ; `#2.585401` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.001974` ; `-- #0.0469` ; `#0.051237` ; `-- #0.060747` ; `#0.44131200000000004` ;
`-- #0.02241` ; `#0.060747` ; `-- #0.36344` ; `-- #0.014413` ; `-- #0.060747` ; `#0.594377` ; `-- #0.014413` ;
`#0.060747` ; `-- #0.377571` ] ; [ `#1.0` ; `#0.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ; `#1.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.002165` ; `#2.585453` ; `#2.000636` ; `#2.000639` ; `#2.51972` ; `#2.000635` ;
`#2.000606` ] ; [ `#0.001975` ; `#2.585404` ; `#2.000001` ; `#2.000001` ; `#2.05794` ; `#2.000001` ;
`#2.000001` ] ; [ `#0.001974` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ;
[ `#0.001975` ; `#2.585402` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.00033` ; `-- #0.036939` ; `#0.050064` ; `#0.057593` ; `-- #0.523604` ; `-- #0.016688` ;
`-- #0.057593` ; `#0.559062` ; `-- #0.016688` ; `#0.057593` ; `-- #0.362427` ; `-- #0.016688` ; `-- #0.057593` ;
`#0.559062` ] ; [ `#1.0` ; `#0.0` ; `#1.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.000403` ; `#2.609586` ; `#2.000023` ; `#2.00002` ; `#2.519733` ; `#2.000019` ; `#2.000024` ] ;
[ `#0.00033` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ; [ `#0.00033` ; `#2.601753` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ] ; [ `#0.00033` ; `#2.6181` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ;
[ [ `#1.0` ] ; [ `-- #0.000886` ; `-- #0.177145` ; `#0.151334` ; `-- #0.103308` ; `#0.774954` ; `#0.041584` ;
`#0.103308` ; `-- #0.677721` ; `#0.00995` ; `-- #0.103308` ; `#1.057518` ; `#0.041584` ; `#0.103308` ;
`-- #0.677721` ] ; [ `#1.0` ; `#0.0` ; `#0.0` ] ; [ ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ; [ `#0.0` ; `#0.0` ; `#0.0` ] ;
[ `#0.000886` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.000887` ; `#2.601712` ; `#2.000001` ;
`#2.000001` ; `#2.000015` ; `#2.000001` ; `#2.000001` ] ; [ `#0.000886` ; `#2.601749` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.000001` ; `#2.0` ] ; [ `#0.000887` ; `#2.601712` ; `#2.000001` ; `#2.000001` ; `#2.000015` ;
`#2.000001` ; `#2.000001` ] ] ; [ [ `#1.0` ] ; [ `-- #0.001328` ; `-- #0.121189` ; `#0.06473` ; `-- #0.084657` ;
`#0.741383` ; `-- #0.016252` ; `#0.084657` ; `-- #0.45858` ; `-- #0.022099` ; `-- #0.084657` ; `#0.911046` ;
`-- #0.016252` ; `#0.084657` ; `-- #0.45858` ] ; [ `#0.0` ] ; [ ] ; [ `#0.0` ] ; [ `#0.0` ] ; [ `#0.0` ] ;
[ `#0.001328` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.52` ; `#2.0` ; `#2.0` ] ; [ `#0.001328` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ;
`#2.0` ] ; [ `#0.006318` ; `#2.52` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.463509` ; `#2.0` ] ;
[ `#0.001328` ; `#2.5854` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ; `#2.0` ] ] ];;
let records = map mk_irecord raw_nonlindatah;;
(*
let nonlindata = [ [ [ 4.0 ] ; [ -0.00289 ; 0.129913 ; -0.060416 ; 0.002372 ; -0.113134 ; 0.01764 ;
-0.002372 ; -0.198777 ; 0.045166 ; 0.002372 ; -0.306092 ; 0.021777 ; -0.002372 ;
-0.259166 ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.003326 ; 2.463509 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ;
2.0 ] ; [ 0.00289 ; 2.463514 ; 2.0 ; 2.463508 ; 2.0 ; 2.000001 ; 2.000001 ] ;
[ 0.003534 ; 2.463509 ; 2.000001 ; 2.463508 ; 2.0 ; 2.0 ; 2.000001 ] ;
[ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ] ;
[ [ 4.0 ] ; [ -0.002889 ; 0.129699 ; -0.060316 ; 0.002264 ; -0.112116 ; 0.019214 ;
-0.002264 ; -0.203309 ; 0.021887 ; 0.002264 ; -0.29619 ; 0.019214 ; -0.002264 ;
-0.203309 ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.003328 ; 2.463509 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ;
2.0 ] ; [ 0.00289 ; 2.463513 ; 2.0 ; 2.463508 ; 2.0 ; 2.000001 ; 2.0 ] ;
[ 0.002889 ; 2.463509 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.002998 ; 2.519915 ; 2.000025 ; 2.000038 ; 2.000022 ; 2.463485 ; 2.000022 ] ] ;
[ [ 4.0 ] ; [ -0.00289 ; 0.129913 ; -0.060416 ; 0.002372 ; -0.113134 ; 0.021777 ;
-0.002372 ; -0.259166 ; 0.045166 ; 0.002372 ; -0.306092 ; 0.01764 ; -0.002372 ;
-0.198777 ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.003326 ; 2.463509 ; 2.0 ; 2.0 ; 2.52 ;
2.0 ; 2.0 ] ; [ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.003534 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ; 2.463508 ; 2.0 ] ;
[ 0.002915 ; 2.519935 ; 2.000027 ; 2.00004 ; 2.000024 ; 2.463484 ; 2.000025 ] ] ;
[ [ 4.0 ] ; [ -0.000426 ; -0.114872 ; 0.133539 ; -0.080919 ; 0.532524 ; 0.148605 ;
0.080919 ; -0.855148 ; 0.08743 ; -0.080919 ; 0.593722 ; 0.148605 ; 0.080919 ;
-0.855148 ] ; [ ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.000426 ; 2.463509 ; 2.0 ; 2.0 ; 2.6508 ;
2.0 ; 2.0 ] ; [ 0.000435 ; 2.463511 ; 2.000001 ; 2.000001 ; 2.000002 ; 2.000002 ;
2.000002 ] ; [ 0.004824 ; 2.46351 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.000435 ; 2.463511 ; 2.000001 ; 2.000001 ; 2.000002 ; 2.000002 ; 2.000002 ] ] ;
[ [ 3.0 ] ; [ -0.00272 ; 0.065103 ; -0.008732 ; -0.024884 ; 0.097156 ; 0.072591 ;
0.024884 ; -0.464803 ; 0.042651 ; -0.024884 ; 0.008797 ; 0.055356 ; 0.024884 ;
-0.458108 ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.002594 ; 2.52 ; 2.0 ; 2.0 ; 2.491729 ; 2.0 ;
2.0 ] ; [ 0.00272 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.463509 ; 2.0 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ] ;
[ [ 3.0 ] ; [ -0.00272 ; 0.065103 ; -0.029778 ; -0.027449 ; 0.170713 ; 0.072591 ;
0.027449 ; -0.485323 ; 0.055356 ; -0.027449 ; -0.039438 ; 0.072591 ; 0.027449 ;
-0.485323 ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.002594 ; 2.52 ; 2.0 ; 2.0 ; 2.491998 ; 2.0 ;
2.0 ] ; [ 0.00272 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.463509 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 3.0 ] ; [ -0.00272 ; 0.065103 ; -0.008732 ; 0.025458 ; -0.30558 ; 0.055356 ;
-0.025458 ; -0.055371 ; 0.072591 ; 0.025458 ; -0.469389 ; 0.037947 ; -0.025458 ;
0.025236 ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.002612 ; 2.463509 ; 2.0 ; 2.0 ;
2.489061 ; 2.0 ; 2.0 ] ; [ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.00272 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ] ; [ [ 3.0 ] ; [ -0.00225 ; -0.114872 ; 0.116669 ; 0.080919 ;
-0.7251449999999999 ; 0.08743 ; -0.080919 ; 0.595546 ; 0.148605 ; 0.080919 ;
-0.853324 ; 0.08743 ; -0.080919 ; 0.595546 ] ; [ ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ] ;
[ 0.00225 ; 2.519989 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.006648 ; 2.46351 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ; [ 0.002259 ; 2.463511 ; 2.000001 ; 2.000001 ; 2.000002 ;
2.000002 ; 2.000002 ] ; [ 0.006648 ; 2.46351 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.00289 ; 0.129913 ; -0.09152 ; 0.002372 ; -0.034749 ; 0.347659 ;
-0.002372 ; -1.030425 ; -0.105208 ; 0.002372 ; 0.072849 ; -0.150931 ; -0.002372 ;
0.176057 ] ; [ ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ;
[ 0.00289 ; 2.52 ; 2.0 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.005089 ; 2.52 ; 2.0 ; 2.463509 ;
2.0 ; 2.0 ; 2.0 ] ; [ 0.00289 ; 2.6508 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.00289 ; 0.129913 ; 0.340765 ; 0.002372 ; -1.124108 ; -0.094917 ;
-0.002372 ; 0.084866 ; -0.150931 ; 0.002372 ; 0.138108 ; -0.094917 ; -0.002372 ;
0.084866 ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ;
[ 0.00289 ; 2.52 ; 2.0 ; 2.463509 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.00289 ; 2.6508 ; 2.0 ; 2.0 ;
2.231754 ; 2.0 ; 2.0 ] ; [ 0.00289 ; 2.520001 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.00289 ; 0.129913 ; -0.09152 ; 0.002372 ; -0.034749 ; 0.291645 ;
-0.002372 ; -0.939234 ; -0.105208 ; 0.002372 ; 0.072849 ; -0.094917 ; -0.002372 ;
0.084866 ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ;
2.0 ] ; [ 0.00289 ; 2.52 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.005089 ; 2.520002 ; 2.000001 ; 2.000001 ; 2.000001 ; 2.463507 ; 2.000001 ] ;
[ 0.00289 ; 2.520001 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.005361 ; 0.128506 ; 0.290371 ; 0.003287 ; -1.026581 ; -0.070878 ;
-0.003287 ; 0.033394 ; -0.097658 ; 0.003287 ; 0.050047 ; -0.121835 ; -0.003287 ;
0.13571 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.005361 ; 2.5854 ; 2.0 ; 2.0 ; 2.52 ;
2.0 ; 2.0 ] ; [ 0.005361 ; 2.585401 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.008408 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.005361 ; 2.6508 ; 2.0 ; 2.0 ; 2.115877 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.005361 ; 0.128506 ; 0.263591 ; 0.003287 ; -0.957343 ; -0.070878 ;
-0.003287 ; 0.033394 ; -0.121835 ; 0.003287 ; 0.083125 ; -0.070878 ; -0.003287 ;
0.033394 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.005361 ; 2.5854 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.005361 ; 2.585401 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ; [ 0.005361 ; 2.6508 ; 2.0 ; 2.0 ; 2.115877 ; 2.0 ; 2.0 ] ;
[ 0.005362 ; 2.585403 ; 2.0 ; 2.000001 ; 2.0 ; 2.463508 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.005361 ; 0.128506 ; -0.066254 ; 0.003287 ; -0.104563 ; 0.234791 ;
-0.003287 ; -0.786309 ; -0.097658 ; 0.003287 ; 0.050047 ; -0.070878 ; -0.003287 ;
0.033394 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.005361 ; 2.5854 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.005361 ; 2.5854 ; 2.0 ; 2.0 ;
2.115877 ; 2.0 ; 2.0 ] ; [ 0.008409 ; 2.585403 ; 2.000001 ; 2.000001 ; 2.000001 ;
2.463508 ; 2.000001 ] ; [ 0.005362 ; 2.585403 ; 2.0 ; 2.000001 ; 2.0 ; 2.463508 ;
2.0 ] ] ; [ [ 2.0 ] ; [ -0.001637 ; 0.127166 ; -0.07331 ; 0.003788 ; -0.105909 ; 0.23984 ;
-0.003788 ; -0.767737 ; -0.096981 ; 0.003788 ; 0.04248 ; -0.069548 ; -0.003788 ;
0.032155 ] ; [ 1.0 ] ; [ 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.001637 ; 2.5854 ; 2.0 ; 2.0 ; 2.5854 ; 2.0 ; 2.0 ] ; [ 0.001637 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.005148 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001637 ; 2.585403 ; 2.0 ; 2.000001 ; 2.0 ; 2.463508 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.00125 ; 0.126777 ; -0.053069 ; 0.003525 ; -0.142652 ; 0.196466 ;
-0.003525 ; -0.667227 ; -0.093532 ; 0.003525 ; 0.035622 ; -0.049865 ; -0.003525 ;
-0.022307 ] ; [ 1.0 ; 1.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.00125 ; 2.6181 ; 2.0 ; 2.0 ; 2.52 ; 2.463509 ; 2.0 ] ;
[ 0.001388 ; 2.6181 ; 2.000001 ; 2.000001 ; 2.0 ; 2.463508 ; 2.0 ] ;
[ 0.004482 ; 2.6508 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001388 ; 2.618101 ; 2.000001 ; 2.000002 ; 2.0 ; 2.463508 ; 2.000001 ] ] ;
[ [ 2.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; 0.060747 ; -0.530637 ; -0.014413 ;
-0.060747 ; 0.594377 ; -0.014413 ; 0.060747 ; -0.377571 ; -0.02241 ; -0.060747 ;
0.608509 ] ; [ 1.0 ; 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ;
[ 0.001974 ; 2.5854 ; 2.0 ; 2.0 ; 2.520037 ; 2.0 ; 2.0 ] ;
[ 0.005733 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001976 ; 2.618027 ; 2.000001 ; 2.000001 ; 2.000002 ; 2.000001 ; 2.000001 ] ;
[ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.057939 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; 0.060747 ; -0.530636 ; -0.014413 ;
-0.060747 ; 0.594377 ; -0.02241 ; 0.060747 ; -0.36344 ; -0.014413 ; -0.060747 ;
0.594377 ] ; [ 1.0 ; 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.001974 ; 2.5854 ; 2.0 ; 2.0 ; 2.520037 ; 2.0 ; 2.0 ] ;
[ 0.005733 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001975 ; 2.585404 ; 2.000001 ; 2.000001 ; 2.05794 ; 2.000001 ; 2.000001 ] ;
[ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; 0.060747 ; -0.530637 ; -0.02241 ;
-0.060747 ; 0.608509 ; -0.014413 ; 0.060747 ; -0.377571 ; -0.014413 ; -0.060747 ;
0.594377 ] ; [ 1.0 ; 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.001974 ; 2.5854 ; 2.0 ; 2.0 ; 2.520037 ; 2.0 ; 2.0 ] ;
[ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.057939 ; 2.0 ; 2.0 ] ;
[ 0.001975 ; 2.585402 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ] ; [ [ 2.0 ] ; [ -0.00033 ; -0.036939 ; 0.050064 ; -0.057593 ; 0.397884 ;
-0.016688 ; 0.057593 ; -0.362427 ; -0.016688 ; -0.057593 ; 0.559062 ; -0.016688 ;
-0.057593 ; 0.559062 ] ; [ 1.0 ; 0.0 ; 1.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.00033 ; 2.618094 ; 2.000003 ; 2.000003 ; 2.520014 ; 2.000003 ;
2.000003 ] ; [ 0.00033 ; 2.601753 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.00033 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.00033 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ] ] ; [ [ 2.0 ] ; [ -0.000417 ; -0.049823 ; 0.047052 ; -0.061687 ; 0.463622 ;
-0.015684 ; 0.061687 ; -0.379191 ; -0.015684 ; -0.061687 ; 0.607807 ; -0.015684 ;
0.061687 ; -0.379191 ] ; [ 1.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.000417 ; 2.60175 ; 2.0 ; 2.0 ; 2.5527 ; 2.0 ; 2.0 ] ;
[ 0.000418 ; 2.601748 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.000417 ; 2.60175 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.000418 ; 2.601748 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000396 ; -0.053582 ; 0.049452 ; -0.06302 ; 0.475514 ; -0.013853 ;
0.06302 ; -0.389234 ; -0.020791 ; -0.06302 ; 0.637132 ; -0.013853 ; -0.062897 ;
0.618101 ] ; [ 1.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.000359 ; 2.601749 ; 2.0 ; 2.0 ; 2.536279 ; 2.0 ; 2.0 ] ;
[ 0.000396 ; 2.601748 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.000396 ; 2.60175 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.000396 ; 2.60175 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.002012 ; -0.066935 ; 0.079693 ; 0.066241 ; -0.605497 ; -0.021495 ;
-0.066241 ; 0.685308 ; -0.021495 ; 0.066241 ; -0.374549 ; -0.036704 ; -0.066241 ;
0.715304 ] ; [ 0.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.00141 ; 2.52 ; 2.0 ; 2.0 ;
2.584895 ; 2.0 ; 2.0 ] ; [ 0.004908 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.002012 ; 2.585399 ; 2.000001 ; 2.000001 ; 2.000001 ; 2.000001 ; 2.0 ] ;
[ 0.002012 ; 2.5854 ; 2.0 ; 2.0 ; 2.115877 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.002012 ; -0.066935 ; 0.028887 ; 0.066241 ; -0.477466 ; -0.021495 ;
-0.066241 ; 0.685308 ; 0.014102 ; 0.066241 ; -0.472584 ; -0.021495 ; -0.066241 ;
0.685308 ] ; [ 0.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.001651 ; 2.5854 ; 2.0 ; 2.0 ; 2.596115 ; 2.0 ; 2.0 ] ;
[ 0.004908 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ; [ 0.002012 ; 2.52 ; 2.0 ; 2.0 ;
2.115878 ; 2.0 ; 2.0 ] ; [ 0.004908 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.002012 ; -0.066935 ; 0.028887 ; -0.066241 ; 0.582391 ; 0.014102 ;
0.066241 ; -0.472584 ; -0.021495 ; -0.066241 ; 0.685308 ; -0.021495 ; 0.066241 ;
-0.374549 ] ; [ 0.0 ] ; [ ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.00141 ; 2.520001 ; 2.000001 ; 2.000001 ; 2.58489 ; 2.000001 ; 2.000001 ] ;
[ 0.002012 ; 2.52 ; 2.0 ; 2.0 ; 2.115878 ; 2.0 ; 2.0 ] ; [ 0.004908 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ; [ 0.002012 ; 2.520001 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000405 ; -0.070081 ; 0.043025 ; 0.06775 ; -0.520998 ; -0.014342 ;
-0.06775 ; 0.681778 ; -0.014342 ; 0.06775 ; -0.402228 ; -0.014342 ; -0.06775 ;
0.681778 ] ; [ 0.0 ; 1.0 ] ; [ 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.000317 ; 2.585399 ; 2.0 ; 2.0 ; 2.612413 ; 2.0 ; 2.0 ] ;
[ 0.004048 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.000405 ; 2.585391 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.004048 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ] ; [ [ 2.0 ] ; [ -0.001161 ; -0.074623 ; 0.079355 ; 0.068595 ;
-0.608613 ; -0.023711 ; -0.068595 ; 0.719631 ; -0.023711 ; 0.068595 ; -0.37789 ;
-0.031932 ; -0.068595 ; 0.735738 ] ; [ 0.0 ; 0.0 ] ; [ 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 1.0 ] ; [ 0.001019 ; 2.52 ; 2.0 ; 2.0 ; 2.61793 ; 2.0 ; 2.0 ] ;
[ 0.004236 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ; [ 0.001162 ; 2.520001 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ; 2.0 ] ; [ 0.001161 ; 2.5527 ; 2.0 ; 2.0 ; 2.057939 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.001161 ; -0.074623 ; 0.019702 ; -0.081204 ; 0.740105 ; -0.023711 ;
0.081204 ; -0.47876 ; -0.031932 ; -0.081204 ; 0.836608 ; 0.035942 ; 0.081204 ;
-0.629086 ] ; [ 0.0 ; 0.0 ] ; [ 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.001084 ; 2.552699 ; 2.000001 ; 2.000001 ; 2.625659 ; 2.000001 ; 2.000001 ] ;
[ 0.001161 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.002657 ; 2.52 ; 2.0 ; 2.463509 ;
2.057939 ; 2.0 ; 2.0 ] ; [ 0.001162 ; 2.52 ; 2.000001 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.001161 ; -0.074623 ; 0.019702 ; -0.068595 ; 0.639237 ; -0.031932 ;
0.068595 ; -0.361784 ; -0.023711 ; -0.068595 ; 0.719631 ; 0.035942 ; 0.068595 ;
-0.528217 ] ; [ 0.0 ; 0.0 ] ; [ 1.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.001084 ; 2.5527 ; 2.0 ; 2.0 ; 2.625659 ; 2.0 ; 2.0 ] ;
[ 0.001161 ; 2.52 ; 2.0 ; 2.0 ; 2.057939 ; 2.0 ; 2.0 ] ; [ 0.004236 ; 2.52 ; 2.0 ; 2.463509 ;
2.0 ; 2.0 ; 2.0 ] ; [ 0.001161 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000308 ; -0.090009 ; 0.04151 ; 0.073665 ; -0.523458 ; -0.013837 ;
-0.073665 ; 0.755879 ; -0.013837 ; 0.073665 ; -0.422755 ; -0.013837 ; -0.073665 ;
0.755879 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 1.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.000308 ; 2.53635 ; 2.0 ; 2.0 ; 2.650799 ; 2.0 ; 2.0 ] ;
[ 0.000308 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.000308 ; 2.536357 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.000308 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000418 ; -0.17025 ; 0.094709 ; 0.098535 ; -0.692034 ; -0.021455 ;
-0.098535 ; 1.087114 ; 0.009749 ; 0.098535 ; -0.568591 ; -0.021455 ; -0.098535 ;
1.087114 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 1.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.000418 ; 2.52 ; 2.0 ; 2.0 ; 2.6508 ; 2.0 ; 2.0 ] ;
[ 0.000418 ; 2.53635 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.000418 ; 2.536343 ; 2.0 ; 2.0 ;
2.000004 ; 2.0 ; 2.0 ] ; [ 0.000418 ; 2.53635 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000644 ; -0.172166 ; 0.09973 ; -0.099785 ; 0.882284 ; 0.014169 ;
0.099785 ; -0.586728 ; -0.017353 ; -0.099785 ; 1.0903 ; 0.014169 ; 0.099785 ;
-0.586728 ] ; [ 0.0 ; 0.0 ] ; [ 1.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.000644 ; 2.5527 ; 2.0 ; 2.0 ; 2.6181 ; 2.0 ; 2.0 ] ; [ 0.000644 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.000644 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.000644 ; 2.5527 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 2.0 ] ; [ -0.000313 ; -0.084789 ; 0.039845 ; -0.071708 ; 0.632521 ; -0.013282 ;
-0.071708 ; 0.731624 ; -0.013282 ; -0.071708 ; 0.731624 ; -0.013282 ; 0.071708 ;
-0.415701 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.000313 ; 2.52 ; 2.0 ; 2.0 ; 2.5854 ; 2.0 ; 2.0 ] ; [ 0.003624 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ; [ 0.003624 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.000314 ; 2.520002 ; 2.000002 ; 2.000001 ; 2.000001 ; 2.000001 ; 2.000001 ] ] ;
[ [ 1.0 ] ; [ -0.00272 ; 0.065103 ; -0.052337 ; -0.02292 ; 0.191326 ; 0.23854 ; 0.02292 ;
-0.867278 ; -0.073933 ; -0.02292 ; 0.286871 ; -0.11227 ; 0.02292 ; -0.019974 ] ;
[ ] ; [ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.002703 ; 2.6508 ; 2.0 ; 2.0 ; 2.474335 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.004959 ; 2.6508 ; 2.0 ; 2.463509 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.002721 ; 2.650799 ; 2.0 ; 2.0 ; 2.231755 ; 2.0 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.00272 ; 0.065103 ; -0.052337 ; 0.02292 ; -0.17539 ; 0.23854 ; -0.02292 ;
-0.500562 ; -0.11227 ; 0.02292 ; -0.019974 ; -0.073933 ; -0.02292 ; 0.286871 ] ;
[ ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.002703 ; 2.650799 ; 2.0 ; 2.000001 ; 2.474442 ;
2.000001 ; 2.0 ] ; [ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.002721 ; 2.650799 ; 2.0 ; 2.0 ; 2.231755 ; 2.0 ; 2.0 ] ;
[ 0.003897 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.00272 ; 0.065103 ; -0.052337 ; 0.02292 ; -0.175391 ; -0.11227 ;
-0.02292 ; 0.346743 ; 0.23854 ; 0.02292 ; -0.867278 ; -0.073933 ; -0.02292 ;
0.286871 ] ; [ ] ; [ ] ; [ 1.0 ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.002703 ; 2.650799 ; 2.0 ; 2.000001 ;
2.474442 ; 2.000001 ; 2.0 ] ; [ 0.00272 ; 2.6508 ; 2.0 ; 2.0 ; 2.231754 ; 2.0 ; 2.0 ] ;
[ 0.00272 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.003897 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ;
2.0 ] ] ; [ [ 1.0 ] ; [ -0.004545 ; 0.062681 ; -0.026929 ; 0.023742 ; -0.242815 ;
-0.06441 ; -0.023742 ; 0.273568 ; 0.176245 ; 0.023742 ; -0.72849 ; -0.084906 ;
-0.023742 ; 0.3039 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ;
[ 0.004424 ; 2.5854 ; 2.0 ; 2.0 ; 2.491903 ; 2.0 ; 2.0 ] ;
[ 0.006469 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.004545 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.004545 ; 2.6508 ; 2.0 ; 2.0 ;
2.115877 ; 2.0 ; 2.0 ] ] ; [ [ 1.0 ] ; [ -0.004545 ; 0.062681 ; -0.026929 ; 0.023742 ;
-0.242815 ; 0.176245 ; -0.023742 ; -0.348621 ; -0.084906 ; 0.023742 ; -0.075969 ;
-0.06441 ; -0.023742 ; 0.273568 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.004424 ; 2.5854 ; 2.0 ; 2.0 ; 2.491903 ; 2.0 ; 2.0 ] ;
[ 0.004545 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.004545 ; 2.6508 ; 2.0 ; 2.0 ;
2.115877 ; 2.0 ; 2.0 ] ; [ 0.006469 ; 2.585401 ; 2.0 ; 2.000001 ; 2.0 ; 2.463508 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.004545 ; 0.062681 ; -0.026929 ; 0.023742 ; -0.242815 ; -0.084906 ;
-0.023742 ; 0.3039 ; 0.176245 ; 0.023742 ; -0.72849 ; -0.06441 ; -0.023742 ;
0.273568 ] ; [ 1.0 ] ; [ ] ; [ 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.004424 ; 2.5854 ; 2.0 ; 2.0 ; 2.491903 ; 2.0 ; 2.0 ] ;
[ 0.004545 ; 2.6508 ; 2.0 ; 2.0 ; 2.115877 ; 2.0 ; 2.0 ] ;
[ 0.004545 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.006469 ; 2.585401 ; 2.0 ; 2.000001 ;
2.0 ; 2.463508 ; 2.0 ] ] ; [ [ 1.0 ] ; [ -0.000884 ; 0.061714 ; -0.014502 ; -0.02407 ;
0.104941 ; 0.134266 ; 0.02407 ; -0.631477 ; -0.059882 ; -0.02407 ; 0.261947 ;
-0.059882 ; -0.02407 ; 0.261947 ] ; [ 1.0 ; 1.0 ] ; [ ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ] ; [ 0.000796 ; 2.6508 ; 2.0 ; 2.0 ; 2.488246 ; 2.0 ; 2.0 ] ;
[ 0.000884 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.003066 ; 2.618101 ; 2.0 ; 2.0 ; 2.0 ;
2.463509 ; 2.0 ] ; [ 0.003066 ; 2.618101 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; 0.060747 ; -0.530637 ; -0.014413 ;
-0.060747 ; 0.594377 ; -0.014413 ; 0.060747 ; -0.377571 ; -0.02241 ; -0.060747 ;
0.608509 ] ; [ 1.0 ; 0.0 ] ; [ ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ;
[ 0.002084 ; 2.585663 ; 2.000116 ; 2.000116 ; 2.519822 ; 2.000113 ; 2.000116 ] ;
[ 0.005733 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001976 ; 2.618027 ; 2.000001 ; 2.000001 ; 2.000002 ; 2.000001 ; 2.000001 ] ;
[ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.057939 ; 2.0 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; -0.073427 ; 0.542756 ; -0.014413 ;
0.073427 ; -0.479016 ; -0.02241 ; -0.073427 ; 0.709954 ; -0.014413 ; 0.073427 ;
-0.479016 ] ; [ 1.0 ; 0.0 ] ; [ ] ; [ 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.001974 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ; 2.0 ] ; [ 0.004138 ; 2.5854 ; 2.0 ; 2.0 ; 2.057939 ; 2.463509 ; 2.0 ] ;
[ 0.001974 ; 2.585401 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.001974 ; -0.0469 ; 0.051237 ; -0.060747 ; 0.44131200000000004 ;
-0.02241 ; 0.060747 ; -0.36344 ; -0.014413 ; -0.060747 ; 0.594377 ; -0.014413 ;
0.060747 ; -0.377571 ] ; [ 1.0 ; 0.0 ] ; [ ] ; [ 0.0 ; 0.0 ; 1.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.0 ; 0.0 ; 0.0 ] ; [ 0.002165 ; 2.585453 ; 2.000636 ; 2.000639 ; 2.51972 ; 2.000635 ;
2.000606 ] ; [ 0.001975 ; 2.585404 ; 2.000001 ; 2.000001 ; 2.05794 ; 2.000001 ;
2.000001 ] ; [ 0.001974 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ;
[ 0.001975 ; 2.585402 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.00033 ; -0.036939 ; 0.050064 ; 0.057593 ; -0.523604 ; -0.016688 ;
-0.057593 ; 0.559062 ; -0.016688 ; 0.057593 ; -0.362427 ; -0.016688 ; -0.057593 ;
0.559062 ] ; [ 1.0 ; 0.0 ; 1.0 ] ; [ ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.000403 ; 2.609586 ; 2.000023 ; 2.00002 ; 2.519733 ; 2.000019 ; 2.000024 ] ;
[ 0.00033 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ; [ 0.00033 ; 2.601753 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ] ; [ 0.00033 ; 2.6181 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ;
[ [ 1.0 ] ; [ -0.000886 ; -0.177145 ; 0.151334 ; -0.103308 ; 0.774954 ; 0.041584 ;
0.103308 ; -0.677721 ; 0.00995 ; -0.103308 ; 1.057518 ; 0.041584 ; 0.103308 ;
-0.677721 ] ; [ 1.0 ; 0.0 ; 0.0 ] ; [ ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ; [ 0.0 ; 0.0 ; 0.0 ] ;
[ 0.000886 ; 2.5854 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.000887 ; 2.601712 ; 2.000001 ;
2.000001 ; 2.000015 ; 2.000001 ; 2.000001 ] ; [ 0.000886 ; 2.601749 ; 2.0 ; 2.0 ; 2.0 ;
2.000001 ; 2.0 ] ; [ 0.000887 ; 2.601712 ; 2.000001 ; 2.000001 ; 2.000015 ;
2.000001 ; 2.000001 ] ] ; [ [ 1.0 ] ; [ -0.001328 ; -0.121189 ; 0.06473 ; -0.084657 ;
0.741383 ; -0.016252 ; 0.084657 ; -0.45858 ; -0.022099 ; -0.084657 ; 0.911046 ;
-0.016252 ; 0.084657 ; -0.45858 ] ; [ 0.0 ] ; [ ] ; [ 0.0 ] ; [ 0.0 ] ; [ 0.0 ] ;
[ 0.001328 ; 2.52 ; 2.0 ; 2.0 ; 2.52 ; 2.0 ; 2.0 ] ; [ 0.001328 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ;
2.0 ] ; [ 0.006318 ; 2.52 ; 2.0 ; 2.0 ; 2.0 ; 2.463509 ; 2.0 ] ;
[ 0.001328 ; 2.5854 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ; 2.0 ] ] ];;
*)
(*
raw data from Mathematica
output /tmp/ineqdata3q1h.ml (with cutoff = 0.0003),
book_code/sphereBook.nb, svn version 1185.
{{{4.}, {-0.00289, 0.129913, -0.060416, 0.002372, -0.113134, 0.01764,
-0.002372, -0.198777, 0.045166, 0.002372, -0.306092, 0.021777, -0.002372,
-0.259166}, {}, {}, {}, {}, {1.}, {0.003326, 2.463509, 2., 2., 2.52, 2.,
2.}, {0.00289, 2.463514, 2., 2.463508, 2., 2.000001, 2.000001},
{0.003534, 2.463509, 2.000001, 2.463508, 2., 2., 2.000001},
{0.00289, 2.52, 2., 2., 2.231754, 2., 2.}},
{{4.}, {-0.002889, 0.129699, -0.060316, 0.002264, -0.112116, 0.019214,
-0.002264, -0.203309, 0.021887, 0.002264, -0.29619, 0.019214, -0.002264,
-0.203309}, {}, {}, {}, {1.}, {0.}, {0.003328, 2.463509, 2., 2., 2.52, 2.,
2.}, {0.00289, 2.463513, 2., 2.463508, 2., 2.000001, 2.},
{0.002889, 2.463509, 2., 2., 2.231754, 2., 2.},
{0.002998, 2.519915, 2.000025, 2.000038, 2.000022, 2.463485, 2.000022}},
{{4.}, {-0.00289, 0.129913, -0.060416, 0.002372, -0.113134, 0.021777,
-0.002372, -0.259166, 0.045166, 0.002372, -0.306092, 0.01764, -0.002372,
-0.198777}, {}, {}, {1.}, {0.}, {0.}, {0.003326, 2.463509, 2., 2., 2.52,
2., 2.}, {0.00289, 2.52, 2., 2., 2.231754, 2., 2.},
{0.003534, 2.463509, 2., 2., 2., 2.463508, 2.},
{0.002915, 2.519935, 2.000027, 2.00004, 2.000024, 2.463484, 2.000025}},
{{4.}, {-0.000426, -0.114872, 0.133539, -0.080919, 0.532524, 0.148605,
0.080919, -0.855148, 0.08743, -0.080919, 0.593722, 0.148605, 0.080919,
-0.855148}, {}, {}, {0.}, {0.}, {0.}, {0.000426, 2.463509, 2., 2., 2.6508,
2., 2.}, {0.000435, 2.463511, 2.000001, 2.000001, 2.000002, 2.000002,
2.000002}, {0.004824, 2.46351, 2., 2., 2., 2.463509, 2.},
{0.000435, 2.463511, 2.000001, 2.000001, 2.000002, 2.000002, 2.000002}},
{{3.}, {-0.00272, 0.065103, -0.008732, -0.024884, 0.097156, 0.072591,
0.024884, -0.464803, 0.042651, -0.024884, 0.008797, 0.055356, 0.024884,
-0.458108}, {}, {}, {}, {}, {1.}, {0.002594, 2.52, 2., 2., 2.491729, 2.,
2.}, {0.00272, 2.463509, 2., 2., 2., 2., 2.},
{0.00272, 2.463509, 2., 2.463509, 2., 2., 2.},
{0.00272, 2.52, 2., 2., 2.231754, 2., 2.}},
{{3.}, {-0.00272, 0.065103, -0.029778, -0.027449, 0.170713, 0.072591,
0.027449, -0.485323, 0.055356, -0.027449, -0.039438, 0.072591, 0.027449,
-0.485323}, {}, {}, {}, {1.}, {0.}, {0.002594, 2.52, 2., 2., 2.491998, 2.,
2.}, {0.00272, 2.463509, 2., 2., 2., 2., 2.},
{0.00272, 2.463509, 2., 2., 2.231754, 2., 2.},
{0.00272, 2.463509, 2., 2., 2., 2., 2.}},
{{3.}, {-0.00272, 0.065103, -0.008732, 0.025458, -0.30558, 0.055356,
-0.025458, -0.055371, 0.072591, 0.025458, -0.469389, 0.037947, -0.025458,
0.025236}, {}, {}, {1.}, {0.}, {0.}, {0.002612, 2.463509, 2., 2.,
2.489061, 2., 2.}, {0.00272, 2.52, 2., 2., 2.231754, 2., 2.},
{0.00272, 2.52, 2., 2., 2., 2., 2.}, {0.00272, 2.463509, 2., 2., 2.,
2.463509, 2.}}, {{3.}, {-0.00225, -0.114872, 0.116669, 0.080919,
-0.7251449999999999, 0.08743, -0.080919, 0.595546, 0.148605, 0.080919,
-0.853324, 0.08743, -0.080919, 0.595546}, {}, {}, {0.}, {0.}, {0.},
{0.00225, 2.519989, 2., 2., 2.52, 2., 2.}, {0.006648, 2.46351, 2., 2., 2.,
2.463509, 2.}, {0.002259, 2.463511, 2.000001, 2.000001, 2.000002,
2.000002, 2.000002}, {0.006648, 2.46351, 2., 2., 2., 2.463509, 2.}},
{{2.}, {-0.00289, 0.129913, -0.09152, 0.002372, -0.034749, 0.347659,
-0.002372, -1.030425, -0.105208, 0.002372, 0.072849, -0.150931, -0.002372,
0.176057}, {}, {}, {}, {}, {1.}, {0.00289, 2.52, 2., 2., 2.52, 2., 2.},
{0.00289, 2.52, 2., 2.463509, 2., 2., 2.}, {0.005089, 2.52, 2., 2.463509,
2., 2., 2.}, {0.00289, 2.6508, 2., 2., 2.231754, 2., 2.}},
{{2.}, {-0.00289, 0.129913, 0.340765, 0.002372, -1.124108, -0.094917,
-0.002372, 0.084866, -0.150931, 0.002372, 0.138108, -0.094917, -0.002372,
0.084866}, {}, {}, {}, {1.}, {0.}, {0.00289, 2.52, 2., 2., 2.52, 2., 2.},
{0.00289, 2.52, 2., 2.463509, 2., 2., 2.}, {0.00289, 2.6508, 2., 2.,
2.231754, 2., 2.}, {0.00289, 2.520001, 2., 2., 2., 2.463509, 2.}},
{{2.}, {-0.00289, 0.129913, -0.09152, 0.002372, -0.034749, 0.291645,
-0.002372, -0.939234, -0.105208, 0.002372, 0.072849, -0.094917, -0.002372,
0.084866}, {}, {}, {1.}, {0.}, {0.}, {0.00289, 2.52, 2., 2., 2.52, 2.,
2.}, {0.00289, 2.52, 2., 2., 2.231754, 2., 2.},
{0.005089, 2.520002, 2.000001, 2.000001, 2.000001, 2.463507, 2.000001},
{0.00289, 2.520001, 2., 2., 2., 2.463509, 2.}},
{{2.}, {-0.005361, 0.128506, 0.290371, 0.003287, -1.026581, -0.070878,
-0.003287, 0.033394, -0.097658, 0.003287, 0.050047, -0.121835, -0.003287,
0.13571}, {1.}, {}, {0.}, {0.}, {0., 1.}, {0.005361, 2.5854, 2., 2., 2.52,
2., 2.}, {0.005361, 2.585401, 2., 2., 2., 2.463509, 2.},
{0.008408, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.005361, 2.6508, 2., 2., 2.115877, 2., 2.}},
{{2.}, {-0.005361, 0.128506, 0.263591, 0.003287, -0.957343, -0.070878,
-0.003287, 0.033394, -0.121835, 0.003287, 0.083125, -0.070878, -0.003287,
0.033394}, {1.}, {}, {0.}, {0., 1.}, {0., 0.},
{0.005361, 2.5854, 2., 2., 2.52, 2., 2.}, {0.005361, 2.585401, 2., 2., 2.,
2.463509, 2.}, {0.005361, 2.6508, 2., 2., 2.115877, 2., 2.},
{0.005362, 2.585403, 2., 2.000001, 2., 2.463508, 2.}},
{{2.}, {-0.005361, 0.128506, -0.066254, 0.003287, -0.104563, 0.234791,
-0.003287, -0.786309, -0.097658, 0.003287, 0.050047, -0.070878, -0.003287,
0.033394}, {1.}, {}, {0., 1.}, {0., 0.}, {0., 0.},
{0.005361, 2.5854, 2., 2., 2.52, 2., 2.}, {0.005361, 2.5854, 2., 2.,
2.115877, 2., 2.}, {0.008409, 2.585403, 2.000001, 2.000001, 2.000001,
2.463508, 2.000001}, {0.005362, 2.585403, 2., 2.000001, 2., 2.463508,
2.}}, {{2.}, {-0.001637, 0.127166, -0.07331, 0.003788, -0.105909, 0.23984,
-0.003788, -0.767737, -0.096981, 0.003788, 0.04248, -0.069548, -0.003788,
0.032155}, {1.}, {1.}, {0., 0.}, {0., 0.}, {0., 0.},
{0.001637, 2.5854, 2., 2., 2.5854, 2., 2.}, {0.001637, 2.5854, 2., 2., 2.,
2., 2.}, {0.005148, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.001637, 2.585403, 2., 2.000001, 2., 2.463508, 2.}},
{{2.}, {-0.00125, 0.126777, -0.053069, 0.003525, -0.142652, 0.196466,
-0.003525, -0.667227, -0.093532, 0.003525, 0.035622, -0.049865, -0.003525,
-0.022307}, {1., 1.}, {0.}, {0., 0.}, {0., 0.}, {0., 0.},
{0.00125, 2.6181, 2., 2., 2.52, 2.463509, 2.},
{0.001388, 2.6181, 2.000001, 2.000001, 2., 2.463508, 2.},
{0.004482, 2.6508, 2., 2., 2., 2.463509, 2.},
{0.001388, 2.618101, 2.000001, 2.000002, 2., 2.463508, 2.000001}},
{{2.}, {-0.001974, -0.0469, 0.051237, 0.060747, -0.530637, -0.014413,
-0.060747, 0.594377, -0.014413, 0.060747, -0.377571, -0.02241, -0.060747,
0.608509}, {1., 0.}, {0.}, {0., 0.}, {0., 0.}, {0., 0., 1.},
{0.001974, 2.5854, 2., 2., 2.520037, 2., 2.},
{0.005733, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.001976, 2.618027, 2.000001, 2.000001, 2.000002, 2.000001, 2.000001},
{0.001974, 2.6181, 2., 2., 2.057939, 2., 2.}},
{{2.}, {-0.001974, -0.0469, 0.051237, 0.060747, -0.530636, -0.014413,
-0.060747, 0.594377, -0.02241, 0.060747, -0.36344, -0.014413, -0.060747,
0.594377}, {1., 0.}, {0.}, {0., 0.}, {0., 0., 1.}, {0., 0., 0.},
{0.001974, 2.5854, 2., 2., 2.520037, 2., 2.},
{0.005733, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.001975, 2.585404, 2.000001, 2.000001, 2.05794, 2.000001, 2.000001},
{0.001974, 2.6181, 2., 2., 2., 2., 2.}},
{{2.}, {-0.001974, -0.0469, 0.051237, 0.060747, -0.530637, -0.02241,
-0.060747, 0.608509, -0.014413, 0.060747, -0.377571, -0.014413, -0.060747,
0.594377}, {1., 0.}, {0.}, {0., 0., 1.}, {0., 0., 0.}, {0., 0., 0.},
{0.001974, 2.5854, 2., 2., 2.520037, 2., 2.},
{0.001974, 2.6181, 2., 2., 2.057939, 2., 2.},
{0.001975, 2.585402, 2., 2., 2., 2., 2.}, {0.001974, 2.6181, 2., 2., 2.,
2., 2.}}, {{2.}, {-0.00033, -0.036939, 0.050064, -0.057593, 0.397884,
-0.016688, 0.057593, -0.362427, -0.016688, -0.057593, 0.559062, -0.016688,
-0.057593, 0.559062}, {1., 0., 1.}, {0.}, {0., 0., 0.}, {0., 0., 0.},
{0., 0., 0.}, {0.00033, 2.618094, 2.000003, 2.000003, 2.520014, 2.000003,
2.000003}, {0.00033, 2.601753, 2., 2., 2., 2., 2.},
{0.00033, 2.6181, 2., 2., 2., 2., 2.}, {0.00033, 2.6181, 2., 2., 2., 2.,
2.}}, {{2.}, {-0.000417, -0.049823, 0.047052, -0.061687, 0.463622,
-0.015684, 0.061687, -0.379191, -0.015684, -0.061687, 0.607807, -0.015684,
0.061687, -0.379191}, {1., 0., 0.}, {0., 1.}, {0., 0., 0.}, {0., 0., 0.},
{0., 0., 0.}, {0.000417, 2.60175, 2., 2., 2.5527, 2., 2.},
{0.000418, 2.601748, 2., 2., 2., 2., 2.}, {0.000417, 2.60175, 2., 2., 2.,
2., 2.}, {0.000418, 2.601748, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000396, -0.053582, 0.049452, -0.06302, 0.475514, -0.013853,
0.06302, -0.389234, -0.020791, -0.06302, 0.637132, -0.013853, -0.062897,
0.618101}, {1., 0., 0.}, {0., 0.}, {0., 0., 0.}, {0., 0., 0.},
{0., 0., 0.}, {0.000359, 2.601749, 2., 2., 2.536279, 2., 2.},
{0.000396, 2.601748, 2., 2., 2., 2., 2.}, {0.000396, 2.60175, 2., 2., 2.,
2., 2.}, {0.000396, 2.60175, 2., 2., 2., 2., 2.}},
{{2.}, {-0.002012, -0.066935, 0.079693, 0.066241, -0.605497, -0.021495,
-0.066241, 0.685308, -0.021495, 0.066241, -0.374549, -0.036704, -0.066241,
0.715304}, {0.}, {}, {0.}, {0.}, {0., 1.}, {0.00141, 2.52, 2., 2.,
2.584895, 2., 2.}, {0.004908, 2.52, 2., 2., 2., 2.463509, 2.},
{0.002012, 2.585399, 2.000001, 2.000001, 2.000001, 2.000001, 2.},
{0.002012, 2.5854, 2., 2., 2.115877, 2., 2.}},
{{2.}, {-0.002012, -0.066935, 0.028887, 0.066241, -0.477466, -0.021495,
-0.066241, 0.685308, 0.014102, 0.066241, -0.472584, -0.021495, -0.066241,
0.685308}, {0.}, {}, {0.}, {0., 1.}, {0., 0.},
{0.001651, 2.5854, 2., 2., 2.596115, 2., 2.},
{0.004908, 2.52, 2., 2., 2., 2.463509, 2.}, {0.002012, 2.52, 2., 2.,
2.115878, 2., 2.}, {0.004908, 2.52, 2., 2., 2., 2.463509, 2.}},
{{2.}, {-0.002012, -0.066935, 0.028887, -0.066241, 0.582391, 0.014102,
0.066241, -0.472584, -0.021495, -0.066241, 0.685308, -0.021495, 0.066241,
-0.374549}, {0.}, {}, {0., 1.}, {0., 0.}, {0., 0.},
{0.00141, 2.520001, 2.000001, 2.000001, 2.58489, 2.000001, 2.000001},
{0.002012, 2.52, 2., 2., 2.115878, 2., 2.}, {0.004908, 2.52, 2., 2., 2.,
2.463509, 2.}, {0.002012, 2.520001, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000405, -0.070081, 0.043025, 0.06775, -0.520998, -0.014342,
-0.06775, 0.681778, -0.014342, 0.06775, -0.402228, -0.014342, -0.06775,
0.681778}, {0., 1.}, {1.}, {0., 0.}, {0., 0.}, {0., 0.},
{0.000317, 2.585399, 2., 2., 2.612413, 2., 2.},
{0.004048, 2.5527, 2., 2., 2., 2.463509, 2.},
{0.000405, 2.585391, 2., 2., 2., 2., 2.}, {0.004048, 2.5527, 2., 2., 2.,
2.463509, 2.}}, {{2.}, {-0.001161, -0.074623, 0.079355, 0.068595,
-0.608613, -0.023711, -0.068595, 0.719631, -0.023711, 0.068595, -0.37789,
-0.031932, -0.068595, 0.735738}, {0., 0.}, {1.}, {0., 0.}, {0., 0.},
{0., 0., 1.}, {0.001019, 2.52, 2., 2., 2.61793, 2., 2.},
{0.004236, 2.52, 2., 2., 2., 2.463509, 2.}, {0.001162, 2.520001, 2., 2.,
2., 2., 2.}, {0.001161, 2.5527, 2., 2., 2.057939, 2., 2.}},
{{2.}, {-0.001161, -0.074623, 0.019702, -0.081204, 0.740105, -0.023711,
0.081204, -0.47876, -0.031932, -0.081204, 0.836608, 0.035942, 0.081204,
-0.629086}, {0., 0.}, {1.}, {0., 0.}, {0., 0., 1.}, {0., 0., 0.},
{0.001084, 2.552699, 2.000001, 2.000001, 2.625659, 2.000001, 2.000001},
{0.001161, 2.52, 2., 2., 2., 2., 2.}, {0.002657, 2.52, 2., 2.463509,
2.057939, 2., 2.}, {0.001162, 2.52, 2.000001, 2., 2., 2., 2.}},
{{2.}, {-0.001161, -0.074623, 0.019702, -0.068595, 0.639237, -0.031932,
0.068595, -0.361784, -0.023711, -0.068595, 0.719631, 0.035942, 0.068595,
-0.528217}, {0., 0.}, {1.}, {0., 0., 1.}, {0., 0., 0.}, {0., 0., 0.},
{0.001084, 2.5527, 2., 2., 2.625659, 2., 2.},
{0.001161, 2.52, 2., 2., 2.057939, 2., 2.}, {0.004236, 2.52, 2., 2.463509,
2., 2., 2.}, {0.001161, 2.52, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000308, -0.090009, 0.04151, 0.073665, -0.523458, -0.013837,
-0.073665, 0.755879, -0.013837, 0.073665, -0.422755, -0.013837, -0.073665,
0.755879}, {0., 0., 1.}, {1., 1.}, {0., 0., 0.}, {0., 0., 0.},
{0., 0., 0.}, {0.000308, 2.53635, 2., 2., 2.650799, 2., 2.},
{0.000308, 2.5527, 2., 2., 2., 2., 2.}, {0.000308, 2.536357, 2., 2., 2.,
2., 2.}, {0.000308, 2.5527, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000418, -0.17025, 0.094709, 0.098535, -0.692034, -0.021455,
-0.098535, 1.087114, 0.009749, 0.098535, -0.568591, -0.021455, -0.098535,
1.087114}, {0., 0., 0.}, {1., 1.}, {0., 0., 0.}, {0., 0., 0.},
{0., 0., 0.}, {0.000418, 2.52, 2., 2., 2.6508, 2., 2.},
{0.000418, 2.53635, 2., 2., 2., 2., 2.}, {0.000418, 2.536343, 2., 2.,
2.000004, 2., 2.}, {0.000418, 2.53635, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000644, -0.172166, 0.09973, -0.099785, 0.882284, 0.014169,
0.099785, -0.586728, -0.017353, -0.099785, 1.0903, 0.014169, 0.099785,
-0.586728}, {0., 0.}, {1., 0.}, {0., 0., 0.}, {0., 0., 0.}, {0., 0., 0.},
{0.000644, 2.5527, 2., 2., 2.6181, 2., 2.}, {0.000644, 2.5527, 2., 2., 2.,
2., 2.}, {0.000644, 2.5527, 2., 2., 2., 2., 2.},
{0.000644, 2.5527, 2., 2., 2., 2., 2.}},
{{2.}, {-0.000313, -0.084789, 0.039845, -0.071708, 0.632521, -0.013282,
-0.071708, 0.731624, -0.013282, -0.071708, 0.731624, -0.013282, 0.071708,
-0.415701}, {0.}, {0.}, {0., 0.}, {0., 0.}, {0., 0.},
{0.000313, 2.52, 2., 2., 2.5854, 2., 2.}, {0.003624, 2.52, 2., 2., 2.,
2.463509, 2.}, {0.003624, 2.52, 2., 2., 2., 2.463509, 2.},
{0.000314, 2.520002, 2.000002, 2.000001, 2.000001, 2.000001, 2.000001}},
{{1.}, {-0.00272, 0.065103, -0.052337, -0.02292, 0.191326, 0.23854, 0.02292,
-0.867278, -0.073933, -0.02292, 0.286871, -0.11227, 0.02292, -0.019974},
{}, {}, {}, {}, {1.}, {0.002703, 2.6508, 2., 2., 2.474335, 2., 2.},
{0.00272, 2.52, 2., 2., 2., 2., 2.}, {0.004959, 2.6508, 2., 2.463509, 2.,
2., 2.}, {0.002721, 2.650799, 2., 2., 2.231755, 2., 2.}},
{{1.}, {-0.00272, 0.065103, -0.052337, 0.02292, -0.17539, 0.23854, -0.02292,
-0.500562, -0.11227, 0.02292, -0.019974, -0.073933, -0.02292, 0.286871},
{}, {}, {}, {1.}, {0.}, {0.002703, 2.650799, 2., 2.000001, 2.474442,
2.000001, 2.}, {0.00272, 2.52, 2., 2., 2., 2., 2.},
{0.002721, 2.650799, 2., 2., 2.231755, 2., 2.},
{0.003897, 2.52, 2., 2., 2., 2.463509, 2.}},
{{1.}, {-0.00272, 0.065103, -0.052337, 0.02292, -0.175391, -0.11227,
-0.02292, 0.346743, 0.23854, 0.02292, -0.867278, -0.073933, -0.02292,
0.286871}, {}, {}, {1.}, {0.}, {0.}, {0.002703, 2.650799, 2., 2.000001,
2.474442, 2.000001, 2.}, {0.00272, 2.6508, 2., 2., 2.231754, 2., 2.},
{0.00272, 2.52, 2., 2., 2., 2., 2.}, {0.003897, 2.52, 2., 2., 2., 2.463509,
2.}}, {{1.}, {-0.004545, 0.062681, -0.026929, 0.023742, -0.242815,
-0.06441, -0.023742, 0.273568, 0.176245, 0.023742, -0.72849, -0.084906,
-0.023742, 0.3039}, {1.}, {}, {0.}, {0.}, {0., 1.},
{0.004424, 2.5854, 2., 2., 2.491903, 2., 2.},
{0.006469, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.004545, 2.5854, 2., 2., 2., 2., 2.}, {0.004545, 2.6508, 2., 2.,
2.115877, 2., 2.}}, {{1.}, {-0.004545, 0.062681, -0.026929, 0.023742,
-0.242815, 0.176245, -0.023742, -0.348621, -0.084906, 0.023742, -0.075969,
-0.06441, -0.023742, 0.273568}, {1.}, {}, {0.}, {0., 1.}, {0., 0.},
{0.004424, 2.5854, 2., 2., 2.491903, 2., 2.},
{0.004545, 2.5854, 2., 2., 2., 2., 2.}, {0.004545, 2.6508, 2., 2.,
2.115877, 2., 2.}, {0.006469, 2.585401, 2., 2.000001, 2., 2.463508, 2.}},
{{1.}, {-0.004545, 0.062681, -0.026929, 0.023742, -0.242815, -0.084906,
-0.023742, 0.3039, 0.176245, 0.023742, -0.72849, -0.06441, -0.023742,
0.273568}, {1.}, {}, {0., 1.}, {0., 0.}, {0., 0.},
{0.004424, 2.5854, 2., 2., 2.491903, 2., 2.},
{0.004545, 2.6508, 2., 2., 2.115877, 2., 2.},
{0.004545, 2.5854, 2., 2., 2., 2., 2.}, {0.006469, 2.585401, 2., 2.000001,
2., 2.463508, 2.}}, {{1.}, {-0.000884, 0.061714, -0.014502, -0.02407,
0.104941, 0.134266, 0.02407, -0.631477, -0.059882, -0.02407, 0.261947,
-0.059882, -0.02407, 0.261947}, {1., 1.}, {}, {0., 0.}, {0., 0.},
{0., 0.}, {0.000796, 2.6508, 2., 2., 2.488246, 2., 2.},
{0.000884, 2.6181, 2., 2., 2., 2., 2.}, {0.003066, 2.618101, 2., 2., 2.,
2.463509, 2.}, {0.003066, 2.618101, 2., 2., 2., 2.463509, 2.}},
{{1.}, {-0.001974, -0.0469, 0.051237, 0.060747, -0.530637, -0.014413,
-0.060747, 0.594377, -0.014413, 0.060747, -0.377571, -0.02241, -0.060747,
0.608509}, {1., 0.}, {}, {0., 0.}, {0., 0.}, {0., 0., 1.},
{0.002084, 2.585663, 2.000116, 2.000116, 2.519822, 2.000113, 2.000116},
{0.005733, 2.5854, 2., 2., 2., 2.463509, 2.},
{0.001976, 2.618027, 2.000001, 2.000001, 2.000002, 2.000001, 2.000001},
{0.001974, 2.6181, 2., 2., 2.057939, 2., 2.}},
{{1.}, {-0.001974, -0.0469, 0.051237, -0.073427, 0.542756, -0.014413,
0.073427, -0.479016, -0.02241, -0.073427, 0.709954, -0.014413, 0.073427,
-0.479016}, {1., 0.}, {}, {0., 0.}, {0., 0., 1.}, {0., 0., 0.},
{0.001974, 2.6181, 2., 2., 2.52, 2., 2.}, {0.001974, 2.5854, 2., 2., 2.,
2., 2.}, {0.004138, 2.5854, 2., 2., 2.057939, 2.463509, 2.},
{0.001974, 2.585401, 2., 2., 2., 2., 2.}},
{{1.}, {-0.001974, -0.0469, 0.051237, -0.060747, 0.44131200000000004,
-0.02241, 0.060747, -0.36344, -0.014413, -0.060747, 0.594377, -0.014413,
0.060747, -0.377571}, {1., 0.}, {}, {0., 0., 1.}, {0., 0., 0.},
{0., 0., 0.}, {0.002165, 2.585453, 2.000636, 2.000639, 2.51972, 2.000635,
2.000606}, {0.001975, 2.585404, 2.000001, 2.000001, 2.05794, 2.000001,
2.000001}, {0.001974, 2.6181, 2., 2., 2., 2., 2.},
{0.001975, 2.585402, 2., 2., 2., 2., 2.}},
{{1.}, {-0.00033, -0.036939, 0.050064, 0.057593, -0.523604, -0.016688,
-0.057593, 0.559062, -0.016688, 0.057593, -0.362427, -0.016688, -0.057593,
0.559062}, {1., 0., 1.}, {}, {0., 0., 0.}, {0., 0., 0.}, {0., 0., 0.},
{0.000403, 2.609586, 2.000023, 2.00002, 2.519733, 2.000019, 2.000024},
{0.00033, 2.6181, 2., 2., 2., 2., 2.}, {0.00033, 2.601753, 2., 2., 2., 2.,
2.}, {0.00033, 2.6181, 2., 2., 2., 2., 2.}},
{{1.}, {-0.000886, -0.177145, 0.151334, -0.103308, 0.774954, 0.041584,
0.103308, -0.677721, 0.00995, -0.103308, 1.057518, 0.041584, 0.103308,
-0.677721}, {1., 0., 0.}, {}, {0., 0., 0.}, {0., 0., 0.}, {0., 0., 0.},
{0.000886, 2.5854, 2., 2., 2.52, 2., 2.}, {0.000887, 2.601712, 2.000001,
2.000001, 2.000015, 2.000001, 2.000001}, {0.000886, 2.601749, 2., 2., 2.,
2.000001, 2.}, {0.000887, 2.601712, 2.000001, 2.000001, 2.000015,
2.000001, 2.000001}}, {{1.}, {-0.001328, -0.121189, 0.06473, -0.084657,
0.741383, -0.016252, 0.084657, -0.45858, -0.022099, -0.084657, 0.911046,
-0.016252, 0.084657, -0.45858}, {0.}, {}, {0.}, {0.}, {0.},
{0.001328, 2.52, 2., 2., 2.52, 2., 2.}, {0.001328, 2.5854, 2., 2., 2., 2.,
2.}, {0.006318, 2.52, 2., 2., 2., 2.463509, 2.},
{0.001328, 2.5854, 2., 2., 2., 2., 2.}}}
*)
(* test that the data covers the entire 13-dimensional domain of octahedra *)
let get_cover i =
let v = List.rev in
let r = map (fun t -> (v t.branch1,v t.branch2,v t.branch3,v t.branch4,v t.branch5)) (filter (fun t -> t.caseno =i ) records) in r;;
let check ((r1,r2,r3,r4,r5),(s1,s2,s3,s4,s5)) =
not(r1=[]) && not(s1=[]) &&
not(hd r1 = hd s1) && (tl r1 = tl s1) &&
(r2 = s2) && (r3 = s3) && (r4=s4) &&(r5=s5);;
let combine
((r1,r2,r3,r4,r5),(s1,s2,s3,s4,s5))=
if check((r1,r2,r3,r4,r5),(s1,s2,s3,s4,s5))
then (hd r1 < hd s1,0),(tl r1,r2,r3,r4,r5)
else if check((r2,r1,r3,r4,r5),(s2,s1,s3,s4,s5))
then (hd r2 < hd s2,1),(r1,tl r2,r3,r4,r5)
else if check((r3,r1,r2,r4,r5),(s3,s1,s2,s4,s5))
then (hd r3 < hd s3,2),(r1,r2,tl r3,r4,r5)
else if check((r4,r1,r2,r3,r5),(s4,s1,s2,s3,s5))
then (hd r4 < hd s4,3),(r1,r2,r3,tl r4,r5)
else if check((r5,r1,r2,r3,r4),(s5,s1,s2,s3,s4))
then (hd r5 < hd s5,4),(r1,r2,r3,r4,tl r5)
else failwith "combine";;
let rec combine_l = function
[] -> []
| [a] -> [a]
| a::b::cs -> try (snd(combine (a,b))) :: cs with Failure _ -> a:: (combine_l (b::cs));;
let rec combine_r x=
let y = combine_l x in
if (y = x) then x else combine_r y;;
let rec nub = function (* from lpproc *)
| [] -> []
| x::xs -> x::filter ((<>) x) (nub xs);;
let domain_cover_calculation = ([[([],[],[],[],[])]] =
nub(map (fun t -> combine_r (get_cover t)) ( 1 -- 4) ));;
(* for testing in cfsqp:
let exec case r =
let d = List.nth records r in
let f = mk_ineq case d in
execute_cfsqp { ineq = f; id = "TEST"; tags = []; doc = ""; };;
*)
end;;