PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/een/normalized-air03.opb
MD5SUM	017636577e3ff026b2ea720fb537705b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	10757
Biggest coefficient in the objective function	6873
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	13748961
Number of bits of the sum of numbers in the objective function	24
Biggest number in a constraint	6873
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	13748961
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	2.22466
Number of variables	10757
Total number of constraints	248
Number of constraints which are clauses	126
Number of constraints which are cardinality constraints (but not clauses)	122
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	3861
Trace number 6987

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 20:50:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5042 boxname=wulflinc26 idbench=388 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  017636577e3ff026b2ea720fb537705b  /oldhome/oroussel/tmp/wulflinc26/normalized-air03.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc26/normalized-air03.opb /oldhome/oroussel/tmp/wulflinc26/normalized-air03.opb
IDLAUNCH: 5042
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        798140 kB
Buffers:         36384 kB
Cached:         159292 kB
SwapCached:       2476 kB
Active:          72812 kB
Inactive:       128236 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        797888 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29876 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:10:18 (client local time) WITH STATUS 10 IN 1200.61 SECONDS
stats: 5042 7 1200.61 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 248 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ============================================================================================================================
c   -- Clauses(.)/Splits(s): ..
c ---[ 242]---> BDD-cost:    3
c ---[ 240]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:    7
c ---[ 236]---> BDD-cost:   19
c ---[ 234]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   21
c ---[ 230]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:   23
c ---[ 226]---> BDD-cost:   25
c ---[ 224]---> BDD-cost:   55
c ---[ 222]---> BDD-cost:   41
c ---[ 220]---> BDD-cost:    1
c ---[ 218]---> BDD-cost:   53
c ---[ 216]---> BDD-cost:   65
c ---[ 214]---> BDD-cost:   81
c ---[ 212]---> BDD-cost:   87
c ---[ 210]---> BDD-cost:   91
c ---[ 208]---> BDD-cost:  103
c ---[ 206]---> BDD-cost:   35
c ---[ 204]---> BDD-cost:  119
c ---[ 202]---> BDD-cost:  121
c ---[ 200]---> BDD-cost:  143
c ---[ 198]---> BDD-cost:  155
c ---[ 196]---> BDD-cost:    1
c ---[ 194]---> BDD-cost:  173
c ---[ 192]---> BDD-cost:  179
c ---[ 190]---> BDD-cost:  201
c ---[ 188]---> BDD-cost:  229
c ---[ 186]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:  233
c ---[ 182]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:  243
c ---[ 178]---> BDD-cost:  265
c ---[ 176]---> BDD-cost:  271
c ---[ 174]---> BDD-cost:  299
c ---[ 172]---> BDD-cost:  309
c ---[ 170]---> BDD-cost:  311
c ---[ 168]---> BDD-cost:  329
c ---[ 166]---> BDD-cost:  333
c ---[ 164]---> BDD-cost:  337
c ---[ 162]---> BDD-cost:  357
c ---[ 160]---> BDD-cost:  347
c ---[ 158]---> BDD-cost:  447
c ---[ 156]---> BDD-cost:  465
c ---[ 154]---> BDD-cost:  475
c ---[ 152]---> BDD-cost:  483
c ---[ 150]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:  551
c ---[ 146]---> BDD-cost:  553
c ---[ 144]---> BDD-cost:    1
c ---[ 142]---> BDD-cost:  651
c ---[ 140]---> BDD-cost:  667
c ---[ 138]---> BDD-cost:  673
c ---[ 136]---> BDD-cost:  699
c ---[ 134]---> BDD-cost:  821
c ---[ 132]---> BDD-cost:  831
c ---[ 130]---> BDD-cost:  863
c ---[ 128]---> BDD-cost:  945
c ---[ 126]---> BDD-cost: 1047
c ---[ 124]---> BDD-cost: 1097
c ---[ 122]---> BDD-cost: 1105
c ---[ 120]---> BDD-cost: 1131
c ---[ 118]---> BDD-cost: 1137
c ---[ 116]---> BDD-cost: 1137
c ---[ 114]---> BDD-cost: 1193
c ---[ 112]---> BDD-cost: 1263
c ---[ 110]---> BDD-cost: 1319
c ---[ 108]---> BDD-cost: 1343
c ---[ 106]---> BDD-cost: 1351
c ---[ 104]---> BDD-cost: 1355
c ---[ 102]---> BDD-cost: 1413
c ---[ 100]---> BDD-cost:    1
c ---[  98]---> BDD-cost: 1437
c ---[  96]---> BDD-cost: 1489
c ---[  94]---> BDD-cost: 1535
c ---[  92]---> BDD-cost: 1543
c ---[  90]---> BDD-cost:    1
c ---[  88]---> BDD-cost: 1587
c ---[  86]---> BDD-cost: 1657
c ---[  84]---> BDD-cost: 1825
c ---[  82]---> BDD-cost:    1
c ---[  80]---> BDD-cost: 1833
c ---[  78]---> BDD-cost:    1
c ---[  76]---> BDD-cost: 1851
c ---[  74]---> BDD-cost: 1861
c ---[  72]---> BDD-cost: 1881
c ---[  70]---> BDD-cost: 1785
c ---[  68]---> BDD-cost: 1941
c ---[  66]---> BDD-cost: 1957
c ---[  64]---> BDD-cost: 1973
c ---[  62]---> BDD-cost: 2037
c ---[  60]---> BDD-cost: 2113
c ---[  58]---> BDD-cost: 2289
c ---[  56]---> BDD-cost: 2339
c ---[  54]---> BDD-cost:    1
c ---[  52]---> BDD-cost: 2395
c ---[  50]---> BDD-cost: 2397
c ---[  48]---> BDD-cost: 2435
c ---[  46]---> BDD-cost: 2457
c ---[  44]---> BDD-cost: 2501
c ---[  42]---> BDD-cost: 2671
c ---[  40]---> BDD-cost:    1
c ---[  38]---> BDD-cost: 2675
c ---[  36]---> BDD-cost: 3389
c ---[  34]---> BDD-cost: 3405
c ---[  32]---> BDD-cost: 3429
c ---[  30]---> BDD-cost: 3517
c ---[  28]---> BDD-cost: 3591
c ---[  26]---> BDD-cost: 3621
c ---[  24]---> BDD-cost: 3783
c ---[  22]---> BDD-cost: 3829
c ---[  20]---> BDD-cost: 3945
c ---[  18]---> BDD-cost:    1
c ---[  16]---> BDD-cost: 4077
c ---[  14]---> BDD-cost: 4109
c ---[  12]---> BDD-cost: 4165
c ---[  10]---> BDD-cost: 4153
c ---[   8]---> BDD-cost: 4965
c ---[   6]---> BDD-cost: 5609
c ---[   4]---> BDD-cost: 5909
c ---[   2]---> BDD-cost: 7511
c ---[   0]---> BDD-cost: 7701
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  409612  1065070 |  122883       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/174509          
c   -- var.elim.:  2000/174509          
c   -- var.elim.:  3000/174509          
c   -- var.elim.:  4000/174509          
c   -- var.elim.:  5000/174509          
c   -- var.elim.:  6000/174509          
c   -- var.elim.:  7000/174509          
c   -- var.elim.:  8000/174509          
c   -- var.elim.:  9000/174509          
c   -- var.elim.:  10000/174509          
c   -- var.elim.:  11000/174509          
c   -- var.elim.:  12000/174509          
c   -- var.elim.:  13000/174509          
c   -- var.elim.:  14000/174509          
c   -- var.elim.:  15000/174509          
c   -- var.elim.:  16000/174509          
c   -- var.elim.:  17000/174509          
c   -- var.elim.:  18000/174509          
c   -- var.elim.:  19000/174509          
c   -- var.elim.:  20000/174509          
c   -- var.elim.:  21000/174509          
c   -- var.elim.:  22000/174509          
c   -- var.elim.:  23000/174509          
c   -- var.elim.:  24000/174509          
c   -- var.elim.:  25000/174509          
c   -- var.elim.:  26000/174509          
c   -- var.elim.:  27000/174509          
c   -- var.elim.:  28000/174509          
c   -- var.elim.:  29000/174509          
c   -- var.elim.:  30000/174509          
c   -- var.elim.:  31000/174509          
c   -- var.elim.:  32000/174509          
c   -- var.elim.:  33000/174509          
c   -- var.elim.:  34000/174509          
c   -- var.elim.:  35000/174509          
c   -- var.elim.:  36000/174509          
c   -- var.elim.:  37000/174509          
c   -- var.elim.:  38000/174509          
c   -- var.elim.:  39000/174509          
c   -- var.elim.:  40000/174509          
c   -- var.elim.:  41000/174509          
c   -- var.elim.:  42000/174509          
c   -- var.elim.:  43000/174509          
c   -- var.elim.:  44000/174509          
c   -- var.elim.:  45000/174509          
c   -- var.elim.:  46000/174509          
c   -- var.elim.:  47000/174509          
c   -- var.elim.:  48000/174509          
c   -- var.elim.:  49000/174509          
c   -- var.elim.:  50000/174509          
c   -- var.elim.:  51000/174509          
c   -- var.elim.:  52000/174509          
c   -- var.elim.:  53000/174509          
c   -- var.elim.:  54000/174509          
c   -- var.elim.:  55000/174509          
c   -- var.elim.:  56000/174509          
c   -- var.elim.:  57000/174509          
c   -- var.elim.:  58000/174509          
c   -- var.elim.:  59000/174509          
c   -- var.elim.:  60000/174509          
c   -- var.elim.:  61000/174509          
c   -- var.elim.:  62000/174509          
c   -- var.elim.:  63000/174509          
c   -- var.elim.:  64000/174509          
c   -- var.elim.:  65000/174509          
c   -- var.elim.:  66000/174509          
c   -- var.elim.:  67000/174509          
c   -- var.elim.:  68000/174509          
c   -- var.elim.:  69000/174509          
c   -- var.elim.:  70000/174509          
c   -- var.elim.:  71000/174509          
c   -- var.elim.:  72000/174509          
c   -- var.elim.:  73000/174509          
c   -- var.elim.:  74000/174509          
c   -- var.elim.:  75000/174509          
c   -- var.elim.:  76000/174509          
c   -- var.elim.:  77000/174509          
c   -- var.elim.:  78000/174509          
c   -- var.elim.:  79000/174509          
c   -- var.elim.:  80000/174509          
c   -- var.elim.:  81000/174509          
c   -- var.elim.:  82000/174509          
c   -- var.elim.:  83000/174509          
c   -- var.elim.:  84000/174509          
c   -- var.elim.:  85000/174509          
c   -- var.elim.:  86000/174509          
c   -- var.elim.:  87000/174509          
c   -- var.elim.:  88000/174509          
c   -- var.elim.:  89000/174509          
c   -- var.elim.:  90000/174509          
c   -- var.elim.:  91000/174509          
c   -- var.elim.:  92000/174509          
c   -- var.elim.:  93000/174509          
c   -- var.elim.:  94000/174509          
c   -- var.elim.:  95000/174509          
c   -- var.elim.:  96000/174509          
c   -- var.elim.:  97000/174509          
c   -- var.elim.:  98000/174509          
c   -- var.elim.:  99000/174509          
c   -- var.elim.:  100000/174509          
c   -- var.elim.:  101000/174509          
c   -- var.elim.:  102000/174509          
c   -- var.elim.:  103000/174509          
c   -- var.elim.:  104000/174509          
c   -- var.elim.:  105000/174509          
c   -- var.elim.:  106000/174509          
c   -- var.elim.:  107000/174509          
c   -- var.elim.:  108000/174509          
c   -- var.elim.:  109000/174509          
c   -- var.elim.:  110000/174509          
c   -- var.elim.:  111000/174509          
c   -- var.elim.:  112000/174509          
c   -- var.elim.:  113000/174509          
c   -- var.elim.:  114000/174509          
c   -- var.elim.:  115000/174509          
c   -- var.elim.:  116000/174509          
c   -- var.elim.:  117000/174509          
c   -- var.elim.:  118000/174509          
c   -- var.elim.:  119000/174509          
c   -- var.elim.:  120000/174509          
c   -- var.elim.:  121000/174509          
c   -- var.elim.:  122000/174509          
c   -- var.elim.:  123000/174509          
c   -- var.elim.:  124000/174509          
c   -- var.elim.:  125000/174509          
c   -- var.elim.:  126000/174509          
c   -- var.elim.:  127000/174509          
c   -- var.elim.:  128000/174509          
c   -- var.elim.:  129000/174509          
c   -- var.elim.:  130000/174509          
c   -- var.elim.:  131000/174509          
c   -- var.elim.:  132000/174509          
c   -- var.elim.:  133000/174509          
c   -- var.elim.:  134000/174509          
c   -- var.elim.:  135000/174509          
c   -- var.elim.:  136000/174509          
c   -- var.elim.:  137000/174509          
c   -- var.elim.:  138000/174509          
c   -- var.elim.:  139000/174509          
c   -- var.elim.:  140000/174509          
c   -- var.elim.:  141000/174509          
c   -- var.elim.:  142000/174509          
c   -- var.elim.:  143000/174509          
c   -- var.elim.:  144000/174509          
c   -- var.elim.:  145000/174509          
c   -- var.elim.:  146000/174509          
c   -- var.elim.:  147000/174509          
c   -- var.elim.:  148000/174509          
c   -- var.elim.:  149000/174509          
c   -- var.elim.:  150000/174509          
c   -- var.elim.:  151000/174509          
c   -- var.elim.:  152000/174509          
c   -- var.elim.:  153000/174509          
c   -- var.elim.:  154000/174509          
c   -- var.elim.:  155000/174509          
c   -- var.elim.:  156000/174509          
c   -- var.elim.:  157000/174509          
c   -- var.elim.:  158000/174509          
c   -- var.elim.:  159000/174509          
c   -- var.elim.:  160000/174509          
c   -- var.elim.:  161000/174509          
c   -- var.elim.:  162000/174509          
c   -- var.elim.:  163000/174509          
c   -- var.elim.:  164000/174509          
c   -- var.elim.:  165000/174509          
c   -- var.elim.:  166000/174509          
c   -- var.elim.:  167000/174509          
c   -- var.elim.:  168000/174509          
c   -- var.elim.:  169000/174509          
c   -- var.elim.:  170000/174509          
c   -- var.elim.:  171000/174509          
c   -- var.elim.:  172000/174509          
c   -- var.elim.:  173000/174509          
c   -- var.elim.:  174000/174509          
c   -- var.elim.:  174509/174509          
c   -- var.elim.:  688/688          
c   -- subsuming                       
c   -- var.elim.:  645/645          
c   -- var.elim.:  796/796          
c   -- subsuming                       
c   -- var.elim.:  635/635          
c   -- var.elim.:  289/289          
c   -- subsuming                       
c   -- var.elim.:  277/277          
c |         0 |  408989  1063078 |      --       0       --      -- |     --   | -601/-1574
c |         0 |  408989  1063078 |  163595       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 14.6128 s)
c ==============================================================================
c [1mFound solution: 190067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 98116   maxlim: 13558894   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        19 | 1095699  3515691 |  328709      19     8491   446.9 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/108881          
c   -- var.elim.:  2000/108881          
c   -- var.elim.:  3000/108881          
c   -- var.elim.:  4000/108881          
c   -- var.elim.:  5000/108881          
c   -- var.elim.:  6000/108881          
c   -- var.elim.:  7000/108881          
c   -- var.elim.:  8000/108881          
c   -- var.elim.:  9000/108881          
c   -- var.elim.:  10000/108881          
c   -- var.elim.:  11000/108881          
c   -- var.elim.:  12000/108881          
c   -- var.elim.:  13000/108881          
c   -- var.elim.:  14000/108881          
c   -- var.elim.:  15000/108881          
c   -- var.elim.:  16000/108881          
c   -- var.elim.:  17000/108881          
c   -- var.elim.:  18000/108881          
c   -- var.elim.:  19000/108881          
c   -- var.elim.:  20000/108881          
c   -- var.elim.:  21000/108881          
c   -- var.elim.:  22000/108881          
c   -- var.elim.:  23000/108881          
c   -- var.elim.:  24000/108881          
c   -- var.elim.:  25000/108881          
c   -- var.elim.:  26000/108881          
c   -- var.elim.:  27000/108881          
c   -- var.elim.:  28000/108881          
c   -- var.elim.:  29000/108881          
c   -- var.elim.:  30000/108881          
c   -- var.elim.:  31000/108881          
c   -- var.elim.:  32000/108881          
c   -- var.elim.:  33000/108881          
c   -- var.elim.:  34000/108881          
c   -- var.elim.:  35000/108881          
c   -- var.elim.:  36000/108881          
c   -- var.elim.:  37000/108881          
c   -- var.elim.:  38000/108881          
c   -- var.elim.:  39000/108881          
c   -- var.elim.:  40000/108881          
c   -- var.elim.:  41000/108881          
c   -- var.elim.:  42000/108881          
c   -- var.elim.:  43000/108881          
c   -- var.elim.:  44000/108881          
c   -- var.elim.:  45000/108881          
c   -- var.elim.:  46000/108881          
c   -- var.elim.:  47000/108881          
c   -- var.elim.:  48000/108881          
c   -- var.elim.:  49000/108881          
c   -- var.elim.:  50000/108881          
c   -- var.elim.:  51000/108881          
c   -- var.elim.:  52000/108881          
c   -- var.elim.:  53000/108881          
c   -- var.elim.:  54000/108881          
c   -- var.elim.:  55000/108881          
c   -- var.elim.:  56000/108881          
c   -- var.elim.:  57000/108881          
c   -- var.elim.:  58000/108881          
c   -- var.elim.:  59000/108881          
c   -- var.elim.:  60000/108881          
c   -- var.elim.:  61000/108881          
c   -- var.elim.:  62000/108881          
c   -- var.elim.:  63000/108881          
c   -- var.elim.:  64000/108881          
c   -- var.elim.:  65000/108881          
c   -- var.elim.:  66000/108881          
c   -- var.elim.:  67000/108881          
c   -- var.elim.:  68000/108881          
c   -- var.elim.:  69000/108881          
c   -- var.elim.:  70000/108881          
c   -- var.elim.:  71000/108881          
c   -- var.elim.:  72000/108881          
c   -- var.elim.:  73000/108881          
c   -- var.elim.:  74000/108881          
c   -- var.elim.:  75000/108881          
c   -- var.elim.:  76000/108881          
c   -- var.elim.:  77000/108881          
c   -- var.elim.:  78000/108881          
c   -- var.elim.:  79000/108881          
c   -- var.elim.:  80000/108881          
c   -- var.elim.:  81000/108881          
c   -- var.elim.:  82000/108881          
c   -- var.elim.:  83000/108881          
c   -- var.elim.:  84000/108881          
c   -- var.elim.:  85000/108881          
c   -- var.elim.:  86000/108881          
c   -- var.elim.:  87000/108881          
c   -- var.elim.:  88000/108881          
c   -- var.elim.:  89000/108881          
c   -- var.elim.:  90000/108881          
c   -- var.elim.:  91000/108881          
c   -- var.elim.:  92000/108881          
c   -- var.elim.:  93000/108881          
c   -- var.elim.:  94000/108881          
c   -- var.elim.:  95000/108881          
c   -- var.elim.:  96000/108881          
c   -- var.elim.:  97000/108881          
c   -- var.elim.:  98000/108881          
c   -- var.elim.:  99000/108881          
c   -- var.elim.:  100000/108881          
c   -- var.elim.:  101000/108881          
c   -- var.elim.:  102000/108881          
c   -- var.elim.:  103000/108881          
c   -- var.elim.:  104000/108881          
c   -- var.elim.:  105000/108881          
c   -- var.elim.:  106000/108881          
c   -- var.elim.:  107000/108881          
c   -- var.elim.:  108000/108881          
c   -- var.elim.:  108881/108881          
c   -- var.elim.:  82/82          
c |        19 | 1095557  3515113 |      --      19       --      -- |     --   | -133/-501
c |        19 | 1095557  3515113 |  438222      19     8491   446.9 |  0.000 % |
c |       119 | 1095557  3515113 |  482045     119    14092   118.4 |  0.055 % |
c |       270 | 1095557  3515113 |  530249     270    75197   278.5 |  0.055 % |
c |       495 | 1095546  3515062 |  583268     493    83266   168.9 |  0.055 % |
c |       832 | 1095546  3515062 |  641595     830    96741   116.6 |  0.055 % |
c |      1340 | 1095546  3515062 |  705755    1338   764846   571.6 |  0.055 % |
c |      2100 | 1095546  3515062 |  776330    2098   871873   415.6 |  0.055 % |
c |      3239 | 1095546  3515062 |  853963    3237  1823637   563.4 |  0.055 % |
c ==============================================================================
c (current CPU-time: 128.468 s)
c ==============================================================================
c [1mFound solution: 146243[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13602718   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3301 | 1095628  3515488 |  328688    3299  1830393   554.8 |  0.055 % |
c   -- subsuming                       
c   -- var.elim.:  102/102          
c   -- var.elim.:  25/25          
c |      3301 | 1095607  3515399 |      --    3299       --      -- |     --   | -21/-77
c |      3301 | 1095607  3515399 |  438242    3297  1830385   555.2 |  0.055 % |
c |      3404 | 1095607  3515399 |  482067    3400  1876985   552.1 |  0.060 % |
c |      3554 | 1095607  3515399 |  530273    3550  1905119   536.7 |  0.060 % |
c |      3779 | 1095607  3515399 |  583301    3775  2091832   554.1 |  0.060 % |
c |      4117 | 1095607  3515399 |  641631    4113  2129348   517.7 |  0.060 % |
c |      4623 | 1095607  3515399 |  705794    4619  2292831   496.4 |  0.060 % |
c |      5385 | 1095607  3515399 |  776373    5381  3716587   690.7 |  0.060 % |
c |      6526 | 1095598  3515364 |  854004    6520  5378123   824.9 |  0.060 % |
c |      8234 | 1095598  3515364 |  939404    8228  5811020   706.2 |  0.060 % |
c |     10796 | 1095598  3515364 | 1033345   10790  7089645   657.1 |  0.060 % |
c |     14644 | 1095598  3515364 | 1136679   14638 10831475   740.0 |  0.060 % |
c |     20410 | 1095598  3515364 | 1250347   20404 14294834   700.6 |  0.060 % |
c |     29059 | 1095552  3515196 | 1375324   29050 18295582   629.8 |  0.063 % |
c ==============================================================================
c (current CPU-time: 464.746 s)
c ==============================================================================
c [1mFound solution: 143873[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13605088   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     29572 | 1095578  3515363 |  328673   29563 19504830   659.8 |  0.063 % |
c   -- subsuming                       
c   -- var.elim.:  57/57          
c   -- var.elim.:  69/69          
c |     29572 | 1095499  3515078 |      --   29563       --      -- |     --   | -79/-279
c |     29572 | 1095499  3515078 |  438199   27606 18103025   655.8 |  0.063 % |
c |     29675 | 1095499  3515078 |  482019   27709 18171059   655.8 |  0.069 % |
c |     29826 | 1095499  3515078 |  530221   27860 18301056   656.9 |  0.069 % |
c |     30051 | 1095242  3514127 |  583106   28028 18324652   653.8 |  0.081 % |
c |     30391 | 1095242  3514127 |  641417   28368 18662671   657.9 |  0.081 % |
c |     30900 | 1095242  3514127 |  705559   28877 20646482   715.0 |  0.081 % |
c |     31660 | 1095242  3514127 |  776115   29637 21125436   712.8 |  0.081 % |
c |     32801 | 1095242  3514127 |  853726   30778 22101683   718.1 |  0.081 % |
c |     34509 | 1095242  3514127 |  939099   32486 25451533   783.5 |  0.081 % |
c |     37073 | 1095235  3514096 | 1033002   35049 30052934   857.5 |  0.082 % |
c |     40917 | 1095235  3514096 | 1136303   38893 32718698   841.2 |  0.082 % |
c |     46683 | 1095235  3514096 | 1249933   44659 44648128   999.8 |  0.082 % |
c ==============================================================================
c (current CPU-time: 1039.06 s)
c ==============================================================================
c [1mFound solution: 129955[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 13619006   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     47457 | 1095274  3514353 |  328582   45433 47615126  1048.0 |  0.082 % |
c   -- subsuming                       
c   -- var.elim.:  153/153          
c   -- var.elim.:  28/28          
c |     47457 | 1095188  3513900 |      --   45433       --      -- |     --   | -86/-442
c |     47457 | 1095188  3513900 |  438075   45313 47496953  1048.2 |  0.082 % |
c |     47559 | 1095188  3513900 |  481882   45415 47531067  1046.6 |  0.088 % |
c |     47709 | 1095061  3513454 |  530009   45548 47575437  1044.5 |  0.095 % |
c |     47934 | 1095061  3513454 |  583010   45773 47662434  1041.3 |  0.095 % |
c |     48272 | 1095030  3513347 |  641293   46106 47785906  1036.4 |  0.096 % |
c |     48778 | 1095030  3513347 |  705422   46612 47858981  1026.8 |  0.096 % |
c |     49548 | 1095030  3513347 |  775964   47382 51123892  1079.0 |  0.096 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 x1 -x2 x3 -x4 -x5 -x6 x7 -x8 -x9 -x10 -x11 -x12 x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 x47 x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 x792 -x793 -x794 -x795 -x796 -x797 x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 -x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 -x2150 -x2151 -x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 -x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 -x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 -x2260 -x2261 -x2262 -x2263 -x2264 -x2265 -x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 -x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 -x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 -x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 -x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 -x2609 -x2610 -x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 -x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 -x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 -x2663 -x2664 -x2665 -x2666 -x2667 -x2668 -x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 -x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 -x2701 -x2702 -x2703 -x2704 -x2705 -x2706 -x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 -x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 -x2759 -x2760 -x2761 -x2762 -x2763 -x2764 -x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 -x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 -x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 -x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 -x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 -x2915 -x2916 -x2917 -x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 -x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 -x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 -x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 -x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 -x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 -x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 -x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 -x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 -x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 -x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 -x3406 -x3407 -x3408 -x3409 -x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 -x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 -x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 -x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 -x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 -x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 -x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 -x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 -x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 -x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 -x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 -x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 -x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x4273 -x4274 -x4275 -x4276 -x4277 -x4278 -x4279 -x4280 -x4281 -x4282 -x4283 -x4284 -x4285 -x4286 -x4287 -x4288 -x4289 -x4290 -x4291 -x4292 -x4293 -x4294 -x4295 -x4296 -x4297 -x4298 -x4299 -x4300 -x4301 -x4302 -x4303 -x4304 -x4305 -x4306 -x4307 -x4308 -x4309 -x4310 -x4311 -x4312 -x4313 -x4314 -x4315 -x4316 -x4317 -x4318 -x4319 -x4320 -x4321 -x4322 -x4323 -x4324 -x4325 -x4326 -x4327 -x4328 -x4329 -x4330 -x4331 -x4332 -x4333 -x4334 -x4335 -x4336 -x4337 -x4338 -x4339 -x4340 -x4341 -x4342 -x4343 -x4344 -x4345 -x4346 -x4347 -x4348 -x4349 -x4350 -x4351 -x4352 -x4353 -x4354 -x4355 -x4356 -x4357 -x4358 -x4359 -x4360 -x4361 -x4362 -x4363 -x4364 -x4365 -x4366 -x4367 -x4368 -x4369 -x4370 -x4371 -x4372 -x4373 -x4374 -x4375 -x4376 -x4377 -x4378 -x4379 -x4380 -x4381 -x4382 -x4383 -x4384 -x4385 -x4386 -x4387 -x4388 -x4389 -x4390 -x4391 -x4392 -x4393 -x4394 -x4395 -x4396 -x4397 -x4398 -x4399 -x4400 -x4401 -x4402 -x4403 -x4404 -x4405 -x4406 -x4407 -x4408 -x4409 -x4410 -x4411 -x4412 -x4413 -x4414 -x4415 -x4416 -x4417 -x4418 -x4419 -x4420 -x4421 -x4422 -x4423 -x4424 -x4425 -x4426 -x4427 -x4428 -x4429 -x4430 -x4431 -x4432 -x4433 -x4434 -x4435 -x4436 -x4437 -x4438 -x4439 -x4440 -x4441 -x4442 -x4443 -x4444 -x4445 -x4446 -x4447 -x4448 -x4449 -x4450 -x4451 -x4452 -x4453 -x4454 -x4455 -x4456 -x4457 -x4458 -x4459 -x4460 -x4461 -x4462 -x4463 -x4464 -x4465 -x4466 -x4467 -x4468 -x4469 -x4470 -x4471 -x4472 -x4473 -x4474 -x4475 -x4476 -x4477 -x4478 -x4479 -x4480 -x4481 -x4482 -x4483 -x4484 -x4485 -x4486 -x4487 -x4488 -x4489 -x4490 -x4491 -x4492 -x4493 -x4494 -x4495 -x4496 -x4497 -x4498 -x4499 -x4500 -x4501 -x4502 -x4503 -x4504 -x4505 -x4506 -x4507 -x4508 -x4509 -x4510 -x4511 -x4512 -x4513 -x4514 -x4515 -x4516 -x4517 -x4518 -x4519 -x4520 -x4521 -x4522 -x4523 -x4524 -x4525 -x4526 -x4527 -x4528 -x4529 -x4530 -x4531 -x4532 -x4533 -x4534 -x4535 -x4536 -x4537 -x4538 -x4539 -x4540 -x4541 -x4542 -x4543 -x4544 -x4545 -x4546 -x4547 -x4548 -x4549 -x4550 -x4551 -x4552 -x4553 -x4554 -x4555 -x4556 -x4557 -x4558 -x4559 -x4560 -x4561 -x4562 -x4563 -x4564 -x4565 -x4566 -x4567 -x4568 -x4569 -x4570 -x4571 -x4572 -x4573 -x4574 -x4575 -x4576 -x4577 -x4578 -x4579 -x4580 -x4581 -x4582 -x4583 -x4584 -x4585 -x4586 -x4587 -x4588 -x4589 -x4590 -x4591 -x4592 -x4593 -x4594 -x4595 -x4596 -x4597 -x4598 -x4599 -x4600 -x4601 -x4602 -x4603 -x4604 -x4605 -x4606 -x4607 -x4608 -x4609 -x4610 -x4611 -x4612 -x4613 -x4614 -x4615 -x4616 -x4617 -x4618 -x4619 -x4620 -x4621 -x4622 -x4623 -x4624 -x4625 -x4626 -x4627 -x4628 -x4629 -x4630 -x4631 -x4632 -x4633 -x4634 -x4635 -x4636 -x4637 -x4638 -x4639 -x4640 -x4641 -x4642 -x4643 -x4644 -x4645 -x4646 -x4647 -x4648 -x4649 -x4650 -x4651 -x4652 -x4653 -x4654 -x4655 -x4656 -x4657 -x4658 -x4659 -x4660 -x4661 -x4662 -x4663 -x4664 -x4665 -x4666 -x4667 -x4668 -x4669 -x4670 -x4671 -x4672 -x4673 -x4674 -x4675 -x4676 -x4677 -x4678 -x4679 -x4680 -x4681 -x4682 -x4683 -x4684 -x4685 -x4686 -x4687 -x4688 -x4689 -x4690 -x4691 -x4692 -x4693 -x4694 -x4695 -x4696 -x4697 -x4698 -x4699 -x4700 -x4701 -x4702 -x4703 -x4704 -x4705 -x4706 -x4707 -x4708 -x4709 -x4710 -x4711 -x4712 -x4713 -x4714 -x4715 -x4716 -x4717 -x4718 -x4719 -x4720 -x4721 -x4722 -x4723 -x4724 -x4725 -x4726 -x4727 -x4728 -x4729 -x4730 -x4731 -x4732 -x4733 -x4734 -x4735 -x4736 -x4737 -x4738 -x4739 -x4740 -x4741 -x4742 -x4743 -x4744 -x4745 -x4746 -x4747 -x4748 -x4749 -x4750 -x4751 -x4752 -x4753 -x4754 -x4755 -x4756 -x4757 -x4758 -x4759 -x4760 -x4761 -x4762 -x4763 -x4764 -x4765 -x4766 -x4767 -x4768 -x4769 -x4770 -x4771 -x4772 -x4773 -x4774 -x4775 -x4776 -x4777 -x4778 -x4779 -x4780 -x4781 -x4782 -x4783 -x4784 -x4785 -x4786 -x4787 -x4788 -x4789 -x4790 -x4791 -x4792 -x4793 -x4794 -x4795 -x4796 -x4797 -x4798 -x4799 -x4800 -x4801 -x4802 -x4803 -x4804 -x4805 -x4806 -x4807 -x4808 -x4809 -x4810 -x4811 -x4812 -x4813 -x4814 -x4815 -x4816 -x4817 -x4818 -x4819 -x4820 -x4821 -x4822 -x4823 -x4824 -x4825 -x4826 -x4827 -x4828 -x4829 -x4830 -x4831 -x4832 -x4833 -x4834 -x4835 -x4836 -x4837 -x4838 -x4839 -x4840 -x4841 -x4842 -x4843 -x4844 -x4845 -x4846 -x4847 -x4848 -x4849 -x4850 -x4851 -x4852 -x4853 -x4854 -x4855 -x4856 -x4857 -x4858 -x4859 -x4860 -x4861 -x4862 -x4863 -x4864 -x4865 -x4866 -x4867 -x4868 -x4869 -x4870 -x4871 -x4872 -x4873 -x4874 -x4875 -x4876 -x4877 -x4878 -x4879 -x4880 -x4881 -x4882 -x4883 -x4884 -x4885 -x4886 -x4887 -x4888 -x4889 -x4890 -x4891 -x4892 -x4893 -x4894 -x4895 -x4896 -x4897 -x4898 -x4899 -x4900 -x4901 -x4902 -x4903 -x4904 -x4905 -x4906 -x4907 -x4908 -x4909 -x4910 -x4911 -x4912 -x4913 -x4914 -x4915 -x4916 -x4917 -x4918 -x4919 -x4920 -x4921 -x4922 -x4923 -x4924 -x4925 -x4926 -x4927 -x4928 -x4929 -x4930 -x4931 -x4932 -x4933 -x4934 -x4935 -x4936 -x4937 -x4938 -x4939 -x4940 -x4941 -x4942 -x4943 -x4944 -x4945 -x4946 -x4947 -x4948 -x4949 -x4950 -x4951 -x4952 -x4953 -x4954 -x4955 -x4956 -x4957 -x4958 -x4959 -x4960 -x4961 -x4962 -x4963 -x4964 -x4965 -x4966 -x4967 -x4968 -x4969 -x4970 -x4971 -x4972 -x4973 -x4974 -x4975 -x4976 -x4977 -x4978 -x4979 -x4980 -x4981 -x4982 -x4983 -x4984 -x4985 -x4986 -x4987 -x4988 -x4989 -x4990 -x4991 -x4992 -x4993 -x4994 -x4995 -x4996 -x4997 -x4998 -x4999 -x5000 -x5001 -x5002 -x5003 -x5004 -x5005 -x5006 -x5007 -x5008 -x5009 -x5010 -x5011 x5012 -x5013 -x5014 -x5015 -x5016 -x5017 -x5018 -x5019 -x5020 -x5021 -x5022 -x5023 -x5024 -x5025 -x5026 -x5027 -x5028 -x5029 -x5030 -x5031 -x5032 -x5033 -x5034 -x5035 -x5036 -x5037 -x5038 -x5039 -x5040 -x5041 -x5042 -x5043 -x5044 -x5045 -x5046 -x5047 -x5048 -x5049 -x5050 -x5051 -x5052 -x5053 -x5054 -x5055 -x5056 -x5057 -x5058 -x5059 -x5060 -x5061 -x5062 -x5063 -x5064 -x5065 -x5066 -x5067 -x5068 -x5069 -x5070 -x5071 -x5072 -x5073 -x5074 -x5075 -x5076 -x5077 -x5078 -x5079 -x5080 -x5081 -x5082 -x5083 -x5084 -x5085 -x5086 -x5087 -x5088 -x5089 -x5090 -x5091 -x5092 -x5093 -x5094 -x5095 -x5096 -x5097 -x5098 -x5099 -x5100 -x5101 -x5102 -x5103 -x5104 -x5105 -x5106 -x5107 -x5108 -x5109 -x5110 -x5111 -x5112 -x5113 -x5114 -x5115 -x5116 -x5117 -x5118 -x5119 -x5120 -x5121 -x5122 -x5123 -x5124 -x5125 -x5126 -x5127 -x5128 -x5129 -x5130 -x5131 -x5132 -x5133 -x5134 -x5135 -x5136 -x5137 -x5138 -x5139 -x5140 -x5141 -x5142 -x5143 -x5144 -x5145 -x5146 -x5147 -x5148 -x5149 -x5150 -x5151 -x5152 -x5153 -x5154 -x5155 -x5156 -x5157 -x5158 -x5159 -x5160 -x5161 -x5162 -x5163 -x5164 -x5165 -x5166 -x5167 -x5168 -x5169 -x5170 -x5171 -x5172 -x5173 -x5174 -x5175 -x5176 -x5177 -x5178 -x5179 -x5180 -x5181 -x5182 -x5183 -x5184 -x5185 -x5186 -x5187 -x5188 -x5189 -x5190 -x5191 -x5192 -x5193 -x5194 -x5195 -x5196 -x5197 -x5198 -x5199 -x5200 -x5201 -x5202 -x5203 -x5204 -x5205 -x5206 -x5207 -x5208 -x5209 -x5210 -x5211 -x5212 -x5213 -x5214 -x5215 -x5216 -x5217 -x5218 -x5219 -x5220 -x5221 -x5222 -x5223 -x5224 -x5225 -x5226 -x5227 -x5228 -x5229 -x5230 -x5231 -x5232 -x5233 -x5234 -x5235 -x5236 -x5237 -x5238 -x5239 -x5240 -x5241 -x5242 -x5243 -x5244 -x5245 -x5246 -x5247 -x5248 -x5249 -x5250 -x5251 -x5252 -x5253 -x5254 -x5255 -x5256 -x5257 -x5258 -x5259 -x5260 -x5261 -x5262 -x5263 -x5264 -x5265 -x5266 -x5267 -x5268 -x5269 -x5270 -x5271 -x5272 -x5273 -x5274 -x5275 -x5276 -x5277 -x5278 -x5279 -x5280 -x5281 -x5282 -x5283 -x5284 -x5285 -x5286 -x5287 -x5288 -x5289 -x5290 -x5291 -x5292 -x5293 -x5294 -x5295 -x5296 -x5297 -x5298 -x5299 -x5300 -x5301 -x5302 -x5303 -x5304 -x5305 -x5306 -x5307 -x5308 -x5309 -x5310 -x5311 -x5312 -x5313 -x5314 -x5315 -x5316 -x5317 -x5318 -x5319 -x5320 -x5321 -x5322 -x5323 -x5324 -x5325 -x5326 -x5327 -x5328 -x5329 -x5330 -x5331 -x5332 -x5333 -x5334 -x5335 -x5336 -x5337 -x5338 -x5339 -x5340 -x5341 -x5342 x5343 -x5344 -x5345 -x5346 -x5347 -x5348 -x5349 -x5350 -x5351 -x5352 -x5353 -x5354 -x5355 -x5356 -x5357 -x5358 -x5359 -x5360 -x5361 -x5362 -x5363 -x5364 -x5365 -x5366 -x5367 -x5368 -x5369 -x5370 -x5371 -x5372 -x5373 -x5374 -x5375 -x5376 -x5377 -x5378 -x5379 -x5380 -x5381 -x5382 -x5383 -x5384 -x5385 -x5386 -x5387 -x5388 -x5389 -x5390 -x5391 -x5392 -x5393 -x5394 -x5395 -x5396 -x5397 -x5398 -x5399 -x5400 -x5401 -x5402 -x5403 -x5404 -x5405 -x5406 -x5407 -x5408 -x5409 -x5410 -x5411 -x5412 -x5413 -x5414 -x5415 -x5416 -x5417 -x5418 -x5419 -x5420 -x5421 -x5422 -x5423 -x5424 -x5425 -x5426 -x5427 -x5428 -x5429 -x5430 -x5431 -x5432 -x5433 -x5434 -x5435 -x5436 -x5437 -x5438 -x5439 -x5440 -x5441 -x5442 -x5443 -x5444 -x5445 -x5446 -x5447 -x5448 -x5449 -x5450 -x5451 -x5452 -x5453 -x5454 -x5455 -x5456 -x5457 -x5458 -x5459 -x5460 -x5461 -x5462 -x5463 -x5464 -x5465 -x5466 -x5467 -x5468 -x5469 -x5470 -x5471 -x5472 -x5473 -x5474 -x5475 -x5476 -x5477 -x5478 -x5479 -x5480 -x5481 -x5482 -x5483 -x5484 -x5485 -x5486 -x5487 -x5488 -x5489 -x5490 -x5491 -x5492 -x5493 -x5494 -x5495 -x5496 -x5497 -x5498 -x5499 -x5500 -x5501 -x5502 -x5503 -x5504 -x5505 -x5506 -x5507 -x5508 -x5509 -x5510 -x5511 -x5512 -x5513 -x5514 -x5515 -x5516 -x5517 -x5518 -x5519 -x5520 -x5521 -x5522 -x5523 -x5524 -x5525 -x5526 -x5527 -x5528 -x5529 -x5530 -x5531 -x5532 -x5533 -x5534 -x5535 -x5536 -x5537 -x5538 -x5539 -x5540 -x5541 -x5542 -x5543 -x5544 -x5545 -x5546 -x5547 -x5548 -x5549 -x5550 -x5551 -x5552 -x5553 -x5554 -x5555 -x5556 -x5557 -x5558 -x5559 -x5560 -x5561 -x5562 -x5563 -x5564 -x5565 -x5566 -x5567 -x5568 -x5569 -x5570 -x5571 -x5572 -x5573 -x5574 -x5575 -x5576 -x5577 -x5578 -x5579 -x5580 -x5581 -x5582 -x5583 -x5584 -x5585 -x5586 -x5587 -x5588 -x5589 -x5590 -x5591 -x5592 -x5593 -x5594 -x5595 -x5596 -x5597 -x5598 -x5599 -x5600 -x5601 -x5602 -x5603 -x5604 -x5605 -x5606 -x5607 -x5608 -x5609 -x5610 -x5611 -x5612 -x5613 -x5614 -x5615 -x5616 -x5617 -x5618 -x5619 -x5620 -x5621 -x5622 -x5623 -x5624 -x5625 -x5626 -x5627 -x5628 -x5629 -x5630 -x5631 -x5632 -x5633 -x5634 -x5635 -x5636 -x5637 -x5638 -x5639 -x5640 -x5641 -x5642 -x5643 -x5644 -x5645 -x5646 -x5647 -x5648 -x5649 -x5650 -x5651 -x5652 -x5653 -x5654 -x5655 -x5656 -x5657 -x5658 -x5659 -x5660 -x5661 -x5662 -x5663 -x5664 -x5665 -x5666 -x5667 -x5668 -x5669 -x5670 -x5671 -x5672 -x5673 -x5674 -x5675 -x5676 -x5677 -x5678 -x5679 -x5680 -x5681 -x5682 -x5683 -x5684 -x5685 -x5686 -x5687 -x5688 -x5689 -x5690 -x5691 -x5692 -x5693 -x5694 -x5695 -x5696 -x5697 -x5698 -x5699 -x5700 -x5701 -x5702 -x5703 -x5704 -x5705 -x5706 -x5707 -x5708 -x5709 -x5710 -x5711 -x5712 -x5713 -x5714 -x5715 -x5716 -x5717 -x5718 -x5719 -x5720 -x5721 -x5722 -x5723 -x5724 -x5725 -x5726 -x5727 -x5728 -x5729 -x5730 -x5731 -x5732 -x5733 -x5734 -x5735 -x5736 -x5737 -x5738 -x5739 -x5740 -x5741 -x5742 -x5743 -x5744 -x5745 -x5746 -x5747 -x5748 -x5749 -x5750 -x5751 -x5752 -x5753 -x5754 -x5755 -x5756 -x5757 -x5758 -x5759 -x5760 -x5761 -x5762 -x5763 -x5764 -x5765 -x5766 -x5767 -x5768 -x5769 -x5770 -x5771 -x5772 -x5773 -x5774 -x5775 -x5776 -x5777 -x5778 -x5779 -x5780 -x5781 -x5782 -x5783 -x5784 -x5785 -x5786 -x5787 -x5788 -x5789 -x5790 -x5791 -x5792 -x5793 -x5794 -x5795 -x5796 -x5797 -x5798 -x5799 -x5800 -x5801 -x5802 -x5803 -x5804 -x5805 -x5806 -x5807 -x5808 -x5809 -x5810 -x5811 -x5812 -x5813 -x5814 -x5815 -x5816 -x5817 -x5818 -x5819 -x5820 -x5821 -x5822 -x5823 -x5824 -x5825 -x5826 -x5827 -x5828 -x5829 -x5830 -x5831 -x5832 -x5833 -x5834 -x5835 -x5836 -x5837 -x5838 -x5839 -x5840 -x5841 -x5842 -x5843 -x5844 -x5845 -x5846 -x5847 -x5848 -x5849 -x5850 -x5851 -x5852 -x5853 -x5854 -x5855 -x5856 -x5857 -x5858 -x5859 -x5860 -x5861 -x5862 -x5863 -x5864 -x5865 -x5866 -x5867 -x5868 -x5869 -x5870 -x5871 -x5872 -x5873 -x5874 -x5875 -x5876 -x5877 -x5878 -x5879 -x5880 -x5881 -x5882 -x5883 -x5884 -x5885 -x5886 -x5887 -x5888 -x5889 -x5890 -x5891 -x5892 -x5893 -x5894 -x5895 -x5896 -x5897 -x5898 -x5899 -x5900 -x5901 -x5902 -x5903 -x5904 -x5905 -x5906 -x5907 -x5908 -x5909 -x5910 -x5911 -x5912 -x5913 -x5914 -x5915 -x5916 -x5917 -x5918 -x5919 -x5920 -x5921 -x5922 -x5923 -x5924 -x5925 -x5926 -x5927 -x5928 -x5929 -x5930 -x5931 -x5932 -x5933 -x5934 -x5935 -x5936 -x5937 -x5938 -x5939 -x5940 -x5941 -x5942 -x5943 -x5944 -x5945 -x5946 -x5947 -x5948 -x5949 -x5950 -x5951 -x5952 -x5953 -x5954 -x5955 -x5956 -x5957 -x5958 -x5959 -x5960 -x5961 -x5962 -x5963 -x5964 -x5965 -x5966 -x5967 -x5968 -x5969 -x5970 -x5971 -x5972 -x5973 -x5974 -x5975 -x5976 -x5977 -x5978 -x5979 -x5980 -x5981 -x5982 -x5983 -x5984 -x5985 -x5986 -x5987 -x5988 -x5989 -x5990 -x5991 -x5992 -x5993 -x5994 -x5995 -x5996 -x5997 -x5998 -x5999 -x6000 -x6001 -x6002 -x6003 -x6004 -x6005 -x6006 -x6007 -x6008 -x6009 -x6010 -x6011 -x6012 -x6013 -x6014 -x6015 -x6016 -x6017 -x6018 -x6019 -x6020 -x6021 -x6022 -x6023 -x6024 -x6025 -x6026 -x6027 -x6028 -x6029 -x6030 -x6031 -x6032 -x6033 -x6034 -x6035 -x6036 -x6037 -x6038 -x6039 -x6040 -x6041 -x6042 -x6043 -x6044 -x6045 -x6046 -x6047 -x6048 -x6049 -x6050 -x6051 -x6052 -x6053 -x6054 -x6055 -x6056 -x6057 -x6058 -x6059 -x6060 -x6061 -x6062 -x6063 -x6064 -x6065 -x6066 -x6067 -x6068 -x6069 -x6070 -x6071 -x6072 -x6073 -x6074 -x6075 -x6076 -x6077 -x6078 -x6079 -x6080 -x6081 -x6082 -x6083 -x6084 -x6085 -x6086 -x6087 -x6088 -x6089 -x6090 -x6091 -x6092 -x6093 -x6094 -x6095 -x6096 -x6097 -x6098 -x6099 -x6100 -x6101 -x6102 -x6103 -x6104 -x6105 -x6106 -x6107 -x6108 -x6109 -x6110 -x6111 -x6112 -x6113 -x6114 -x6115 -x6116 -x6117 -x6118 -x6119 -x6120 -x6121 -x6122 -x6123 -x6124 -x6125 -x6126 -x6127 -x6128 -x6129 -x6130 -x6131 -x6132 -x6133 -x6134 -x6135 -x6136 -x6137 -x6138 -x6139 -x6140 -x6141 -x6142 -x6143 -x6144 -x6145 -x6146 -x6147 -x6148 -x6149 -x6150 -x6151 -x6152 -x6153 -x6154 -x6155 -x6156 -x6157 -x6158 -x6159 -x6160 -x6161 -x6162 -x6163 -x6164 -x6165 -x6166 -x6167 -x6168 -x6169 -x6170 -x6171 -x6172 -x6173 -x6174 -x6175 -x6176 -x6177 -x6178 -x6179 -x6180 -x6181 -x6182 -x6183 -x6184 -x6185 -x6186 -x6187 -x6188 -x6189 -x6190 -x6191 -x6192 -x6193 -x6194 -x6195 -x6196 -x6197 -x6198 -x6199 -x6200 -x6201 -x6202 -x6203 -x6204 -x6205 -x6206 -x6207 -x6208 -x6209 -x6210 -x6211 -x6212 -x6213 -x6214 -x6215 -x6216 -x6217 -x6218 -x6219 -x6220 -x6221 -x6222 -x6223 -x6224 -x6225 -x6226 -x6227 -x6228 -x6229 -x6230 -x6231 -x6232 -x6233 -x6234 -x6235 -x6236 -x6237 -x6238 -x6239 -x6240 -x6241 -x6242 -x6243 -x6244 -x6245 -x6246 -x6247 -x6248 -x6249 -x6250 -x6251 -x6252 -x6253 -x6254 -x6255 -x6256 -x6257 -x6258 -x6259 -x6260 -x6261 -x6262 -x6263 -x6264 -x6265 -x6266 -x6267 -x6268 -x6269 -x6270 -x6271 -x6272 -x6273 -x6274 -x6275 -x6276 -x6277 -x6278 -x6279 -x6280 -x6281 -x6282 -x6283 -x6284 -x6285 -x6286 -x6287 -x6288 -x6289 -x6290 -x6291 -x6292 -x6293 -x6294 -x6295 -x6296 -x6297 -x6298 -x6299 -x6300 -x6301 -x6302 -x6303 -x6304 -x6305 -x6306 -x6307 -x6308 -x6309 -x6310 -x6311 -x6312 -x6313 -x6314 -x6315 -x6316 -x6317 -x6318 -x6319 -x6320 -x6321 -x6322 -x6323 -x6324 -x6325 -x6326 -x6327 -x6328 -x6329 -x6330 -x6331 -x6332 -x6333 -x6334 -x6335 -x6336 -x6337 -x6338 -x6339 -x6340 -x6341 -x6342 -x6343 -x6344 -x6345 -x6346 -x6347 -x6348 -x6349 -x6350 -x6351 -x6352 -x6353 -x6354 -x6355 -x6356 -x6357 -x6358 -x6359 -x6360 -x6361 -x6362 -x6363 -x6364 -x6365 -x6366 -x6367 -x6368 -x6369 -x6370 -x6371 -x6372 -x6373 -x6374 -x6375 -x6376 -x6377 -x6378 -x6379 -x6380 -x6381 -x6382 -x6383 -x6384 -x6385 -x6386 -x6387 -x6388 -x6389 -x6390 -x6391 -x6392 -x6393 -x6394 -x6395 -x6396 -x6397 -x6398 -x6399 -x6400 -x6401 -x6402 -x6403 -x6404 -x6405 -x6406 -x6407 -x6408 -x6409 -x6410 -x6411 -x6412 -x6413 -x6414 -x6415 -x6416 -x6417 -x6418 -x6419 -x6420 -x6421 -x6422 -x6423 -x6424 -x6425 -x6426 -x6427 -x6428 -x6429 -x6430 -x6431 -x6432 -x6433 -x6434 -x6435 -x6436 -x6437 -x6438 -x6439 -x6440 -x6441 x6442 -x6443 -x6444 -x6445 -x6446 -x6447 -x6448 -x6449 -x6450 -x6451 -x6452 -x6453 -x6454 -x6455 -x6456 -x6457 -x6458 -x6459 -x6460 -x6461 -x6462 -x6463 -x6464 -x6465 -x6466 -x6467 -x6468 -x6469 -x6470 -x6471 -x6472 -x6473 -x6474 -x6475 -x6476 -x6477 -x6478 -x6479 -x6480 -x6481 -x6482 -x6483 -x6484 -x6485 -x6486 -x6487 -x6488 -x6489 -x6490 -x6491 -x6492 -x6493 -x6494 -x6495 -x6496 -x6497 -x6498 -x6499 -x6500 -x6501 -x6502 -x6503 -x6504 -x6505 -x6506 -x6507 -x6508 -x6509 -x6510 -x6511 -x6512 -x6513 -x6514 -x6515 -x6516 -x6517 -x6518 -x6519 -x6520 -x6521 -x6522 -x6523 -x6524 -x6525 -x6526 -x6527 -x6528 -x6529 -x6530 -x6531 -x6532 -x6533 -x6534 -x6535 -x6536 -x6537 -x6538 -x6539 -x6540 -x6541 -x6542 -x6543 -x6544 -x6545 -x6546 -x6547 -x6548 -x6549 -x6550 -x6551 -x6552 -x6553 -x6554 -x6555 -x6556 -x6557 -x6558 -x6559 -x6560 -x6561 -x6562 -x6563 -x6564 -x6565 -x6566 -x6567 -x6568 -x6569 -x6570 -x6571 -x6572 -x6573 -x6574 -x6575 -x6576 -x6577 -x6578 -x6579 -x6580 -x6581 -x6582 -x6583 -x6584 -x6585 -x6586 -x6587 -x6588 -x6589 -x6590 -x6591 -x6592 -x6593 -x6594 -x6595 -x6596 -x6597 -x6598 -x6599 -x6600 -x6601 -x6602 -x6603 -x6604 -x6605 -x6606 -x6607 -x6608 -x6609 -x6610 -x6611 -x6612 -x6613 -x6614 -x6615 -x6616 -x6617 -x6618 -x6619 -x6620 -x6621 -x6622 -x6623 -x6624 -x6625 -x6626 -x6627 -x6628 -x6629 -x6630 -x6631 -x6632 -x6633 -x6634 -x6635 -x6636 -x6637 -x6638 -x6639 -x6640 -x6641 -x6642 -x6643 -x6644 -x6645 -x6646 -x6647 -x6648 -x6649 -x6650 -x6651 -x6652 -x6653 -x6654 -x6655 -x6656 -x6657 -x6658 -x6659 -x6660 -x6661 -x6662 -x6663 -x6664 -x6665 -x6666 -x6667 -x6668 -x6669 -x6670 -x6671 -x6672 -x6673 -x6674 -x6675 -x6676 -x6677 -x6678 -x6679 -x6680 -x6681 -x6682 -x6683 -x6684 -x6685 -x6686 -x6687 -x6688 -x6689 -x6690 -x6691 -x6692 -x6693 -x6694 -x6695 -x6696 -x6697 -x6698 -x6699 -x6700 -x6701 -x6702 -x6703 -x6704 -x6705 -x6706 -x6707 -x6708 -x6709 -x6710 -x6711 -x6712 -x6713 -x6714 -x6715 -x6716 -x6717 -x6718 -x6719 -x6720 -x6721 -x6722 -x6723 -x6724 -x6725 -x6726 -x6727 -x6728 -x6729 -x6730 -x6731 -x6732 -x6733 -x6734 -x6735 -x6736 -x6737 -x6738 -x6739 -x6740 -x6741 -x6742 -x6743 -x6744 -x6745 -x6746 -x6747 -x6748 -x6749 -x6750 -x6751 -x6752 -x6753 -x6754 -x6755 -x6756 -x6757 -x6758 -x6759 -x6760 -x6761 -x6762 -x6763 -x6764 -x6765 -x6766 -x6767 -x6768 -x6769 -x6770 -x6771 -x6772 -x6773 -x6774 -x6775 -x6776 -x6777 -x6778 -x6779 -x6780 -x6781 -x6782 -x6783 -x6784 -x6785 -x6786 -x6787 -x6788 -x6789 -x6790 -x6791 -x6792 -x6793 -x6794 -x6795 -x6796 -x6797 -x6798 -x6799 -x6800 -x6801 -x6802 -x6803 -x6804 -x6805 -x6806 -x6807 -x6808 -x6809 -x6810 -x6811 -x6812 -x6813 -x6814 -x6815 -x6816 -x6817 -x6818 -x6819 -x6820 -x6821 -x6822 -x6823 -x6824 -x6825 -x6826 -x6827 -x6828 -x6829 -x6830 -x6831 -x6832 -x6833 -x6834 -x6835 -x6836 -x6837 -x6838 -x6839 -x6840 -x6841 -x6842 -x6843 -x6844 -x6845 -x6846 -x6847 -x6848 -x6849 -x6850 -x6851 -x6852 -x6853 -x6854 -x6855 -x6856 -x6857 -x6858 -x6859 -x6860 -x6861 -x6862 -x6863 -x6864 -x6865 -x6866 -x6867 -x6868 -x6869 -x6870 -x6871 -x6872 -x6873 -x6874 -x6875 -x6876 -x6877 -x6878 -x6879 -x6880 -x6881 -x6882 -x6883 -x6884 -x6885 -x6886 -x6887 -x6888 -x6889 -x6890 -x6891 -x6892 -x6893 -x6894 -x6895 -x6896 -x6897 -x6898 -x6899 -x6900 -x6901 -x6902 -x6903 -x6904 -x6905 -x6906 -x6907 -x6908 -x6909 -x6910 -x6911 -x6912 -x6913 -x6914 -x6915 -x6916 -x6917 -x6918 -x6919 -x6920 -x6921 -x6922 -x6923 -x6924 -x6925 -x6926 -x6927 -x6928 -x6929 -x6930 -x6931 -x6932 -x6933 -x6934 -x6935 -x6936 -x6937 -x6938 -x6939 -x6940 -x6941 -x6942 -x6943 -x6944 -x6945 -x6946 -x6947 -x6948 -x6949 -x6950 -x6951 -x6952 -x6953 -x6954 -x6955 -x6956 -x6957 -x6958 -x6959 -x6960 -x6961 -x6962 -x6963 -x6964 -x6965 -x6966 -x6967 -x6968 -x6969 -x6970 -x6971 -x6972 -x6973 -x6974 -x6975 -x6976 -x6977 -x6978 -x6979 -x6980 -x6981 -x6982 -x6983 -x6984 -x6985 -x6986 -x6987 -x6988 -x6989 -x6990 -x6991 -x6992 -x6993 -x6994 -x6995 -x6996 -x6997 -x6998 -x6999 -x7000 -x7001 -x7002 -x7003 -x7004 -x7005 -x7006 -x7007 -x7008 -x7009 -x7010 -x7011 -x7012 -x7013 -x7014 -x7015 -x7016 -x7017 -x7018 -x7019 -x7020 -x7021 -x7022 -x7023 -x7024 -x7025 -x7026 -x7027 -x7028 -x7029 -x7030 -x7031 -x7032 -x7033 -x7034 -x7035 -x7036 -x7037 -x7038 -x7039 -x7040 -x7041 -x7042 -x7043 -x7044 -x7045 -x7046 -x7047 -x7048 -x7049 -x7050 -x7051 -x7052 -x7053 -x7054 -x7055 -x7056 -x7057 -x7058 -x7059 -x7060 -x7061 -x7062 -x7063 -x7064 -x7065 -x7066 -x7067 -x7068 -x7069 -x7070 -x7071 -x7072 -x7073 -x7074 -x7075 -x7076 -x7077 -x7078 -x7079 -x7080 -x7081 -x7082 -x7083 -x7084 -x7085 -x7086 -x7087 -x7088 -x7089 -x7090 -x7091 -x7092 -x7093 -x7094 -x7095 -x7096 -x7097 -x7098 -x7099 -x7100 -x7101 -x7102 -x7103 -x7104 -x7105 -x7106 -x7107 -x7108 -x7109 -x7110 -x7111 -x7112 -x7113 -x7114 -x7115 -x7116 -x7117 -x7118 -x7119 -x7120 -x7121 -x7122 -x7123 -x7124 -x7125 -x7126 -x7127 -x7128 -x7129 -x7130 -x7131 -x7132 -x7133 -x7134 -x7135 -x7136 -x7137 -x7138 -x7139 -x7140 -x7141 -x7142 -x7143 -x7144 -x7145 -x7146 -x7147 -x7148 -x7149 -x7150 -x7151 -x7152 -x7153 -x7154 -x7155 -x7156 -x7157 -x7158 -x7159 -x7160 -x7161 -x7162 -x7163 -x7164 -x7165 -x7166 -x7167 -x7168 -x7169 -x7170 -x7171 -x7172 -x7173 -x7174 -x7175 -x7176 -x7177 -x7178 -x7179 -x7180 -x7181 -x7182 -x7183 -x7184 -x7185 -x7186 -x7187 -x7188 -x7189 -x7190 -x7191 -x7192 -x7193 -x7194 -x7195 -x7196 -x7197 -x7198 -x7199 -x7200 -x7201 -x7202 -x7203 -x7204 -x7205 -x7206 -x7207 -x7208 -x7209 -x7210 -x7211 -x7212 -x7213 -x7214 -x7215 -x7216 -x7217 -x7218 -x7219 -x7220 -x7221 -x7222 -x7223 -x7224 -x7225 -x7226 -x7227 -x7228 -x7229 -x7230 -x7231 -x7232 -x7233 -x7234 -x7235 -x7236 -x7237 -x7238 -x7239 -x7240 -x7241 -x7242 -x7243 -x7244 -x7245 -x7246 -x7247 -x7248 -x7249 -x7250 -x7251 -x7252 -x7253 -x7254 -x7255 -x7256 -x7257 -x7258 -x7259 -x7260 -x7261 -x7262 -x7263 -x7264 -x7265 -x7266 -x7267 -x7268 -x7269 -x7270 -x7271 -x7272 -x7273 -x7274 -x7275 -x7276 -x7277 -x7278 -x7279 -x7280 -x7281 -x7282 -x7283 -x7284 -x7285 -x7286 -x7287 -x7288 -x7289 -x7290 -x7291 -x7292 -x7293 -x7294 -x7295 -x7296 -x7297 -x7298 -x7299 -x7300 -x7301 -x7302 -x7303 -x7304 -x7305 -x7306 -x7307 -x7308 -x7309 -x7310 -x7311 -x7312 -x7313 -x7314 -x7315 -x7316 -x7317 -x7318 -x7319 -x7320 -x7321 -x7322 -x7323 -x7324 -x7325 -x7326 -x7327 -x7328 -x7329 -x7330 -x7331 -x7332 -x7333 -x7334 -x7335 -x7336 -x7337 -x7338 -x7339 -x7340 -x7341 -x7342 -x7343 -x7344 -x7345 -x7346 -x7347 -x7348 -x7349 -x7350 -x7351 -x7352 -x7353 -x7354 -x7355 -x7356 -x7357 -x7358 -x7359 -x7360 -x7361 -x7362 -x7363 -x7364 -x7365 -x7366 -x7367 -x7368 -x7369 -x7370 -x7371 -x7372 -x7373 -x7374 -x7375 -x7376 -x7377 -x7378 -x7379 -x7380 -x7381 -x7382 -x7383 -x7384 -x7385 -x7386 -x7387 -x7388 -x7389 -x7390 -x7391 -x7392 -x7393 -x7394 -x7395 -x7396 -x7397 -x7398 -x7399 -x7400 -x7401 -x7402 -x7403 -x7404 -x7405 -x7406 -x7407 -x7408 -x7409 -x7410 -x7411 -x7412 -x7413 -x7414 -x7415 -x7416 -x7417 -x7418 -x7419 -x7420 -x7421 -x7422 -x7423 -x7424 -x7425 -x7426 -x7427 -x7428 -x7429 -x7430 -x7431 -x7432 -x7433 -x7434 -x7435 -x7436 -x7437 -x7438 -x7439 -x7440 -x7441 -x7442 -x7443 -x7444 -x7445 -x7446 -x7447 -x7448 -x7449 -x7450 -x7451 -x7452 -x7453 -x7454 -x7455 -x7456 -x7457 -x7458 -x7459 -x7460 -x7461 -x7462 -x7463 -x7464 -x7465 -x7466 -x7467 -x7468 -x7469 -x7470 -x7471 -x7472 -x7473 -x7474 -x7475 -x7476 -x7477 -x7478 -x7479 -x7480 -x7481 -x7482 -x7483 -x7484 -x7485 -x7486 -x7487 -x7488 -x7489 -x7490 -x7491 -x7492 -x7493 -x7494 -x7495 -x7496 -x7497 -x7498 -x7499 -x7500 -x7501 -x7502 -x7503 -x7504 -x7505 -x7506 -x7507 -x7508 -x7509 -x7510 -x7511 -x7512 -x7513 -x7514 -x7515 -x7516 -x7517 -x7518 -x7519 -x7520 -x7521 -x7522 -x7523 -x7524 -x7525 -x7526 -x7527 -x7528 -x7529 -x7530 -x7531 -x7532 -x7533 -x7534 -x7535 -x7536 -x7537 -x7538 -x7539 -x7540 -x7541 -x7542 -x7543 -x7544 -x7545 -x7546 -x7547 -x7548 -x7549 -x7550 -x7551 -x7552 -x7553 -x7554 -x7555 -x7556 -x7557 -x7558 -x7559 -x7560 -x7561 -x7562 -x7563 -x7564 -x7565 -x7566 -x7567 -x7568 -x7569 -x7570 -x7571 -x7572 -x7573 -x7574 -x7575 -x7576 -x7577 -x7578 -x7579 -x7580 -x7581 -x7582 -x7583 -x7584 -x7585 -x7586 -x7587 -x7588 -x7589 -x7590 -x7591 -x7592 -x7593 -x7594 -x7595 -x7596 -x7597 -x7598 -x7599 -x7600 -x7601 -x7602 -x7603 -x7604 -x7605 -x7606 -x7607 -x7608 -x7609 -x7610 -x7611 -x7612 -x7613 -x7614 -x7615 -x7616 -x7617 -x7618 -x7619 -x7620 -x7621 -x7622 -x7623 -x7624 -x7625 -x7626 -x7627 -x7628 -x7629 -x7630 -x7631 -x7632 -x7633 -x7634 -x7635 -x7636 -x7637 -x7638 -x7639 -x7640 -x7641 -x7642 -x7643 -x7644 -x7645 -x7646 -x7647 -x7648 -x7649 -x7650 -x7651 -x7652 -x7653 -x7654 -x7655 -x7656 -x7657 -x7658 -x7659 -x7660 -x7661 -x7662 -x7663 -x7664 -x7665 -x7666 -x7667 -x7668 -x7669 -x7670 -x7671 -x7672 -x7673 -x7674 -x7675 -x7676 -x7677 -x7678 -x7679 -x7680 -x7681 -x7682 -x7683 -x7684 -x7685 -x7686 -x7687 -x7688 -x7689 -x7690 -x7691 -x7692 -x7693 -x7694 -x7695 -x7696 -x7697 -x7698 -x7699 -x7700 -x7701 -x7702 -x7703 -x7704 -x7705 -x7706 -x7707 -x7708 -x7709 -x7710 -x7711 -x7712 -x7713 -x7714 -x7715 -x7716 -x7717 -x7718 -x7719 -x7720 -x7721 -x7722 -x7723 -x7724 -x7725 -x7726 -x7727 -x7728 -x7729 -x7730 -x7731 -x7732 -x7733 -x7734 -x7735 -x7736 -x7737 -x7738 -x7739 -x7740 -x7741 -x7742 -x7743 -x7744 -x7745 -x7746 -x7747 -x7748 -x7749 -x7750 -x7751 -x7752 -x7753 -x7754 -x7755 -x7756 -x7757 -x7758 -x7759 -x7760 -x7761 -x7762 -x7763 -x7764 -x7765 -x7766 -x7767 -x7768 -x7769 -x7770 -x7771 -x7772 -x7773 -x7774 -x7775 -x7776 -x7777 -x7778 -x7779 -x7780 -x7781 -x7782 -x7783 -x7784 -x7785 -x7786 -x7787 -x7788 -x7789 -x7790 -x7791 -x7792 -x7793 -x7794 -x7795 -x7796 -x7797 -x7798 -x7799 -x7800 -x7801 -x7802 -x7803 -x7804 -x7805 -x7806 -x7807 -x7808 -x7809 -x7810 -x7811 -x7812 -x7813 -x7814 -x7815 -x7816 -x7817 -x7818 -x7819 -x7820 -x7821 -x7822 -x7823 -x7824 -x7825 -x7826 -x7827 -x7828 -x7829 -x7830 -x7831 -x7832 -x7833 -x7834 -x7835 -x7836 -x7837 -x7838 -x7839 -x7840 -x7841 -x7842 -x7843 -x7844 -x7845 -x7846 -x7847 -x7848 -x7849 -x7850 -x7851 -x7852 -x7853 -x7854 -x7855 -x7856 -x7857 -x7858 -x7859 -x7860 -x7861 -x7862 -x7863 -x7864 -x7865 -x7866 -x7867 -x7868 -x7869 -x7870 -x7871 -x7872 -x7873 -x7874 -x7875 -x7876 -x7877 -x7878 -x7879 -x7880 -x7881 -x7882 -x7883 -x7884 -x7885 -x7886 -x7887 -x7888 -x7889 -x7890 -x7891 -x7892 -x7893 -x7894 -x7895 -x7896 -x7897 -x7898 -x7899 -x7900 -x7901 -x7902 -x7903 -x7904 -x7905 -x7906 -x7907 -x7908 -x7909 -x7910 -x7911 -x7912 -x7913 -x7914 -x7915 -x7916 -x7917 -x7918 -x7919 -x7920 -x7921 -x7922 -x7923 -x7924 -x7925 -x7926 -x7927 -x7928 -x7929 -x7930 -x7931 -x7932 -x7933 -x7934 -x7935 -x7936 -x7937 -x7938 -x7939 -x7940 -x7941 -x7942 -x7943 -x7944 -x7945 -x7946 -x7947 -x7948 -x7949 -x7950 -x7951 -x7952 -x7953 -x7954 -x7955 -x7956 -x7957 -x7958 -x7959 -x7960 -x7961 -x7962 -x7963 -x7964 -x7965 -x7966 -x7967 -x7968 -x7969 -x7970 -x7971 -x7972 -x7973 -x7974 -x7975 -x7976 -x7977 -x7978 -x7979 -x7980 -x7981 -x7982 -x7983 -x7984 -x7985 -x7986 -x7987 -x7988 -x7989 -x7990 -x7991 -x7992 -x7993 -x7994 -x7995 -x7996 -x7997 -x7998 -x7999 -x8000 -x8001 -x8002 -x8003 -x8004 -x8005 -x8006 -x8007 -x8008 -x8009 -x8010 -x8011 -x8012 -x8013 -x8014 -x8015 -x8016 -x8017 -x8018 -x8019 -x8020 -x8021 -x8022 -x8023 -x8024 -x8025 -x8026 -x8027 -x8028 -x8029 -x8030 -x8031 -x8032 -x8033 -x8034 -x8035 -x8036 -x8037 -x8038 -x8039 -x8040 -x8041 -x8042 -x8043 -x8044 -x8045 -x8046 -x8047 -x8048 -x8049 -x8050 -x8051 -x8052 -x8053 -x8054 -x8055 -x8056 -x8057 -x8058 -x8059 -x8060 -x8061 -x8062 -x8063 -x8064 -x8065 -x8066 -x8067 -x8068 -x8069 -x8070 -x8071 -x8072 -x8073 -x8074 -x8075 -x8076 -x8077 -x8078 -x8079 -x8080 -x8081 -x8082 -x8083 -x8084 -x8085 -x8086 -x8087 -x8088 -x8089 -x8090 -x8091 -x8092 -x8093 -x8094 -x8095 -x8096 -x8097 -x8098 -x8099 -x8100 -x8101 -x8102 -x8103 -x8104 -x8105 -x8106 -x8107 -x8108 -x8109 -x8110 -x8111 -x8112 -x8113 -x8114 -x8115 -x8116 -x8117 -x8118 -x8119 -x8120 -x8121 -x8122 -x8123 -x8124 -x8125 -x8126 -x8127 -x8128 -x8129 -x8130 -x8131 -x8132 -x8133 -x8134 -x8135 -x8136 -x8137 -x8138 -x8139 -x8140 -x8141 -x8142 -x8143 -x8144 -x8145 -x8146 -x8147 -x8148 -x8149 -x8150 -x8151 -x8152 -x8153 -x8154 -x8155 -x8156 -x8157 -x8158 -x8159 -x8160 -x8161 -x8162 -x8163 -x8164 -x8165 -x8166 -x8167 -x8168 -x8169 -x8170 -x8171 -x8172 -x8173 -x8174 -x8175 -x8176 -x8177 -x8178 -x8179 -x8180 -x8181 -x8182 -x8183 -x8184 -x8185 -x8186 -x8187 -x8188 -x8189 -x8190 -x8191 -x8192 -x8193 -x8194 -x8195 -x8196 -x8197 -x8198 -x8199 -x8200 -x8201 -x8202 -x8203 -x8204 -x8205 -x8206 -x8207 -x8208 -x8209 -x8210 -x8211 -x8212 -x8213 -x8214 -x8215 -x8216 -x8217 -x8218 -x8219 -x8220 -x8221 -x8222 -x8223 -x8224 -x8225 -x8226 -x8227 -x8228 -x8229 -x8230 -x8231 -x8232 -x8233 -x8234 -x8235 -x8236 -x8237 -x8238 -x8239 -x8240 -x8241 -x8242 -x8243 -x8244 -x8245 -x8246 -x8247 -x8248 -x8249 -x8250 -x8251 -x8252 -x8253 -x8254 -x8255 -x8256 -x8257 -x8258 -x8259 -x8260 -x8261 -x8262 -x8263 -x8264 -x8265 -x8266 -x8267 -x8268 -x8269 -x8270 -x8271 -x8272 -x8273 -x8274 -x8275 -x8276 -x8277 -x8278 -x8279 -x8280 -x8281 -x8282 -x8283 -x8284 -x8285 -x8286 -x8287 -x8288 -x8289 -x8290 -x8291 -x8292 -x8293 -x8294 -x8295 -x8296 -x8297 -x8298 -x8299 -x8300 -x8301 -x8302 -x8303 -x8304 -x8305 -x8306 -x8307 -x8308 -x8309 -x8310 -x8311 -x8312 -x8313 -x8314 -x8315 -x8316 -x8317 -x8318 -x8319 -x8320 -x8321 -x8322 -x8323 -x8324 -x8325 -x8326 -x8327 -x8328 -x8329 -x8330 -x8331 -x8332 -x8333 -x8334 -x8335 -x8336 -x8337 -x8338 -x8339 -x8340 -x8341 -x8342 -x8343 -x8344 -x8345 -x8346 -x8347 -x8348 -x8349 -x8350 -x8351 -x8352 -x8353 -x8354 -x8355 -x8356 -x8357 -x8358 -x8359 -x8360 -x8361 -x8362 -x8363 -x8364 -x8365 -x8366 -x8367 -x8368 -x8369 -x8370 -x8371 -x8372 -x8373 -x8374 -x8375 -x8376 -x8377 -x8378 -x8379 -x8380 -x8381 -x8382 -x8383 -x8384 -x8385 -x8386 -x8387 -x8388 -x8389 -x8390 -x8391 -x8392 -x8393 -x8394 -x8395 -x8396 -x8397 -x8398 -x8399 -x8400 -x8401 -x8402 -x8403 -x8404 -x8405 -x8406 -x8407 -x8408 -x8409 -x8410 -x8411 x8412 -x8413 -x8414 -x8415 -x8416 -x8417 -x8418 -x8419 -x8420 -x8421 -x8422 -x8423 -x8424 -x8425 -x8426 -x8427 -x8428 -x8429 -x8430 -x8431 -x8432 -x8433 -x8434 -x8435 -x8436 -x8437 -x8438 -x8439 -x8440 -x8441 -x8442 -x8443 -x8444 -x8445 -x8446 -x8447 -x8448 -x8449 -x8450 -x8451 -x8452 -x8453 -x8454 -x8455 -x8456 -x8457 -x8458 -x8459 -x8460 -x8461 -x8462 -x8463 -x8464 -x8465 -x8466 -x8467 -x8468 -x8469 -x8470 -x8471 -x8472 -x8473 -x8474 -x8475 -x8476 -x8477 -x8478 -x8479 -x8480 -x8481 -x8482 -x8483 -x8484 -x8485 -x8486 -x8487 -x8488 -x8489 -x8490 -x8491 -x8492 -x8493 -x8494 -x8495 -x8496 -x8497 -x8498 -x8499 -x8500 -x8501 -x8502 -x8503 -x8504 -x8505 -x8506 -x8507 -x8508 -x8509 -x8510 -x8511 -x8512 -x8513 -x8514 -x8515 -x8516 -x8517 -x8518 -x8519 -x8520 -x8521 -x8522 -x8523 -x8524 -x8525 -x8526 -x8527 -x8528 -x8529 -x8530 -x8531 -x8532 -x8533 -x8534 -x8535 -x8536 -x8537 -x8538 -x8539 -x8540 -x8541 -x8542 -x8543 -x8544 -x8545 -x8546 -x8547 -x8548 -x8549 -x8550 -x8551 -x8552 -x8553 -x8554 -x8555 -x8556 -x8557 -x8558 -x8559 -x8560 -x8561 -x8562 -x8563 -x8564 -x8565 -x8566 -x8567 -x8568 -x8569 -x8570 -x8571 -x8572 -x8573 -x8574 -x8575 -x8576 -x8577 -x8578 -x8579 -x8580 -x8581 -x8582 -x8583 -x8584 -x8585 -x8586 -x8587 -x8588 -x8589 -x8590 -x8591 -x8592 -x8593 -x8594 -x8595 -x8596 -x8597 -x8598 -x8599 -x8600 -x8601 -x8602 -x8603 -x8604 -x8605 -x8606 -x8607 -x8608 -x8609 -x8610 -x8611 -x8612 -x8613 -x8614 -x8615 -x8616 -x8617 -x8618 -x8619 -x8620 -x8621 -x8622 -x8623 -x8624 -x8625 -x8626 -x8627 -x8628 -x8629 -x8630 -x8631 -x8632 -x8633 -x8634 -x8635 -x8636 -x8637 -x8638 -x8639 -x8640 -x8641 -x8642 -x8643 -x8644 -x8645 -x8646 -x8647 -x8648 -x8649 -x8650 -x8651 -x8652 -x8653 -x8654 -x8655 -x8656 -x8657 -x8658 -x8659 -x8660 -x8661 -x8662 -x8663 -x8664 -x8665 -x8666 -x8667 -x8668 -x8669 -x8670 -x8671 -x8672 -x8673 -x8674 -x8675 -x8676 -x8677 -x8678 -x8679 -x8680 -x8681 -x8682 -x8683 -x8684 -x8685 -x8686 -x8687 -x8688 -x8689 -x8690 -x8691 -x8692 -x8693 -x8694 -x8695 -x8696 -x8697 -x8698 -x8699 -x8700 -x8701 -x8702 -x8703 -x8704 -x8705 -x8706 -x8707 -x8708 -x8709 -x8710 -x8711 -x8712 -x8713 -x8714 -x8715 -x8716 -x8717 -x8718 -x8719 -x8720 -x8721 -x8722 -x8723 -x8724 -x8725 -x8726 -x8727 -x8728 -x8729 -x8730 -x8731 -x8732 -x8733 -x8734 -x8735 -x8736 -x8737 -x8738 -x8739 -x8740 -x8741 -x8742 -x8743 -x8744 -x8745 -x8746 -x8747 -x8748 -x8749 -x8750 -x8751 -x8752 -x8753 -x8754 -x8755 -x8756 -x8757 -x8758 -x8759 -x8760 -x8761 -x8762 -x8763 -x8764 -x8765 -x8766 -x8767 -x8768 -x8769 -x8770 -x8771 -x8772 -x8773 -x8774 -x8775 -x8776 -x8777 -x8778 -x8779 -x8780 -x8781 -x8782 -x8783 -x8784 -x8785 -x8786 -x8787 -x8788 -x8789 -x8790 -x8791 -x8792 -x8793 -x8794 -x8795 -x8796 -x8797 -x8798 -x8799 -x8800 -x8801 -x8802 -x8803 -x8804 -x8805 -x8806 -x8807 -x8808 -x8809 -x8810 -x8811 -x8812 -x8813 -x8814 -x8815 -x8816 -x8817 -x8818 -x8819 -x8820 -x8821 -x8822 -x8823 -x8824 -x8825 -x8826 -x8827 -x8828 -x8829 -x8830 -x8831 -x8832 -x8833 -x8834 -x8835 -x8836 -x8837 -x8838 -x8839 -x8840 -x8841 -x8842 -x8843 -x8844 -x8845 -x8846 -x8847 -x8848 -x8849 -x8850 -x8851 -x8852 -x8853 -x8854 -x8855 -x8856 -x8857 -x8858 -x8859 -x8860 -x8861 -x8862 -x8863 -x8864 -x8865 -x8866 -x8867 -x8868 -x8869 -x8870 -x8871 -x8872 -x8873 -x8874 -x8875 -x8876 -x8877 -x8878 -x8879 -x8880 -x8881 -x8882 -x8883 -x8884 -x8885 -x8886 -x8887 -x8888 -x8889 -x8890 -x8891 -x8892 -x8893 -x8894 -x8895 -x8896 -x8897 -x8898 -x8899 -x8900 -x8901 -x8902 -x8903 -x8904 -x8905 -x8906 -x8907 -x8908 -x8909 -x8910 -x8911 -x8912 -x8913 -x8914 -x8915 -x8916 -x8917 -x8918 -x8919 -x8920 -x8921 -x8922 -x8923 -x8924 -x8925 -x8926 -x8927 -x8928 -x8929 -x8930 -x8931 -x8932 -x8933 -x8934 -x8935 -x8936 -x8937 -x8938 -x8939 -x8940 -x8941 -x8942 -x8943 -x8944 -x8945 -x8946 -x8947 -x8948 -x8949 -x8950 -x8951 -x8952 -x8953 -x8954 -x8955 -x8956 -x8957 -x8958 -x8959 -x8960 -x8961 -x8962 -x8963 -x8964 -x8965 -x8966 -x8967 -x8968 -x8969 -x8970 -x8971 -x8972 -x8973 -x8974 -x8975 -x8976 -x8977 -x8978 -x8979 -x8980 -x8981 -x8982 -x8983 -x8984 -x8985 -x8986 -x8987 -x8988 -x8989 -x8990 -x8991 -x8992 -x8993 -x8994 -x8995 -x8996 -x8997 -x8998 -x8999 -x9000 -x9001 -x9002 -x9003 -x9004 -x9005 -x9006 -x9007 -x9008 -x9009 -x9010 -x9011 -x9012 -x9013 -x9014 -x9015 -x9016 -x9017 -x9018 -x9019 -x9020 -x9021 -x9022 -x9023 -x9024 -x9025 -x9026 -x9027 -x9028 -x9029 -x9030 -x9031 -x9032 -x9033 -x9034 -x9035 -x9036 -x9037 -x9038 -x9039 -x9040 -x9041 -x9042 -x9043 -x9044 -x9045 -x9046 -x9047 -x9048 -x9049 -x9050 -x9051 -x9052 -x9053 -x9054 -x9055 -x9056 -x9057 -x9058 -x9059 -x9060 -x9061 -x9062 -x9063 -x9064 -x9065 -x9066 -x9067 -x9068 -x9069 -x9070 -x9071 -x9072 -x9073 -x9074 -x9075 -x9076 -x9077 -x9078 -x9079 -x9080 -x9081 -x9082 -x9083 -x9084 -x9085 -x9086 -x9087 -x9088 -x9089 -x9090 -x9091 -x9092 -x9093 -x9094 -x9095 -x9096 -x9097 -x9098 -x9099 -x9100 -x9101 -x9102 -x9103 -x9104 -x9105 -x9106 -x9107 -x9108 -x9109 -x9110 -x9111 -x9112 -x9113 -x9114 -x9115 -x9116 -x9117 -x9118 -x9119 -x9120 -x9121 -x9122 -x9123 -x9124 -x9125 -x9126 -x9127 -x9128 -x9129 -x9130 -x9131 -x9132 -x9133 -x9134 -x9135 -x9136 -x9137 -x9138 -x9139 -x9140 -x9141 -x9142 -x9143 -x9144 -x9145 -x9146 -x9147 -x9148 -x9149 -x9150 -x9151 -x9152 -x9153 -x9154 -x9155 -x9156 -x9157 -x9158 -x9159 -x9160 -x9161 -x9162 -x9163 -x9164 -x9165 -x9166 -x9167 -x9168 -x9169 -x9170 -x9171 -x9172 -x9173 -x9174 -x9175 -x9176 -x9177 -x9178 -x9179 -x9180 -x9181 -x9182 -x9183 -x9184 -x9185 -x9186 -x9187 -x9188 -x9189 -x9190 -x9191 -x9192 -x9193 -x9194 -x9195 -x9196 -x9197 -x9198 -x9199 -x9200 -x9201 -x9202 -x9203 -x9204 -x9205 -x9206 -x9207 -x9208 -x9209 -x9210 -x9211 -x9212 -x9213 -x9214 -x9215 -x9216 -x9217 -x9218 -x9219 -x9220 -x9221 -x9222 -x9223 -x9224 -x9225 -x9226 -x9227 -x9228 -x9229 -x9230 -x9231 -x9232 -x9233 -x9234 -x9235 -x9236 -x9237 -x9238 -x9239 -x9240 -x9241 -x9242 -x9243 -x9244 -x9245 -x9246 -x9247 -x9248 -x9249 -x9250 -x9251 -x9252 -x9253 -x9254 -x9255 -x9256 -x9257 -x9258 -x9259 -x9260 -x9261 -x9262 -x9263 -x9264 -x9265 -x9266 -x9267 -x9268 -x9269 -x9270 -x9271 -x9272 -x9273 -x9274 -x9275 -x9276 -x9277 -x9278 -x9279 -x9280 -x9281 -x9282 -x9283 -x9284 -x9285 -x9286 -x9287 -x9288 -x9289 -x9290 -x9291 -x9292 -x9293 -x9294 -x9295 -x9296 -x9297 -x9298 -x9299 -x9300 -x9301 -x9302 -x9303 -x9304 -x9305 -x9306 -x9307 -x9308 -x9309 -x9310 -x9311 -x9312 -x9313 -x9314 -x9315 -x9316 -x9317 -x9318 -x9319 -x9320 -x9321 -x9322 -x9323 -x9324 -x9325 -x9326 -x9327 -x9328 -x9329 -x9330 -x9331 -x9332 -x9333 -x9334 -x9335 -x9336 -x9337 -x9338 -x9339 -x9340 -x9341 -x9342 -x9343 -x9344 -x9345 -x9346 -x9347 -x9348 -x9349 -x9350 -x9351 -x9352 -x9353 -x9354 -x9355 -x9356 -x9357 -x9358 -x9359 -x9360 -x9361 -x9362 -x9363 -x9364 -x9365 -x9366 -x9367 -x9368 -x9369 -x9370 -x9371 -x9372 -x9373 -x9374 -x9375 -x9376 -x9377 -x9378 -x9379 -x9380 -x9381 -x9382 -x9383 -x9384 -x9385 -x9386 -x9387 -x9388 -x9389 -x9390 -x9391 -x9392 -x9393 -x9394 -x9395 -x9396 -x9397 -x9398 -x9399 -x9400 -x9401 -x9402 -x9403 -x9404 -x9405 -x9406 -x9407 -x9408 -x9409 -x9410 -x9411 -x9412 -x9413 -x9414 -x9415 -x9416 -x9417 -x9418 -x9419 -x9420 -x9421 -x9422 -x9423 -x9424 -x9425 -x9426 -x9427 -x9428 -x9429 -x9430 -x9431 -x9432 -x9433 -x9434 -x9435 -x9436 -x9437 -x9438 -x9439 -x9440 -x9441 -x9442 -x9443 -x9444 -x9445 -x9446 -x9447 -x9448 -x9449 -x9450 -x9451 -x9452 -x9453 -x9454 -x9455 -x9456 -x9457 -x9458 -x9459 -x9460 -x9461 -x9462 -x9463 -x9464 -x9465 -x9466 -x9467 -x9468 -x9469 -x9470 -x9471 -x9472 -x9473 -x9474 -x9475 -x9476 -x9477 -x9478 -x9479 -x9480 -x9481 -x9482 -x9483 -x9484 -x9485 -x9486 -x9487 -x9488 -x9489 -x9490 -x9491 -x9492 -x9493 -x9494 -x9495 -x9496 -x9497 -x9498 -x9499 -x9500 -x9501 -x9502 -x9503 -x9504 -x9505 -x9506 -x9507 -x9508 -x9509 -x9510 -x9511 -x9512 -x9513 -x9514 -x9515 -x9516 -x9517 -x9518 -x9519 -x9520 -x9521 -x9522 -x9523 -x9524 -x9525 -x9526 -x9527 -x9528 -x9529 -x9530 -x9531 -x9532 -x9533 -x9534 -x9535 -x9536 -x9537 -x9538 -x9539 -x9540 -x9541 -x9542 -x9543 -x9544 -x9545 -x9546 -x9547 -x9548 -x9549 -x9550 -x9551 -x9552 -x9553 -x9554 -x9555 -x9556 -x9557 -x9558 -x9559 -x9560 -x9561 -x9562 -x9563 -x9564 -x9565 -x9566 -x9567 -x9568 -x9569 -x9570 -x9571 -x9572 -x9573 -x9574 -x9575 -x9576 -x9577 -x9578 -x9579 -x9580 -x9581 -x9582 -x9583 -x9584 -x9585 -x9586 -x9587 -x9588 -x9589 -x9590 -x9591 -x9592 -x9593 -x9594 -x9595 -x9596 -x9597 -x9598 -x9599 -x9600 -x9601 -x9602 -x9603 -x9604 -x9605 -x9606 -x9607 -x9608 -x9609 -x9610 -x9611 -x9612 -x9613 -x9614 -x9615 -x9616 -x9617 -x9618 -x9619 -x9620 -x9621 -x9622 -x9623 -x9624 -x9625 -x9626 -x9627 -x9628 -x9629 -x9630 -x9631 -x9632 -x9633 -x9634 -x9635 -x9636 -x9637 -x9638 -x9639 -x9640 -x9641 -x9642 -x9643 -x9644 -x9645 -x9646 -x9647 -x9648 -x9649 -x9650 -x9651 -x9652 -x9653 -x9654 -x9655 -x9656 -x9657 -x9658 -x9659 -x9660 -x9661 -x9662 -x9663 -x9664 -x9665 -x9666 -x9667 -x9668 -x9669 -x9670 -x9671 -x9672 -x9673 -x9674 -x9675 -x9676 -x9677 -x9678 -x9679 -x9680 -x9681 -x9682 -x9683 -x9684 -x9685 -x9686 -x9687 -x9688 -x9689 -x9690 -x9691 -x9692 -x9693 -x9694 -x9695 -x9696 -x9697 -x9698 -x9699 -x9700 -x9701 -x9702 -x9703 -x9704 -x9705 -x9706 -x9707 -x9708 -x9709 -x9710 -x9711 -x9712 -x9713 -x9714 -x9715 -x9716 -x9717 -x9718 -x9719 -x9720 -x9721 -x9722 -x9723 -x9724 -x9725 -x9726 -x9727 -x9728 -x9729 -x9730 -x9731 -x9732 -x9733 -x9734 -x9735 -x9736 -x9737 -x9738 -x9739 -x9740 -x9741 -x9742 -x9743 -x9744 -x9745 -x9746 -x9747 -x9748 -x9749 -x9750 -x9751 -x9752 -x9753 -x9754 -x9755 -x9756 -x9757 -x9758 -x9759 -x9760 -x9761 -x9762 -x9763 -x9764 -x9765 -x9766 -x9767 -x9768 -x9769 -x9770 -x9771 -x9772 -x9773 -x9774 -x9775 -x9776 -x9777 -x9778 -x9779 -x9780 -x9781 -x9782 -x9783 -x9784 -x9785 -x9786 -x9787 -x9788 -x9789 -x9790 -x9791 -x9792 -x9793 -x9794 -x9795 -x9796 -x9797 -x9798 -x9799 -x9800 -x9801 -x9802 -x9803 -x9804 -x9805 -x9806 -x9807 -x9808 -x9809 -x9810 -x9811 -x9812 -x9813 -x9814 -x9815 -x9816 -x9817 -x9818 -x9819 -x9820 -x9821 -x9822 -x9823 -x9824 -x9825 -x9826 -x9827 -x9828 -x9829 -x9830 -x9831 -x9832 -x9833 -x9834 -x9835 -x9836 -x9837 -x9838 -x9839 -x9840 -x9841 -x9842 -x9843 -x9844 -x9845 -x9846 -x9847 -x9848 -x9849 -x9850 -x9851 -x9852 -x9853 -x9854 -x9855 -x9856 -x9857 -x9858 -x9859 -x9860 -x9861 -x9862 -x9863 -x9864 -x9865 -x9866 -x9867 -x9868 -x9869 -x9870 -x9871 -x9872 -x9873 -x9874 -x9875 -x9876 -x9877 -x9878 -x9879 -x9880 -x9881 -x9882 -x9883 -x9884 -x9885 -x9886 -x9887 -x9888 -x9889 -x9890 -x9891 -x9892 -x9893 -x9894 -x9895 x9896 x9897 -x9898 -x9899 -x9900 -x9901 -x9902 -x9903 -x9904 -x9905 -x9906 -x9907 -x9908 -x9909 -x9910 -x9911 -x9912 -x9913 -x9914 -x9915 -x9916 -x9917 -x9918 -x9919 -x9920 -x9921 -x9922 -x9923 -x9924 -x9925 -x9926 -x9927 -x9928 -x9929 -x9930 -x9931 -x9932 -x9933 -x9934 -x9935 -x9936 -x9937 -x9938 -x9939 -x9940 -x9941 -x9942 -x9943 -x9944 -x9945 -x9946 -x9947 -x9948 -x9949 -x9950 -x9951 -x9952 -x9953 -x9954 -x9955 -x9956 -x9957 -x9958 -x9959 -x9960 -x9961 -x9962 -x9963 -x9964 -x9965 -x9966 -x9967 -x9968 -x9969 -x9970 -x9971 -x9972 -x9973 -x9974 -x9975 -x9976 -x9977 -x9978 -x9979 -x9980 -x9981 -x9982 -x9983 -x9984 -x9985 -x9986 -x9987 -x9988 -x9989 -x9990 -x9991 -x9992 -x9993 -x9994 -x9995 -x9996 -x9997 -x9998 -x9999 -x10000 -x10001 -x10002 -x10003 -x10004 -x10005 -x10006 -x10007 -x10008 -x10009 -x10010 -x10011 -x10012 -x10013 -x10014 -x10015 -x10016 -x10017 -x10018 -x10019 -x10020 -x10021 -x10022 -x10023 -x10024 -x10025 -x10026 -x10027 -x10028 -x10029 -x10030 -x10031 -x10032 -x10033 -x10034 -x10035 -x10036 -x10037 -x10038 -x10039 -x10040 -x10041 -x10042 -x10043 -x10044 -x10045 -x10046 -x10047 -x10048 -x10049 -x10050 -x10051 -x10052 -x10053 -x10054 -x10055 -x10056 -x10057 -x10058 -x10059 -x10060 -x10061 -x10062 -x10063 -x10064 -x10065 -x10066 -x10067 -x10068 -x10069 -x10070 -x10071 -x10072 -x10073 -x10074 -x10075 -x10076 -x10077 -x10078 -x10079 -x10080 -x10081 -x10082 -x10083 -x10084 -x10085 -x10086 -x10087 -x10088 -x10089 -x10090 -x10091 -x10092 -x10093 -x10094 -x10095 -x10096 -x10097 -x10098 -x10099 -x10100 -x10101 -x10102 -x10103 -x10104 -x10105 -x10106 -x10107 -x10108 -x10109 -x10110 -x10111 -x10112 -x10113 -x10114 -x10115 -x10116 -x10117 -x10118 -x10119 -x10120 -x10121 -x10122 -x10123 -x10124 -x10125 -x10126 -x10127 -x10128 -x10129 -x10130 -x10131 -x10132 -x10133 -x10134 -x10135 -x10136 -x10137 -x10138 -x10139 -x10140 -x10141 -x10142 -x10143 -x10144 -x10145 -x10146 -x10147 -x10148 -x10149 -x10150 -x10151 -x10152 -x10153 -x10154 -x10155 -x10156 -x10157 -x10158 -x10159 -x10160 -x10161 -x10162 -x10163 -x10164 -x10165 -x10166 -x10167 -x10168 -x10169 -x10170 -x10171 -x10172 -x10173 -x10174 -x10175 -x10176 -x10177 -x10178 -x10179 -x10180 x10181 -x10182 -x10183 -x10184 -x10185 -x10186 -x10187 -x10188 -x10189 -x10190 -x10191 -x10192 -x10193 -x10194 -x10195 -x10196 -x10197 -x10198 -x10199 -x10200 -x10201 -x10202 -x10203 -x10204 -x10205 -x10206 -x10207 -x10208 -x10209 -x10210 -x10211 -x10212 -x10213 -x10214 -x10215 -x10216 -x10217 -x10218 -x10219 -x10220 -x10221 -x10222 -x10223 -x10224 -x10225 -x10226 -x10227 -x10228 -x10229 -x10230 -x10231 -x10232 -x10233 -x10234 -x10235 -x10236 -x10237 -x10238 -x10239 -x10240 -x10241 -x10242 -x10243 -x10244 -x10245 -x10246 -x10247 -x10248 -x10249 -x10250 -x10251 -x10252 -x10253 -x10254 -x10255 -x10256 -x10257 -x10258 -x10259 -x10260 -x10261 -x10262 -x10263 -x10264 -x10265 -x10266 -x10267 -x10268 -x10269 -x10270 -x10271 -x10272 -x10273 -x10274 -x10275 -x10276 -x10277 -x10278 -x10279 -x10280 -x10281 -x10282 -x10283 -x10284 -x10285 -x10286 -x10287 -x10288 -x10289 -x10290 -x10291 -x10292 -x10293 -x10294 -x10295 -x10296 -x10297 -x10298 -x10299 -x10300 -x10301 -x10302 -x10303 -x10304 -x10305 -x10306 -x10307 -x10308 -x10309 -x10310 -x10311 -x10312 -x10313 -x10314 -x10315 -x10316 -x10317 -x10318 -x10319 -x10320 -x10321 -x10322 -x10323 -x10324 -x10325 -x10326 -x10327 -x10328 -x10329 -x10330 -x10331 -x10332 -x10333 -x10334 -x10335 -x10336 -x10337 -x10338 -x10339 -x10340 -x10341 -x10342 -x10343 -x10344 -x10345 -x10346 -x10347 -x10348 -x10349 -x10350 -x10351 -x10352 -x10353 -x10354 -x10355 -x10356 -x10357 -x10358 -x10359 -x10360 -x10361 -x10362 -x10363 -x10364 -x10365 -x10366 -x10367 -x10368 -x10369 -x10370 -x10371 -x10372 -x10373 -x10374 -x10375 -x10376 -x10377 -x10378 -x10379 -x10380 -x10381 -x10382 -x10383 -x10384 -x10385 -x10386 -x10387 -x10388 -x10389 -x10390 -x10391 -x10392 -x10393 -x10394 -x10395 -x10396 -x10397 -x10398 -x10399 -x10400 -x10401 -x10402 -x10403 -x10404 -x10405 -x10406 -x10407 -x10408 -x10409 -x10410 -x10411 -x10412 -x10413 -x10414 -x10415 -x10416 -x10417 -x10418 -x10419 -x10420 -x10421 -x10422 -x10423 -x10424 -x10425 -x10426 -x10427 -x10428 -x10429 -x10430 -x10431 -x10432 -x10433 -x10434 -x10435 -x10436 -x10437 -x10438 -x10439 -x10440 -x10441 -x10442 -x10443 -x10444 -x10445 -x10446 -x10447 -x10448 -x10449 -x10450 -x10451 -x10452 -x10453 -x10454 -x10455 -x10456 -x10457 -x10458 -x10459 -x10460 -x10461 -x10462 -x10463 -x10464 -x10465 -x10466 -x10467 -x10468 -x10469 -x10470 -x10471 -x10472 -x10473 -x10474 -x10475 -x10476 -x10477 -x10478 -x10479 -x10480 -x10481 -x10482 -x10483 -x10484 -x10485 -x10486 -x10487 -x10488 -x10489 -x10490 -x10491 -x10492 -x10493 -x10494 -x10495 -x10496 -x10497 -x10498 -x10499 -x10500 -x10501 -x10502 -x10503 -x10504 -x10505 -x10506 -x10507 -x10508 -x10509 -x10510 -x10511 -x10512 -x10513 -x10514 -x10515 -x10516 -x10517 -x10518 -x10519 -x10520 -x10521 -x10522 -x10523 -x10524 -x10525 -x10526 -x10527 -x10528 -x10529 -x10530 -x10531 -x10532 -x10533 -x10534 -x10535 -x10536 -x10537 -x10538 -x10539 -x10540 -x10541 -x10542 -x10543 -x10544 -x10545 -x10546 -x10547 -x10548 -x10549 -x10550 -x10551 -x10552 -x10553 -x10554 -x10555 -x10556 -x10557 -x10558 -x10559 -x10560 -x10561 -x10562 -x10563 -x10564 -x10565 -x10566 -x10567 -x10568 -x10569 -x10570 -x10571 -x10572 -x10573 -x10574 -x10575 -x10576 -x10577 -x10578 -x10579 -x10580 -x10581 -x10582 -x10583 -x10584 -x10585 -x10586 -x10587 -x10588 -x10589 -x10590 -x10591 -x10592 -x10593 -x10594 -x10595 -x10596 -x10597 -x10598 -x10599 -x10600 -x10601 -x10602 -x10603 -x10604 -x10605 -x10606 -x10607 -x10608 -x10609 -x10610 -x10611 -x10612 -x10613 -x10614 -x10615 -x10616 -x10617 -x10618 -x10619 -x10620 -x10621 -x10622 -x10623 -x10624 -x10625 -x10626 -x10627 -x10628 -x10629 -x10630 -x10631 -x10632 -x10633 -x10634 -x10635 -x10636 -x10637 -x10638 -x10639 -x10640 -x10641 -x10642 -x10643 -x10644 -x10645 -x#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.69 2/54 5099
Raw data (stat): 5099 (runsolver) R 5098 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487608945 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.93 0.95 0.69 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 24841 0 0 0 939 59 0 0 25 0 1 0 487608945 113881088 24486 4294967295 134512640 134672761 3221224576 3221223120 134621407 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27803 24486 603 41 0 27762 0
vsize: 111212
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.70 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 46112 0 0 0 1888 110 0 0 25 0 1 0 487608945 153612288 33752 4294967295 134512640 134672761 3221224576 3221223884 134593757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37503 33752 603 41 0 37462 0
vsize: 150012
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 46112 0 0 0 2887 111 0 0 25 0 1 0 487608945 142811136 31115 4294967295 134512640 134672761 3221224576 3221223280 134597218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34866 31115 603 41 0 34825 0
vsize: 139464
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.96 0.70 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 85622 0 0 0 3793 205 0 0 25 0 1 0 487608945 275034112 61397 4294967295 134512640 134672761 3221224576 3221221860 134544039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67147 61397 603 41 0 67106 0
vsize: 268588
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.96 0.71 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 108604 0 0 0 4736 263 0 0 25 0 1 0 487608945 388808704 84357 4294967295 134512640 134672761 3221224576 3221223120 134621359 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94924 84357 603 41 0 94883 0
vsize: 379696
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.96 0.71 3/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 110990 0 0 0 5730 268 0 0 25 0 1 0 487608945 391946240 85211 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95690 85211 603 41 0 95649 0
vsize: 382760
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 111144 0 0 0 6729 269 0 0 25 0 1 0 487608945 392347648 85365 4294967295 134512640 134672761 3221224576 3221223728 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95788 85365 603 41 0 95747 0
vsize: 383152
[startup+80.0027 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 111382 0 0 0 7729 270 0 0 25 0 1 0 487608945 393383936 85603 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96041 85603 603 41 0 96000 0
vsize: 384164
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 111760 0 0 0 8729 270 0 0 25 0 1 0 487608945 394874880 85981 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96405 85981 603 41 0 96364 0
vsize: 385620
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 112058 0 0 0 9728 271 0 0 25 0 1 0 487608945 397123584 86279 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96954 86279 603 41 0 96913 0
vsize: 387816
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 112202 0 0 0 10728 271 0 0 25 0 1 0 487608945 397656064 86423 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97084 86423 603 41 0 97043 0
vsize: 388336
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 112536 0 0 0 11727 272 0 0 25 0 1 0 487608945 399081472 86757 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97432 86757 603 41 0 97391 0
vsize: 389728
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 112883 0 0 0 12727 273 0 0 25 0 1 0 487608945 400547840 87104 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97790 87104 603 41 0 97749 0
vsize: 391160
[startup+140.111 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 131091 0 0 0 13684 326 0 0 25 0 1 0 487608945 401825792 87354 4294967295 134512640 134672761 3221224576 3221222704 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98102 87354 603 41 0 98061 0
vsize: 392408
[startup+150.11 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 132892 0 0 0 14681 329 0 0 25 0 1 0 487608945 402399232 87470 4294967295 134512640 134672761 3221224576 3221222768 134523000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98242 87470 603 41 0 98201 0
vsize: 392968
[startup+160.111 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 136038 0 0 0 15671 340 0 0 25 0 1 0 487608945 454713344 88302 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111014 88302 603 41 0 110973 0
vsize: 444056
[startup+170.111 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 136042 0 0 0 16671 340 0 0 25 0 1 0 487608945 454713344 88306 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111014 88306 603 41 0 110973 0
vsize: 444056
[startup+180.111 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 136086 0 0 0 17671 340 0 0 25 0 1 0 487608945 455237632 88350 4294967295 134512640 134672761 3221224576 3221223760 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111142 88350 603 41 0 111101 0
vsize: 444568
[startup+190.111 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 136439 0 0 0 18670 341 0 0 25 0 1 0 487608945 456589312 88703 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111472 88703 603 41 0 111431 0
vsize: 445888
[startup+200.111 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 136778 0 0 0 19670 341 0 0 25 0 1 0 487608945 457998336 89042 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111816 89042 603 41 0 111775 0
vsize: 447264
[startup+210.11 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 137628 0 0 0 20668 343 0 0 25 0 1 0 487608945 461549568 89892 4294967295 134512640 134672761 3221224576 3221223700 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 112683 89892 603 41 0 112642 0
vsize: 450732
[startup+220.111 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 137897 0 0 0 21667 344 0 0 25 0 1 0 487608945 462630912 90161 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 112947 90161 603 41 0 112906 0
vsize: 451788
[startup+230.111 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 138391 0 0 0 22666 346 0 0 25 0 1 0 487608945 464674816 90655 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113446 90655 603 41 0 113405 0
vsize: 453784
[startup+240.111 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 139033 0 0 0 23664 347 0 0 25 0 1 0 487608945 467210240 91297 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114065 91297 603 41 0 114024 0
vsize: 456260
[startup+250.11 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 139466 0 0 0 24663 349 0 0 25 0 1 0 487608945 469045248 91730 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114513 91730 603 41 0 114472 0
vsize: 458052
[startup+260.111 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 139839 0 0 0 25662 350 0 0 25 0 1 0 487608945 470491136 92103 4294967295 134512640 134672761 3221224576 3221223568 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114866 92103 603 41 0 114825 0
vsize: 459464
[startup+270.111 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 140073 0 0 0 26662 350 0 0 25 0 1 0 487608945 471543808 92337 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115123 92337 603 41 0 115082 0
vsize: 460492
[startup+280.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 141102 0 0 0 27660 353 0 0 25 0 1 0 487608945 475721728 93366 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116143 93366 603 41 0 116102 0
vsize: 464572
[startup+290.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 141311 0 0 0 28660 353 0 0 25 0 1 0 487608945 476532736 93575 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116341 93575 603 41 0 116300 0
vsize: 465364
[startup+300.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 141682 0 0 0 29659 353 0 0 25 0 1 0 487608945 478056448 93946 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116713 93946 603 41 0 116672 0
vsize: 466852
[startup+310.112 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 142172 0 0 0 30658 355 0 0 25 0 1 0 487608945 480133120 94436 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117220 94436 603 41 0 117179 0
vsize: 468880
[startup+320.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 142451 0 0 0 31657 356 0 0 25 0 1 0 487608945 481288192 94715 4294967295 134512640 134672761 3221224576 3221223776 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117502 94715 603 41 0 117461 0
vsize: 470008
[startup+330.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 143096 0 0 0 32656 357 0 0 25 0 1 0 487608945 483848192 95360 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118127 95360 603 41 0 118086 0
vsize: 472508
[startup+340.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 143572 0 0 0 33655 358 0 0 25 0 1 0 487608945 485810176 95836 4294967295 134512640 134672761 3221224576 3221223760 134615544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118606 95836 603 41 0 118565 0
vsize: 474424
[startup+350.112 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 144119 0 0 0 34654 359 0 0 25 0 1 0 487608945 488022016 96383 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119146 96383 603 41 0 119105 0
vsize: 476584
[startup+360.113 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 144466 0 0 0 35653 361 0 0 25 0 1 0 487608945 489455616 96730 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119496 96730 603 41 0 119455 0
vsize: 477984
[startup+370.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 145362 0 0 0 36652 362 0 0 25 0 1 0 487608945 493125632 97626 4294967295 134512640 134672761 3221224576 3221223444 1075349616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120392 97626 603 41 0 120351 0
vsize: 481568
[startup+380.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 147021 0 0 0 37648 365 0 0 25 0 1 0 487608945 500031488 99285 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122078 99285 603 41 0 122037 0
vsize: 488312
[startup+390.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 148211 0 0 0 38646 369 0 0 25 0 1 0 487608945 504868864 100475 4294967295 134512640 134672761 3221224576 3221223744 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123259 100475 603 41 0 123218 0
vsize: 493036
[startup+400.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 148785 0 0 0 39644 370 0 0 25 0 1 0 487608945 507162624 101049 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123819 101049 603 41 0 123778 0
vsize: 495276
[startup+410.113 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 148982 0 0 0 40644 370 0 0 25 0 1 0 487608945 508067840 101246 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124040 101246 603 41 0 123999 0
vsize: 496160
[startup+420.113 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 149291 0 0 0 41643 371 0 0 25 0 1 0 487608945 509206528 101555 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124318 101555 603 41 0 124277 0
vsize: 497272
[startup+430.114 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 149898 0 0 0 42642 373 0 0 25 0 1 0 487608945 511737856 102162 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124936 102162 603 41 0 124895 0
vsize: 499744
[startup+440.113 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 150508 0 0 0 43640 375 0 0 25 0 1 0 487608945 514146304 102772 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125524 102772 603 41 0 125483 0
vsize: 502096
[startup+450.113 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 151604 0 0 0 44638 377 0 0 25 0 1 0 487608945 518717440 103868 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126640 103868 603 41 0 126599 0
vsize: 506560
[startup+460.114 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 152444 0 0 0 45636 380 0 0 25 0 1 0 487608945 522067968 104708 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127458 104708 603 41 0 127417 0
vsize: 509832
[startup+470.113 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 161681 0 0 0 46611 405 0 0 25 0 1 0 487608945 528064512 106120 4294967295 134512640 134672761 3221224576 3220535216 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128922 106120 603 41 0 128881 0
vsize: 515688
[startup+480.114 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 172110 0 0 0 47583 432 0 0 25 0 1 0 487608945 527306752 105898 4294967295 134512640 134672761 3221224576 3221222992 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128737 105898 603 41 0 128696 0
vsize: 514948
[startup+490.114 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 173356 0 0 0 48581 434 0 0 25 0 1 0 487608945 528302080 106069 4294967295 134512640 134672761 3221224576 3221221680 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128980 106069 603 41 0 128939 0
vsize: 515920
[startup+500.113 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175863 0 0 0 49575 441 0 0 25 0 1 0 487608945 526499840 105803 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128540 105803 603 41 0 128499 0
vsize: 514160
[startup+510.113 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175863 0 0 0 50575 441 0 0 25 0 1 0 487608945 526499840 105803 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128540 105803 603 41 0 128499 0
vsize: 514160
[startup+520.113 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175863 0 0 0 51575 441 0 0 25 0 1 0 487608945 526499840 105803 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128540 105803 603 41 0 128499 0
vsize: 514160
[startup+530.113 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175863 0 0 0 52575 441 0 0 25 0 1 0 487608945 526499840 105803 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128540 105803 603 41 0 128499 0
vsize: 514160
[startup+540.113 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175863 0 0 0 53575 441 0 0 25 0 1 0 487608945 526499840 105803 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128540 105803 603 41 0 128499 0
vsize: 514160
[startup+550.113 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 175956 0 0 0 54576 441 0 0 25 0 1 0 487608945 526954496 105896 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128651 105896 603 41 0 128610 0
vsize: 514604
[startup+560.113 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 176399 0 0 0 55575 442 0 0 25 0 1 0 487608945 528736256 106339 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129086 106339 603 41 0 129045 0
vsize: 516344
[startup+570.113 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 176901 0 0 0 56574 443 0 0 25 0 1 0 487608945 530771968 106841 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129583 106841 603 41 0 129542 0
vsize: 518332
[startup+580.114 s]
Raw data (loadavg): 0.99 0.97 0.82 2/54 5099
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 177445 0 0 0 57573 444 0 0 25 0 1 0 487608945 533098496 107385 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130151 107385 603 41 0 130110 0
vsize: 520604
[startup+590.115 s]
Raw data (loadavg): 1.07 0.99 0.82 2/57 5134
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 177713 0 0 0 58572 445 0 0 25 0 1 0 487608945 534196224 107653 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130419 107653 603 41 0 130378 0
vsize: 521676
[startup+600.131 s]
Raw data (loadavg): 1.14 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 178327 0 0 0 59573 446 0 0 25 0 1 0 487608945 536670208 108267 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131023 108267 603 41 0 130982 0
vsize: 524092
[startup+610.131 s]
Raw data (loadavg): 1.11 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 178536 0 0 0 60573 446 0 0 25 0 1 0 487608945 537456640 108476 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131215 108476 603 41 0 131174 0
vsize: 524860
[startup+620.131 s]
Raw data (loadavg): 1.10 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 178879 0 0 0 61572 447 0 0 25 0 1 0 487608945 538877952 108819 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 131562 108819 603 41 0 131521 0
vsize: 526248
[startup+630.131 s]
Raw data (loadavg): 1.08 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 179501 0 0 0 62572 448 0 0 25 0 1 0 487608945 541474816 109441 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132196 109441 603 41 0 132155 0
vsize: 528784
[startup+640.131 s]
Raw data (loadavg): 1.07 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 179979 0 0 0 63571 449 0 0 25 0 1 0 487608945 543432704 109919 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 132674 109919 603 41 0 132633 0
vsize: 530696
[startup+650.131 s]
Raw data (loadavg): 1.06 1.00 0.83 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 180471 0 0 0 64570 450 0 0 25 0 1 0 487608945 545472512 110411 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133172 110411 603 41 0 133131 0
vsize: 532688
[startup+660.131 s]
Raw data (loadavg): 1.05 1.00 0.84 2/54 5152
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 181175 0 0 0 65569 451 0 0 25 0 1 0 487608945 548274176 111115 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133856 111115 603 41 0 133815 0
vsize: 535424
[startup+670.131 s]
Raw data (loadavg): 1.04 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 181608 0 0 0 66568 452 0 0 25 0 1 0 487608945 550023168 111548 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134283 111548 603 41 0 134242 0
vsize: 537132
[startup+680.132 s]
Raw data (loadavg): 1.03 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 181775 0 0 0 67568 452 0 0 25 0 1 0 487608945 550789120 111715 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134470 111715 603 41 0 134429 0
vsize: 537880
[startup+690.131 s]
Raw data (loadavg): 1.03 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 182129 0 0 0 68567 453 0 0 25 0 1 0 487608945 552189952 112069 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 134812 112069 603 41 0 134771 0
vsize: 539248
[startup+700.132 s]
Raw data (loadavg): 1.02 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 182610 0 0 0 69567 454 0 0 25 0 1 0 487608945 554266624 112550 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135319 112550 603 41 0 135278 0
vsize: 541276
[startup+710.132 s]
Raw data (loadavg): 1.02 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 183021 0 0 0 70566 455 0 0 25 0 1 0 487608945 556023808 112961 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135748 112961 603 41 0 135707 0
vsize: 542992
[startup+720.131 s]
Raw data (loadavg): 1.02 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 183244 0 0 0 71566 455 0 0 25 0 1 0 487608945 556978176 113184 4294967295 134512640 134672761 3221224576 3221223760 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 135981 113184 603 41 0 135940 0
vsize: 543924
[startup+730.132 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 183461 0 0 0 72565 456 0 0 25 0 1 0 487608945 557740032 113401 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136167 113401 603 41 0 136126 0
vsize: 544668
[startup+740.132 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 183666 0 0 0 73565 457 0 0 25 0 1 0 487608945 558641152 113606 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136387 113606 603 41 0 136346 0
vsize: 545548
[startup+750.132 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 184087 0 0 0 74564 457 0 0 25 0 1 0 487608945 560357376 114027 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 136806 114027 603 41 0 136765 0
vsize: 547224
[startup+760.132 s]
Raw data (loadavg): 1.01 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 184686 0 0 0 75563 459 0 0 25 0 1 0 487608945 562786304 114626 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 137399 114626 603 41 0 137358 0
vsize: 549596
[startup+770.132 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 185318 0 0 0 76562 460 0 0 25 0 1 0 487608945 565428224 115258 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138044 115258 603 41 0 138003 0
vsize: 552176
[startup+780.133 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 186085 0 0 0 77561 461 0 0 25 0 1 0 487608945 568590336 116025 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 138816 116025 603 41 0 138775 0
vsize: 555264
[startup+790.133 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 187204 0 0 0 78559 464 0 0 25 0 1 0 487608945 573136896 117144 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 139926 117144 603 41 0 139885 0
vsize: 559704
[startup+800.132 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 188864 0 0 0 79554 468 0 0 25 0 1 0 487608945 579878912 118804 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141572 118804 603 41 0 141531 0
vsize: 566288
[startup+810.133 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 189085 0 0 0 80554 469 0 0 25 0 1 0 487608945 580792320 119025 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141795 119025 603 41 0 141754 0
vsize: 567180
[startup+820.133 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 189986 0 0 0 81552 471 0 0 25 0 1 0 487608945 584470528 119926 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142693 119926 603 41 0 142652 0
vsize: 570772
[startup+830.133 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 190198 0 0 0 82552 471 0 0 25 0 1 0 487608945 585404416 120138 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 142921 120138 603 41 0 142880 0
vsize: 571684
[startup+840.134 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 190636 0 0 0 83551 472 0 0 25 0 1 0 487608945 587198464 120576 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143359 120576 603 41 0 143318 0
vsize: 573436
[startup+850.134 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 191147 0 0 0 84551 473 0 0 25 0 1 0 487608945 589205504 121087 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 143849 121087 603 41 0 143808 0
vsize: 575396
[startup+860.134 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 191763 0 0 0 85549 475 0 0 25 0 1 0 487608945 591826944 121703 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144489 121703 603 41 0 144448 0
vsize: 577956
[startup+870.135 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 192692 0 0 0 86548 476 0 0 25 0 1 0 487608945 595566592 122632 4294967295 134512640 134672761 3221224576 3221223616 134612578 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 145402 122632 603 41 0 145361 0
vsize: 581608
[startup+880.136 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 193539 0 0 0 87547 478 0 0 25 0 1 0 487608945 599109632 123479 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146267 123479 603 41 0 146226 0
vsize: 585068
[startup+890.136 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 194040 0 0 0 88545 479 0 0 25 0 1 0 487608945 601153536 123980 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 146766 123980 603 41 0 146725 0
vsize: 587064
[startup+900.136 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 194738 0 0 0 89544 481 0 0 25 0 1 0 487608945 603910144 124678 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 147439 124678 603 41 0 147398 0
vsize: 589756
[startup+910.137 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 196056 0 0 0 90541 484 0 0 25 0 1 0 487608945 609325056 125996 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 148761 125996 603 41 0 148720 0
vsize: 595044
[startup+920.14 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5154
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 196475 0 0 0 91541 485 0 0 25 0 1 0 487608945 611033088 126415 4294967295 134512640 134672761 3221224576 3221223616 134612972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149178 126415 603 41 0 149137 0
vsize: 596712
[startup+930.141 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 197013 0 0 0 92540 486 0 0 25 0 1 0 487608945 613322752 126953 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 149737 126953 603 41 0 149696 0
vsize: 598948
[startup+940.142 s]
Raw data (loadavg): 1.07 1.02 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 197506 0 0 0 93539 487 0 0 25 0 1 0 487608945 615247872 127446 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150207 127446 603 41 0 150166 0
vsize: 600828
[startup+950.149 s]
Raw data (loadavg): 1.06 1.02 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 197963 0 0 0 94539 488 0 0 25 0 1 0 487608945 617111552 127903 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 150662 127903 603 41 0 150621 0
vsize: 602648
[startup+960.149 s]
Raw data (loadavg): 1.05 1.01 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 198439 0 0 0 95539 489 0 0 25 0 1 0 487608945 619048960 128379 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151135 128379 603 41 0 151094 0
vsize: 604540
[startup+970.15 s]
Raw data (loadavg): 1.04 1.01 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 198948 0 0 0 96537 490 0 0 25 0 1 0 487608945 621248512 128888 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 151672 128888 603 41 0 151631 0
vsize: 606688
[startup+980.151 s]
Raw data (loadavg): 1.04 1.01 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 199303 0 0 0 97537 491 0 0 25 0 1 0 487608945 622600192 129243 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152002 129243 603 41 0 151961 0
vsize: 608008
[startup+990.15 s]
Raw data (loadavg): 1.03 1.01 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 199741 0 0 0 98536 492 0 0 25 0 1 0 487608945 624455680 129681 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152455 129681 603 41 0 152414 0
vsize: 609820
[startup+1000.15 s]
Raw data (loadavg): 1.02 1.01 0.87 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 200282 0 0 0 99535 493 0 0 25 0 1 0 487608945 626634752 130222 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 152987 130222 603 41 0 152946 0
vsize: 611948
[startup+1010.15 s]
Raw data (loadavg): 1.02 1.01 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 200579 0 0 0 100534 494 0 0 25 0 1 0 487608945 627904512 130519 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153297 130519 603 41 0 153256 0
vsize: 613188
[startup+1020.15 s]
Raw data (loadavg): 1.02 1.01 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 200968 0 0 0 101534 495 0 0 25 0 1 0 487608945 629514240 130908 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 153690 130908 603 41 0 153649 0
vsize: 614760
[startup+1030.15 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 201974 0 0 0 102532 497 0 0 25 0 1 0 487608945 633651200 131914 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 154700 131914 603 41 0 154659 0
vsize: 618800
[startup+1040.15 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 203195 0 0 0 103529 500 0 0 25 0 1 0 487608945 638652416 133135 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 155921 133135 603 41 0 155880 0
vsize: 623684
[startup+1050.15 s]
Raw data (loadavg): 1.01 1.01 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 221222 0 0 0 104480 549 0 0 25 0 1 0 487608945 641441792 133752 4294967295 134512640 134672761 3221224576 3221222848 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156602 133752 603 41 0 156561 0
vsize: 626408
[startup+1060.15 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 223186 0 0 0 105474 554 0 0 25 0 1 0 487608945 641310720 133728 4294967295 134512640 134672761 3221224576 3221223136 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156570 133728 603 41 0 156529 0
vsize: 626280
[startup+1070.15 s]
Raw data (loadavg): 1.01 1.00 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226067 0 0 0 106468 561 0 0 25 0 1 0 487608945 640602112 133643 4294967295 134512640 134672761 3221224576 3221223832 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156397 133643 603 41 0 156356 0
vsize: 625588
[startup+1080.15 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226067 0 0 0 107468 561 0 0 25 0 1 0 487608945 640602112 133643 4294967295 134512640 134672761 3221224576 3221223720 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156397 133643 603 41 0 156356 0
vsize: 625588
[startup+1090.15 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226082 0 0 0 108468 561 0 0 25 0 1 0 487608945 640733184 133658 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156429 133658 603 41 0 156388 0
vsize: 625716
[startup+1100.15 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226131 0 0 0 109468 561 0 0 25 0 1 0 487608945 640868352 133707 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156462 133707 603 41 0 156421 0
vsize: 625848
[startup+1110.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226349 0 0 0 110468 561 0 0 25 0 1 0 487608945 641785856 133925 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 156686 133925 603 41 0 156645 0
vsize: 626744
[startup+1120.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 226776 0 0 0 111467 562 0 0 25 0 1 0 487608945 643538944 134352 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157114 134352 603 41 0 157073 0
vsize: 628456
[startup+1130.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 227252 0 0 0 112467 563 0 0 25 0 1 0 487608945 645537792 134828 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 157602 134828 603 41 0 157561 0
vsize: 630408
[startup+1140.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 227830 0 0 0 113466 564 0 0 25 0 1 0 487608945 647892992 135406 4294967295 134512640 134672761 3221224576 3221223760 134615544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158177 135406 603 41 0 158136 0
vsize: 632708
[startup+1150.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 228647 0 0 0 114464 566 0 0 25 0 1 0 487608945 651198464 136223 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 158984 136223 603 41 0 158943 0
vsize: 635936
[startup+1160.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 229257 0 0 0 115463 567 0 0 25 0 1 0 487608945 653721600 136833 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159600 136833 603 41 0 159559 0
vsize: 638400
[startup+1170.15 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 229540 0 0 0 116463 568 0 0 25 0 1 0 487608945 654921728 137116 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 159893 137116 603 41 0 159852 0
vsize: 639572
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 230375 0 0 0 117461 570 0 0 25 0 1 0 487608945 658309120 137951 4294967295 134512640 134672761 3221224576 3221223584 134522540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 160720 137951 603 41 0 160679 0
vsize: 642880
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 231860 0 0 0 118459 572 0 0 25 0 1 0 487608945 664342528 139436 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 162193 139436 603 41 0 162152 0
vsize: 648772
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 5156
Raw data (stat): 5099 (minisat+) R 5098 22612 22611 0 -1 0 233735 0 0 0 119455 576 0 0 25 0 1 0 487608945 672104448 141311 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 164088 141311 603 41 0 164047 0
vsize: 656352
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.45 s]
Raw data (loadavg): 1.00 1.00 0.89 1/54 5156
Raw data (stat): 5099 (minisat+) Z 5098 22612 22611 0 -1 12 233736 0 0 0 119457 603 0 0 25 0 1 0 487608945 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.45
CPU time (s): 1200.61
CPU user time (s): 1194.57
CPU system time (s): 6.03508
CPU usage (%): 100.013
Max. virtual memory (Kb): 656352
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####