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/web/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ss97-2.opb
MD5SUM	5e8935802e4aa1a1ac8f2a923d842947
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	22547
Optimality of the best value was proved	NO
Number of terms in the objective function	6892
Biggest coefficient in the objective function	667
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	371779
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	667
Number of bits of the biggest number in a constraint	10
Biggest sum of numbers in a constraint	371779
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	8405
Total number of constraints	19071
Number of constraints which are clauses	9918
Number of constraints which are cardinality constraints (but not clauses)	9153
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	351
Trace number 5654

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 01:17:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4114 boxname=wulflinc4 idbench=354 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5e8935802e4aa1a1ac8f2a923d842947  /oldhome/oroussel/tmp/wulflinc4/normalized-ss97-2.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc4/normalized-ss97-2.opb /oldhome/oroussel/tmp/wulflinc4/normalized-ss97-2.opb
IDLAUNCH: 4114
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898740 kB
Buffers:         35308 kB
Cached:          80836 kB
SwapCached:          0 kB
Active:          55212 kB
Inactive:        63848 kB
HighTotal:      131008 kB
HighFree:        46340 kB
LowTotal:       903652 kB
LowFree:        852400 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11268 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:38:08 (client local time) WITH STATUS 10 IN 1208.97 SECONDS
stats: 4114 7 1208.97 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 11366 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[11365]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11364]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11363]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11362]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11361]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11360]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11359]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11358]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11357]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11356]---> Adder-cost: 686   maxlim: 311   bits: 9/9
c ---[11355]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11354]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11353]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11352]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11351]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11350]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11349]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11348]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11347]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11346]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11345]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11344]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11343]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11342]---> Adder-cost: 688   maxlim: 321   bits: 9/9
c ---[11341]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11340]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11339]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11338]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11337]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11336]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11335]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11334]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11333]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11332]---> Adder-cost: 46   maxlim: 26   bits: 6/5
c ---[11331]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11330]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11329]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11328]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11327]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11326]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11325]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11324]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11323]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11322]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11321]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11320]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11319]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11318]---> Adder-cost: 9   maxlim: 21   bits: 6/5
c ---[11316]---> BDD-cost:   17
c ---[11314]---> BDD-cost:   25
c ---[11312]---> BDD-cost:   17
c ---[11310]---> BDD-cost:   25
c ---[11308]---> BDD-cost:   17
c ---[11306]---> BDD-cost:   25
c ---[11304]---> BDD-cost:   17
c ---[11302]---> BDD-cost:   25
c ---[11300]---> BDD-cost:   17
c ---[11298]---> BDD-cost:   25
c ---[11296]---> BDD-cost:   17
c ---[11294]---> BDD-cost:   25
c ---[11292]---> BDD-cost:   17
c ---[11290]---> BDD-cost:   25
c ---[11288]---> BDD-cost:   17
c ---[11286]---> BDD-cost:   25
c ---[11284]---> BDD-cost:   17
c ---[11282]---> BDD-cost:   25
c ---[11280]---> BDD-cost:   17
c ---[11278]---> BDD-cost:   25
c ---[11276]---> BDD-cost:   17
c ---[11274]---> BDD-cost:   25
c ---[11272]---> BDD-cost:   17
c ---[11270]---> BDD-cost:   25
c ---[11268]---> BDD-cost:   17
c ---[11266]---> BDD-cost:   25
c ---[11264]---> BDD-cost:   17
c ---[11262]---> BDD-cost:   25
c ---[11260]---> BDD-cost:   17
c ---[11258]---> BDD-cost:   25
c ---[11256]---> BDD-cost:   17
c ---[11254]---> BDD-cost:   25
c ---[11252]---> BDD-cost:   17
c ---[11250]---> BDD-cost:   25
c ---[11248]---> BDD-cost:   17
c ---[11246]---> BDD-cost:   25
c ---[11244]---> BDD-cost:   17
c ---[11242]---> BDD-cost:   25
c ---[11240]---> BDD-cost:   17
c ---[11238]---> BDD-cost:   25
c ---[11236]---> BDD-cost:   17
c ---[11234]---> BDD-cost:   25
c ---[11232]---> BDD-cost:   17
c ---[11230]---> BDD-cost:   25
c ---[11228]---> BDD-cost:   17
c ---[11226]---> BDD-cost:   25
c ---[11224]---> BDD-cost:   17
c ---[11222]---> BDD-cost:   25
c ---[11220]---> BDD-cost:   17
c ---[11218]---> BDD-cost:   25
c ---[11216]---> BDD-cost:   17
c ---[11214]---> BDD-cost:   25
c ---[11212]---> BDD-cost:   17
c ---[11210]---> BDD-cost:   25
c ---[11208]---> BDD-cost:   17
c ---[11206]---> BDD-cost:   25
c ---[11204]---> BDD-cost:   17
c ---[11202]---> BDD-cost:   25
c ---[11200]---> BDD-cost:   17
c ---[11198]---> BDD-cost:   25
c ---[11196]---> BDD-cost:   17
c ---[11194]---> BDD-cost:   25
c ---[11192]---> BDD-cost:   17
c ---[11190]---> BDD-cost:   25
c ---[11188]---> BDD-cost:   17
c ---[11186]---> BDD-cost:   25
c ---[11184]---> BDD-cost:   17
c ---[11182]---> BDD-cost:   25
c ---[11180]---> BDD-cost:   17
c ---[11178]---> BDD-cost:   25
c ---[11176]---> BDD-cost:   17
c ---[11174]---> BDD-cost:   25
c ---[11172]---> BDD-cost:   17
c ---[11170]---> BDD-cost:   25
c ---[11168]---> BDD-cost:   17
c ---[11166]---> BDD-cost:   25
c ---[11164]---> BDD-cost:   17
c ---[11162]---> BDD-cost:   25
c ---[11160]---> BDD-cost:   17
c ---[11158]---> BDD-cost:   25
c ---[11156]---> BDD-cost:   17
c ---[11154]---> BDD-cost:   25
c ---[11152]---> BDD-cost:   17
c ---[11150]---> BDD-cost:   25
c ---[11148]---> BDD-cost:   17
c ---[11146]---> BDD-cost:   25
c ---[11144]---> BDD-cost:   17
c ---[11142]---> BDD-cost:   25
c ---[11140]---> BDD-cost:   17
c ---[11138]---> BDD-cost:   25
c ---[11136]---> BDD-cost:   17
c ---[11134]---> BDD-cost:   25
c ---[11132]---> BDD-cost:   17
c ---[11130]---> BDD-cost:   25
c ---[11128]---> BDD-cost:   17
c ---[11126]---> BDD-cost:   25
c ---[11124]---> BDD-cost:   17
c ---[11122]---> BDD-cost:   25
c ---[11120]---> BDD-cost:   17
c ---[11118]---> BDD-cost:   25
c ---[11116]---> BDD-cost:   17
c ---[11114]---> BDD-cost:   25
c ---[11112]---> BDD-cost:   17
c ---[11110]---> BDD-cost:   25
c ---[11108]---> BDD-cost:   17
c ---[11106]---> BDD-cost:   25
c ---[11104]---> BDD-cost:   17
c ---[11102]---> BDD-cost:   25
c ---[11100]---> BDD-cost:   25
c ---[11098]---> BDD-cost:   17
c ---[11096]---> BDD-cost:   25
c ---[11094]---> BDD-cost:   17
c ---[11092]---> BDD-cost:   25
c ---[11090]---> BDD-cost:   17
c ---[11088]---> BDD-cost:   25
c ---[11086]---> BDD-cost:   17
c ---[11084]---> BDD-cost:   25
c ---[11082]---> BDD-cost:   17
c ---[11080]---> BDD-cost:   25
c ---[11078]---> BDD-cost:   17
c ---[11076]---> BDD-cost:   25
c ---[11074]---> BDD-cost:   17
c ---[11072]---> BDD-cost:   25
c ---[11070]---> BDD-cost:   25
c ---[11068]---> BDD-cost:   17
c ---[11066]---> BDD-cost:   25
c ---[11064]---> BDD-cost:   17
c ---[11062]---> BDD-cost:   25
c ---[11060]---> BDD-cost:   17
c ---[11058]---> BDD-cost:   25
c ---[11056]---> BDD-cost:   17
c ---[11054]---> BDD-cost:   25
c ---[11052]---> BDD-cost:   17
c ---[11050]---> BDD-cost:   25
c ---[11048]---> BDD-cost:   17
c ---[11046]---> BDD-cost:   25
c ---[11044]---> BDD-cost:   17
c ---[11042]---> BDD-cost:   25
c ---[11040]---> BDD-cost:   17
c ---[11038]---> BDD-cost:   25
c ---[11036]---> BDD-cost:   17
c ---[11034]---> BDD-cost:   25
c ---[11032]---> BDD-cost:   17
c ---[11030]---> BDD-cost:   25
c ---[11028]---> BDD-cost:   17
c ---[11026]---> BDD-cost:   25
c ---[11024]---> BDD-cost:   17
c ---[11022]---> BDD-cost:   25
c ---[11020]---> BDD-cost:   17
c ---[11018]---> BDD-cost:   25
c ---[11016]---> BDD-cost:   17
c ---[11014]---> BDD-cost:   25
c ---[11012]---> BDD-cost:   17
c ---[11010]---> BDD-cost:   25
c ---[11008]---> BDD-cost:   25
c ---[11006]---> BDD-cost:   17
c ---[11004]---> BDD-cost:   25
c ---[11002]---> BDD-cost:   17
c ---[11000]---> BDD-cost:   25
c ---[10998]---> BDD-cost:   17
c ---[10996]---> BDD-cost:   25
c ---[10994]---> BDD-cost:   17
c ---[10992]---> BDD-cost:   25
c ---[10990]---> BDD-cost:   17
c ---[10988]---> BDD-cost:   25
c ---[10986]---> BDD-cost:   17
c ---[10984]---> BDD-cost:   25
c ---[10982]---> BDD-cost:   17
c ---[10980]---> BDD-cost:   25
c ---[10978]---> BDD-cost:   17
c ---[10976]---> BDD-cost:   25
c ---[10974]---> BDD-cost:   17
c ---[10972]---> BDD-cost:   25
c ---[10970]---> BDD-cost:   17
c ---[10968]---> BDD-cost:   25
c ---[10966]---> BDD-cost:   17
c ---[10964]---> BDD-cost:   25
c ---[10962]---> BDD-cost:   17
c ---[10960]---> BDD-cost:   25
c ---[10958]---> BDD-cost:   17
c ---[10956]---> BDD-cost:   25
c ---[10954]---> BDD-cost:   17
c ---[10952]---> BDD-cost:   25
c ---[10950]---> BDD-cost:   17
c ---[10948]---> BDD-cost:   25
c ---[10946]---> BDD-cost:   17
c ---[10944]---> BDD-cost:   25
c ---[10942]---> BDD-cost:   17
c ---[10940]---> BDD-cost:   25
c ---[10938]---> BDD-cost:   17
c ---[10936]---> BDD-cost:   25
c ---[10934]---> BDD-cost:   17
c ---[10932]---> BDD-cost:   25
c ---[10930]---> BDD-cost:   17
c ---[10928]---> BDD-cost:   25
c ---[10926]---> BDD-cost:   17
c ---[10924]---> BDD-cost:   25
c ---[10922]---> BDD-cost:   17
c ---[10920]---> BDD-cost:   25
c ---[10918]---> BDD-cost:   17
c ---[10916]---> BDD-cost:   25
c ---[10914]---> BDD-cost:   17
c ---[10912]---> BDD-cost:   25
c ---[10910]---> BDD-cost:   17
c ---[10908]---> BDD-cost:   25
c ---[10906]---> BDD-cost:   25
c ---[10904]---> BDD-cost:   17
c ---[10902]---> BDD-cost:   25
c ---[10900]---> BDD-cost:   17
c ---[10898]---> BDD-cost:   25
c ---[10896]---> BDD-cost:   17
c ---[10894]---> BDD-cost:   25
c ---[10892]---> BDD-cost:   17
c ---[10890]---> BDD-cost:   25
c ---[10888]---> BDD-cost:   17
c ---[10886]---> BDD-cost:   25
c ---[10884]---> BDD-cost:   17
c ---[10882]---> BDD-cost:   25
c ---[10880]---> BDD-cost:   17
c ---[10878]---> BDD-cost:   25
c ---[10876]---> BDD-cost:   17
c ---[10874]---> BDD-cost:   25
c ---[10872]---> BDD-cost:   17
c ---[10870]---> BDD-cost:   25
c ---[10868]---> BDD-cost:   17
c ---[10866]---> BDD-cost:   25
c ---[10864]---> BDD-cost:   17
c ---[10862]---> BDD-cost:   25
c ---[10860]---> BDD-cost:   17
c ---[10858]---> BDD-cost:   25
c ---[10856]---> BDD-cost:   17
c ---[10854]---> BDD-cost:   25
c ---[10852]---> BDD-cost:   17
c ---[10850]---> BDD-cost:   25
c ---[10848]---> BDD-cost:   17
c ---[10846]---> BDD-cost:   25
c ---[10844]---> BDD-cost:   17
c ---[10842]---> BDD-cost:   25
c ---[10840]---> BDD-cost:   17
c ---[10838]---> BDD-cost:   25
c ---[10836]---> BDD-cost:   17
c ---[10834]---> BDD-cost:   25
c ---[10832]---> BDD-cost:   17
c ---[10830]---> BDD-cost:   25
c ---[10828]---> BDD-cost:   17
c ---[10826]---> BDD-cost:   25
c ---[10824]---> BDD-cost:   17
c ---[10822]---> BDD-cost:   25
c ---[10820]---> BDD-cost:   17
c ---[10818]---> BDD-cost:   25
c ---[10816]---> BDD-cost:   17
c ---[10814]---> BDD-cost:   25
c ---[10812]---> BDD-cost:   17
c ---[10810]---> BDD-cost:   25
c ---[10808]---> BDD-cost:   17
c ---[10806]---> BDD-cost:   25
c ---[10804]---> BDD-cost:   17
c ---[10802]---> BDD-cost:   25
c ---[10800]---> BDD-cost:   17
c ---[10798]---> BDD-cost:   25
c ---[10796]---> BDD-cost:   17
c ---[10794]---> BDD-cost:   25
c ---[10792]---> BDD-cost:   17
c ---[10790]---> BDD-cost:   25
c ---[10788]---> BDD-cost:   17
c ---[10786]---> BDD-cost:   25
c ---[10784]---> BDD-cost:   17
c ---[10782]---> BDD-cost:   25
c ---[10780]---> BDD-cost:   17
c ---[10778]---> BDD-cost:   25
c ---[10776]---> BDD-cost:   17
c ---[10774]---> BDD-cost:   25
c ---[10772]---> BDD-cost:   17
c ---[10770]---> BDD-cost:   25
c ---[10768]---> BDD-cost:   17
c ---[10766]---> BDD-cost:   25
c ---[10764]---> BDD-cost:   17
c ---[10762]---> BDD-cost:   25
c ---[10760]---> BDD-cost:   17
c ---[10758]---> BDD-cost:   25
c ---[10756]---> BDD-cost:   17
c ---[10754]---> BDD-cost:   25
c ---[10752]---> BDD-cost:   17
c ---[10750]---> BDD-cost:   25
c ---[10748]---> BDD-cost:   17
c ---[10746]---> BDD-cost:   25
c ---[10744]---> BDD-cost:   17
c ---[10742]---> BDD-cost:   25
c ---[10740]---> BDD-cost:   17
c ---[10738]---> BDD-cost:   25
c ---[10736]---> BDD-cost:   17
c ---[10734]---> BDD-cost:   25
c ---[10732]---> BDD-cost:   17
c ---[10730]---> BDD-cost:   25
c ---[10728]---> BDD-cost:   17
c ---[10726]---> BDD-cost:   25
c ---[10724]---> BDD-cost:   17
c ---[10722]---> BDD-cost:   25
c ---[10720]---> BDD-cost:   17
c ---[10718]---> BDD-cost:   25
c ---[10716]---> BDD-cost:   17
c ---[10714]---> BDD-cost:   25
c ---[10712]---> BDD-cost:   17
c ---[10710]---> BDD-cost:   25
c ---[10708]---> BDD-cost:   17
c ---[10706]---> BDD-cost:   25
c ---[10704]---> BDD-cost:   17
c ---[10702]---> BDD-cost:   25
c ---[10700]---> BDD-cost:   17
c ---[10698]---> BDD-cost:   25
c ---[10696]---> BDD-cost:   17
c ---[10694]---> BDD-cost:   25
c ---[10692]---> BDD-cost:   17
c ---[10690]---> BDD-cost:   25
c ---[10688]---> BDD-cost:   17
c ---[10686]---> BDD-cost:   25
c ---[10684]---> BDD-cost:   17
c ---[10682]---> BDD-cost:   25
c ---[10680]---> BDD-cost:   17
c ---[10678]---> BDD-cost:   25
c ---[10676]---> BDD-cost:   17
c ---[10674]---> BDD-cost:   25
c ---[10672]---> BDD-cost:   17
c ---[10670]---> BDD-cost:   25
c ---[10668]---> BDD-cost:   17
c ---[10666]---> BDD-cost:   25
c ---[10664]---> BDD-cost:   17
c ---[10662]---> BDD-cost:   25
c ---[10660]---> BDD-cost:   17
c ---[10658]---> BDD-cost:   25
c ---[10656]---> BDD-cost:   17
c ---[10654]---> BDD-cost:   25
c ---[10652]---> BDD-cost:   17
c ---[10650]---> BDD-cost:   25
c ---[10648]---> BDD-cost:   17
c ---[10646]---> BDD-cost:   25
c ---[10644]---> BDD-cost:   17
c ---[10642]---> BDD-cost:   25
c ---[10640]---> BDD-cost:   17
c ---[10638]---> BDD-cost:   25
c ---[10636]---> BDD-cost:   17
c ---[10634]---> BDD-cost:   25
c ---[10632]---> BDD-cost:   17
c ---[10630]---> BDD-cost:   25
c ---[10628]---> BDD-cost:   17
c ---[10626]---> BDD-cost:   25
c ---[10624]---> BDD-cost:   17
c ---[10622]---> BDD-cost:   25
c ---[10620]---> BDD-cost:   25
c ---[10618]---> BDD-cost:   17
c ---[10616]---> BDD-cost:   25
c ---[10614]---> BDD-cost:   17
c ---[10612]---> BDD-cost:   25
c ---[10610]---> BDD-cost:   17
c ---[10608]---> BDD-cost:   25
c ---[10606]---> BDD-cost:   17
c ---[10604]---> BDD-cost:   25
c ---[10602]---> BDD-cost:   17
c ---[10600]---> BDD-cost:   25
c ---[10598]---> BDD-cost:   17
c ---[10596]---> BDD-cost:   25
c ---[10594]---> BDD-cost:   17
c ---[10592]---> BDD-cost:   25
c ---[10590]---> BDD-cost:   17
c ---[10588]---> BDD-cost:   17
c ---[10586]---> BDD-cost:   25
c ---[10584]---> BDD-cost:   17
c ---[10582]---> BDD-cost:   25
c ---[10580]---> BDD-cost:   17
c ---[10578]---> BDD-cost:   25
c ---[10576]---> BDD-cost:   17
c ---[10574]---> BDD-cost:   25
c ---[10572]---> BDD-cost:   17
c ---[10570]---> BDD-cost:   25
c ---[10568]---> BDD-cost:   17
c ---[10566]---> BDD-cost:   25
c ---[10564]---> BDD-cost:   17
c ---[10562]---> BDD-cost:   25
c ---[10560]---> BDD-cost:   17
c ---[10558]---> BDD-cost:   25
c ---[10556]---> BDD-cost:   17
c ---[10554]---> BDD-cost:   25
c ---[10552]---> BDD-cost:   17
c ---[10550]---> BDD-cost:   25
c ---[10548]---> BDD-cost:   17
c ---[10546]---> BDD-cost:   25
c ---[10544]---> BDD-cost:   17
c ---[10542]---> BDD-cost:   25
c ---[10540]---> BDD-cost:   17
c ---[10538]---> BDD-cost:   25
c ---[10536]---> BDD-cost:   17
c ---[10534]---> BDD-cost:   25
c ---[10532]---> BDD-cost:   17
c ---[10530]---> BDD-cost:   25
c ---[10528]---> BDD-cost:   17
c ---[10526]---> BDD-cost:   25
c ---[10524]---> BDD-cost:   17
c ---[10522]---> BDD-cost:   25
c ---[10520]---> BDD-cost:   17
c ---[10518]---> BDD-cost:   25
c ---[10516]---> BDD-cost:   17
c ---[10514]---> BDD-cost:   25
c ---[10512]---> BDD-cost:   17
c ---[10510]---> BDD-cost:   25
c ---[10508]---> BDD-cost:   17
c ---[10506]---> BDD-cost:   25
c ---[10504]---> BDD-cost:   17
c ---[10502]---> BDD-cost:   25
c ---[10500]---> BDD-cost:   17
c ---[10498]---> BDD-cost:   25
c ---[10496]---> BDD-cost:   17
c ---[10494]---> BDD-cost:   25
c ---[10492]---> BDD-cost:   17
c ---[10490]---> BDD-cost:   25
c ---[10488]---> BDD-cost:   17
c ---[10486]---> BDD-cost:   25
c ---[10484]---> BDD-cost:   17
c ---[10482]---> BDD-cost:   25
c ---[10480]---> BDD-cost:   17
c ---[10478]---> BDD-cost:   25
c ---[10476]---> BDD-cost:   17
c ---[10474]---> BDD-cost:   25
c ---[10472]---> BDD-cost:   17
c ---[10470]---> BDD-cost:   25
c ---[10468]---> BDD-cost:   17
c ---[10466]---> BDD-cost:   25
c ---[10464]---> BDD-cost:   17
c ---[10462]---> BDD-cost:   25
c ---[10460]---> BDD-cost:   17
c ---[10458]---> BDD-cost:   25
c ---[10456]---> BDD-cost:   17
c ---[10454]---> BDD-cost:   25
c ---[10452]---> BDD-cost:   17
c ---[10450]---> BDD-cost:   25
c ---[10448]---> BDD-cost:   17
c ---[10446]---> BDD-cost:   25
c ---[10444]---> BDD-cost:   17
c ---[10442]---> BDD-cost:   25
c ---[10440]---> BDD-cost:   17
c ---[10438]---> BDD-cost:   25
c ---[10436]---> BDD-cost:   17
c ---[10434]---> BDD-cost:   25
c ---[10432]---> BDD-cost:   17
c ---[10430]---> BDD-cost:   25
c ---[10428]---> BDD-cost:   17
c ---[10426]---> BDD-cost:   25
c ---[10424]---> BDD-cost:   17
c ---[10422]---> BDD-cost:   25
c ---[10420]---> BDD-cost:   17
c ---[10418]---> BDD-cost:   25
c ---[10416]---> BDD-cost:   17
c ---[10414]---> BDD-cost:   25
c ---[10412]---> BDD-cost:   17
c ---[10410]---> BDD-cost:   25
c ---[10408]---> BDD-cost:   17
c ---[10406]---> BDD-cost:   17
c ---[10404]---> BDD-cost:   25
c ---[10402]---> BDD-cost:   17
c ---[10400]---> BDD-cost:   25
c ---[10398]---> BDD-cost:   17
c ---[10396]---> BDD-cost:   25
c ---[10394]---> BDD-cost:   17
c ---[10392]---> BDD-cost:   25
c ---[10390]---> BDD-cost:   17
c ---[10388]---> BDD-cost:   25
c ---[10386]---> BDD-cost:   17
c ---[10384]---> BDD-cost:   25
c ---[10382]---> BDD-cost:   17
c ---[10380]---> BDD-cost:   25
c ---[10378]---> BDD-cost:   17
c ---[10376]---> BDD-cost:   25
c ---[10374]---> BDD-cost:   17
c ---[10372]---> BDD-cost:   25
c ---[10370]---> BDD-cost:   17
c ---[10368]---> BDD-cost:   25
c ---[10366]---> BDD-cost:   17
c ---[10364]---> BDD-cost:   25
c ---[10362]---> BDD-cost:   17
c ---[10360]---> BDD-cost:   25
c ---[10358]---> BDD-cost:   17
c ---[10356]---> BDD-cost:   25
c ---[10354]---> BDD-cost:   17
c ---[10352]---> BDD-cost:   25
c ---[10350]---> BDD-cost:   17
c ---[10348]---> BDD-cost:   25
c ---[10346]---> BDD-cost:   17
c ---[10344]---> BDD-cost:   25
c ---[10342]---> BDD-cost:   17
c ---[10340]---> BDD-cost:   25
c ---[10338]---> BDD-cost:   17
c ---[10336]---> BDD-cost:   25
c ---[10334]---> BDD-cost:   17
c ---[10332]---> BDD-cost:   25
c ---[10330]---> BDD-cost:   17
c ---[10328]---> BDD-cost:   25
c ---[10326]---> BDD-cost:   17
c ---[10324]---> BDD-cost:   25
c ---[10322]---> BDD-cost:   17
c ---[10320]---> BDD-cost:   25
c ---[10318]---> BDD-cost:   17
c ---[10316]---> BDD-cost:   25
c ---[10314]---> BDD-cost:   17
c ---[10312]---> BDD-cost:   25
c ---[10310]---> BDD-cost:   17
c ---[10308]---> BDD-cost:   25
c ---[10306]---> BDD-cost:   17
c ---[10304]---> BDD-cost:   25
c ---[10302]---> BDD-cost:   17
c ---[10300]---> BDD-cost:   25
c ---[10298]---> BDD-cost:   17
c ---[10296]---> BDD-cost:   25
c ---[10294]---> BDD-cost:   17
c ---[10292]---> BDD-cost:   25
c ---[10290]---> BDD-cost:   17
c ---[10288]---> BDD-cost:   25
c ---[10286]---> BDD-cost:   17
c ---[10284]---> BDD-cost:   25
c ---[10282]---> BDD-cost:   17
c ---[10280]---> BDD-cost:   25
c ---[10278]---> BDD-cost:   17
c ---[10276]---> BDD-cost:   25
c ---[10274]---> BDD-cost:   17
c ---[10272]---> BDD-cost:   25
c ---[10270]---> BDD-cost:   17
c ---[10268]---> BDD-cost:   25
c ---[10266]---> BDD-cost:   17
c ---[10264]---> BDD-cost:   25
c ---[10262]---> BDD-cost:   17
c ---[10260]---> BDD-cost:   25
c ---[10258]---> BDD-cost:   17
c ---[10256]---> BDD-cost:   25
c ---[10254]---> BDD-cost:   17
c ---[10252]---> BDD-cost:   25
c ---[10250]---> BDD-cost:   17
c ---[10248]---> BDD-cost:   25
c ---[10246]---> BDD-cost:   17
c ---[10244]---> BDD-cost:   25
c ---[10242]---> BDD-cost:   17
c ---[10240]---> BDD-cost:   25
c ---[10238]---> BDD-cost:   17
c ---[10236]---> BDD-cost:   25
c ---[10234]---> BDD-cost:   17
c ---[10232]---> BDD-cost:   25
c ---[10230]---> BDD-cost:   17
c ---[10228]---> BDD-cost:   25
c ---[10226]---> BDD-cost:   17
c ---[10224]---> BDD-cost:   25
c ---[10222]---> BDD-cost:   17
c ---[10220]---> BDD-cost:   25
c ---[10218]---> BDD-cost:   17
c ---[10216]---> BDD-cost:   25
c ---[10214]---> BDD-cost:   17
c ---[10212]---> BDD-cost:   25
c ---[10210]---> BDD-cost:   25
c ---[10208]---> BDD-cost:   17
c ---[10206]---> BDD-cost:   25
c ---[10204]---> BDD-cost:   17
c ---[10202]---> BDD-cost:   25
c ---[10200]---> BDD-cost:   17
c ---[10198]---> BDD-cost:   25
c ---[10196]---> BDD-cost:   17
c ---[10194]---> BDD-cost:   25
c ---[10192]---> BDD-cost:   17
c ---[10190]---> BDD-cost:   25
c ---[10188]---> BDD-cost:   17
c ---[10186]---> BDD-cost:   25
c ---[10184]---> BDD-cost:   17
c ---[10182]---> BDD-cost:   25
c ---[10180]---> BDD-cost:   17
c ---[10178]---> BDD-cost:   25
c ---[10176]---> BDD-cost:   17
c ---[10174]---> BDD-cost:   25
c ---[10172]---> BDD-cost:   17
c ---[10170]---> BDD-cost:   25
c ---[10168]---> BDD-cost:   17
c ---[10166]---> BDD-cost:   25
c ---[10164]---> BDD-cost:   17
c ---[10162]---> BDD-cost:   25
c ---[10160]---> BDD-cost:   17
c ---[10158]---> BDD-cost:   25
c ---[10156]---> BDD-cost:   17
c ---[10154]---> BDD-cost:   25
c ---[10152]---> BDD-cost:   25
c ---[10150]---> BDD-cost:   17
c ---[10148]---> BDD-cost:   25
c ---[10146]---> BDD-cost:   17
c ---[10144]---> BDD-cost:   25
c ---[10142]---> BDD-cost:   17
c ---[10140]---> BDD-cost:   25
c ---[10138]---> BDD-cost:   17
c ---[10136]---> BDD-cost:   25
c ---[10134]---> BDD-cost:   17
c ---[10132]---> BDD-cost:   25
c ---[10130]---> BDD-cost:   17
c ---[10128]---> BDD-cost:   17
c ---[10126]---> BDD-cost:   25
c ---[10124]---> BDD-cost:   17
c ---[10122]---> BDD-cost:   25
c ---[10120]---> BDD-cost:   17
c ---[10118]---> BDD-cost:   25
c ---[10116]---> BDD-cost:   17
c ---[10114]---> BDD-cost:   25
c ---[10112]---> BDD-cost:   17
c ---[10110]---> BDD-cost:   25
c ---[10108]---> BDD-cost:   17
c ---[10106]---> BDD-cost:   25
c ---[10104]---> BDD-cost:   17
c ---[10102]---> BDD-cost:   25
c ---[10100]---> BDD-cost:   17
c ---[10098]---> BDD-cost:   25
c ---[10096]---> BDD-cost:   17
c ---[10094]---> BDD-cost:   25
c ---[10092]---> BDD-cost:   17
c ---[10090]---> BDD-cost:   25
c ---[10088]---> BDD-cost:   17
c ---[10086]---> BDD-cost:   25
c ---[10084]---> BDD-cost:   17
c ---[10082]---> BDD-cost:   25
c ---[10080]---> BDD-cost:   17
c ---[10078]---> BDD-cost:   25
c ---[10076]---> BDD-cost:   17
c ---[10074]---> BDD-cost:   25
c ---[10072]---> BDD-cost:   17
c ---[10070]---> BDD-cost:   17
c ---[10068]---> BDD-cost:   25
c ---[10066]---> BDD-cost:   17
c ---[10064]---> BDD-cost:   25
c ---[10062]---> BDD-cost:   17
c ---[10060]---> BDD-cost:   25
c ---[10058]---> BDD-cost:   17
c ---[10056]---> BDD-cost:   25
c ---[10054]---> BDD-cost:   17
c ---[10052]---> BDD-cost:   25
c ---[10050]---> BDD-cost:   17
c ---[10048]---> BDD-cost:   25
c ---[10046]---> BDD-cost:   17
c ---[10044]---> BDD-cost:   25
c ---[10042]---> BDD-cost:   17
c ---[10040]---> BDD-cost:   25
c ---[10038]---> BDD-cost:   17
c ---[10036]---> BDD-cost:   25
c ---[10034]---> BDD-cost:   17
c ---[10032]---> BDD-cost:   25
c ---[10030]---> BDD-cost:   17
c ---[10028]---> BDD-cost:   25
c ---[10026]---> BDD-cost:   17
c ---[10024]---> BDD-cost:   25
c ---[10022]---> BDD-cost:   17
c ---[10020]---> BDD-cost:   25
c ---[10018]---> BDD-cost:   17
c ---[10016]---> BDD-cost:   25
c ---[10014]---> BDD-cost:   17
c ---[10012]---> BDD-cost:   25
c ---[10010]---> BDD-cost:   17
c ---[10008]---> BDD-cost:   25
c ---[10006]---> BDD-cost:   17
c ---[10004]---> BDD-cost:   25
c ---[10002]---> BDD-cost:   17
c ---[10000]---> BDD-cost:   25
c ---[9998]---> BDD-cost:   17
c ---[9996]---> BDD-cost:   25
c ---[9994]---> BDD-cost:   17
c ---[9992]---> BDD-cost:   25
c ---[9990]---> BDD-cost:   17
c ---[9988]---> BDD-cost:   25
c ---[9986]---> BDD-cost:   17
c ---[9984]---> BDD-cost:   25
c ---[9982]---> BDD-cost:   17
c ---[9980]---> BDD-cost:   25
c ---[9978]---> BDD-cost:   17
c ---[9976]---> BDD-cost:   25
c ---[9974]---> BDD-cost:   17
c ---[9972]---> BDD-cost:   25
c ---[9970]---> BDD-cost:   17
c ---[9968]---> BDD-cost:   25
c ---[9966]---> BDD-cost:   17
c ---[9964]---> BDD-cost:   25
c ---[9962]---> BDD-cost:   17
c ---[9960]---> BDD-cost:   25
c ---[9958]---> BDD-cost:   17
c ---[9956]---> BDD-cost:   25
c ---[9954]---> BDD-cost:   17
c ---[9952]---> BDD-cost:   25
c ---[9950]---> BDD-cost:   17
c ---[9948]---> BDD-cost:   25
c ---[9946]---> BDD-cost:   17
c ---[9944]---> BDD-cost:   25
c ---[9942]---> BDD-cost:   17
c ---[9940]---> BDD-cost:   25
c ---[9938]---> BDD-cost:   17
c ---[9936]---> BDD-cost:   25
c ---[9934]---> BDD-cost:   17
c ---[9932]---> BDD-cost:   25
c ---[9930]---> BDD-cost:   17
c ---[9928]---> BDD-cost:   25
c ---[9926]---> BDD-cost:   17
c ---[9924]---> BDD-cost:   25
c ---[9922]---> BDD-cost:   17
c ---[9920]---> BDD-cost:   17
c ---[9918]---> BDD-cost:   25
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  163482   533506 |   49044       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/38842          
c   -- var.elim.:  2000/38842          
c   -- var.elim.:  3000/38842          
c   -- var.elim.:  4000/38842          
c   -- var.elim.:  5000/38842          
c   -- var.elim.:  6000/38842          
c   -- var.elim.:  7000/38842          
c   -- var.elim.:  8000/38842          
c   -- var.elim.:  9000/38842          
c   -- var.elim.:  10000/38842          
c   -- var.elim.:  11000/38842          
c   -- var.elim.:  12000/38842          
c   -- var.elim.:  13000/38842          
c   -- var.elim.:  14000/38842          
c   -- var.elim.:  15000/38842          
c   -- var.elim.:  16000/38842          
c   -- var.elim.:  17000/38842          
c   -- var.elim.:  18000/38842          
c   -- var.elim.:  19000/38842          
c   -- var.elim.:  20000/38842          
c   -- var.elim.:  21000/38842          
c   -- var.elim.:  22000/38842          
c   -- var.elim.:  23000/38842          
c   -- var.elim.:  24000/38842          
c   -- var.elim.:  25000/38842          
c   -- var.elim.:  26000/38842          
c   -- var.elim.:  27000/38842          
c   -- var.elim.:  28000/38842          
c   -- var.elim.:  29000/38842          
c   -- var.elim.:  30000/38842          
c   -- var.elim.:  31000/38842          
c   -- var.elim.:  32000/38842          
c   -- var.elim.:  33000/38842          
c   -- var.elim.:  34000/38842          
c   -- var.elim.:  35000/38842          
c   -- var.elim.:  36000/38842          
c   -- var.elim.:  37000/38842          
c   -- var.elim.:  38000/38842          
c   -- var.elim.:  38842/38842          
c   -- var.elim.:  1000/6860          
c   -- var.elim.:  2000/6860          
c   -- var.elim.:  3000/6860          
c   -- var.elim.:  4000/6860          
c   -- var.elim.:  5000/6860          
c   -- var.elim.:  6000/6860          
c   -- var.elim.:  6860/6860          
c   -- subsuming                       
c   -- var.elim.:  1000/2940          
c   -- var.elim.:  2000/2940          
c   -- var.elim.:  2940/2940          
c   -- var.elim.:  1000/2800          
c   -- var.elim.:  2000/2800          
c   -- var.elim.:  2800/2800          
c   -- subsuming                       
c   -- var.elim.:  1000/2100          
c   -- var.elim.:  2000/2100          
c   -- var.elim.:  2100/2100          
c |         0 |  156754   510006 |      --       0       --      -- |     --   | -6274/-19482
c |         0 |  156754   510006 |   62701       0        0     nan |  0.000 % |
c |       100 |  156754   510006 |   68971     100     1345    13.4 |  3.558 % |
c |       250 |  156754   510006 |   75868     250     1813     7.3 |  3.558 % |
c |       475 |  156754   510006 |   83455     475     2455     5.2 |  3.558 % |
c |       812 |  156754   510006 |   91801     812     3435     4.2 |  3.558 % |
c |      1318 |  156754   510006 |  100981    1318     5237     4.0 |  3.558 % |
c |      2077 |  156754   510006 |  111079    2077     7623     3.7 |  3.558 % |
c |      3216 |  156754   510006 |  122187    3216    12205     3.8 |  3.558 % |
c |      4926 |  156754   510006 |  134406    4926    62336    12.7 |  3.558 % |
c |      7488 |  156754   510006 |  147847    7488    73521     9.8 |  3.558 % |
c |     11332 |  156754   510006 |  162631   11332   101529     9.0 |  3.558 % |
c |     17099 |  156754   510006 |  178894   17099   137532     8.0 |  3.558 % |
c |     25748 |  156754   510006 |  196784   25748   526964    20.5 |  3.558 % |
c |     38722 |  156754   510006 |  216462   38722   738895    19.1 |  3.558 % |
c |     58185 |  156754   510006 |  238109   58185  1893914    32.5 |  3.558 % |
c |     87377 |  156754   510006 |  261920   87377  6378701    73.0 |  3.558 % |
c |    131166 |  156754   510006 |  288112  131166 10449697    79.7 |  3.558 % |
c |    196850 |  156754   510006 |  316923  196850 13147568    66.8 |  3.558 % |
c ==============================================================================
c (current CPU-time: 494.229 s)
c ==============================================================================
c [1mFound solution: 24625[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:505980     Base: 5 5 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    274430 | 1180861  2900541 |  354258  274430 22507764    82.0 |  3.558 % |
c   -- subsuming                       
c   -- var.elim.:  1000/444382          
c   -- var.elim.:  2000/444382          
c   -- var.elim.:  3000/444382          
c   -- var.elim.:  4000/444382          
c   -- var.elim.:  5000/444382          
c   -- var.elim.:  6000/444382          
c   -- var.elim.:  7000/444382          
c   -- var.elim.:  8000/444382          
c   -- var.elim.:  9000/444382          
c   -- var.elim.:  10000/444382          
c   -- var.elim.:  11000/444382          
c   -- var.elim.:  12000/444382          
c   -- var.elim.:  13000/444382          
c   -- var.elim.:  14000/444382          
c   -- var.elim.:  15000/444382          
c   -- var.elim.:  16000/444382          
c   -- var.elim.:  17000/444382          
c   -- var.elim.:  18000/444382          
c   -- var.elim.:  19000/444382          
c   -- var.elim.:  20000/444382          
c   -- var.elim.:  21000/444382          
c   -- var.elim.:  22000/444382          
c   -- var.elim.:  23000/444382          
c   -- var.elim.:  24000/444382          
c   -- var.elim.:  25000/444382          
c   -- var.elim.:  26000/444382          
c   -- var.elim.:  27000/444382          
c   -- var.elim.:  28000/444382          
c   -- var.elim.:  29000/444382          
c   -- var.elim.:  30000/444382          
c   -- var.elim.:  31000/444382          
c   -- var.elim.:  32000/444382          
c   -- var.elim.:  33000/444382          
c   -- var.elim.:  34000/444382          
c   -- var.elim.:  35000/444382          
c   -- var.elim.:  36000/444382          
c   -- var.elim.:  37000/444382          
c   -- var.elim.:  38000/444382          
c   -- var.elim.:  39000/444382          
c   -- var.elim.:  40000/444382          
c   -- var.elim.:  41000/444382          
c   -- var.elim.:  42000/444382          
c   -- var.elim.:  43000/444382          
c   -- var.elim.:  44000/444382          
c   -- var.elim.:  45000/444382          
c   -- var.elim.:  46000/444382          
c   -- var.elim.:  47000/444382          
c   -- var.elim.:  48000/444382          
c   -- var.elim.:  49000/444382          
c   -- var.elim.:  50000/444382          
c   -- var.elim.:  51000/444382          
c   -- var.elim.:  52000/444382          
c   -- var.elim.:  53000/444382          
c   -- var.elim.:  54000/444382          
c   -- var.elim.:  55000/444382          
c   -- var.elim.:  56000/444382          
c   -- var.elim.:  57000/444382          
c   -- var.elim.:  58000/444382          
c   -- var.elim.:  59000/444382          
c   -- var.elim.:  60000/444382          
c   -- var.elim.:  61000/444382          
c   -- var.elim.:  62000/444382          
c   -- var.elim.:  63000/444382          
c   -- var.elim.:  64000/444382          
c   -- var.elim.:  65000/444382          
c   -- var.elim.:  66000/444382          
c   -- var.elim.:  67000/444382          
c   -- var.elim.:  68000/444382          
c   -- var.elim.:  69000/444382          
c   -- var.elim.:  70000/444382          
c   -- var.elim.:  71000/444382          
c   -- var.elim.:  72000/444382          
c   -- var.elim.:  73000/444382          
c   -- var.elim.:  74000/444382          
c   -- var.elim.:  75000/444382          
c   -- var.elim.:  76000/444382          
c   -- var.elim.:  77000/444382          
c   -- var.elim.:  78000/444382          
c   -- var.elim.:  79000/444382          
c   -- var.elim.:  80000/444382          
c   -- var.elim.:  81000/444382          
c   -- var.elim.:  82000/444382          
c   -- var.elim.:  83000/444382          
c   -- var.elim.:  84000/444382          
c   -- var.elim.:  85000/444382          
c   -- var.elim.:  86000/444382          
c   -- var.elim.:  87000/444382          
c   -- var.elim.:  88000/444382          
c   -- var.elim.:  89000/444382          
c   -- var.elim.:  90000/444382          
c   -- var.elim.:  91000/444382          
c   -- var.elim.:  92000/444382          
c   -- var.elim.:  93000/444382          
c   -- var.elim.:  94000/444382          
c   -- var.elim.:  95000/444382          
c   -- var.elim.:  96000/444382          
c   -- var.elim.:  97000/444382          
c   -- var.elim.:  98000/444382          
c   -- var.elim.:  99000/444382          
c   -- var.elim.:  100000/444382          
c   -- var.elim.:  101000/444382          
c   -- var.elim.:  102000/444382          
c   -- var.elim.:  103000/444382          
c   -- var.elim.:  104000/444382          
c   -- var.elim.:  105000/444382          
c   -- var.elim.:  106000/444382          
c   -- var.elim.:  107000/444382          
c   -- var.elim.:  108000/444382          
c   -- var.elim.:  109000/444382          
c   -- var.elim.:  110000/444382          
c   -- var.elim.:  111000/444382          
c   -- var.elim.:  112000/444382          
c   -- var.elim.:  113000/444382          
c   -- var.elim.:  114000/444382          
c   -- var.elim.:  115000/444382          
c   -- var.elim.:  116000/444382          
c   -- var.elim.:  117000/444382          
c   -- var.elim.:  118000/444382          
c   -- var.elim.:  119000/444382          
c   -- var.elim.:  120000/444382          
c   -- var.elim.:  121000/444382          
c   -- var.elim.:  122000/444382          
c   -- var.elim.:  123000/444382          
c   -- var.elim.:  124000/444382          
c   -- var.elim.:  125000/444382          
c   -- var.elim.:  126000/444382          
c   -- var.elim.:  127000/444382          
c   -- var.elim.:  128000/444382          
c   -- var.elim.:  129000/444382          
c   -- var.elim.:  130000/444382          
c   -- var.elim.:  131000/444382          
c   -- var.elim.:  132000/444382          
c   -- var.elim.:  133000/444382          
c   -- var.elim.:  134000/444382          
c   -- var.elim.:  135000/444382          
c   -- var.elim.:  136000/444382          
c   -- var.elim.:  137000/444382          
c   -- var.elim.:  138000/444382          
c   -- var.elim.:  139000/444382          
c   -- var.elim.:  140000/444382          
c   -- var.elim.:  141000/444382          
c   -- var.elim.:  142000/444382          
c   -- var.elim.:  143000/444382          
c   -- var.elim.:  144000/444382          
c   -- var.elim.:  145000/444382          
c   -- var.elim.:  146000/444382          
c   -- var.elim.:  147000/444382          
c   -- var.elim.:  148000/444382          
c   -- var.elim.:  149000/444382          
c   -- var.elim.:  150000/444382          
c   -- var.elim.:  151000/444382          
c   -- var.elim.:  152000/444382          
c   -- var.elim.:  153000/444382          
c   -- var.elim.:  154000/444382          
c   -- var.elim.:  155000/444382          
c   -- var.elim.:  156000/444382          
c   -- var.elim.:  157000/444382          
c   -- var.elim.:  158000/444382          
c   -- var.elim.:  159000/444382          
c   -- var.elim.:  160000/444382          
c   -- var.elim.:  161000/444382          
c   -- var.elim.:  162000/444382          
c   -- var.elim.:  163000/444382          
c   -- var.elim.:  164000/444382          
c   -- var.elim.:  165000/444382          
c   -- var.elim.:  166000/444382          
c   -- var.elim.:  167000/444382          
c   -- var.elim.:  168000/444382          
c   -- var.elim.:  169000/444382          
c   -- var.elim.:  170000/444382          
c   -- var.elim.:  171000/444382          
c   -- var.elim.:  172000/444382          
c   -- var.elim.:  173000/444382          
c   -- var.elim.:  174000/444382          
c   -- var.elim.:  175000/444382          
c   -- var.elim.:  176000/444382          
c   -- var.elim.:  177000/444382          
c   -- var.elim.:  178000/444382          
c   -- var.elim.:  179000/444382          
c   -- var.elim.:  180000/444382          
c   -- var.elim.:  181000/444382          
c   -- var.elim.:  182000/444382          
c   -- var.elim.:  183000/444382          
c   -- var.elim.:  184000/444382          
c   -- var.elim.:  185000/444382          
c   -- var.elim.:  186000/444382          
c   -- var.elim.:  187000/444382          
c   -- var.elim.:  188000/444382          
c   -- var.elim.:  189000/444382          
c   -- var.elim.:  190000/444382          
c   -- var.elim.:  191000/444382          
c   -- var.elim.:  192000/444382          
c   -- var.elim.:  193000/444382          
c   -- var.elim.:  194000/444382          
c   -- var.elim.:  195000/444382          
c   -- var.elim.:  196000/444382          
c   -- var.elim.:  197000/444382          
c   -- var.elim.:  198000/444382          
c   -- var.elim.:  199000/444382          
c   -- var.elim.:  200000/444382          
c   -- var.elim.:  201000/444382          
c   -- var.elim.:  202000/444382          
c   -- var.elim.:  203000/444382          
c   -- var.elim.:  204000/444382          
c   -- var.elim.:  205000/444382          
c   -- var.elim.:  206000/444382          
c   -- var.elim.:  207000/444382          
c   -- var.elim.:  208000/444382          
c   -- var.elim.:  209000/444382          
c   -- var.elim.:  210000/444382          
c   -- var.elim.:  211000/444382          
c   -- var.elim.:  212000/444382          
c   -- var.elim.:  213000/444382          
c   -- var.elim.:  214000/444382          
c   -- var.elim.:  215000/444382          
c   -- var.elim.:  216000/444382          
c   -- var.elim.:  217000/444382          
c   -- var.elim.:  218000/444382          
c   -- var.elim.:  219000/444382          
c   -- var.elim.:  220000/444382          
c   -- var.elim.:  221000/444382          
c   -- var.elim.:  222000/444382          
c   -- var.elim.:  223000/444382          
c   -- var.elim.:  224000/444382          
c   -- var.elim.:  225000/444382          
c   -- var.elim.:  226000/444382          
c   -- var.elim.:  227000/444382          
c   -- var.elim.:  228000/444382          
c   -- var.elim.:  229000/444382          
c   -- var.elim.:  230000/444382          
c   -- var.elim.:  231000/444382          
c   -- var.elim.:  232000/444382          
c   -- var.elim.:  233000/444382          
c   -- var.elim.:  234000/444382          
c   -- var.elim.:  235000/444382          
c   -- var.elim.:  236000/444382          
c   -- var.elim.:  237000/444382          
c   -- var.elim.:  238000/444382          
c   -- var.elim.:  239000/444382          
c   -- var.elim.:  240000/444382          
c   -- var.elim.:  241000/444382          
c   -- var.elim.:  242000/444382          
c   -- var.elim.:  243000/444382          
c   -- var.elim.:  244000/444382          
c   -- var.elim.:  245000/444382          
c   -- var.elim.:  246000/444382          
c   -- var.elim.:  247000/444382          
c   -- var.elim.:  248000/444382          
c   -- var.elim.:  249000/444382          
c   -- var.elim.:  250000/444382          
c   -- var.elim.:  251000/444382          
c   -- var.elim.:  252000/444382          
c   -- var.elim.:  253000/444382          
c   -- var.elim.:  254000/444382          
c   -- var.elim.:  255000/444382          
c   -- var.elim.:  256000/444382          
c   -- var.elim.:  257000/444382          
c   -- var.elim.:  258000/444382          
c   -- var.elim.:  259000/444382          
c   -- var.elim.:  260000/444382          
c   -- var.elim.:  261000/444382          
c   -- var.elim.:  262000/444382          
c   -- var.elim.:  263000/444382          
c   -- var.elim.:  264000/444382          
c   -- var.elim.:  265000/444382          
c   -- var.elim.:  266000/444382          
c   -- var.elim.:  267000/444382          
c   -- var.elim.:  268000/444382          
c   -- var.elim.:  269000/444382          
c   -- var.elim.:  270000/444382          
c   -- var.elim.:  271000/444382          
c   -- var.elim.:  272000/444382          
c   -- var.elim.:  273000/444382          
c   -- var.elim.:  274000/444382          
c   -- var.elim.:  275000/444382          
c   -- var.elim.:  276000/444382          
c   -- var.elim.:  277000/444382          
c   -- var.elim.:  278000/444382          
c   -- var.elim.:  279000/444382          
c   -- var.elim.:  280000/444382          
c   -- var.elim.:  281000/444382          
c   -- var.elim.:  282000/444382          
c   -- var.elim.:  283000/444382          
c   -- var.elim.:  284000/444382          
c   -- var.elim.:  285000/444382          
c   -- var.elim.:  286000/444382          
c   -- var.elim.:  287000/444382          
c   -- var.elim.:  288000/444382          
c   -- var.elim.:  289000/444382          
c   -- var.elim.:  290000/444382          
c   -- var.elim.:  291000/444382          
c   -- var.elim.:  292000/444382          
c   -- var.elim.:  293000/444382          
c   -- var.elim.:  294000/444382          
c   -- var.elim.:  295000/444382          
c   -- var.elim.:  296000/444382          
c   -- var.elim.:  297000/444382          
c   -- var.elim.:  298000/444382          
c   -- var.elim.:  299000/444382          
c   -- var.elim.:  300000/444382          
c   -- var.elim.:  301000/444382          
c   -- var.elim.:  302000/444382          
c   -- var.elim.:  303000/444382          
c   -- var.elim.:  304000/444382          
c   -- var.elim.:  305000/444382          
c   -- var.elim.:  306000/444382          
c   -- var.elim.:  307000/444382          
c   -- var.elim.:  308000/444382          
c   -- var.elim.:  309000/444382          
c   -- var.elim.:  310000/444382          
c   -- var.elim.:  311000/444382          
c   -- var.elim.:  312000/444382          
c   -- var.elim.:  313000/444382          
c   -- var.elim.:  314000/444382          
c   -- var.elim.:  315000/444382          
c   -- var.elim.:  316000/444382          
c   -- var.elim.:  317000/444382          
c   -- var.elim.:  318000/444382          
c   -- var.elim.:  319000/444382          
c   -- var.elim.:  320000/444382          
c   -- var.elim.:  321000/444382          
c   -- var.elim.:  322000/444382          
c   -- var.elim.:  323000/444382          
c   -- var.elim.:  324000/444382          
c   -- var.elim.:  325000/444382          
c   -- var.elim.:  326000/444382          
c   -- var.elim.:  327000/444382          
c   -- var.elim.:  328000/444382          
c   -- var.elim.:  329000/444382          
c   -- var.elim.:  330000/444382          
c   -- var.elim.:  331000/444382          
c   -- var.elim.:  332000/444382          
c   -- var.elim.:  333000/444382          
c   -- var.elim.:  334000/444382          
c   -- var.elim.:  335000/444382          
c   -- var.elim.:  336000/444382          
c   -- var.elim.:  337000/444382          
c   -- var.elim.:  338000/444382          
c   -- var.elim.:  339000/444382          
c   -- var.elim.:  340000/444382          
c   -- var.elim.:  341000/444382          
c   -- var.elim.:  342000/444382          
c   -- var.elim.:  343000/444382          
c   -- var.elim.:  344000/444382          
c   -- var.elim.:  345000/444382          
c   -- var.elim.:  346000/444382          
c   -- var.elim.:  347000/444382          
c   -- var.elim.:  348000/444382          
c   -- var.elim.:  349000/444382          
c   -- var.elim.:  350000/444382          
c   -- var.elim.:  351000/444382          
c   -- var.elim.:  352000/444382          
c   -- var.elim.:  353000/444382          
c   -- var.elim.:  354000/444382          
c   -- var.elim.:  355000/444382          
c   -- var.elim.:  356000/444382          
c   -- var.elim.:  357000/444382          
c   -- var.elim.:  358000/444382          
c   -- var.elim.:  359000/444382          
c   -- var.elim.:  360000/444382          
c   -- var.elim.:  361000/444382          
c   -- var.elim.:  362000/444382          
c   -- var.elim.:  363000/444382          
c   -- var.elim.:  364000/444382          
c   -- var.elim.:  365000/444382          
c   -- var.elim.:  366000/444382          
c   -- var.elim.:  367000/444382          
c   -- var.elim.:  368000/444382          
c   -- var.elim.:  369000/444382          
c   -- var.elim.:  370000/444382          
c   -- var.elim.:  371000/444382          
c   -- var.elim.:  372000/444382          
c   -- var.elim.:  373000/444382          
c   -- var.elim.:  374000/444382          
c   -- var.elim.:  375000/444382          
c   -- var.elim.:  376000/444382          
c   -- var.elim.:  377000/444382          
c   -- var.elim.:  378000/444382          
c   -- var.elim.:  379000/444382          
c   -- var.elim.:  380000/444382          
c   -- var.elim.:  381000/444382          
c   -- var.elim.:  382000/444382          
c   -- var.elim.:  383000/444382          
c   -- var.elim.:  384000/444382          
c   -- var.elim.:  385000/444382          
c   -- var.elim.:  386000/444382          
c   -- var.elim.:  387000/444382          
c   -- var.elim.:  388000/444382          
c   -- var.elim.:  389000/444382          
c   -- var.elim.:  390000/444382          
c   -- var.elim.:  391000/444382          
c   -- var.elim.:  392000/444382          
c   -- var.elim.:  393000/444382          
c   -- var.elim.:  394000/444382          
c   -- var.elim.:  395000/444382          
c   -- var.elim.:  396000/444382          
c   -- var.elim.:  397000/444382          
c   -- var.elim.:  398000/444382          
c   -- var.elim.:  399000/444382          
c   -- var.elim.:  400000/444382          
c   -- var.elim.:  401000/444382          
c   -- var.elim.:  402000/444382          
c   -- var.elim.:  403000/444382          
c   -- var.elim.:  404000/444382          
c   -- var.elim.:  405000/444382          
c   -- var.elim.:  406000/444382          
c   -- var.elim.:  407000/444382          
c   -- var.elim.:  408000/444382          
c   -- var.elim.:  409000/444382          
c   -- var.elim.:  410000/444382          
c   -- var.elim.:  411000/444382          
c   -- var.elim.:  412000/444382          
c   -- var.elim.:  413000/444382          
c   -- var.elim.:  414000/444382          
c   -- var.elim.:  415000/444382          
c   -- var.elim.:  416000/444382          
c   -- var.elim.:  417000/444382          
c   -- var.elim.:  418000/444382          
c   -- var.elim.:  419000/444382          
c   -- var.elim.:  420000/444382          
c   -- var.elim.:  421000/444382          
c   -- var.elim.:  422000/444382          
c   -- var.elim.:  423000/444382          
c   -- var.elim.:  424000/444382          
c   -- var.elim.:  425000/444382          
c   -- var.elim.:  426000/444382          
c   -- var.elim.:  427000/444382          
c   -- var.elim.:  428000/444382          
c   -- var.elim.:  429000/444382          
c   -- var.elim.:  430000/444382          
c   -- var.elim.:  431000/444382          
c   -- var.elim.:  432000/444382          
c   -- var.elim.:  433000/444382          
c   -- var.elim.:  434000/444382          
c   -- var.elim.:  435000/444382          
c   -- var.elim.:  436000/444382          
c   -- var.elim.:  437000/444382          
c   -- var.elim.:  438000/444382          
c   -- var.elim.:  439000/444382          
c   -- var.elim.:  440000/444382          
c   -- var.elim.:  441000/444382          
c   -- var.elim.:  442000/444382          
c   -- var.elim.:  443000/444382          
c   -- var.elim.:  444000/444382          
c   -- var.elim.:  444382/444382          
c   -- var.elim.:  1000/234176          
c   -- var.elim.:  2000/234176          
c   -- var.elim.:  3000/234176          
c   -- var.elim.:  4000/234176          
c   -- var.elim.:  5000/234176          
c   -- var.elim.:  6000/234176          
c   -- var.elim.:  7000/234176          
c   -- var.elim.:  8000/234176          
c   -- var.elim.:  9000/234176          
c   -- var.elim.:  10000/234176          
c   -- var.elim.:  11000/234176          
c   -- var.elim.:  12000/234176          
c   -- var.elim.:  13000/234176          
c   -- var.elim.:  14000/234176          
c   -- var.elim.:  15000/234176          
c   -- var.elim.:  16000/234176          
c   -- var.elim.:  17000/234176          
c   -- var.elim.:  18000/234176          
c   -- var.elim.:  19000/234176          
c   -- var.elim.:  20000/234176          
c   -- var.elim.:  21000/234176          
c   -- var.elim.:  22000/234176          
c   -- var.elim.:  23000/234176          
c   -- var.elim.:  24000/234176          
c   -- var.elim.:  25000/234176          
c   -- var.elim.:  26000/234176          
c   -- var.elim.:  27000/234176          
c   -- var.elim.:  28000/234176          
c   -- var.elim.:  29000/234176          
c   -- var.elim.:  30000/234176          
c   -- var.elim.:  31000/234176          
c   -- var.elim.:  32000/234176          
c   -- var.elim.:  33000/234176          
c   -- var.elim.:  34000/234176          
c   -- var.elim.:  35000/234176          
c   -- var.elim.:  36000/234176          
c   -- var.elim.:  37000/234176          
c   -- var.elim.:  38000/234176          
c   -- var.elim.:  39000/234176          
c   -- var.elim.:  40000/234176          
c   -- var.elim.:  41000/234176          
c   -- var.elim.:  42000/234176          
c   -- var.elim.:  43000/234176          
c   -- var.elim.:  44000/234176          
c   -- var.elim.:  45000/234176          
c   -- var.elim.:  46000/234176          
c   -- var.elim.:  47000/234176          
c   -- var.elim.:  48000/234176          
c   -- var.elim.:  49000/234176          
c   -- var.elim.:  50000/234176          
c   -- var.elim.:  51000/234176          
c   -- var.elim.:  52000/234176          
c   -- var.elim.:  53000/234176          
c   -- var.elim.:  54000/234176          
c   -- var.elim.:  55000/234176          
c   -- var.elim.:  56000/234176          
c   -- var.elim.:  57000/234176          
c   -- var.elim.:  58000/234176          
c   -- var.elim.:  59000/234176          
c   -- var.elim.:  60000/234176          
c   -- var.elim.:  61000/234176          
c   -- var.elim.:  62000/234176          
c   -- var.elim.:  63000/234176          
c   -- var.elim.:  64000/234176          
c   -- var.elim.:  65000/234176          
c   -- var.elim.:  66000/234176          
c   -- var.elim.:  67000/234176          
c   -- var.elim.:  68000/234176          
c   -- var.elim.:  69000/234176          
c   -- var.elim.:  70000/234176          
c   -- var.elim.:  71000/234176          
c   -- var.elim.:  72000/234176          
c   -- var.elim.:  73000/234176          
c   -- var.elim.:  74000/234176          
c   -- var.elim.:  75000/234176          
c   -- var.elim.:  76000/234176          
c   -- var.elim.:  77000/234176          
c   -- var.elim.:  78000/234176          
c   -- var.elim.:  79000/234176          
c   -- var.elim.:  80000/234176          
c   -- var.elim.:  81000/234176          
c   -- var.elim.:  82000/234176          
c   -- var.elim.:  83000/234176          
c   -- var.elim.:  84000/234176          
c   -- var.elim.:  85000/234176          
c   -- var.elim.:  86000/234176          
c   -- var.elim.:  87000/234176          
c   -- var.elim.:  88000/234176          
c   -- var.elim.:  89000/234176          
c   -- var.elim.:  90000/234176          
c   -- var.elim.:  91000/234176          
c   -- var.elim.:  92000/234176          
c   -- var.elim.:  93000/234176          
c   -- var.elim.:  94000/234176          
c   -- var.elim.:  95000/234176          
c   -- var.elim.:  96000/234176          
c   -- var.elim.:  97000/234176          
c   -- var.elim.:  98000/234176          
c   -- var.elim.:  99000/234176          
c   -- var.elim.:  100000/234176          
c   -- var.elim.:  101000/234176          
c   -- var.elim.:  102000/234176          
c   -- var.elim.:  103000/234176          
c   -- var.elim.:  104000/234176          
c   -- var.elim.:  105000/234176          
c   -- var.elim.:  106000/234176          
c   -- var.elim.:  107000/234176          
c   -- var.elim.:  108000/234176          
c   -- var.elim.:  109000/234176          
c   -- var.elim.:  110000/234176          
c   -- var.elim.:  111000/234176          
c   -- var.elim.:  112000/234176          
c   -- var.elim.:  113000/234176          
c   -- var.elim.:  114000/234176          
c   -- var.elim.:  115000/234176          
c   -- var.elim.:  116000/234176          
c   -- var.elim.:  117000/234176          
c   -- var.elim.:  118000/234176          
c   -- var.elim.:  119000/234176          
c   -- var.elim.:  120000/234176          
c   -- var.elim.:  121000/234176          
c   -- var.elim.:  122000/234176          
c   -- var.elim.:  123000/234176          
c   -- var.elim.:  124000/234176          
c   -- var.elim.:  125000/234176          
c   -- var.elim.:  126000/234176          
c   -- var.elim.:  127000/234176          
c   -- var.elim.:  128000/234176          
c   -- var.elim.:  129000/234176          
c   -- var.elim.:  130000/234176          
c   -- var.elim.:  131000/234176          
c   -- var.elim.:  132000/234176          
c   -- var.elim.:  133000/234176          
c   -- var.elim.:  134000/234176          
c   -- var.elim.:  135000/234176          
c   -- var.elim.:  136000/234176          
c   -- var.elim.:  137000/234176          
c   -- var.elim.:  138000/234176          
c   -- var.elim.:  139000/234176          
c   -- var.elim.:  140000/234176          
c   -- var.elim.:  141000/234176          
c   -- var.elim.:  142000/234176          
c   -- var.elim.:  143000/234176          
c   -- var.elim.:  144000/234176          
c   -- var.elim.:  145000/234176          
c   -- var.elim.:  146000/234176          
c   -- var.elim.:  147000/234176          
c   -- var.elim.:  148000/234176          
c   -- var.elim.:  149000/234176          
c   -- var.elim.:  150000/234176          
c   -- var.elim.:  151000/234176          
c   -- var.elim.:  152000/234176          
c   -- var.elim.:  153000/234176          
c   -- var.elim.:  154000/234176          
c   -- var.elim.:  155000/234176          
c   -- var.elim.:  156000/234176          
c   -- var.elim.:  157000/234176          
c   -- var.elim.:  158000/234176          
c   -- var.elim.:  159000/234176          
c   -- var.elim.:  160000/234176          
c   -- var.elim.:  161000/234176          
c   -- var.elim.:  162000/234176          
c   -- var.elim.:  163000/234176          
c   -- var.elim.:  164000/234176          
c   -- var.elim.:  165000/234176          
c   -- var.elim.:  166000/234176          
c   -- var.elim.:  167000/234176          
c   -- var.elim.:  168000/234176          
c   -- var.elim.:  169000/234176          
c   -- var.elim.:  170000/234176          
c   -- var.elim.:  171000/234176          
c   -- var.elim.:  172000/234176          
c   -- var.elim.:  173000/234176          
c   -- var.elim.:  174000/234176          
c   -- var.elim.:  175000/234176          
c   -- var.elim.:  176000/234176          
c   -- var.elim.:  177000/234176          
c   -- var.elim.:  178000/234176          
c   -- var.elim.:  179000/234176          
c   -- var.elim.:  180000/234176          
c   -- var.elim.:  181000/234176          
c   -- var.elim.:  182000/234176          
c   -- var.elim.:  183000/234176          
c   -- var.elim.:  184000/234176          
c   -- var.elim.:  185000/234176          
c   -- var.elim.:  186000/234176          
c   -- var.elim.:  187000/234176          
c   -- var.elim.:  188000/234176          
c   -- var.elim.:  189000/234176          
c   -- var.elim.:  190000/234176          
c   -- var.elim.:  191000/234176          
c   -- var.elim.:  192000/234176          
c   -- var.elim.:  193000/234176          
c   -- var.elim.:  194000/234176          
c   -- var.elim.:  195000/234176          
c   -- var.elim.:  196000/234176          
c   -- var.elim.:  197000/234176          
c   -- var.elim.:  198000/234176          
c   -- var.elim.:  199000/234176          
c   -- var.elim.:  200000/234176          
c   -- var.elim.:  201000/234176          
c   -- var.elim.:  202000/234176          
c   -- var.elim.:  203000/234176          
c   -- var.elim.:  204000/234176          
c   -- var.elim.:  205000/234176          
c   -- var.elim.:  206000/234176          
c   -- var.elim.:  207000/234176          
c   -- var.elim.:  208000/234176          
c   -- var.elim.:  209000/234176          
c   -- var.elim.:  210000/234176          
c   -- var.elim.:  211000/234176          
c   -- var.elim.:  212000/234176          
c   -- var.elim.:  213000/234176          
c   -- var.elim.:  214000/234176          
c   -- var.elim.:  215000/234176          
c   -- var.elim.:  216000/234176          
c   -- var.elim.:  217000/234176          
c   -- var.elim.:  218000/234176          
c   -- var.elim.:  219000/234176          
c   -- var.elim.:  220000/234176          
c   -- var.elim.:  221000/234176          
c   -- var.elim.:  222000/234176          
c   -- var.elim.:  223000/234176          
c   -- var.elim.:  224000/234176          
c   -- var.elim.:  225000/234176          
c   -- var.elim.:  226000/234176          
c   -- var.elim.:  227000/234176          
c   -- var.elim.:  228000/234176          
c   -- var.elim.:  229000/234176          
c   -- var.elim.:  230000/234176          
c   -- var.elim.:  231000/234176          
c   -- var.elim.:  232000/234176          
c   -- var.elim.:  233000/234176          
c   -- var.elim.:  234000/234176          
c   -- var.elim.:  234176/234176          
c   -- var.elim.:  1000/57439          
c   -- var.elim.:  2000/57439          
c   -- var.elim.:  3000/57439          
c   -- var.elim.:  4000/57439          
c   -- var.elim.:  5000/57439          
c   -- var.elim.:  6000/57439          
c   -- var.elim.:  7000/57439          
c   -- var.elim.:  8000/57439          
c   -- var.elim.:  9000/57439          
c   -- var.elim.:  10000/57439          
c   -- var.elim.:  11000/57439          
c   -- var.elim.:  12000/57439          
c   -- var.elim.:  13000/57439          
c   -- var.elim.:  14000/57439          
c   -- var.elim.:  15000/57439          
c   -- var.elim.:  16000/57439          
c   -- var.elim.:  17000/57439          
c   -- var.elim.:  18000/57439          
c   -- var.elim.:  19000/57439          
c   -- var.elim.:  20000/57439          
c   -- var.elim.:  21000/57439          
c   -- var.elim.:  22000/57439          
c   -- var.elim.:  23000/57439          
c   -- var.elim.:  24000/57439          
c   -- var.elim.:  25000/57439          
c   -- var.elim.:  26000/57439          
c   -- var.elim.:  27000/57439          
c   -- var.elim.:  28000/57439          
c   -- var.elim.:  29000/57439          
c   -- var.elim.:  30000/57439          
c   -- var.elim.:  31000/57439          
c   -- var.elim.:  32000/57439          
c   -- var.elim.:  33000/57439          
c   -- var.elim.:  34000/57439          
c   -- var.elim.:  35000/57439          
c   -- var.elim.:  36000/57439          
c   -- var.elim.:  37000/57439          
c   -- var.elim.:  38000/57439          
c   -- var.elim.:  39000/57439          
c   -- var.elim.:  40000/57439          
c   -- var.elim.:  41000/57439          
c   -- var.elim.:  42000/57439          
c   -- var.elim.:  43000/57439          
c   -- var.elim.:  44000/57439          
c   -- var.elim.:  45000/57439          
c   -- var.elim.:  46000/57439          
c   -- var.elim.:  47000/57439          
c   -- var.elim.:  48000/57439          
c   -- var.elim.:  49000/57439          
c   -- var.elim.:  50000/57439          
c   -- var.elim.:  51000/57439          
c   -- var.elim.:  52000/57439          
c   -- var.elim.:  53000/57439          
c   -- var.elim.:  54000/57439          
c   -- var.elim.:  55000/57439          
c   -- var.elim.:  56000/57439          
c   -- var.elim.:  57000/57439          
c   -- var.elim.:  57439/57439          
c   -- var.elim.:  1000/57606          
c   -- var.elim.:  2000/57606          
c   -- var.elim.:  3000/57606          
c   -- var.elim.:  4000/57606          
c   -- var.elim.:  5000/57606          
c   -- var.elim.:  6000/57606          
c   -- var.elim.:  7000/57606          
c   -- var.elim.:  8000/57606          
c   -- var.elim.:  9000/57606          
c   -- var.elim.:  10000/57606          
c   -- var.elim.:  11000/57606          
c   -- var.elim.:  12000/57606          
c   -- var.elim.:  13000/57606          
c   -- var.elim.:  14000/57606          
c   -- var.elim.:  15000/57606          
c   -- var.elim.:  16000/57606          
c   -- var.elim.:  17000/57606          
c   -- var.elim.:  18000/57606          
c   -- var.elim.:  19000/57606          
c   -- var.elim.:  20000/57606          
c   -- var.elim.:  21000/57606          
c   -- var.elim.:  22000/57606          
c   -- var.elim.:  23000/57606          
c   -- var.elim.:  24000/57606          
c   -- var.elim.:  25000/57606          
c   -- var.elim.:  26000/57606          
c   -- var.elim.:  27000/57606          
c   -- var.elim.:  28000/57606          
c   -- var.elim.:  29000/57606          
c   -- var.elim.:  30000/57606          
c   -- var.elim.:  31000/57606          
c   -- var.elim.:  32000/57606          
c   -- var.elim.:  33000/57606          
c   -- var.elim.:  34000/57606          
c   -- var.elim.:  35000/57606          
c   -- var.elim.:  36000/57606          
c   -- var.elim.:  37000/57606          
c   -- var.elim.:  38000/57606          
c   -- var.elim.:  39000/57606          
c   -- var.elim.:  40000/57606          
c   -- var.elim.:  41000/57606          
c   -- var.elim.:  42000/57606          
c   -- var.elim.:  43000/57606          
c   -- var.elim.:  44000/57606          
c   -- var.elim.:  45000/57606          
c   -- var.elim.:  46000/57606          
c   -- var.elim.:  47000/57606          
c   -- var.elim.:  48000/57606          
c   -- var.elim.:  49000/57606          
c   -- var.elim.:  50000/57606          
c   -- var.elim.:  51000/57606          
c   -- var.elim.:  52000/57606          
c   -- var.elim.:  53000/57606          
c   -- var.elim.:  54000/57606          
c   -- var.elim.:  55000/57606          
c   -- var.elim.:  56000/57606          
c   -- var.elim.:  57000/57606          
c   -- var.elim.:  57606/57606          
c   -- var.elim.:  1000/55759          
c   -- var.elim.:  2000/55759          
c   -- var.elim.:  3000/55759          
c   -- var.elim.:  4000/55759          
c   -- var.elim.:  5000/55759          
c   -- var.elim.:  6000/55759          
c   -- var.elim.:  7000/55759          
c   -- var.elim.:  8000/55759          
c   -- var.elim.:  9000/55759          
c   -- var.elim.:  10000/55759          
c   -- var.elim.:  11000/55759          
c   -- var.elim.:  12000/55759          
c   -- var.elim.:  13000/55759          
c   -- var.elim.:  14000/55759          
c   -- var.elim.:  15000/55759          
c   -- var.elim.:  16000/55759          
c   -- var.elim.:  17000/55759          
c   -- var.elim.:  18000/55759          
c   -- var.elim.:  19000/55759          
c   -- var.elim.:  20000/55759          
c   -- var.elim.:  21000/55759          
c   -- var.elim.:  22000/55759          
c   -- var.elim.:  23000/55759          
c   -- var.elim.:  24000/55759          
c   -- var.elim.:  25000/55759          
c   -- var.elim.:  26000/55759          
c   -- var.elim.:  27000/55759          
c   -- var.elim.:  28000/55759          
c   -- var.elim.:  29000/55759          
c   -- var.elim.:  30000/55759          
c   -- var.elim.:  31000/55759          
c   -- var.elim.:  32000/55759          
c 
c *** TERMINATED ***
s SATISFIABLE
v v1 -v1048 -v1397 -v2444 -v3142 -v4193 -v4544 -v4895 -v6650 -v7001 -v7352 -v7703 -v8054 -v2 -v1049 -v1398 v3143 -v4194 -v4545 -v4896 -v6651 -v7002 -v7353 -v7704 -v3 v1399 -v2795 -v3493 -v4195 -v4546 -v4897 -v4 -v1400 -v4196 -v4547 -v4898 -v5249 -v1052 -v2448 v3146 -v5601 -v6654 -v7005 -v7356 -v7707 -v355 -v704 -v1751 -v2100 v5602 -v5953 -v6304 -v356 -v705 v2101 -v5603 -v5954 -v6305 v1055 -v3149 -v6657 -v7008 -v7359 -v7710 -v1754 -v10 -v359 -v708 -v1057 -v1406 v1755 -v2104 -v3151 -v4202 -v4553 v4904 -v5606 -v5957 -v6308 -v6659 -v7010 -v7361 -v7712 v11 -v360 -v709 -v1058 -v1407 -v1756 -v2105 -v3152 -v4203 -v4554 -v4905 -v5607 -v5958 v6309 -v6660 -v7011 -v7362 -v7713 -v12 -v361 -v710 -v1059 -v1408 -v1757 -v2106 v3153 -v4204 -v4555 -v4906 -v5257 -v5608 -v5959 -v6310 -v6661 -v7012 -v7363 -v7714 -v362 -v711 -v1060 -v1758 -v2107 v3154 -v5258 -v5609 -v5960 -v6311 -v6662 -v7013 -v7364 -v7715 -v363 -v712 -v1759 -v2108 -v2457 v5610 -v5961 -v6312 -v8067 -v364 -v713 -v2109 -v2458 -v5611 -v5962 -v6313 -v8069 -v366 -v715 -v2111 -v2460 -v5613 v5964 -v6315 -v8071 -v1764 v2811 -v3509 -v20 -v369 -v718 -v1067 -v1416 -v1765 -v2114 v3161 -v4212 -v4563 -v4914 v5265 -v5616 -v5967 -v6318 -v6669 -v7020 -v7371 -v7722 -v21 -v370 -v719 -v1068 -v1417 -v1766 -v2115 v3162 -v4213 -v4564 -v4915 -v5617 -v5968 -v6319 -v6670 -v7021 -v7372 -v7723 -v2815 -v3513 -v3864 -v373 -v2467 -v5269 -v25 -v374 -v723 -v1072 -v1421 -v1770 -v2119 v3166 -v4217 -v4568 -v4919 -v5621 -v5972 v6323 -v6674 -v7025 -v7376 -v7727 -v26 v1422 -v4218 -v4569 -v4920 v8079 v2819 -v3517 v8080 -v377 -v726 -v1773 -v2122 -v5273 v5624 -v5975 -v6326 -v8081 -v2821 -v3519 -v5274 -v1077 -v3171 -v3871 -v6679 v7030 -v7381 -v7732 -v1078 -v3172 -v3872 -v6680 -v7031 -v7382 -v7733 -v32 -v381 -v730 -v1079 v1428 -v1777 -v2126 -v3173 -v4224 -v4575 -v4926 -v5277 -v5628 -v5979 -v6330 -v6681 v7032 -v7383 -v7734 -v1778 -v2825 -v3523 -v8086 -v1779 -v8087 -v35 -v1431 -v2827 -v3525 -v4227 -v4578 -v4929 -v5280 -v7737 -v2479 -v3877 -v386 -v735 -v1782 -v2131 -v2480 -v3878 -v5282 v5633 -v5984 -v6335 -v8090 -v2830 -v3528 -v5283 -v40 -v1436 -v4232 -v4583 -v4934 -v8093 -v2833 -v3531 -v5286 -v391 v740 -v1787 -v2136 -v3883 v5287 -v5638 -v5989 -v6340 -v5288 -v2487 -v2836 -v3534 -v8097 -v5290 -v6343 -v2489 -v3887 -v47 -v1443 -v2839 -v3537 -v4239 -v4590 -v4941 -v48 -v397 -v746 -v1444 -v1793 v2142 -v2491 -v4240 v4591 -v4942 -v5293 -v5644 -v5995 -v6346 -v8101 -v49 -v1445 -v4241 -v4592 -v4943 -v5294 -v50 -v399 v748 -v1446 -v1795 -v2144 -v4242 -v4593 -v4944 v5295 -v5646 -v5997 -v6348 -v51 -v1098 -v1447 v3192 -v4243 -v4594 -v4945 -v6700 -v7051 -v7402 -v7753 -v401 v750 -v1099 -v1797 -v2146 -v3193 v5297 -v5648 -v5999 -v6350 -v6701 -v7052 -v7403 -v7754 -v53 -v402 -v751 v1449 -v1798 -v2147 -v2496 -v4245 -v4596 -v4947 -v5298 -v5649 -v6000 -v6351 -v8106 -v54 -v403 -v752 -v1450 -v1799 -v2148 -v4246 -v4597 -v4948 -v5299 -v5650 -v6001 -v6352 -v3545 -v5300 -v8108 -v2847 -v3546 v5301 -v56 -v405 -v754 -v1103 -v1452 -v1801 -v2150 v3197 -v4249 -v4600 -v4951 -v5302 -v5653 -v6004 -v6355 -v6706 -v7057 -v7408 -v7759 -v2849 v3548 -v3899 -v2850 -v3549 -v8112 -v59 -v408 -v757 -v1455 -v1804 v2153 -v4252 v4603 -v4954 -v5305 -v5656 -v6007 -v6358 -v60 -v409 -v758 -v1107 -v1456 -v1805 v2154 -v3201 -v4253 v4604 -v4955 -v5657 -v6008 -v6359 -v6710 -v7061 -v7412 -v7763 -v61 -v410 v759 -v1108 -v1457 -v1806 -v2155 -v3202 -v4254 v4605 -v4956 -v5658 -v6009 -v6360 -v6711 -v7062 -v7413 -v7764 -v3553 -v5308 v8116 -v62 -v1458 v4256 -v4607 -v4958 -v5309 -v412 v761 -v1808 -v2157 -v5310 -v5661 -v6012 -v6363 -v2856 v3556 -v8119 -v414 v763 -v1112 -v1810 -v2159 -v3206 v5312 -v5663 -v6014 -v6365 -v6716 -v7067 -v7418 -v7769 -v2858 v3558 -v8121 -v67 -v1463 v2859 -v3559 v4261 -v4612 -v4963 -v5314 -v68 -v1464 -v4262 -v4613 v4964 -v5315 -v2861 v3561 -v5316 -v70 -v419 v768 -v1466 -v1815 -v2164 -v4264 -v4615 -v4966 -v5317 -v5668 -v6019 -v6370 -v71 -v420 v769 -v1467 -v1816 -v2165 -v4265 -v4616 -v4967 -v5318 -v5669 -v6020 -v6371 -v72 -v421 -v770 -v1119 -v1468 v1817 -v2166 -v3213 -v4266 -v4617 v4968 -v5319 -v5670 -v6021 -v6372 -v6723 -v7074 -v7425 -v7776 -v73 -v1469 -v2865 v3565 -v4267 -v4618 -v4969 -v2866 -v3566 -v8129 -v75 -v1471 -v2867 -v3567 -v4269 -v4620 -v4971 v8131 -v3569 -v3920 -v4271 -v4622 -v4973 -v5324 -v5675 -v6026 v6377 -v77 -v1124 -v1473 -v3218 -v4272 -v4623 -v4974 v6729 -v7080 -v7431 -v7782 -v427 -v776 -v1125 -v2172 v3219 -v5677 -v6028 -v6379 -v6730 -v7081 -v7432 -v7783 -v79 -v1126 -v1475 -v3220 -v4274 -v4625 -v4976 -v6731 -v7082 -v7433 -v7784 -v80 -v1476 -v2872 -v3573 -v4275 -v4626 -v4977 -v81 -v430 -v779 -v1477 v1826 -v2175 -v4276 -v4627 -v4978 -v5329 -v5680 -v6031 -v6382 -v82 -v1478 -v4277 -v4628 -v4979 -v5330 -v8138 -v83 -v1479 -v1828 -v4278 v4629 -v4980 -v5331 -v84 -v433 -v782 -v1131 -v1480 -v1829 -v2178 -v3225 -v4279 v4630 -v4981 -v5683 -v6034 -v6385 -v6736 -v7087 -v7438 -v7789 -v434 v783 -v1830 -v2179 -v5333 -v5684 -v6035 -v6386 -v86 -v1482 -v4281 -v4632 v4983 -v5334 -v87 -v1134 -v1483 -v3228 -v4282 -v4633 -v4984 -v6739 -v7090 -v7441 -v7792 -v1135 -v3229 -v3932 -v6740 -v7091 -v7442 -v7793 -v89 -v1485 -v4284 -v4635 -v4986 -v5337 -v90 -v439 v788 -v1486 -v2184 -v4285 -v4636 -v4987 -v5689 -v6040 -v6391 -v440 -v789 -v1138 -v2185 -v3232 -v5690 -v6041 -v6392 v6743 -v7094 -v7445 -v7796 -v1837 v2884 -v3585 -v5340 -v93 -v1140 v1489 -v2536 -v2885 -v3234 -v3586 -v3937 -v4288 -v4639 -v4990 -v6745 -v7096 -v7447 -v7798 -v8149 -v94 -v443 -v792 -v1490 v2188 -v4289 -v4640 v4991 -v5693 -v6044 -v6395 -v95 -v1491 -v3939 -v4290 -v4641 -v4992 v445 -v794 -v1143 -v2190 -v3237 -v5695 -v6046 -v6397 -v6748 -v7099 v7450 -v7801 -v98 v1494 -v1843 -v4293 -v4644 -v4995 -v5346 -v448 -v797 -v1146 v2193 -v3240 -v5698 -v6049 -v6400 -v6751 -v7102 -v7453 -v7804 -v100 -v1496 -v4295 v4646 -v4997 -v5348 -v101 v450 -v799 -v1497 -v2195 -v4296 v4647 -v4998 -v5700 -v6051 -v6402 -v3595 -v5350 -v451 -v800 -v1149 -v2196 v3243 -v5702 -v6053 -v6404 -v6755 -v7106 -v7457 -v7808 -v103 -v1499 v1848 -v4299 -v4650 -v5001 v104 -v1500 -v3949 -v4300 -v4651 -v5002 -v454 -v803 v1850 -v2199 -v5354 -v5705 -v6056 -v6407 -v455 -v804 -v1153 -v2200 v3247 -v5706 -v6057 v6408 -v6759 -v7110 -v7461 -v7812 -v2550 -v5356 -v8164 -v457 v806 -v1853 -v2202 -v2551 -v2900 -v3602 -v5357 -v5708 -v6059 -v6410 v8165 -v458 -v807 -v1156 -v1854 -v2203 -v3250 -v3954 -v5358 -v5709 -v6060 -v6411 -v6762 v7113 -v7464 -v7815 -v2553 -v2902 -v3604 -v8167 -v111 -v460 -v809 -v1507 -v1856 v2205 -v4307 -v4658 v5009 -v5360 -v5711 -v6062 -v6413 -v2904 -v3606 v8169 -v113 -v1509 -v1858 -v4309 -v4660 -v5011 v114 -v1510 -v4310 -v4661 -v5012 -v5363 v2907 -v3609 -v8172 -v1163 -v3257 -v3961 v6769 -v7120 -v7471 -v7822 v117 -v466 -v815 -v1513 -v1862 -v2211 -v2909 -v3611 -v3962 -v4313 -v4664 -v5015 -v5366 -v5717 v6068 -v6419 v2910 -v3612 -v5367 -v1864 -v5368 -v469 -v818 -v1167 -v1865 v2214 -v2912 -v3261 -v3614 -v5369 -v5720 -v6071 -v6422 -v6773 v7124 -v7475 -v7826 -v121 -v1517 -v4317 -v4668 -v5019 -v5370 -v122 -v471 -v820 -v1518 v2216 -v2914 -v3616 -v4318 -v4669 -v5020 -v5722 -v6073 -v6424 -v1170 -v3264 -v3968 -v6776 -v7127 -v7478 -v7829 -v8180 -v473 -v822 -v1869 v2218 -v5373 -v5724 -v6075 -v6426 -v125 -v474 -v823 -v1172 -v1521 -v2219 v2917 -v3266 -v3619 -v3970 -v4321 v4672 -v5023 -v5725 -v6076 -v6427 -v6778 -v7129 -v7480 -v7831 -v126 -v1522 -v4322 v4673 -v5024 -v5375 -v1872 v5376 -v128 -v477 -v826 -v1524 -v1873 -v2222 -v4324 v4675 -v5026 -v5377 -v5728 -v6079 -v6430 -v7483 -v1176 -v2921 -v3270 -v3623 -v6782 -v7133 -v7484 -v7835 -v130 -v479 -v828 -v1526 -v1875 -v2224 -v4326 -v4677 -v5028 -v5379 -v5730 v6081 -v6432 -v131 -v1527 -v4327 -v4678 -v5029 -v5380 -v481 v830 -v1179 -v1877 -v2226 -v2575 -v3273 v5381 -v5732 -v6083 -v6434 -v6785 -v7136 -v7487 -v7838 -v8189 -v133 -v482 -v831 -v1180 -v1529 -v1878 -v2227 -v3274 -v4329 -v4680 -v5031 -v5382 -v5733 -v6084 v6435 -v6786 -v7137 -v7488 -v7839 -v1181 -v1879 -v3275 -v5383 -v6787 -v7138 -v7489 -v7840 -v1880 -v8192 -v136 -v485 -v834 -v1183 -v1532 -v1881 -v2230 -v3277 -v4332 -v4683 -v5034 -v5385 -v5736 -v6087 -v6438 -v6789 v7140 -v7491 -v7842 -v137 -v486 -v835 -v1533 -v1882 -v2231 -v4333 -v4684 -v5035 -v5386 v5737 -v6088 -v6439 -v487 -v836 -v1185 v1883 -v2232 -v3279 -v5387 -v5738 -v6089 -v6440 v6791 -v7142 -v7493 -v7844 -v488 -v837 -v1186 v1884 -v2233 -v3280 -v5388 -v5739 -v6090 -v6441 -v6792 -v7143 -v7494 -v7845 -v1187 -v2932 -v3281 -v3634 -v6793 -v7144 -v7495 -v7846 -v141 -v1537 v1886 -v2235 -v2933 -v3635 v4337 -v4688 -v5039 -v5741 -v491 v840 -v1189 -v1887 -v2236 -v3283 -v5391 -v5742 -v6093 -v6444 v6795 -v7146 -v7497 -v7848 -v143 -v1190 -v1539 -v3284 -v4339 -v4690 v5041 -v5392 -v6796 -v7147 -v7498 -v7849 -v145 v1192 -v1541 -v2937 -v3286 -v3639 -v4341 -v4692 -v5043 -v6798 -v7149 -v7500 -v7851 -v146 -v1542 -v2589 v4342 -v4693 -v5044 -v496 -v845 -v1194 -v1892 -v2241 -v3288 -v5396 v5747 -v6098 -v6449 -v6800 -v7151 -v7502 -v7853 -v497 -v846 v1893 -v2242 -v3993 -v5397 -v5748 -v6099 -v6450 -v498 -v847 v1894 -v2243 -v2941 -v3643 -v5398 -v5749 -v6100 -v6451 -v2593 v2942 -v3644 v5399 -v8207 -v500 -v849 -v1896 -v2245 -v5400 -v5751 -v6102 -v6453 -v2595 -v2944 -v3646 -v8209 -v153 -v502 -v851 -v1200 v1549 -v1898 -v2247 -v3294 -v4349 -v4700 -v5051 -v5402 -v5753 -v6104 -v6455 -v6806 -v7157 v7508 -v7859 -v154 v1550 -v1899 -v4350 -v4701 -v5052 -v8211 -v155 v1551 -v2947 -v3649 -v4351 -v4702 -v5053 -v5404 v8212 -v505 -v854 v1901 -v2250 -v5405 -v5756 -v6107 -v6458 -v1204 -v3298 v6810 -v7161 -v7512 -v7863 v158 -v507 -v856 -v1205 -v1554 -v1903 -v2252 -v3299 -v4354 -v4705 -v5056 -v5407 v5758 -v6109 -v6460 -v6811 -v7162 -v7513 -v7864 -v508 -v857 v1904 -v2253 -v5408 -v5759 -v6110 -v6461 v1906 -v2604 -v5410 v8218 -v162 -v1209 -v1558 -v3303 -v4007 -v4358 v4709 -v5060 -v6815 -v7166 -v7517 -v7868 -v163 -v512 -v861 -v1210 -v1559 v1908 -v2257 -v3304 -v4359 -v4710 -v5061 -v5412 -v5763 -v6114 -v6465 -v6816 -v7167 -v7518 -v7869 -v164 -v1560 -v2956 -v3658 -v4009 -v4360 -v4711 v5062 -v165 -v514 -v863 v1561 -v1910 -v2259 -v4361 -v4712 -v5063 -v5414 -v5765 v6116 -v6467 -v515 -v864 -v1911 -v2260 -v5415 -v5766 v6117 -v6468 -v516 -v865 -v1912 v2261 -v2959 -v3661 v5416 -v5767 -v6118 -v6469 v517 -v866 -v1215 -v1913 -v2262 -v3309 -v4013 -v5417 -v5768 -v6119 -v6470 v6821 -v7172 -v7523 -v7874 -v169 v1565 -v2961 v3663 -v4365 -v4716 -v5067 -v5418 -v8226 -v170 -v519 -v868 -v1566 -v1915 v2264 -v4015 -v4366 -v4717 -v5068 -v5419 -v5770 -v6121 -v6472 -v1916 -v8228 -v172 -v521 -v870 -v1568 -v1917 v2266 -v4368 -v4719 -v5070 -v5421 -v5772 -v6123 -v6474 -v4720 -v5422 -v173 -v522 -v871 -v1569 -v1918 v2267 -v4370 -v4721 -v5072 -v5423 -v5774 -v6125 -v6476 v174 -v1570 -v2966 -v3669 -v4371 -v4722 -v5073 -v524 v873 -v1920 -v2269 v5425 -v5776 -v6127 -v6478 v1223 -v1921 -v3317 -v4022 -v5426 -v6830 -v7181 -v7532 -v7883 -v526 v875 -v1224 -v2271 -v3318 -v4023 -v5778 -v6129 -v6480 -v6831 -v7182 v7533 -v7884 v1226 -v2622 -v3320 v5429 -v6833 -v7184 -v7535 -v7886 -v8237 -v180 -v529 -v878 -v1576 -v1925 -v2274 -v2972 -v181 -v1228 -v1577 -v2973 -v3322 -v3675 -v4377 -v4728 v5079 -v6834 -v7185 -v7536 -v7887 -v185 -v1232 v1581 -v3326 -v4381 -v4732 -v5083 -v6838 v7189 -v7540 -v7891 -v186 -v535 v884 -v1233 -v1582 -v2280 -v3327 v4031 -v4382 -v4733 -v5084 -v5786 -v6137 -v6488 -v6839 -v7190 -v7541 -v7892 -v1234 -v3328 v6840 -v7191 -v7542 -v7893 -v8244 -v537 v886 -v1235 -v1933 -v2282 -v3329 -v4033 -v5437 -v5788 -v6139 -v6490 -v6841 -v7192 -v7543 -v7894 -v189 -v1585 -v4385 -v4736 v5087 -v7895 -v8246 v190 -v539 -v888 -v1237 -v1586 -v1935 -v2284 -v3331 -v4035 -v4386 -v4737 -v5088 v5439 -v5790 -v6141 -v6492 -v6843 -v7194 -v7545 -v7896 -v8247 -v8248 -v541 -v890 v1937 -v2286 -v5441 -v5792 -v6143 -v6494 -v193 -v542 -v891 -v1240 -v1589 -v1938 v2287 -v3334 -v4389 -v4740 -v5091 -v5442 -v5793 -v6144 -v6495 v6846 -v7197 -v7548 -v7899 -v194 -v1241 -v1590 -v3335 -v4390 -v4741 -v5092 -v6847 v7198 -v7549 -v7900 -v195 -v544 -v893 -v1242 -v1591 v1940 -v2289 -v3336 -v4391 -v4742 v5093 -v5444 -v5795 -v6146 -v6497 -v6848 -v7199 -v7550 -v7901 -v196 -v1243 -v1592 -v3337 -v4392 -v4743 -v5094 v6849 -v7200 -v7551 -v7902 -v197 -v546 -v895 -v1244 -v1593 -v1942 v2291 -v3338 -v4393 -v4744 v5095 -v5446 -v5797 -v6148 -v6499 -v6850 -v7201 -v7552 -v7903 -v1245 -v3339 -v4043 -v6851 -v7202 v7553 -v7904 -v1246 -v2642 -v3340 -v6852 -v7203 -v7554 -v7905 -v8256 -v200 -v1596 -v2643 -v2992 -v3694 -v4396 -v4747 -v5098 -v8257 v1248 -v2644 -v3342 -v6854 -v7205 -v7556 -v7907 -v8258 -v202 -v551 -v900 -v1598 v1947 -v2296 -v2645 -v4398 -v4749 -v5100 -v5451 -v5802 -v6153 -v6504 -v8259 -v203 -v552 -v901 -v1250 -v1599 v1948 -v2297 -v3344 -v4399 -v4750 -v5101 -v5452 -v5803 -v6154 -v6505 -v6856 -v7207 -v7558 v7909 -v204 -v553 -v902 -v1600 v1949 -v2298 -v4400 -v4751 -v5102 -v5453 -v5804 -v6155 -v6506 -v205 -v554 v903 -v1601 -v1950 -v2299 -v4050 -v4401 -v4752 -v5103 -v5454 -v5805 -v6156 -v6507 v206 -v1602 -v4402 -v4753 -v5104 -v207 -v556 -v905 -v1254 -v1603 v1952 -v2301 -v3348 -v4403 -v4754 -v5105 -v5807 -v6158 -v6509 -v6860 -v7211 -v7562 v7913 -v208 -v1255 v1953 -v2302 v5106 -v5457 -v5808 -v6159 -v6510 -v6861 -v209 -v1605 v1954 -v4405 -v4756 -v5107 -v5458 -v8266 -v210 -v1606 -v2653 v4055 -v4406 -v4757 -v5108 -v211 -v1607 v1956 -v4407 -v4758 v5109 -v5460 -v8268 -v561 -v910 -v1957 -v2306 -v5461 -v5812 -v6163 -v6514 -v213 -v1609 -v2656 -v4409 -v4760 -v5111 -v214 -v1610 -v2657 -v4410 -v4761 -v5112 -v5463 -v8271 -v3007 -v3709 -v5464 -v1263 -v3357 -v5816 -v6869 -v7220 -v7571 -v7922 -v3009 -v3711 v6168 -v218 -v1265 -v1614 -v3359 -v4414 -v4765 -v5116 -v6871 -v7222 -v7573 v7924 -v568 -v917 -v1266 -v1964 -v2313 -v3360 -v5468 -v5819 -v6170 -v6521 -v6872 v7223 -v7574 -v7925 v220 -v1616 -v4065 -v4416 -v4767 -v5118 -v5469 -v5119 v6172 -v222 -v1269 v1618 -v2665 -v3014 -v3363 -v3716 -v4418 -v4769 -v5120 -v6875 v7226 -v7577 -v7928 -v8279 -v1968 -v5472 -v224 v1620 -v4069 -v4420 -v4771 -v5122 -v225 -v574 v923 -v1272 -v1621 -v1970 -v2319 -v3366 -v4421 -v4772 -v5123 -v5474 -v5825 -v6176 -v6527 -v6878 -v7229 -v7580 -v7931 -v226 -v1273 v1622 -v3367 -v227 v1623 -v4422 -v4773 -v5124 -v8283 -v228 -v577 v926 -v1275 -v1624 -v1973 -v2322 -v3369 -v4423 -v4774 -v5125 -v5476 -v5827 -v6178 -v6529 -v6880 v7231 -v7582 -v7933 -v229 -v1625 -v3021 -v3722 v4424 -v4775 -v5126 -v5477 -v8285 -v230 -v1626 -v4425 -v4776 -v5127 -v8286 -v231 v580 -v929 -v1278 -v1627 -v2325 -v3372 -v4075 v4426 -v4777 -v5128 -v5830 -v6181 -v6532 -v6883 -v7234 -v7585 -v7936 -v581 -v930 -v2326 -v2675 v4076 -v5831 -v6182 -v6533 -v8288 -v3025 v3726 -v8289 -v234 -v1630 -v1979 -v4429 -v4780 v5131 -v1980 -v2678 -v5483 -v8291 -v237 -v1633 -v1982 v4432 -v4783 -v5134 -v587 -v936 -v1285 v2332 -v3379 -v4082 -v5837 -v6188 -v6539 -v6890 -v7241 -v7592 -v7943 v5136 -v6189 -v1985 -v5488 -v241 v1288 -v1637 -v2684 -v3382 -v4436 -v4787 -v5138 -v6893 -v7244 -v7595 -v7946 -v8297 -v591 -v940 v1289 -v1987 -v2336 -v3383 -v5490 -v5841 v6192 -v6543 -v6894 -v7245 -v7596 -v7947 -v243 -v1290 -v1639 -v2686 -v3384 v4438 -v4789 -v5140 -v6895 -v7246 -v7597 -v7948 -v8299 -v1989 v2687 -v5492 -v5843 -v8300 -v245 -v1292 v1641 -v3386 -v4440 -v4791 -v5142 -v6897 -v7248 -v7599 -v7950 -v246 -v1293 v1642 -v3387 -v4441 -v4792 -v5143 -v6898 -v7249 -v7600 -v7951 -v8302 -v3039 -v3740 -v5495 -v2691 -v5496 v8304 -v249 -v598 -v947 -v1296 -v1645 -v2343 -v3390 -v4444 -v4795 -v5146 -v5848 -v6199 -v6550 -v6901 -v7252 v7603 -v7954 -v250 -v1297 v1646 -v3391 -v4445 -v4796 -v5147 -v6902 -v7253 -v7604 -v7955 -v3043 v3744 -v5499 -v252 -v601 -v950 -v1299 v1648 -v1997 -v2346 -v3393 -v4447 -v4798 -v5149 -v5500 -v5851 -v6202 -v6553 -v6904 v7255 -v7606 -v7957 -v253 -v602 -v951 -v1300 -v1649 v2347 -v3394 -v4097 -v4448 -v4799 -v5150 -v5852 -v6203 -v6554 -v6905 v7256 -v7607 -v7958 -v3046 -v3747 v8310 -v604 -v953 -v2000 -v2349 -v5503 -v5854 v6205 -v6556 -v256 -v1652 -v2001 -v4451 -v4802 v5153 -v5504 -v257 -v606 -v955 -v1653 -v2002 -v2351 -v4452 v4803 -v5154 -v5505 -v5856 -v6207 -v6558 v3050 -v3751 -v5506 -v259 -v1655 v2004 -v4454 v4805 -v5156 -v609 v958 -v1307 -v2005 -v2354 -v3401 -v5508 -v5859 -v6210 -v6561 v6912 -v7263 -v7614 -v7965 -v261 -v1657 -v4456 -v4807 -v5158 -v262 v1658 -v4457 -v4808 -v5159 -v8318 -v2706 -v5511 -v8319 -v264 -v1660 -v4459 -v4810 -v5161 -v5512 v2708 -v5513 -v8321 -v266 -v615 -v964 -v1313 -v1662 -v2360 -v3407 -v4461 -v4812 -v5163 -v5865 -v6216 -v6567 v6918 -v7269 -v7620 -v7971 -v267 -v1663 -v4462 -v4813 -v5164 -v8323 -v617 v966 -v2013 -v2362 -v2711 -v5516 -v5867 -v6218 -v6569 -v8324 -v3061 -v3762 -v8325 v1317 -v2015 -v3411 -v6922 -v7273 -v7624 -v7975 -v271 -v620 -v969 v1667 -v2365 -v4466 -v4817 -v5168 v5870 -v6221 -v6572 -v272 -v1319 -v1668 -v3413 -v4116 v4467 -v4818 -v5169 -v6924 -v7275 -v7626 -v7977 -v5521 v8329 -v623 -v972 -v1321 v2368 -v3415 -v5873 -v6224 -v6575 -v6926 v7277 -v7628 -v7979 -v2718 -v3067 -v3768 -v8331 -v4120 v5875 -v6226 -v6577 -v276 -v625 -v974 -v1323 v1672 -v2021 -v2370 -v3417 -v4472 -v4823 -v5174 -v5525 -v5876 -v6227 -v6578 -v6929 v7280 -v7631 -v7982 v277 -v1324 -v1673 -v3418 -v4473 -v4824 -v5175 -v6930 -v7281 -v7632 -v7983 -v278 -v627 -v976 -v1325 v1674 -v2023 -v2372 -v3419 -v4474 -v4825 -v5176 -v5527 -v5878 -v6229 -v6580 -v6931 -v7282 v7633 -v7984 -v279 -v628 -v977 -v1675 -v2024 v2373 -v3071 -v3773 -v4475 -v4826 -v5177 -v5879 -v6230 -v6581 -v3072 v3774 -v5529 -v8337 -v281 v1328 -v1677 -v3422 v4477 -v4828 -v5179 -v6934 -v7285 -v7636 -v7987 -v282 v1329 -v1678 -v3423 -v4127 v4478 -v4829 -v5180 -v6935 -v7286 -v7637 -v7988 v1330 -v2726 -v3424 -v5532 -v6936 -v7287 -v7638 -v7989 -v8340 v1331 -v3425 -v5533 -v6937 -v7288 -v7639 -v7990 -v285 -v1332 -v1681 -v3426 v4481 -v4832 -v5183 -v6938 -v7289 -v7640 -v7991 v1333 -v3078 -v3427 -v3780 -v6939 -v7290 -v7641 -v7992 -v2730 -v5536 -v8344 -v637 -v986 -v2033 -v2382 -v4133 -v5537 v5888 -v6239 -v6590 -v638 -v987 -v2034 -v2383 -v3081 -v3783 -v4134 -v5538 v5889 -v6240 -v6591 -v8347 -v290 v1337 -v1686 -v2733 -v3431 -v4487 -v4838 -v5189 -v6944 -v7295 -v7646 -v7997 v8348 -v8349 -v1339 -v2735 -v3433 -v6946 -v7297 -v7648 -v7999 v8350 v293 -v1689 -v4490 -v4841 -v5192 -v8351 -v294 -v643 -v992 v1341 -v1690 -v2039 -v2388 -v3435 -v4491 -v4842 -v5193 -v5544 -v5895 v6246 -v6597 -v6948 -v7299 -v7650 -v8001 -v295 -v644 -v993 -v1691 -v2389 -v3087 -v645 v994 -v1343 -v2041 -v2390 -v3437 -v5545 -v5896 -v6247 -v6598 -v6949 -v7300 v7651 -v8002 -v297 -v646 v995 -v1344 -v1693 -v2042 -v2391 -v3438 -v4493 -v4844 -v5195 -v5546 -v5897 -v6248 -v6599 -v6950 -v7301 -v7652 -v8003 v298 -v647 -v996 -v1345 -v1694 -v2043 -v2392 -v3439 -v4494 -v4845 -v5196 -v5547 -v5898 -v6249 -v6600 -v6951 -v7302 v7653 -v8004 -v299 -v648 -v997 v1695 -v2044 -v2393 -v4495 -v4846 -v5197 -v5899 -v6250 -v6601 -v301 -v650 -v999 v1348 -v1697 -v2046 -v2395 -v3442 -v4497 -v4848 -v5199 -v5550 -v5901 -v6252 -v6603 -v6954 -v7305 -v7656 -v8007 -v8358 -v2047 -v3094 -v3796 -v5200 -v5551 -v6253 -v8359 -v303 -v652 -v1001 -v1699 -v2048 -v2397 v3095 -v3797 -v4499 -v4850 v5201 -v5552 -v5903 -v6254 -v6605 -v304 v1700 -v4500 -v4851 -v5202 -v5553 v2749 -v3098 -v3800 -v8363 -v656 -v1005 -v2052 -v2401 v2750 -v3099 v3801 -v4152 -v5556 -v5907 -v6258 -v6609 -v8364 -v657 -v1006 -v2053 -v2402 -v3100 -v3802 -v4153 -v5557 -v5908 v6259 -v6610 -v309 -v658 v1007 -v1356 -v1705 -v2054 -v2403 -v3450 -v4154 -v4505 -v4856 -v5207 -v5558 -v5909 -v6260 -v6611 -v6962 -v7313 -v7664 -v8015 -v310 -v1706 -v660 -v1009 -v1358 -v2056 -v2405 -v3452 v4155 -v5559 -v5910 -v6261 -v6612 -v6963 -v7314 -v7665 -v8016 -v312 v661 -v1010 -v1359 -v1708 -v2057 -v2406 -v3104 -v3453 -v3805 -v4156 -v4507 -v4858 -v5209 -v5560 -v5911 -v6262 -v6613 -v6964 v7315 -v7666 -v8017 -v313 -v662 v1011 -v1360 -v1709 -v2058 -v2407 -v3454 v4508 -v4859 -v5210 -v5561 -v5912 -v6263 -v6614 -v6965 -v7316 -v7667 -v8018 v1361 -v3106 -v3455 -v3807 -v5562 -v6966 -v7317 -v7668 -v8019 v664 -v1013 -v2409 -v3107 -v3808 -v5914 -v6265 -v6616 -v2061 v3108 -v3809 -v5564 -v317 v666 -v1015 -v1713 -v2062 -v2411 v4512 -v4863 -v5214 -v5565 -v5916 -v6267 -v6618 v318 -v1714 v4162 -v4513 -v4864 -v5215 v668 -v1017 -v2064 -v2413 -v4163 -v5567 -v5918 -v6269 -v6620 -v1367 -v3112 -v3461 -v3813 -v6972 -v7323 v7674 -v8025 -v321 -v1717 v3113 -v3814 -v4165 -v4516 -v4867 v5218 -v1369 -v3114 -v3463 -v3815 v6974 -v7325 -v7676 -v8027 -v5571 v673 -v1022 -v1371 -v2069 -v2418 -v3465 -v5572 -v5923 -v6274 -v6625 v6976 -v7327 -v7678 -v8029 v325 -v1372 -v1721 -v3466 -v4520 -v4871 -v5222 -v5573 -v6977 -v7328 -v7679 -v8030 -v1373 v3467 -v5574 -v6978 -v7329 -v7680 -v8031 -v327 -v1374 -v1723 -v3468 v4522 -v4873 -v5224 -v5575 -v6979 -v7330 -v7681 -v8032 -v2771 -v3120 -v3821 -v8384 -v329 v1376 -v1725 -v3121 -v3470 -v3822 v4524 -v4875 -v5226 -v6981 -v7332 -v7683 -v8034 -v2773 -v3122 -v3823 -v8386 -v331 -v680 -v1029 v1727 -v2425 -v4526 -v4877 -v5228 v5930 -v6281 -v6632 -v3124 -v3825 -v4176 -v5580 -v333 -v682 -v1031 -v1380 v1729 -v2078 -v2427 -v3474 -v4528 -v4879 -v5230 -v5581 v5932 -v6283 -v6634 -v6985 -v7336 -v7687 -v8038 -v2777 -v4178 -v6284 -v335 -v684 -v1033 v1382 -v1731 -v2080 -v2429 -v2778 -v3476 v4179 -v4530 -v4881 -v5232 -v5583 -v5934 -v6285 -v6636 -v6987 -v7338 -v7689 -v8040 -v8391 v685 -v1034 -v2081 -v2430 -v2779 v5233 -v5584 -v5935 -v6286 -v6637 -v8392 -v2082 -v8393 -v338 v687 -v1036 -v1385 -v1734 -v2083 -v2432 -v3479 -v4533 -v4884 v5235 -v5586 -v5937 -v6288 -v6639 -v6990 -v7341 -v7692 -v8043 -v2782 -v3131 -v3832 -v8395 -v340 v689 -v1038 -v1736 -v2085 -v2434 -v6992 -v7343 v7694 -v8045 -v341 -v1737 -v4536 -v4887 -v5238 -v5589 -v691 v1040 -v2436 -v2785 -v5941 -v6292 -v6643 -v343 -v692 -v1041 -v1390 -v1739 -v2437 -v3135 -v3484 -v3836 v4187 -v4538 -v4889 -v5240 -v5942 -v6293 -v6644 -v6995 -v7346 -v7697 -v8048 -v1391 -v3485 -v6996 -v7347 -v7698 -v8049 -v8400 -v345 -v694 -v1043 -v1392 -v1741 v2090 -v2439 -v3486 -v4540 v4891 -v5242 -v5593 -v5944 -v6295 -v6646 -v6997 -v7348 -v7699 -v8050 -v1393 -v2091 -v2440 -v3138 -v3487 -v3839 -v4190 -v5945 -v6998 -v7349 -v7700 -v8051 -v3139 -v6999 -v7350 -v7701 -v8052 -v2094 v2792 -v350 -v699 -v1746 -v2095 -v3842 -v5246 v5597 -v5948 -v6299 -v351 -v700 -v1747 -v2096 -v2445 -v2794 -v3492 -v3843 -v5247 -v5598 v5949 -v6300 -v8055 -v352 -v701 -v1050 -v1748 -v2097 -v3144 v5599 -v5950 -v6301 -v6652 -v7003 -v7354 -v7705 -v353 -v702 -v1051 -v1749 -v2098 -v2447 -v2796 v3145 v3494 -v3845 -v5600 -v5951 -v6302 -v6653 -v7004 -v7355 -v7706 -v8057 -v5 -v1401 -v4197 -v4548 v4899 -v5250 -v1752 -v2450 -v2799 v3497 -v5252 -v8060 -v1753 -v3849 -v5253 -v9 -v358 -v707 -v1056 -v1405 -v2103 -v2452 v2801 -v3150 -v3499 -v4201 -v4552 -v4903 -v5254 -v5605 v5956 -v6307 -v6658 -v7009 -v7360 -v7711 -v8062 -v2453 -v2802 -v3500 -v5255 -v8063 -v2454 -v2803 -v3501 -v3852 -v5256 -v8064 -v2455 -v2804 v3502 -v3853 -v8065 -v13 -v1409 -v2456 -v2805 v3503 -v3854 -v4205 -v4556 -v4907 -v8066 -v14 v1061 -v1410 -v2806 -v3155 -v3504 -v3855 -v4206 -v4557 -v4908 -v6663 -v7014 -v7365 -v7716 -v15 -v1062 -v1411 -v1760 v2807 -v3156 -v3505 -v4207 v4558 -v4909 -v5260 -v6664 -v7015 -v7366 -v7717 -v8068 -v16 -v365 -v714 -v1063 -v1412 -v1761 -v2110 v3157 -v3857 -v4208 -v4559 -v4910 -v5261 -v5612 -v5963 -v6314 -v6665 -v7016 -v7367 -v7718 -v17 -v1064 -v1413 -v1762 v2809 -v3158 -v3507 -v4209 -v4560 -v4911 -v5262 -v6666 -v7017 -v7368 -v7719 -v18 -v367 -v716 -v1065 -v1414 -v1763 -v2112 -v2461 v2810 -v3159 -v3508 -v3859 v4210 -v4561 -v4912 -v5263 -v5614 -v5965 -v6316 -v6667 -v7018 -v7369 -v7720 -v19 -v368 -v717 -v1066 -v1415 -v2113 -v2462 -v3160 -v3860 -v4211 -v4562 -v4913 -v5264 -v5615 -v5966 -v6317 -v6668 v7019 -v7370 -v7721 -v8072 -v2463 -v2812 -v3510 -v3861 -v8073 -v2464 -v2813 -v3511 v3862 -v8074 -v2465 -v8075 -v23 -v372 -v721 -v1070 -v1419 -v1768 -v2117 -v2466 v3164 v4215 -v4566 -v4917 -v5268 -v5619 -v5970 -v6321 -v6672 -v7023 -v7374 -v7725 -v8076 -v24 -v1071 -v1420 -v2816 -v3165 -v3514 v3865 -v4216 -v4567 -v4918 -v6673 -v7024 -v7375 -v7726 -v8077 -v2817 -v3515 -v3866 -v5270 -v1073 -v2469 -v3167 -v3867 -v6675 -v7026 -v7377 -v7728 -v27 -v376 -v725 -v1074 -v1423 -v1772 -v2121 -v2470 -v3168 -v3868 -v4219 -v4570 -v4921 -v5272 -v5623 -v5974 -v6325 -v6676 -v7027 -v7378 -v7729 -v28 v1075 -v1424 -v2471 -v2820 -v3169 -v3518 -v3869 -v4220 -v4571 -v4922 -v6677 -v7028 -v7379 -v7730 -v29 -v378 -v727 -v1076 -v1425 -v1774 -v2123 -v2472 v3170 -v3870 -v4221 -v4572 -v4923 v5625 -v5976 -v6327 -v6678 -v7029 -v7380 -v7731 -v8082 -v30 -v379 -v728 -v1426 -v1775 -v2124 v2822 -v3520 -v4222 -v4573 -v4924 -v5275 -v5626 -v5977 -v6328 -v31 -v380 -v729 -v1427 -v1776 -v2125 v2823 -v3521 -v4223 -v4574 -v4925 -v5276 v5627 -v5978 -v6329 -v2475 -v2824 -v3522 -v3873 -v8085 -v33 -v382 -v731 -v1080 -v1429 -v2127 v2476 -v3174 -v3874 -v4225 -v4576 v4927 -v5278 -v5629 -v5980 -v6331 -v6682 -v7033 -v7384 -v7735 -v34 -v383 -v732 -v1081 -v1430 -v2128 -v2826 v3175 -v3524 -v3875 -v4226 -v4577 -v4928 -v5279 v5630 -v5981 -v6332 -v6683 -v7034 -v7385 -v7736 -v384 -v733 -v1780 -v2129 -v2478 -v3876 v5631 -v5982 -v6333 -v8088 -v37 -v1084 -v1433 v2829 -v3178 -v3527 -v4229 -v4580 -v4931 -v6686 -v7037 -v7388 -v7739 -v2481 -v8091 -v388 -v737 -v1784 -v2133 v2482 -v3880 -v5284 -v5635 -v5986 -v6337 -v8092 -v389 -v738 -v1785 -v2134 -v2832 -v3530 -v3881 v5636 -v5987 -v6338 -v2484 -v8094 -v42 -v1089 -v1438 -v2485 -v3183 -v4234 -v4585 -v4936 -v6691 -v7042 -v7393 -v7744 -v8095 -v2486 -v2835 -v3533 -v3884 v8096 -v393 -v742 -v1789 -v2138 -v5289 v5640 -v5991 -v6342 -v2488 -v2837 -v3535 v8098 -v396 -v745 -v1094 -v1792 -v2141 -v2490 v3188 v3888 -v5292 -v5643 -v5994 -v6345 -v6696 -v7047 -v7398 -v7749 -v8100 -v1095 -v2840 -v3189 -v3538 -v3889 -v6697 -v7048 -v7399 -v7750 -v1096 -v2492 -v2841 -v3190 -v3539 v3890 -v6698 -v7049 -v7400 -v7751 -v8102 -v1097 -v2493 -v2842 -v3191 -v3540 -v3891 -v6699 -v7050 -v7401 -v7752 -v8103 -v400 -v749 -v1796 -v2145 -v2494 -v2843 v3541 -v3892 -v5296 -v5647 -v5998 -v6349 -v8104 -v2495 -v2844 -v3542 -v8105 -v1100 -v2845 -v3194 -v3543 -v3894 -v6702 -v7053 -v7404 v7755 -v1101 -v2497 v2846 -v3195 -v3544 -v3895 -v6703 -v7054 -v7405 v7756 -v8107 -v3896 -v4247 -v4598 -v4949 -v5651 -v6002 v6353 -v6704 -v7055 -v7406 -v7757 -v55 v404 -v753 -v1102 -v1451 -v1800 -v2149 -v2498 -v3196 -v3897 -v4248 -v4599 -v4950 -v5652 -v6003 -v6354 -v6705 -v7056 -v7407 -v7758 -v8109 -v2499 -v2848 -v3547 -v3898 v8110 -v57 -v406 -v755 -v1104 -v1453 -v1802 -v2151 -v2500 v3198 -v4250 -v4601 -v4952 -v5303 -v5654 -v6005 -v6356 -v6707 -v7058 -v7409 -v7760 -v8111 -v58 -v407 -v756 -v1105 -v1454 -v1803 -v2152 -v2501 v3199 -v3900 -v4251 -v4602 -v4953 -v5304 -v5655 -v6006 v6357 -v6708 -v7059 -v7410 -v7761 -v1106 -v2502 -v2851 -v3200 -v3550 -v3901 -v6709 -v7060 -v7411 -v7762 -v8113 -v2503 -v2852 -v3551 -v3902 -v5306 -v8114 -v2504 -v2853 -v3552 -v3903 -v5307 -v8115 -v3904 -v4255 -v4606 -v4957 -v5659 -v6010 -v6361 -v6712 -v7063 -v7414 -v7765 -v2505 -v2854 -v3554 -v8117 -v1110 -v2506 -v2855 -v3204 v3555 -v3906 -v6714 -v7065 -v7416 -v7767 -v8118 -v64 -v413 -v762 -v1111 v1460 -v1809 -v2158 -v2507 -v3205 -v3907 -v4258 -v4609 -v4960 -v5311 -v5662 -v6013 -v6364 -v6715 -v7066 -v7417 -v7768 -v65 -v1461 -v2508 -v2857 -v3557 -v3908 -v4259 -v4610 -v4961 -v8120 v66 -v415 -v764 -v1113 -v1462 -v1811 -v2160 -v2509 -v3207 -v3909 -v4260 -v4611 -v4962 -v5313 -v5664 -v6015 -v6366 -v6717 -v7068 -v7419 -v7770 -v416 -v765 -v1114 -v1812 -v2161 -v2510 -v3208 -v3910 -v5665 -v6016 -v6367 -v6718 -v7069 -v7420 -v7771 -v8122 -v1115 -v2511 -v2860 -v3209 -v3560 -v3911 -v6719 -v7070 -v7421 -v7772 -v8123 -v69 v418 -v767 -v1116 -v1465 -v1814 -v2163 -v2512 -v3210 -v3912 -v4263 -v4614 -v4965 -v5667 -v6018 -v6369 -v6720 -v7071 -v7422 -v7773 -v8124 -v1117 -v2513 -v2862 -v3211 -v3562 -v3913 -v6721 -v7072 -v7423 -v7774 v8125 -v1118 -v2514 -v2863 -v3212 -v3563 -v3914 -v6722 -v7073 -v7424 -v7775 v8126 -v2515 -v2864 -v3564 -v3915 -v8127 v422 -v771 -v1818 -v2167 -v2516 -v3916 -v5320 -v5671 -v6022 -v6373 -v8128 -v74 -v423 -v772 -v1121 v1470 -v1819 -v2168 -v3215 -v3917 -v4268 -v4619 -v4970 -v5321 -v5672 -v6023 -v6374 -v6725 -v7076 -v7427 v7778 -v424 -v773 -v1122 -v1820 v2169 -v2518 -v3216 -v3918 -v5322 -v5673 -v6024 -v6375 -v6726 -v7077 -v7428 v7779 -v8130 -v76 -v425 -v774 -v1123 -v1472 -v1821 -v2170 -v2519 v2868 -v3217 -v3568 -v3919 -v4270 -v4621 -v4972 -v5323 -v5674 -v6025 -v6376 -v6727 -v7078 -v7429 -v7780 -v6728 -v7079 -v7430 -v7781 -v8132 -v2520 -v2869 -v3570 -v3921 -v8133 -v2521 -v2870 -v3571 -v3922 -v8134 v428 -v777 -v1824 -v2173 -v2522 -v2871 v3572 -v3923 -v5327 -v5678 -v6029 -v6380 -v8135 -v429 -v778 -v1127 -v1825 -v2174 -v2523 v3221 -v3924 -v5328 -v5679 -v6030 -v6381 -v6732 -v7083 -v7434 -v7785 v8136 -v1128 -v2524 -v2873 -v3222 -v3574 -v3925 -v6733 v7084 -v7435 -v7786 -v8137 -v431 -v780 -v1129 -v1827 -v2176 -v2525 -v2874 v3223 -v3575 -v3926 -v5681 v6032 -v6383 -v6734 -v7085 -v7436 -v7787 -v432 -v781 -v1130 -v2177 v2526 -v2875 -v3224 -v3576 -v3927 -v5682 -v6033 -v6384 -v6735 -v7086 -v7437 -v7788 -v8139 v2527 -v2876 -v3577 -v3928 -v8140 -v85 -v1132 -v1481 -v2528 -v2877 -v3226 -v3578 -v3929 v4280 -v4631 -v4982 -v6737 -v7088 -v7439 -v7790 -v8141 -v435 -v784 -v1133 -v1831 -v2180 -v2529 v2878 -v3227 -v3579 -v3930 -v5685 -v6036 -v6387 -v6738 -v7089 -v7440 -v7791 -v8142 -v2530 -v2879 -v3580 -v3931 -v8143 -v2880 -v3581 -v438 -v787 -v1834 -v2183 -v2532 -v2881 -v3582 -v3933 -v5688 -v6039 v6390 -v8145 -v1137 -v1835 -v2533 -v2882 -v3231 -v3583 -v3934 v5338 -v6742 -v7093 -v7444 -v7795 -v8146 -v92 -v441 -v790 -v1139 -v1488 -v2186 -v2535 -v3233 -v3936 v4287 -v4638 -v4989 -v5691 -v6042 -v6393 -v6744 -v7095 -v7446 -v7797 -v8148 -v442 -v791 -v1838 -v2187 -v5341 -v5692 v6043 -v6394 -v2537 -v2886 -v3587 -v3938 -v8150 -v2538 -v2887 -v3588 -v8151 -v96 -v1492 -v2539 -v2888 -v3589 -v3940 -v4291 -v4642 -v4993 -v447 -v796 -v1145 -v2192 -v2541 -v2890 -v3239 -v3591 -v3942 -v5697 -v6048 v6399 -v6750 -v7101 -v7452 -v7803 -v8154 -v2542 -v2891 -v3592 -v3943 -v8155 -v449 -v798 -v1147 -v1845 v2194 -v2543 -v2892 -v3241 -v3593 -v3944 -v5699 -v6050 -v6401 -v6752 -v7103 -v7454 -v7805 -v8156 -v2544 -v2893 -v3594 -v3945 -v8157 -v3946 -v4297 -v4648 -v4999 -v5701 -v6052 -v6403 -v6754 -v7105 -v7456 v7807 -v8158 -v452 -v801 -v2197 -v2895 -v3597 -v3948 -v5703 -v6054 -v6405 -v2547 -v2896 -v3598 -v8161 -v105 -v1152 -v1501 -v2548 -v2897 -v3246 -v3599 -v3950 -v4301 -v4652 -v5003 -v6758 v7109 -v7460 -v7811 -v8162 -v106 -v1502 -v2549 -v2898 -v3600 -v4302 -v4653 -v5004 -v107 -v1503 -v2899 -v3601 -v3952 -v4303 -v4654 -v5005 -v108 -v1155 -v1504 -v3249 -v3953 -v4304 -v4655 -v5006 -v6761 -v7112 -v7463 -v7814 -v109 -v1505 -v2552 v2901 -v3603 -v4305 -v4656 -v5007 -v8166 -v110 -v459 -v808 -v1157 -v1506 -v1855 v2204 -v3251 -v3955 -v4306 -v4657 -v5008 v5359 -v5710 -v6061 -v6412 -v6763 -v7114 -v7465 -v7816 -v1158 -v2554 -v2903 -v3252 -v3605 -v3956 -v6764 -v7115 -v7466 -v7817 -v8168 -v112 -v461 -v810 v1159 -v1508 -v1857 -v2206 -v2555 -v3253 -v3957 -v4308 -v4659 -v5010 -v5361 -v5712 -v6063 -v6414 -v6765 -v7116 -v7467 -v7818 -v1160 v2556 -v2905 -v3254 -v3607 -v6766 -v7117 -v7468 v7819 -v8170 -v2557 -v8171 -v115 -v464 -v813 -v1162 -v1511 -v1860 -v2209 -v3256 -v3960 v4311 -v4662 -v5013 -v5364 -v5715 -v6066 -v6417 -v6768 -v7119 -v7470 -v7821 -v465 -v814 -v1861 -v2210 v2559 -v2908 -v3610 -v5365 -v5716 -v6067 -v6418 -v8173 -v1164 -v2560 -v3258 -v6770 -v7121 -v7472 -v7823 -v8174 -v467 -v816 -v1165 -v1863 -v2212 -v2561 -v3259 -v3963 -v5718 v6069 -v6420 -v6771 -v7122 -v7473 -v7824 -v8175 -v2562 -v2911 v3613 -v3964 -v8176 -v120 -v1516 -v2563 -v3965 -v4316 -v4667 -v5018 -v8177 -v1168 v2564 -v2913 -v3262 -v3615 -v3966 -v6774 v7125 -v7476 -v7827 -v8178 -v1169 -v1867 -v2565 -v3263 -v3967 -v5371 -v6775 v7126 -v7477 -v7828 -v8179 -v124 -v1171 -v1520 -v2567 -v2916 -v3265 -v3618 -v3969 v4320 -v4671 -v5022 -v6777 -v7128 -v7479 -v7830 -v8181 -v1870 -v2568 -v5374 -v8182 -v475 -v824 -v1173 -v1871 -v2220 v2569 -v2918 -v3267 -v3620 -v3971 -v5726 -v6077 -v6428 -v6779 -v7130 -v7481 -v7832 -v8183 v2570 -v2919 -v3621 -v3972 -v8184 -v2571 -v2920 -v3622 -v8185 -v3974 -v1177 v2573 -v2922 -v3271 -v3624 -v3975 -v6783 -v7134 -v7485 -v7836 -v8187 -v1178 v2574 -v2923 -v3272 -v3625 -v3976 -v6784 v7135 -v7486 -v7837 -v8188 -v132 -v1528 -v2924 -v3626 -v3977 -v4328 -v4679 -v5030 v2576 -v2925 -v3627 -v3978 -v8190 -v134 -v483 -v832 -v1530 -v2228 v2577 -v3979 -v4330 -v4681 -v5032 -v5734 -v6085 -v6436 -v8191 -v135 -v484 -v833 -v1182 -v1531 -v2229 v2578 -v2927 -v3276 -v3629 -v3980 -v4331 -v4682 v5033 -v5384 -v5735 -v6086 -v6437 -v6788 -v7139 -v7490 -v7841 v2579 -v2928 -v3630 -v3981 -v8193 -v1184 v2580 -v2929 -v3278 -v3631 -v3982 -v6790 -v7141 -v7492 -v7843 -v8194 -v138 -v1534 -v2581 -v2930 -v3632 -v3983 -v4334 -v4685 -v5036 -v8195 -v2582 -v2931 -v3633 -v3984 -v8196 -v140 v1536 -v4336 -v4687 -v5038 -v142 -v1538 -v2585 -v2934 -v3636 -v3987 -v4338 -v4689 -v5040 -v8199 -v2586 -v2935 -v3637 -v3988 -v8200 -v144 -v493 v842 -v1191 -v1540 -v1889 -v2238 -v2587 -v2936 -v3285 -v3638 -v3989 -v4340 -v4691 -v5042 -v5393 -v5744 -v6095 -v6446 -v6797 -v7148 -v7499 v7850 -v8201 -v494 -v843 -v1890 -v2239 -v2588 -v3990 v5394 -v5745 -v6096 -v6447 -v8202 -v495 -v844 -v1891 -v2240 -v2938 -v3640 -v3991 -v5395 -v5746 -v6097 -v6448 -v8203 -v147 v1543 -v2590 -v2939 -v3641 -v3992 -v4343 -v4694 -v5045 -v8204 -v1195 -v2591 -v2940 -v3289 -v3642 -v6801 -v7152 v7503 -v7854 -v8205 -v1196 -v2592 -v3290 -v3994 -v6802 -v7153 v7504 -v7855 -v8206 -v150 -v499 -v848 -v1197 -v1546 -v1895 -v2244 -v3291 -v3995 -v4346 -v4697 -v5048 -v5750 -v6101 -v6452 -v6803 -v7154 -v7505 -v7856 -v151 -v1547 v2943 -v3645 -v3996 -v4347 -v4698 -v5049 -v501 -v850 -v1199 -v1897 -v2246 v3293 -v3997 v5401 -v5752 -v6103 -v6454 -v6805 -v7156 -v7507 -v7858 -v2596 -v2945 -v3647 -v3998 -v8210 -v503 -v852 -v1201 -v2248 -v2597 -v2946 -v3295 -v3648 -v3999 -v5403 -v5754 -v6105 -v6456 -v6807 -v7158 -v7509 v7860 -v504 -v853 -v1202 -v1900 -v2249 -v2598 -v3296 -v4000 -v5755 -v6106 -v6457 -v6808 -v7159 -v7510 -v7861 -v156 -v1203 -v1552 -v2599 -v2948 -v3297 -v3650 -v4001 -v4352 -v4703 -v5054 -v6809 v7160 -v7511 -v7862 -v8213 -v2600 -v2949 -v3651 -v4002 -v8214 -v2601 -v2950 -v3652 -v4003 -v8215 -v1206 -v2602 -v2951 -v3300 v3653 -v4004 -v6812 -v7163 -v7514 -v7865 -v8216 -v2603 -v2952 -v3654 -v4005 -v8217 -v161 -v510 -v859 -v1208 -v1557 -v2255 -v2953 -v3302 -v3655 -v4006 -v4357 -v4708 -v5059 -v5761 -v6112 -v6463 -v6814 -v7165 -v7516 -v7867 -v511 -v860 -v1907 -v2256 v2605 -v2954 -v3656 -v5411 -v5762 -v6113 -v6464 -v8219 -v2606 -v2955 -v3657 -v4008 v8220 -v513 -v862 -v1211 -v1909 -v2258 v2607 -v3305 -v5413 -v5764 -v6115 -v6466 -v6817 -v7168 -v7519 -v7870 -v8221 -v1212 -v2608 -v2957 -v3306 -v3659 -v6818 -v7169 -v7520 -v7871 -v8222 -v2609 -v2958 -v3660 -v8223 -v167 -v1214 -v1563 -v2610 -v3308 -v4012 -v4363 -v4714 -v5065 -v6820 -v7171 -v7522 -v7873 -v8224 -v168 -v1564 -v2611 -v2960 -v3662 -v4364 -v4715 -v5066 -v8225 -v518 -v867 -v1216 -v1914 -v2263 -v2612 -v3310 -v4014 -v5769 -v6120 -v6471 -v6822 -v7173 -v7524 -v7875 -v1217 -v2613 -v2962 -v3311 -v3664 -v6823 -v7174 v7525 -v7876 -v8227 v520 -v869 -v1218 -v2265 -v2614 -v2963 -v3312 -v3665 -v4016 -v5420 -v5771 -v6122 -v6473 -v6824 -v7175 v7526 -v7877 -v1219 -v2615 -v2964 -v3313 -v3666 -v6825 -v7176 -v7527 -v7878 v8229 -v3667 -v1220 -v2616 -v2965 -v3314 -v3668 -v6827 -v7178 -v7529 -v7880 -v8231 -v523 -v872 -v1919 -v2268 -v2617 -v4020 v5424 -v5775 -v6126 -v6477 -v8232 -v175 -v1222 -v1571 -v3316 -v4021 -v4372 -v4723 -v5074 -v6829 -v7180 -v7531 -v7882 -v176 -v525 -v874 -v1572 -v2270 -v2619 -v2968 -v3671 -v4373 v4724 -v5075 -v5777 -v6128 -v6479 -v8234 -v177 -v1573 -v1922 -v2620 -v2969 -v3672 -v4374 -v4725 -v5076 -v5427 -v8235 -v527 -v876 -v1923 -v2272 -v5428 -v5779 -v6130 -v6481 -v179 -v528 -v877 -v1575 -v1924 -v2273 -v2971 -v3674 -v4025 -v4376 -v4727 -v5078 -v5780 -v6131 -v6482 -v1227 v2623 -v3321 -v530 -v879 -v1926 -v2275 v2624 -v4026 -v5430 -v5781 -v6132 -v6483 -v8238 -v2625 -v8239 -v2626 -v8240 -v2976 -v3678 -v534 -v883 -v1930 -v2279 -v2628 -v4030 -v5434 -v5785 -v6136 -v6487 -v8242 -v1931 -v2629 -v2978 -v3680 -v5435 -v8243 -v187 v536 -v885 -v1583 -v1932 -v2281 -v2630 -v2979 -v3681 -v4032 -v4383 -v4734 -v5085 -v5436 -v5787 -v6138 -v6489 -v2631 -v2980 -v3682 -v8245 -v538 -v887 -v1934 -v2283 -v2632 -v2981 -v3683 -v4034 -v5438 -v5789 -v6140 -v6491 -v2633 -v2982 -v3684 v191 -v540 -v889 -v1238 -v1587 -v1936 -v2285 -v2983 -v3332 -v3685 -v4036 -v4387 -v4738 -v5089 -v5791 -v6142 -v6493 -v6844 -v7195 -v7546 v7897 -v2984 -v3686 -v2636 -v2985 -v3687 -v4038 -v8250 v543 -v892 -v1939 -v2288 -v4039 -v5443 -v5794 -v6145 -v6496 -v2638 -v2987 -v3689 -v4040 -v8252 v545 -v894 -v1941 -v2290 -v4041 -v5445 -v5796 -v6147 -v6498 -v2640 -v2989 -v3691 -v4042 -v8254 -v198 -v547 v896 -v1594 -v1943 -v2292 -v2641 -v2990 -v3692 -v4394 -v4745 -v5096 -v5447 -v5798 -v6149 -v6500 -v8255 -v199 -v548 -v897 -v1595 -v1944 v2293 -v2991 -v3693 -v4395 -v4746 -v5097 v5448 -v5799 -v6150 -v6501 -v549 -v898 -v1247 -v1945 v2294 -v3341 -v4045 v5449 -v5800 -v6151 -v6502 -v6853 -v7204 -v7555 -v7906 -v201 -v1597 -v2993 -v3695 -v4397 -v4748 v5099 -v1249 -v3343 -v6855 -v7206 -v7557 v7908 -v2646 -v2995 -v3697 -v4048 -v8260 -v1251 -v2647 -v2996 -v3345 -v3698 v4049 -v6857 -v7208 -v7559 -v7910 -v8261 -v1252 -v2648 -v2997 -v3346 -v3699 -v6858 v7209 -v7560 -v7911 -v8262 -v2649 -v2998 -v3700 -v8263 -v2650 -v2999 -v3701 -v4052 -v8264 -v558 -v907 -v2303 -v2652 -v3001 -v3703 -v4054 -v5809 -v6160 -v6511 v559 -v908 -v1257 -v1955 -v2304 -v3002 -v3351 -v3704 -v5459 -v5810 -v6161 -v6512 -v6863 -v7214 -v7565 -v7916 -v8267 -v560 -v909 -v2305 -v2654 -v3003 -v3705 -v4056 -v5811 -v6162 -v6513 v212 -v1259 -v1608 -v3004 -v3353 -v3706 -v4408 -v4759 -v5110 v6865 -v7216 -v7567 -v7918 v562 -v911 -v1260 -v1958 -v2307 -v3354 v5462 -v5813 -v6164 -v6515 -v6866 -v7217 -v7568 -v7919 -v8270 v563 -v912 -v1261 -v1959 -v2308 -v3006 -v3355 -v3708 v4059 -v5814 -v6165 -v6516 -v6867 -v7218 -v7569 -v7920 v564 -v913 -v1262 -v1960 -v2309 -v2658 -v3356 -v4060 -v5815 -v6166 -v6517 v6868 -v7219 -v7570 -v7921 -v8272 v216 -v1612 -v3008 -v3710 -v4412 -v4763 -v5114 v217 -v1613 -v2660 -v4413 -v4764 -v5115 -v8274 v2661 -v3010 -v3712 -v4063 -v8275 -v219 -v1615 v2662 -v4415 -v4766 -v5117 -v8276 -v569 -v918 -v1267 -v1965 -v2314 -v2663 -v3012 -v3361 -v3714 -v5820 v6171 -v6522 -v6873 -v7224 -v7575 -v7926 -v8277 v2664 -v3013 -v3715 -v8278 -v571 -v920 -v1967 -v2316 -v4067 -v5471 -v5822 -v6173 -v6524 -v223 -v572 -v921 -v1270 -v1619 -v2317 v2666 -v3015 -v3364 -v3717 v4068 -v4419 -v4770 -v5121 -v5823 -v6174 -v6525 -v6876 -v7227 -v7578 -v7929 -v8280 -v573 -v922 -v1271 -v1969 -v2318 -v2667 -v3016 -v3365 -v3718 -v5473 -v5824 -v6175 -v6526 -v6877 -v7228 -v7579 v7930 -v8281 -v2668 -v3017 -v3719 v4070 -v8282 -v2669 -v576 -v925 -v1274 -v1972 -v2321 -v3019 -v3368 -v3720 -v5826 -v6177 -v6528 -v6879 -v7230 -v7581 -v7932 -v2671 -v3020 -v3721 -v4072 -v8284 -v578 -v927 v1276 -v1974 -v2323 -v2672 -v3370 -v4073 -v5828 -v6179 -v6530 -v6881 -v7232 -v7583 -v7934 -v579 -v928 -v1277 -v1975 -v2324 v3022 -v3371 -v3723 -v5829 -v6180 -v6531 -v6882 -v7233 -v7584 v7935 -v2674 -v3023 -v3724 -v8287 -v232 -v1279 -v1628 -v1977 -v3024 v3373 -v3725 -v4427 -v4778 -v5129 -v5480 -v6884 -v7235 -v7586 -v7937 -v583 -v932 -v1281 -v2328 -v2677 v3026 -v3375 -v3727 -v4078 -v5482 -v5833 -v6184 -v6535 -v6886 -v7237 -v7588 -v7939 -v8290 v235 -v584 -v933 -v1631 -v2329 -v3027 v3728 -v4430 -v4781 -v5132 -v5834 -v6185 -v6536 -v4080 -v1284 -v2680 -v3029 -v3378 -v3730 -v4081 -v6889 -v7240 -v7591 -v7942 -v8293 -v238 -v1634 -v1983 -v2681 -v3030 v3731 -v4433 -v4784 -v5135 -v5486 -v8294 -v2682 -v3031 -v3732 -v4083 -v8295 -v589 -v938 -v1287 -v2334 -v2683 -v3032 -v3381 -v3733 -v4084 -v5839 -v6190 -v6541 -v6892 v7243 -v7594 -v7945 -v8296 -v590 -v939 -v1986 -v2335 -v3033 v3734 -v4085 -v5489 -v5840 -v6191 -v6542 -v2685 -v3034 -v3735 -v4086 -v8298 -v592 -v941 -v1988 -v2337 v3035 -v3736 -v4087 -v5491 -v5842 -v6193 -v6544 -v244 -v1640 -v4088 v4439 -v4790 -v5141 -v594 -v943 -v1990 -v2339 -v2688 -v3037 -v3738 -v4089 -v5493 -v5844 -v6195 v6546 -v8301 -v3038 -v3739 -v247 -v596 -v945 v1294 -v1643 -v1992 -v2341 -v2690 -v3388 -v4091 -v4442 -v4793 -v5144 -v5846 -v6197 v6548 -v6899 -v7250 -v7601 -v7952 -v8303 -v248 v1295 -v1644 -v3040 -v3389 -v3741 -v4092 -v4443 -v4794 -v5145 -v6900 -v7251 -v7602 -v7953 -v1994 -v2692 v3041 -v3742 -v4093 -v5497 -v8305 -v599 -v948 -v1995 -v2344 -v2693 -v3042 -v3743 v4094 -v5498 -v5849 -v6200 -v6551 -v8306 v251 -v600 -v949 -v1298 -v1647 -v1996 -v2345 -v2694 -v3392 -v4095 -v4446 -v4797 -v5148 -v5850 -v6201 -v6552 -v6903 -v7254 -v7605 -v7956 -v8307 -v2695 -v3044 -v3745 -v4096 -v8308 -v1998 -v2696 -v3045 -v3746 -v5501 -v8309 -v254 -v603 -v952 -v1301 -v1650 -v1999 -v2348 v3395 -v4098 -v4449 -v4800 -v5151 -v5502 -v5853 -v6204 -v6555 -v6906 -v7257 -v7608 -v7959 -v2698 -v3047 -v3748 -v4099 -v8311 -v605 -v954 -v1303 -v2350 -v2699 v3048 -v3397 -v3749 -v4100 -v5855 -v6206 -v6557 -v6908 -v7259 -v7610 -v7961 -v8312 -v1304 -v2700 v3049 -v3398 -v3750 -v4101 -v6909 -v7260 -v7611 -v7962 -v8313 -v258 -v607 -v956 -v1305 -v1654 -v2003 -v2352 -v2701 -v3399 v4102 -v4453 -v4804 -v5155 -v5857 -v6208 -v6559 -v6910 -v7261 -v7612 -v7963 -v8314 -v2702 -v3051 -v3752 -v4103 -v5507 -v8315 -v2703 -v3052 -v3753 -v4104 -v8316 -v2704 -v3053 -v3754 -v8317 -v611 -v960 -v1309 -v2007 -v2356 -v2705 -v3054 -v3403 -v3755 -v4106 -v5510 -v5861 -v6212 -v6563 -v6914 v7265 -v7616 -v7967 -v263 -v1659 -v3055 -v3756 -v4458 -v4809 -v5160 -v613 -v962 -v1311 -v2009 -v2358 -v2707 v3056 -v3405 -v3757 -v4108 v5863 -v6214 -v6565 -v6916 -v7267 -v7618 -v7969 -v8320 -v265 -v614 -v963 -v1312 -v1661 -v2010 -v2359 -v3057 -v3406 -v3758 -v4109 -v4460 -v4811 -v5162 -v5864 -v6215 v6566 -v6917 -v7268 -v7619 -v7970 -v3058 -v3759 -v616 -v965 v1314 -v2012 -v2361 -v2710 -v3059 -v3408 -v3760 -v4111 -v5515 v5866 -v6217 -v6568 -v6919 -v7270 -v7621 -v7972 -v268 -v1315 -v1664 -v3060 -v3409 -v3761 -v4112 -v4463 -v4814 -v5165 -v6920 -v7271 -v7622 v7973 -v269 -v618 -v967 v1316 -v1665 -v2014 -v2363 -v2712 -v3410 -v4113 -v4464 -v4815 -v5166 -v5517 v5868 -v6219 -v6570 -v6921 -v7272 -v7623 -v7974 -v270 -v619 -v968 -v1666 -v2364 -v2713 -v3062 -v3763 -v4114 -v4465 -v4816 -v5167 -v5518 v5869 -v6220 -v6571 -v8326 -v2714 -v3063 -v3764 -v4115 -v8327 -v2017 -v3064 -v3765 -v5520 v273 -v622 -v971 -v1320 -v1669 -v2018 -v2367 -v3414 -v4117 -v4468 -v4819 -v5170 -v5872 -v6223 -v6574 -v6925 -v7276 -v7627 -v7978 -v2717 -v3066 -v3767 -v4118 -v8330 -v275 v624 -v973 -v1322 -v1671 -v2020 -v2369 -v3416 -v4119 -v4470 -v4821 -v5172 -v5523 -v5874 -v6225 -v6576 -v6927 -v7278 -v7629 v7980 -v3769 -v2719 -v3068 -v3770 -v4121 -v8333 -v626 -v975 -v2022 -v2371 -v2720 -v3069 -v3771 -v4122 -v5526 -v5877 -v6228 v6579 -v8334 -v2721 -v3070 -v3772 -v4123 -v8335 -v2722 -v8336 -v280 -v629 -v978 -v1327 -v1676 -v2025 -v2374 -v3421 -v4125 -v4476 -v4827 -v5178 -v5880 -v6231 -v6582 -v6933 -v7284 -v7635 -v7986 -v630 -v979 -v2026 -v2375 -v3073 -v3775 -v4126 -v5530 -v5881 -v6232 -v6583 -v631 -v980 -v2027 -v2376 -v2725 -v3074 -v3776 -v5531 -v5882 -v6233 -v6584 -v8339 -v283 -v632 -v981 -v1679 -v2028 -v2377 -v4128 -v4479 -v4830 -v5181 -v5883 -v6234 v6585 -v284 -v633 -v982 -v1680 -v2029 -v2378 -v2727 -v3076 -v3778 -v4129 -v4480 -v4831 -v5182 -v5884 -v6235 v6586 -v8341 -v286 -v635 -v984 -v1682 -v2031 -v2380 -v2729 v4131 -v4482 -v4833 -v5184 -v5535 -v5886 -v6237 -v6588 -v8343 -v636 -v985 -v2032 -v2381 -v4132 -v5887 -v6238 v6589 -v2731 -v3080 -v3782 -v8345 -v2732 -v8346 -v4486 -v4837 -v5188 -v5539 -v5890 -v6241 v6592 -v6943 -v7294 -v7645 -v7996 -v639 -v988 -v2035 -v2384 -v3082 -v3785 -v4136 -v5540 -v5891 -v6242 -v6593 -v291 -v1338 -v1687 -v3432 -v4488 -v4839 -v5190 -v6945 -v7296 v7647 -v7998 v292 -v641 -v990 -v1688 -v2037 -v2386 -v3084 -v3787 -v4138 -v4489 -v4840 -v5191 -v5542 -v5893 -v6244 -v6595 -v642 -v991 -v1340 -v2038 -v2387 -v3085 -v3434 -v3788 -v4139 -v5543 -v5894 -v6245 -v6596 -v6947 -v7298 v7649 -v8000 -v2737 -v3086 -v3789 -v4140 -v8352 -v2040 -v2738 -v296 -v1692 -v2739 -v3088 -v3790 -v4141 -v4492 -v4843 -v5194 -v8353 -v2740 -v3089 v3791 -v4142 -v8354 -v2741 -v3090 -v3792 -v4143 -v8355 -v1346 -v2742 -v3091 -v3440 -v3793 -v4144 -v6952 -v7303 -v7654 v8005 -v8356 v300 -v649 -v998 -v1347 -v1696 -v2045 -v2394 -v2743 -v3092 -v3441 -v3794 v4145 -v4496 -v4847 -v5198 -v5549 -v5900 -v6251 -v6602 -v6953 -v7304 -v7655 -v8006 -v8357 -v2744 -v3093 -v3795 v4146 -v1350 -v2746 -v3444 -v4148 -v6956 -v7307 -v7658 -v8009 -v8360 -v1351 -v2747 -v3096 -v3445 v3798 -v4149 -v6957 -v7308 -v7659 -v8010 -v8361 -v306 -v655 -v1004 -v1353 -v1702 -v2051 -v2400 -v3447 -v4151 -v4502 -v4853 -v5204 -v5555 -v5906 -v6257 -v6608 -v6959 -v7310 -v7661 v8012 -v307 -v1354 -v1703 -v3448 -v4503 -v4854 -v5205 -v6960 -v7311 -v7662 -v8013 v308 -v1355 -v1704 -v2751 -v3449 -v4504 -v4855 -v5206 -v6961 -v7312 -v7663 -v8014 -v8365 -v2752 -v3101 v3803 -v8366 -v2755 -v8368 -v2756 -v3105 -v3806 -v4157 -v8369 -v314 -v663 -v1012 -v1710 -v2059 -v2408 -v2757 v4158 -v4509 -v4860 -v5211 -v5913 -v6264 -v6615 -v8370 -v315 -v1362 -v1711 -v2060 -v2758 -v3456 -v4159 -v4510 v4861 -v5212 -v5563 -v6967 -v7318 -v7669 -v8020 -v8371 -v316 -v665 -v1014 -v1712 -v2410 -v2759 -v4160 -v4511 v4862 -v5213 -v5915 -v6266 -v6617 -v8372 -v1364 -v2760 -v3109 -v3458 -v3810 -v4161 -v6969 -v7320 -v7671 -v8022 -v8373 -v667 -v1016 -v1365 -v2063 -v2412 -v2761 -v3110 -v3459 -v3811 -v5566 -v5917 -v6268 -v6619 -v6970 -v7321 -v7672 -v8023 -v8374 -v319 -v1366 -v1715 -v2762 -v3111 -v3460 -v3812 -v4514 -v4865 -v5216 -v6971 -v7322 v7673 -v8024 -v8375 v669 -v1018 -v2065 -v2414 -v2763 -v4164 -v5568 -v5919 -v6270 -v6621 -v8376 -v2765 -v8378 -v323 v672 -v1021 -v1370 -v1719 -v2068 -v2417 -v2766 -v3115 -v3464 -v3816 -v4167 -v4518 -v4869 -v5220 -v5922 -v6273 -v6624 -v6975 -v7326 v7677 -v8028 -v8379 -v324 -v1720 -v2767 -v3116 -v3817 -v4168 -v4519 -v4870 -v5221 -v8380 -v2768 -v3117 -v3818 -v8381 -v326 -v675 -v1024 -v1722 -v2071 -v2420 -v2769 -v3118 -v3819 -v4170 -v4521 -v4872 -v5223 -v5925 -v6276 v6627 -v8382 -v2770 -v3119 -v3820 -v8383 -v328 -v677 -v1026 -v1375 v1724 -v2073 -v2422 -v3469 -v4172 -v4523 -v4874 -v5225 -v5576 -v5927 -v6278 v6629 -v6980 -v7331 -v7682 -v8033 -v678 -v1027 -v2074 -v2423 -v2772 -v4173 -v5577 -v5928 -v6279 -v6630 -v8385 -v330 -v679 -v1028 -v1377 -v1726 v2075 -v2424 -v3471 -v4174 -v4525 -v4876 -v5227 -v5578 -v5929 -v6280 -v6631 v6982 -v7333 -v7684 -v8035 -v2774 -v3123 -v3824 -v4175 -v8387 -v332 -v681 -v1030 -v1379 -v1728 v2077 -v2426 -v2775 -v3473 -v4527 -v4878 -v5229 -v5931 -v6282 -v6633 -v6984 -v7335 -v7686 v8037 -v2776 -v3125 -v3826 -v4177 -v8389 -v334 -v1381 -v1730 -v3475 -v4529 v4880 -v5231 -v6986 -v7337 -v7688 -v8039 -v4180 -v337 -v686 -v1035 -v1384 v1733 -v2431 -v2780 -v3129 -v3478 -v3830 -v4181 -v4532 -v4883 -v5234 v5585 -v5936 -v6287 -v6638 -v6989 -v7340 -v7691 -v8042 -v2781 -v3130 -v3831 -v4182 -v8394 -v2783 -v3132 -v4184 -v4535 -v4886 -v5237 -v5588 -v5939 -v6290 -v6641 -v8396 -v690 -v1039 -v1388 v2086 -v2435 -v2784 -v3482 -v5940 -v6291 -v6642 -v6993 -v7344 -v7695 -v8046 -v8397 -v342 -v1389 -v1738 -v2087 -v3483 -v4186 -v4537 -v4888 -v5239 -v5590 -v6994 -v7345 -v7696 -v8047 -v8398 v2088 -v2786 -v5591 -v8399 v344 -v1740 -v3136 -v3837 -v4188 -v4539 -v4890 -v5241 -v2788 -v3137 -v3838 -v4189 -v8401 -v2789 -v8402 -v3840 -v4542 v4893 -v5244 -v5595 -v5946 -v6297 -v6648 -v8403 -v348 -v697 -v1046 -v1395 -v1744 -v2093 v2442 -v3140 -v3489 -v349 -v698 -v1047 -v1396 -v1745 -v2443 -v3141 -v3490 -v3841 -v4192 -v4543 -v4894 -v5245 -v5596 -v5947 -v6298 -v6649 -v7000 -v7351 -v7702 v8053 -v8404 one -v6 -v7 -v8 -v22 -v36 -v38 -v39 -v41 -v43 -v44 -v45 -v46 -v52 -v63 -v78 -v88 -v91 v97 -v99 -v102 -v116 -v118 -v119 -v123 -v127 v129 -v139 -v148 -v149 -v152 -v157 -v159 -v160 -v166 -v171 -v178 -v182 -v183 v184 -v188 -v192 -v215 -v221 -v233 -v236 -v239 v240 -v242 v255 -v260 -v274 -v287 v288 -v289 v302 -v305 v311 -v320 -v322 -v336 -v339 -v346 -v347 -v354 -v357 -v371 -v375 -v385 v387 -v390 -v392 -v394 -v395 -v398 -v411 -v417 -v426 v436 -v437 -v444 -v446 -v453 -v456 -v462 -v463 -v468 -v470 -v472 -v476 -v478 -v480 -v489 -v490 -v492 -v506 -v509 -v531 -v532 -v533 -v550 -v555 -v557 -v565 -v566 -v567 -v570 -v575 v582 -v585 -v586 -v588 -v593 -v595 -v597 -v608 v610 v612 -v621 -v634 -v640 -v651 -v653 -v654 v659 -v670 -v671 -v674 -v676 -v683 -v688 -v693 v695 -v696 -v703 -v706 -v720 -v722 -v724 -v734 -v736 -v739 -v741 -v743 -v744 -v747 -v760 -v766 -v775 -v785 -v786 -v793 -v795 -v802 -v805 -v811 -v812 -v817 -v819 -v821 -v825 -v827 -v829 -v838 -v839 v841 -v855 v858 v880 v881 -v882 -v899 -v904 -v906 -v914 -v915 -v916 -v919 -v924 -v931 -v934 -v935 -v937 -v942 -v944 -v946 -v957 -v959 -v961 -v970 -v983 -v989 -v1000 -v1002 -v1003 -v1008 -v1019 -v1020 -v1023 -v1025 -v1032 -v1037 -v1042 -v1044 -v1045 v1053 -v1054 -v1069 v1082 -v1083 -v1085 -v1086 v1087 -v1088 -v1090 -v1091 -v1092 -v1093 v1109 -v1120 -v1136 -v1141 -v1142 -v1144 -v1148 -v1150 -v1151 -v1154 -v1161 v1166 -v1174 -v1175 -v1188 v1193 -v1198 -v1207 v1213 -v1221 -v1225 -v1229 -v1230 -v1231 -v1236 -v1239 -v1253 -v1256 -v1258 -v1264 -v1268 -v1280 -v1282 -v1283 -v1286 -v1291 -v1302 -v1306 -v1308 -v1310 -v1318 -v1326 v1334 -v1335 -v1336 v1342 -v1349 -v1352 -v1357 -v1363 -v1368 -v1378 -v1383 -v1386 -v1387 v1394 -v1402 -v1403 -v1404 -v1418 -v1432 -v1434 -v1435 -v1437 -v1439 -v1440 -v1441 v1442 -v1448 -v1459 -v1474 -v1484 v1487 -v1493 -v1495 -v1498 -v1512 -v1514 -v1515 -v1519 -v1523 -v1525 -v1535 -v1544 -v1545 -v1548 v1553 -v1555 -v1556 -v1562 -v1567 -v1574 -v1578 -v1579 -v1580 -v1584 -v1588 -v1604 -v1611 -v1617 -v1629 -v1632 -v1635 -v1636 -v1638 -v1651 -v1656 -v1670 -v1683 -v1684 -v1685 -v1698 -v1701 -v1707 -v1716 -v1718 -v1732 -v1735 -v1742 -v1743 -v1750 -v1767 -v1769 -v1771 -v1781 -v1783 -v1786 -v1788 -v1790 -v1791 -v1794 -v1807 v1813 v1822 -v1823 -v1832 -v1833 -v1836 -v1839 -v1840 -v1841 -v1842 -v1844 -v1846 -v1847 -v1849 -v1851 -v1852 -v1859 -v1866 -v1868 -v1874 -v1876 -v1885 -v1888 -v1902 -v1905 -v1927 -v1928 -v1929 -v1946 -v1951 -v1961 -v1962 -v1963 -v1966 -v1971 -v1976 -v1978 -v1981 -v1984 -v1991 -v1993 -v2006 -v2008 -v2011 -v2016 -v2019 -v2030 -v2036 -v2049 -v2050 -v2055 -v2066 -v2067 -v2070 -v2072 -v2076 -v2079 -v2084 -v2089 -v2092 -v2099 -v2102 -v2116 v2118 -v2120 -v2130 -v2132 -v2135 -v2137 -v2139 -v2140 v2143 -v2156 -v2162 -v2171 -v2181 v2182 -v2189 -v2191 -v2198 -v2201 -v2207 -v2208 -v2213 -v2215 -v2217 -v2221 -v2223 -v2225 -v2234 -v2237 -v2251 -v2254 -v2276 -v2277 -v2278 -v2295 -v2300 -v2310 -v2311 -v2312 -v2315 -v2320 -v2327 -v2330 v2331 v2333 -v2338 -v2340 -v2342 -v2353 -v2355 -v2357 -v2366 -v2379 -v2385 -v2396 -v2398 -v2399 -v2404 -v2415 v2416 -v2419 v2421 v2428 v2433 -v2438 -v2441 -v2446 -v2449 -v2451 -v2459 -v2468 -v2473 -v2474 -v2477 -v2483 -v2517 -v2531 -v2534 -v2540 -v2545 -v2546 -v2558 -v2566 -v2572 -v2583 -v2584 -v2594 -v2618 -v2621 -v2627 -v2634 -v2635 -v2637 -v2639 -v2651 -v2655 -v2659 -v2670 -v2673 -v2676 -v2679 -v2689 -v2697 v2709 v2715 -v2716 v2723 -v2724 v2728 -v2734 -v2736 -v2745 -v2748 -v2753 -v2754 -v2764 -v2787 -v2790 -v2791 -v2793 -v2797 -v2798 -v2800 -v2808 v2814 -v2818 v2828 -v2831 -v2834 -v2838 -v2883 -v2889 -v2894 -v2906 v2915 -v2926 -v2967 v2970 -v2974 -v2975 -v2977 -v2986 -v2988 -v2994 -v3000 -v3005 -v3011 -v3018 -v3028 -v3036 -v3065 -v3075 -v3077 -v3079 v3083 v3097 -v3102 -v3103 -v3126 -v3127 -v3128 -v3133 -v3134 -v3147 -v3148 -v3163 -v3176 -v3177 -v3179 -v3180 -v3181 v3182 v3184 v3185 v3186 -v3187 -v3203 -v3214 v3230 -v3235 v3236 -v3238 -v3242 -v3244 -v3245 v3248 -v3255 -v3260 -v3268 v3269 -v3282 -v3287 -v3292 -v3301 -v3307 -v3315 -v3319 -v3323 -v3324 -v3325 v3330 -v3333 -v3347 -v3349 -v3350 -v3352 -v3358 -v3362 -v3374 -v3376 v3377 -v3380 -v3385 -v3396 -v3400 -v3402 -v3404 -v3412 -v3420 -v3428 -v3429 v3430 -v3436 -v3443 -v3446 -v3451 -v3457 -v3462 -v3472 -v3477 -v3480 -v3481 -v3488 -v3491 -v3495 -v3496 -v3498 v3506 -v3512 -v3516 -v3526 -v3529 -v3532 -v3536 -v3584 -v3590 -v3596 -v3608 -v3617 v3628 -v3670 -v3673 -v3676 -v3677 -v3679 -v3688 -v3690 -v3696 -v3702 -v3707 -v3713 -v3729 -v3737 -v3766 -v3777 -v3779 -v3781 -v3784 -v3786 -v3799 -v3804 -v3827 -v3828 -v3829 -v3833 v3834 v3835 -v3844 -v3846 -v3847 -v3848 -v3850 -v3851 -v3856 -v3858 -v3863 -v3879 -v3882 -v3885 -v3886 -v3893 -v3905 -v3935 -v3941 -v3947 -v3951 -v3958 -v3959 -v3973 -v3985 -v3986 -v4010 -v4011 -v4017 -v4018 v4019 -v4024 -v4027 -v4028 -v4029 v4037 -v4044 -v4046 -v4047 -v4051 -v4053 -v4057 -v4058 -v4061 -v4062 -v4064 -v4066 -v4071 -v4074 -v4077 -v4079 -v4090 -v4105 -v4107 -v4110 -v4124 -v4130 -v4135 -v4137 -v4147 -v4150 -v4166 -v4169 -v4171 -v4183 -v4185 -v4191 -v4198 -v4199 -v4200 -v4214 -v4228 -v4230 -v4231 -v4233 -v4235 -v4236 -v4237 -v4238 -v4244 -v4257 -v4273 -v4283 -v4286 -v4292 -v4294 -v4298 -v4312 -v4314 -v4315 -v4319 -v4323 -v4325 -v4335 -v4344 -v4345 -v4348 -v4353 -v4355 -v4356 -v4362 -v4367 -v4369 -v4375 -v4378 -v4379 -v4380 -v4384 -v4388 -v4404 -v4411 -v4417 -v4428 -v4431 -v4434 -v4435 -v4437 -v4450 -v4455 -v4469 -v4471 -v4483 -v4484 -v4485 -v4498 -v4501 -v4506 -v4515 -v4517 -v4531 -v4534 -v4541 -v4549 -v4550 v4551 -v4565 -v4579 -v4581 -v4582 v4584 -v4586 -v4587 -v4588 -v4589 -v4595 -v4608 v4624 v4634 -v4637 -v4643 -v4645 -v4649 -v4663 -v4665 -v4666 v4670 -v4674 -v4676 v4686 -v4695 -v4696 -v4699 -v4704 -v4706 -v4707 -v4713 -v4718 -v4726 -v4729 -v4730 -v4731 -v4735 -v4739 -v4755 -v4762 -v4768 -v4779 -v4782 -v4785 -v4786 -v4788 -v4801 -v4806 -v4820 -v4822 -v4834 -v4835 -v4836 -v4849 -v4852 -v4857 -v4866 -v4868 -v4882 -v4885 -v4892 -v4900 -v4901 -v4902 -v4916 -v4930 -v4932 -v4933 -v4935 -v4937 -v4938 -v4939 -v4940 -v4946 -v4959 -v4975 -v4985 -v4988 -v4994 v4996 v5000 -v5014 -v5016 -v5017 -v5021 -v5025 -v5027 -v5037 -v5046 -v5047 -v5050 -v5055 -v5057 -v5058 -v5064 -v5069 -v5071 v5077 -v5080 -v5081 -v5082 v5086 -v5090 -v5113 -v5130 -v5133 -v5137 -v5139 -v5152 -v5157 -v5171 -v5173 -v5185 -v5186 -v5187 -v5203 -v5208 -v5217 -v5219 -v5236 -v5243 -v5248 -v5251 -v5259 -v5266 -v5267 -v5271 -v5281 -v5285 -v5291 -v5325 -v5326 -v5332 v5335 -v5336 -v5339 -v5342 -v5343 -v5344 -v5345 -v5347 -v5349 -v5351 -v5352 v5353 -v5355 -v5362 -v5372 -v5378 -v5389 -v5390 -v5406 -v5409 -v5431 -v5432 -v5433 -v5440 -v5450 -v5455 -v5456 v5465 -v5466 -v5467 -v5470 v5475 -v5478 -v5479 -v5481 -v5484 -v5485 -v5487 -v5494 -v5509 -v5514 -v5519 -v5522 -v5524 -v5528 -v5534 -v5541 -v5548 -v5554 -v5569 -v5570 -v5579 -v5582 -v5587 -v5592 v5594 -v5604 -v5618 -v5620 -v5622 -v5632 -v5634 -v5637 -v5639 -v5641 -v5642 -v5645 -v5660 -v5666 -v5676 -v5686 -v5687 -v5694 -v5696 -v5704 -v5707 -v5713 -v5714 -v5719 -v5721 -v5723 -v5727 -v5729 -v5731 -v5740 -v5743 -v5757 -v5760 -v5773 -v5782 -v5783 -v5784 -v5801 -v5806 -v5817 -v5818 -v5821 -v5832 -v5835 -v5836 -v5838 -v5845 -v5847 -v5858 -v5860 -v5862 -v5871 -v5885 -v5892 -v5902 -v5904 -v5905 -v5920 -v5921 -v5924 -v5926 -v5933 -v5938 -v5943 -v5952 -v5955 -v5969 -v5971 -v5973 -v5983 -v5985 -v5988 -v5990 -v5992 -v5993 -v5996 -v6011 -v6017 -v6027 -v6037 -v6038 v6045 -v6047 -v6055 v6058 -v6064 -v6065 -v6070 -v6072 -v6074 -v6078 -v6080 -v6082 v6091 -v6092 -v6094 -v6108 -v6111 -v6124 -v6133 -v6134 v6135 -v6152 v6157 -v6167 -v6169 -v6183 -v6186 -v6187 -v6194 -v6196 -v6198 -v6209 -v6211 -v6213 -v6222 -v6236 -v6243 -v6255 -v6256 -v6271 -v6272 -v6275 -v6277 -v6289 -v6294 -v6296 -v6303 -v6306 -v6320 -v6322 -v6324 -v6334 -v6336 -v6339 -v6341 -v6344 -v6347 -v6362 -v6368 -v6378 -v6388 -v6389 -v6396 -v6398 -v6406 -v6409 -v6415 -v6416 -v6421 -v6423 -v6425 -v6429 -v6431 -v6433 -v6442 -v6443 -v6445 -v6459 -v6462 -v6475 -v6484 -v6485 -v6486 -v6503 -v6508 -v6518 -v6519 -v6520 -v6523 -v6534 v6537 -v6538 -v6540 -v6545 v6547 -v6549 -v6560 -v6562 -v6564 -v6573 -v6587 -v6594 -v6604 -v6606 -v6607 -v6622 -v6623 v6626 -v6628 -v6635 -v6640 v6645 -v6647 -v6655 -v6656 v6671 -v6684 -v6685 -v6687 -v66#### 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.98 0.95 2/54 10814
Raw data (stat): 10814 (runsolver) R 10813 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422344019 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 7923 0 0 0 974 23 0 0 25 0 1 0 422344019 33542144 6814 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8189 6814 603 41 0 8148 0
vsize: 32756
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 7923 0 0 0 1974 23 0 0 25 0 1 0 422344019 33542144 6814 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8189 6814 603 41 0 8148 0
vsize: 32756
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 7958 0 0 0 2974 23 0 0 25 0 1 0 422344019 33673216 6849 4294967295 134512640 134672761 3221224576 3221223840 134618046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 6849 603 41 0 8180 0
vsize: 32884
[startup+40.001 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 7964 0 0 0 3974 23 0 0 25 0 1 0 422344019 33673216 6855 4294967295 134512640 134672761 3221224576 3221223700 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8221 6855 603 41 0 8180 0
vsize: 32884
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8003 0 0 0 4974 23 0 0 25 0 1 0 422344019 33804288 6894 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8253 6894 603 41 0 8212 0
vsize: 33012
[startup+60.002 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8044 0 0 0 5974 24 0 0 25 0 1 0 422344019 33939456 6935 4294967295 134512640 134672761 3221224576 3221223700 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8286 6935 603 41 0 8245 0
vsize: 33144
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8095 0 0 0 6974 24 0 0 25 0 1 0 422344019 34295808 6986 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8373 6986 603 41 0 8332 0
vsize: 33492
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8166 0 0 0 7974 24 0 0 25 0 1 0 422344019 34566144 7057 4294967295 134512640 134672761 3221224576 3221223760 134615649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7057 603 41 0 8398 0
vsize: 33756
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8598 0 0 0 8973 26 0 0 25 0 1 0 422344019 36282368 7489 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8858 7489 603 41 0 8817 0
vsize: 35432
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8737 0 0 0 9973 26 0 0 25 0 1 0 422344019 36818944 7628 4294967295 134512640 134672761 3221224576 3221223760 134616042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8989 7628 603 41 0 8948 0
vsize: 35956
[startup+110.003 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 8892 0 0 0 10972 27 0 0 25 0 1 0 422344019 37486592 7783 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9152 7783 603 41 0 9111 0
vsize: 36608
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 9035 0 0 0 11972 27 0 0 25 0 1 0 422344019 38154240 7926 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9315 7926 603 41 0 9274 0
vsize: 37260
[startup+130.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 9212 0 0 0 12972 28 0 0 25 0 1 0 422344019 38825984 8103 4294967295 134512640 134672761 3221224576 3221223700 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 8103 603 41 0 9438 0
vsize: 37916
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 9915 0 0 0 13969 30 0 0 25 0 1 0 422344019 41725952 8806 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10187 8806 603 41 0 10146 0
vsize: 40748
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 11218 0 0 0 14965 35 0 0 25 0 1 0 422344019 47280128 10109 4294967295 134512640 134672761 3221224576 3221223760 134615964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11543 10109 603 41 0 11502 0
vsize: 46172
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 12418 0 0 0 15960 40 0 0 25 0 1 0 422344019 52056064 11309 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12709 11309 603 41 0 12668 0
vsize: 50836
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 13375 0 0 0 16959 41 0 0 25 0 1 0 422344019 56012800 12266 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13675 12266 603 41 0 13634 0
vsize: 54700
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 14262 0 0 0 17956 44 0 0 25 0 1 0 422344019 59600896 13153 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14551 13153 603 41 0 14510 0
vsize: 58204
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 15098 0 0 0 18953 47 0 0 25 0 1 0 422344019 63016960 13989 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15385 13989 603 41 0 15344 0
vsize: 61540
[startup+200.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 15350 0 0 0 19953 48 0 0 25 0 1 0 422344019 64086016 14241 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15646 14241 603 41 0 15605 0
vsize: 62584
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 15679 0 0 0 20952 49 0 0 25 0 1 0 422344019 65417216 14570 4294967295 134512640 134672761 3221224576 3221223760 134615985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15971 14570 603 41 0 15930 0
vsize: 63884
[startup+220.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 16185 0 0 0 21950 51 0 0 25 0 1 0 422344019 67416064 15076 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16459 15076 603 41 0 16418 0
vsize: 65836
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 17604 0 0 0 22947 54 0 0 25 0 1 0 422344019 73232384 16495 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17879 16495 603 41 0 17838 0
vsize: 71516
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 18763 0 0 0 23943 58 0 0 25 0 1 0 422344019 77991936 17654 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19041 17654 603 41 0 19000 0
vsize: 76164
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 19784 0 0 0 24941 61 0 0 25 0 1 0 422344019 82624512 18675 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20172 18675 603 41 0 20131 0
vsize: 80688
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 20855 0 0 0 25938 64 0 0 25 0 1 0 422344019 86994944 19746 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21239 19746 603 41 0 21198 0
vsize: 84956
[startup+270.008 s]
Raw data (loadavg): 1.07 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 21570 0 0 0 26935 67 0 0 25 0 1 0 422344019 89923584 20461 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21954 20461 603 41 0 21913 0
vsize: 87816
[startup+280.009 s]
Raw data (loadavg): 1.06 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 21806 0 0 0 27934 68 0 0 25 0 1 0 422344019 90988544 20697 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22214 20697 603 41 0 22173 0
vsize: 88856
[startup+290.009 s]
Raw data (loadavg): 1.05 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 21867 0 0 0 28934 68 0 0 25 0 1 0 422344019 91123712 20758 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22247 20758 603 41 0 22206 0
vsize: 88988
[startup+300.01 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 21945 0 0 0 29934 68 0 0 25 0 1 0 422344019 91529216 20836 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22346 20836 603 41 0 22305 0
vsize: 89384
[startup+310.01 s]
Raw data (loadavg): 1.04 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 22018 0 0 0 30935 68 0 0 25 0 1 0 422344019 91799552 20909 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22412 20909 603 41 0 22371 0
vsize: 89648
[startup+320.01 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 22204 0 0 0 31934 69 0 0 25 0 1 0 422344019 92463104 21095 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22574 21095 603 41 0 22533 0
vsize: 90296
[startup+330.01 s]
Raw data (loadavg): 1.03 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 22668 0 0 0 32933 70 0 0 25 0 1 0 422344019 94334976 21559 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23031 21559 603 41 0 22990 0
vsize: 92124
[startup+340.01 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 23456 0 0 0 33930 73 0 0 25 0 1 0 422344019 97509376 22347 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23806 22347 603 41 0 23765 0
vsize: 95224
[startup+350.011 s]
Raw data (loadavg): 1.02 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 24281 0 0 0 34928 75 0 0 25 0 1 0 422344019 100835328 23172 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24618 23172 603 41 0 24577 0
vsize: 98472
[startup+360.011 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 25381 0 0 0 35925 78 0 0 25 0 1 0 422344019 105345024 24272 4294967295 134512640 134672761 3221224576 3221223776 134610493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25719 24272 603 41 0 25678 0
vsize: 102876
[startup+370.011 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 26206 0 0 0 36923 80 0 0 25 0 1 0 422344019 108670976 25097 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26531 25097 603 41 0 26490 0
vsize: 106124
[startup+380.011 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 26821 0 0 0 37921 83 0 0 25 0 1 0 422344019 111190016 25712 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27146 25712 603 41 0 27105 0
vsize: 108584
[startup+390.011 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 27333 0 0 0 38920 84 0 0 25 0 1 0 422344019 113315840 26224 4294967295 134512640 134672761 3221224576 3221223760 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27665 26224 603 41 0 27624 0
vsize: 110660
[startup+400.012 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 27961 0 0 0 39919 86 0 0 25 0 1 0 422344019 115847168 26852 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28283 26852 603 41 0 28242 0
vsize: 113132
[startup+410.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 28648 0 0 0 40916 88 0 0 25 0 1 0 422344019 118755328 27539 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28993 27539 603 41 0 28952 0
vsize: 115972
[startup+420.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 29164 0 0 0 41915 90 0 0 25 0 1 0 422344019 120811520 28055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29495 28055 603 41 0 29454 0
vsize: 117980
[startup+430.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 29669 0 0 0 42913 92 0 0 25 0 1 0 422344019 122941440 28560 4294967295 134512640 134672761 3221224576 3221223616 134612616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30015 28560 603 41 0 29974 0
vsize: 120060
[startup+440.013 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 30163 0 0 0 43912 93 0 0 25 0 1 0 422344019 124956672 29054 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30507 29054 603 41 0 30466 0
vsize: 122028
[startup+450.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 30783 0 0 0 44910 95 0 0 25 0 1 0 422344019 127483904 29674 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31124 29674 603 41 0 31083 0
vsize: 124496
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 31736 0 0 0 45907 98 0 0 25 0 1 0 422344019 131428352 30627 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32087 30627 603 41 0 32046 0
vsize: 128348
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 32406 0 0 0 46906 100 0 0 25 0 1 0 422344019 134078464 31297 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32734 31297 603 41 0 32693 0
vsize: 130936
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 33064 0 0 0 47904 102 0 0 25 0 1 0 422344019 137928704 31955 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33674 31955 603 41 0 33633 0
vsize: 134696
[startup+490.015 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 33527 0 0 0 48903 103 0 0 25 0 1 0 422344019 139812864 32418 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34134 32418 603 41 0 34093 0
vsize: 136536
[startup+500.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 59202 0 0 0 49842 163 0 0 25 0 1 0 422344019 245956608 55592 4294967295 134512640 134672761 3221224576 3221167048 1075347139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60048 55592 603 41 0 60007 0
vsize: 240192
[startup+510.016 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 94897 0 0 0 50753 252 0 0 25 0 1 0 422344019 398696448 91287 4294967295 134512640 134672761 3221224576 3221223216 134622626 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 97338 91287 603 41 0 97297 0
vsize: 389352
[startup+520.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 97438 0 0 0 51690 289 0 0 25 0 1 0 422344019 405749760 92927 4294967295 134512640 134672761 3221224576 3221222608 134566562 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99060 92927 603 41 0 99019 0
vsize: 396240
[startup+530.017 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99159 0 0 0 52631 322 0 0 25 0 1 0 422344019 412921856 94648 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100811 94648 603 41 0 100770 0
vsize: 403244
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99160 0 0 0 53631 322 0 0 25 0 1 0 422344019 412921856 94649 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100811 94649 603 41 0 100770 0
vsize: 403244
[startup+550.018 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99160 0 0 0 54630 322 0 0 25 0 1 0 422344019 412921856 94649 4294967295 134512640 134672761 3221224576 3221223024 134643567 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100811 94649 603 41 0 100770 0
vsize: 403244
[startup+560.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99164 0 0 0 55630 323 0 0 25 0 1 0 422344019 412921856 94653 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100811 94653 603 41 0 100770 0
vsize: 403244
[startup+570.019 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99164 0 0 0 56630 323 0 0 25 0 1 0 422344019 412921856 94653 4294967295 134512640 134672761 3221224576 3221223024 134643570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94653 603 41 0 100770 0
vsize: 403244
[startup+580.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99164 0 0 0 57631 323 0 0 25 0 1 0 422344019 412921856 94653 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94653 603 41 0 100770 0
vsize: 403244
[startup+590.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 58631 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+600.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 59631 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 60631 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+620.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 61631 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+630.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 62632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+640.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 63632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+650.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 64632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134644032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+660.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 65632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+670.022 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 66632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+680.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 67632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+690.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 68632 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+700.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 69633 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+710.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 70633 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+720.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 71633 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+730.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99168 0 0 0 72633 323 0 0 25 0 1 0 422344019 412921856 94657 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100811 94657 603 41 0 100770 0
vsize: 403244
[startup+740.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99201 0 0 0 73633 323 0 0 25 0 1 0 422344019 413048832 94690 4294967295 134512640 134672761 3221224576 3221222992 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100842 94690 603 41 0 100801 0
vsize: 403368
[startup+750.024 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99530 0 0 0 74563 346 0 0 25 0 1 0 422344019 414793728 95019 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101268 95019 603 41 0 101227 0
vsize: 405072
[startup+760.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99842 0 0 0 75516 369 0 0 25 0 1 0 422344019 414093312 94865 4294967295 134512640 134672761 3221224576 3221223024 134643567 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101097 94865 603 41 0 101056 0
vsize: 404388
[startup+770.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99842 0 0 0 76515 369 0 0 25 0 1 0 422344019 414093312 94865 4294967295 134512640 134672761 3221224576 3221223024 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101097 94865 603 41 0 101056 0
vsize: 404388
[startup+780.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99875 0 0 0 77513 370 0 0 25 0 1 0 422344019 414351360 94898 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101160 94898 603 41 0 101119 0
vsize: 404640
[startup+790.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99887 0 0 0 78512 371 0 0 25 0 1 0 422344019 414351360 94910 4294967295 134512640 134672761 3221224576 3221223024 134643471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101160 94910 603 41 0 101119 0
vsize: 404640
[startup+800.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99887 0 0 0 79511 372 0 0 25 0 1 0 422344019 414351360 94910 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101160 94910 603 41 0 101119 0
vsize: 404640
[startup+810.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99897 0 0 0 80508 374 0 0 25 0 1 0 422344019 414314496 94919 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101151 94919 603 41 0 101110 0
vsize: 404604
[startup+820.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99900 0 0 0 81505 376 0 0 25 0 1 0 422344019 414314496 94919 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101151 94919 603 41 0 101110 0
vsize: 404604
[startup+830.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99913 0 0 0 82498 383 0 0 25 0 1 0 422344019 414314496 94919 4294967295 134512640 134672761 3221224576 3221222992 134644251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101151 94919 603 41 0 101110 0
vsize: 404604
[startup+840.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99914 0 0 0 83496 385 0 0 25 0 1 0 422344019 414314496 94920 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101151 94920 603 41 0 101110 0
vsize: 404604
[startup+850.028 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99914 0 0 0 84495 386 0 0 25 0 1 0 422344019 414314496 94920 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101151 94920 603 41 0 101110 0
vsize: 404604
[startup+860.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 85490 390 0 0 25 0 1 0 422344019 414437376 94937 4294967295 134512640 134672761 3221224576 3221223024 134643719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101181 94937 603 41 0 101140 0
vsize: 404724
[startup+870.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 86486 393 0 0 25 0 1 0 422344019 414339072 94926 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101157 94926 603 41 0 101116 0
vsize: 404628
[startup+880.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 87484 395 0 0 25 0 1 0 422344019 414339072 94926 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101157 94926 603 41 0 101116 0
vsize: 404628
[startup+890.029 s]
Raw data (loadavg): 1.08 1.02 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 88477 401 0 0 25 0 1 0 422344019 414339072 94926 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101157 94926 603 41 0 101116 0
vsize: 404628
[startup+900.03 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 89475 403 0 0 25 0 1 0 422344019 414339072 94926 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101157 94926 603 41 0 101116 0
vsize: 404628
[startup+910.031 s]
Raw data (loadavg): 1.06 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99931 0 0 0 90474 404 0 0 25 0 1 0 422344019 414339072 94926 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101157 94926 603 41 0 101116 0
vsize: 404628
[startup+920.031 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99933 0 0 0 91469 408 0 0 25 0 1 0 422344019 414355456 94928 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101161 94928 603 41 0 101120 0
vsize: 404644
[startup+930.032 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99942 0 0 0 92467 409 0 0 25 0 1 0 422344019 414490624 94937 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101194 94937 603 41 0 101153 0
vsize: 404776
[startup+940.031 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99942 0 0 0 93466 410 0 0 25 0 1 0 422344019 414457856 94937 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101186 94937 603 41 0 101145 0
vsize: 404744
[startup+950.032 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99952 0 0 0 94460 416 0 0 25 0 1 0 422344019 414355456 94931 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101161 94931 603 41 0 101120 0
vsize: 404644
[startup+960.033 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99952 0 0 0 95450 420 0 0 25 0 1 0 422344019 414355456 94931 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101161 94931 603 41 0 101120 0
vsize: 404644
[startup+970.032 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 99953 0 0 0 96446 424 0 0 25 0 1 0 422344019 414416896 94928 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101176 94928 603 41 0 101135 0
vsize: 404704
[startup+980.032 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100034 0 0 0 97438 432 0 0 25 0 1 0 422344019 413630464 94776 4294967295 134512640 134672761 3221224576 3221223024 134643948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100984 94776 603 41 0 100943 0
vsize: 403936
[startup+990.033 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100036 0 0 0 98426 443 0 0 25 0 1 0 422344019 413540352 94756 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100962 94756 603 41 0 100921 0
vsize: 403848
[startup+1000.03 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100037 0 0 0 99415 454 0 0 25 0 1 0 422344019 413540352 94757 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94757 603 41 0 100921 0
vsize: 403848
[startup+1010.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100038 0 0 0 100409 459 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1020.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100038 0 0 0 101403 464 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643545 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 102401 466 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 103399 467 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221221936 134566554 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 104398 468 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 105396 470 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 106396 471 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 107395 471 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 108393 472 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 109393 473 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221222840 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100096 0 0 0 110392 473 0 0 25 0 1 0 422344019 413540352 94759 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94759 603 41 0 100921 0
vsize: 403848
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100097 0 0 0 111389 476 0 0 25 0 1 0 422344019 413540352 94760 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100962 94760 603 41 0 100921 0
vsize: 403848
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 112388 476 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 113388 476 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643719 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 114388 476 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 115387 478 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221222856 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 116387 478 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134644014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 117387 478 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 118385 480 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 119384 481 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
[startup+1210.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 10814
Raw data (stat): 10814 (minisat+) R 10813 5897 5896 0 -1 0 100152 0 0 0 120384 481 0 0 25 0 1 0 422344019 413540352 94758 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100962 94758 603 41 0 100921 0
vsize: 403848
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.35 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 10814
Raw data (stat): 10814 (minisat+) Z 10813 5897 5896 0 -1 12 100153 0 0 0 120385 510 0 0 25 0 1 0 422344019 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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): 1210.35
CPU time (s): 1208.97
CPU user time (s): 1203.86
CPU system time (s): 5.10822
CPU usage (%): 99.8855
Max. virtual memory (Kb): 405072
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####