PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/een/normalized-air05.opb
MD5SUM	95088621f0c51b4be3bb24a2abf2d630
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	7195
Biggest coefficient in the objective function	2679
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	3908448
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	2679
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	3908448
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.35779
Number of variables	7195
Total number of constraints	852
Number of constraints which are clauses	426
Number of constraints which are cardinality constraints (but not clauses)	426
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	404
Trace number 6917

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 20:25:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4984 boxname=wulflinc11 idbench=384 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  95088621f0c51b4be3bb24a2abf2d630  /oldhome/oroussel/tmp/wulflinc11/normalized-air05.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-air05.opb
IDLAUNCH: 4984
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        859880 kB
Buffers:         36664 kB
Cached:         113104 kB
SwapCached:       4932 kB
Active:          64928 kB
Inactive:        92704 kB
HighTotal:      131008 kB
HighFree:        14000 kB
LowTotal:       903652 kB
LowFree:        845880 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11640 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 20:45:19 (client local time) WITH STATUS 10 IN 1200.31 SECONDS
stats: 4984 7 1200.31 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 852 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): .....
c ---[ 850]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:    9
c ---[ 840]---> BDD-cost:   11
c ---[ 838]---> BDD-cost:   13
c ---[ 836]---> BDD-cost:   15
c ---[ 834]---> BDD-cost:   17
c ---[ 830]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:   17
c ---[ 824]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   23
c ---[ 820]---> BDD-cost:   23
c ---[ 818]---> BDD-cost:   25
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   27
c ---[ 812]---> BDD-cost:   29
c ---[ 810]---> BDD-cost:   29
c ---[ 808]---> BDD-cost:   31
c ---[ 806]---> BDD-cost:   25
c ---[ 804]---> BDD-cost:   23
c ---[ 802]---> BDD-cost:   33
c ---[ 800]---> BDD-cost:   29
c ---[ 798]---> BDD-cost:   35
c ---[ 796]---> BDD-cost:   27
c ---[ 790]---> BDD-cost:   39
c ---[ 788]---> BDD-cost:   39
c ---[ 786]---> BDD-cost:    0
c ---[ 784]---> BDD-cost:   37
c ---[ 782]---> BDD-cost:   39
c ---[ 780]---> BDD-cost:   43
c ---[ 776]---> BDD-cost:   39
c ---[ 774]---> BDD-cost:   47
c ---[ 772]---> BDD-cost:   47
c ---[ 770]---> BDD-cost:   43
c ---[ 768]---> BDD-cost:   43
c ---[ 766]---> BDD-cost:   49
c ---[ 764]---> BDD-cost:   49
c ---[ 762]---> BDD-cost:   51
c ---[ 760]---> BDD-cost:   47
c ---[ 758]---> BDD-cost:   51
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:   53
c ---[ 752]---> BDD-cost:   53
c ---[ 750]---> BDD-cost:   53
c ---[ 748]---> BDD-cost:   55
c ---[ 746]---> BDD-cost:   55
c ---[ 744]---> BDD-cost:   55
c ---[ 742]---> BDD-cost:   57
c ---[ 740]---> BDD-cost:   51
c ---[ 738]---> BDD-cost:   65
c ---[ 736]---> BDD-cost:   63
c ---[ 734]---> BDD-cost:   65
c ---[ 732]---> BDD-cost:   65
c ---[ 730]---> BDD-cost:   67
c ---[ 728]---> BDD-cost:   67
c ---[ 726]---> BDD-cost:   69
c ---[ 724]---> BDD-cost:   65
c ---[ 722]---> BDD-cost:   71
c ---[ 720]---> BDD-cost:   71
c ---[ 718]---> BDD-cost:   67
c ---[ 716]---> BDD-cost:   65
c ---[ 714]---> BDD-cost:   75
c ---[ 712]---> BDD-cost:   73
c ---[ 710]---> BDD-cost:   77
c ---[ 708]---> BDD-cost:   77
c ---[ 706]---> BDD-cost:   81
c ---[ 704]---> BDD-cost:   81
c ---[ 700]---> BDD-cost:   55
c ---[ 698]---> BDD-cost:   83
c ---[ 696]---> BDD-cost:   45
c ---[ 694]---> BDD-cost:   85
c ---[ 692]---> BDD-cost:   89
c ---[ 690]---> BDD-cost:   89
c ---[ 688]---> BDD-cost:   89
c ---[ 686]---> BDD-cost:   79
c ---[ 684]---> BDD-cost:   91
c ---[ 682]---> BDD-cost:   93
c ---[ 680]---> BDD-cost:   67
c ---[ 678]---> BDD-cost:   91
c ---[ 676]---> BDD-cost:   93
c ---[ 674]---> BDD-cost:    0
c ---[ 672]---> BDD-cost:   89
c ---[ 670]---> BDD-cost:   95
c ---[ 668]---> BDD-cost:   95
c ---[ 666]---> BDD-cost:  101
c ---[ 664]---> BDD-cost:  101
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  103
c ---[ 658]---> BDD-cost:  103
c ---[ 656]---> BDD-cost:  103
c ---[ 654]---> BDD-cost:  103
c ---[ 652]---> BDD-cost:  105
c ---[ 650]---> BDD-cost:   75
c ---[ 648]---> BDD-cost:  103
c ---[ 646]---> BDD-cost:   69
c ---[ 644]---> BDD-cost:  109
c ---[ 642]---> BDD-cost:  111
c ---[ 640]---> BDD-cost:  111
c ---[ 638]---> BDD-cost:  111
c ---[ 636]---> BDD-cost:    0
c ---[ 634]---> BDD-cost:   77
c ---[ 632]---> BDD-cost:  107
c ---[ 630]---> BDD-cost:  113
c ---[ 628]---> BDD-cost:   81
c ---[ 626]---> BDD-cost:   97
c ---[ 624]---> BDD-cost:   85
c ---[ 622]---> BDD-cost:  101
c ---[ 620]---> BDD-cost:   99
c ---[ 618]---> BDD-cost:  119
c ---[ 616]---> BDD-cost:  121
c ---[ 614]---> BDD-cost:  119
c ---[ 612]---> BDD-cost:  127
c ---[ 610]---> BDD-cost:  131
c ---[ 608]---> BDD-cost:  123
c ---[ 606]---> BDD-cost:  131
c ---[ 604]---> BDD-cost:   99
c ---[ 602]---> BDD-cost:    0
c ---[ 600]---> BDD-cost:  133
c ---[ 598]---> BDD-cost:  123
c ---[ 596]---> BDD-cost:  129
c ---[ 594]---> BDD-cost:  135
c ---[ 592]---> BDD-cost:  137
c ---[ 590]---> BDD-cost:  137
c ---[ 588]---> BDD-cost:   99
c ---[ 586]---> BDD-cost:  137
c ---[ 584]---> BDD-cost:  119
c ---[ 582]---> BDD-cost:  135
c ---[ 580]---> BDD-cost:  141
c ---[ 578]---> BDD-cost:  141
c ---[ 576]---> BDD-cost:  105
c ---[ 574]---> BDD-cost:   87
c ---[ 572]---> BDD-cost:   89
c ---[ 570]---> BDD-cost:  129
c ---[ 568]---> BDD-cost:  145
c ---[ 567]---> BDD-cost:  149
c ---[ 565]---> BDD-cost:  149
c ---[ 563]---> BDD-cost:  125
c ---[ 561]---> BDD-cost:  141
c ---[ 557]---> BDD-cost:    0
c ---[ 555]---> BDD-cost:  149
c ---[ 553]---> BDD-cost:  143
c ---[ 551]---> BDD-cost:   11
c ---[ 548]---> BDD-cost:  151
c ---[ 546]---> BDD-cost:  153
c ---[ 544]---> BDD-cost:  153
c ---[ 542]---> BDD-cost:  155
c ---[ 540]---> BDD-cost:   43
c ---[ 538]---> BDD-cost:  157
c ---[ 536]---> BDD-cost:   93
c ---[ 534]---> BDD-cost:  157
c ---[ 532]---> BDD-cost:  145
c ---[ 530]---> BDD-cost:  159
c ---[ 528]---> BDD-cost:  157
c ---[ 526]---> BDD-cost:  129
c ---[ 524]---> BDD-cost:  163
c ---[ 522]---> BDD-cost:  165
c ---[ 520]---> BDD-cost:  167
c ---[ 518]---> BDD-cost:  131
c ---[ 516]---> BDD-cost:  169
c ---[ 514]---> BDD-cost:  169
c ---[ 512]---> BDD-cost:  169
c ---[ 510]---> BDD-cost:  171
c ---[ 508]---> BDD-cost:  141
c ---[ 506]---> BDD-cost:  149
c ---[ 504]---> BDD-cost:  163
c ---[ 502]---> BDD-cost:  175
c ---[ 500]---> BDD-cost:  165
c ---[ 498]---> BDD-cost:  169
c ---[ 496]---> BDD-cost:  107
c ---[ 494]---> BDD-cost:  149
c ---[ 492]---> BDD-cost:  115
c ---[ 490]---> BDD-cost:  177
c ---[ 488]---> BDD-cost:  181
c ---[ 486]---> BDD-cost:  179
c ---[ 484]---> BDD-cost:  183
c ---[ 482]---> BDD-cost:  183
c ---[ 480]---> BDD-cost:  173
c ---[ 478]---> BDD-cost:  185
c ---[ 476]---> BDD-cost:  185
c ---[ 474]---> BDD-cost:  137
c ---[ 472]---> BDD-cost:  189
c ---[ 470]---> BDD-cost:  189
c ---[ 468]---> BDD-cost:  189
c ---[ 464]---> BDD-cost:  189
c ---[ 462]---> BDD-cost:  191
c ---[ 460]---> BDD-cost:  191
c ---[ 458]---> BDD-cost:  125
c ---[ 456]---> BDD-cost:  193
c ---[ 454]---> BDD-cost:  193
c ---[ 452]---> BDD-cost:  197
c ---[ 450]---> BDD-cost:  165
c ---[ 448]---> BDD-cost:  101
c ---[ 446]---> BDD-cost:  185
c ---[ 444]---> BDD-cost:  199
c ---[ 442]---> BDD-cost:  201
c ---[ 440]---> BDD-cost:  203
c ---[ 438]---> BDD-cost:  187
c ---[ 436]---> BDD-cost:  203
c ---[ 434]---> BDD-cost:  207
c ---[ 432]---> BDD-cost:  201
c ---[ 430]---> BDD-cost:  207
c ---[ 429]---> BDD-cost:  167
c ---[ 427]---> BDD-cost:  133
c ---[ 425]---> BDD-cost:  207
c ---[ 422]---> BDD-cost:  211
c ---[ 420]---> BDD-cost:  209
c ---[ 418]---> BDD-cost:  213
c ---[ 416]---> BDD-cost:  213
c ---[ 414]---> BDD-cost:  145
c ---[ 412]---> BDD-cost:  117
c ---[ 410]---> BDD-cost:  163
c ---[ 408]---> BDD-cost:  215
c ---[ 406]---> BDD-cost:  151
c ---[ 404]---> BDD-cost:  217
c ---[ 402]---> BDD-cost:  185
c ---[ 400]---> BDD-cost:  221
c ---[ 398]---> BDD-cost:  223
c ---[ 395]---> BDD-cost:  225
c ---[ 393]---> BDD-cost:  223
c ---[ 391]---> BDD-cost:  223
c ---[ 390]---> BDD-cost:  213
c ---[ 388]---> BDD-cost:  191
c ---[ 386]---> BDD-cost:  147
c ---[ 384]---> BDD-cost:   41
c ---[ 382]---> BDD-cost:  227
c ---[ 380]---> BDD-cost:   83
c ---[ 378]---> BDD-cost:  229
c ---[ 376]---> BDD-cost:  231
c ---[ 374]---> BDD-cost:  223
c ---[ 372]---> BDD-cost:  231
c ---[ 370]---> BDD-cost:  233
c ---[ 368]---> BDD-cost:   99
c ---[ 366]---> BDD-cost:  223
c ---[ 364]---> BDD-cost:  235
c ---[ 362]---> BDD-cost:  237
c ---[ 360]---> BDD-cost:  223
c ---[ 358]---> BDD-cost:  237
c ---[ 356]---> BDD-cost:  107
c ---[ 354]---> BDD-cost:  215
c ---[ 352]---> BDD-cost:  243
c ---[ 350]---> BDD-cost:  241
c ---[ 348]---> BDD-cost:  243
c ---[ 346]---> BDD-cost:  211
c ---[ 344]---> BDD-cost:  211
c ---[ 342]---> BDD-cost:  247
c ---[ 340]---> BDD-cost:  253
c ---[ 338]---> BDD-cost:  253
c ---[ 335]---> BDD-cost:  215
c ---[ 333]---> BDD-cost:  203
c ---[ 331]---> BDD-cost:  253
c ---[ 330]---> BDD-cost:  253
c ---[ 328]---> BDD-cost:  167
c ---[ 326]---> BDD-cost:  247
c ---[ 324]---> BDD-cost:  187
c ---[ 322]---> BDD-cost:  257
c ---[ 320]---> BDD-cost:  263
c ---[ 318]---> BDD-cost:  247
c ---[ 314]---> BDD-cost:  265
c ---[ 312]---> BDD-cost:  271
c ---[ 310]---> BDD-cost:  265
c ---[ 308]---> BDD-cost:  271
c ---[ 306]---> BDD-cost:  273
c ---[ 304]---> BDD-cost:  275
c ---[ 302]---> BDD-cost:  269
c ---[ 300]---> BDD-cost:  279
c ---[ 298]---> BDD-cost:  239
c ---[ 296]---> BDD-cost:  281
c ---[ 294]---> BDD-cost:  279
c ---[ 290]---> BDD-cost:  283
c ---[ 288]---> BDD-cost:  257
c ---[ 286]---> BDD-cost:  281
c ---[ 284]---> BDD-cost:  287
c ---[ 282]---> BDD-cost:  199
c ---[ 280]---> BDD-cost:  287
c ---[ 278]---> BDD-cost:  291
c ---[ 276]---> BDD-cost:  293
c ---[ 274]---> BDD-cost:  293
c ---[ 272]---> BDD-cost:  287
c ---[ 270]---> BDD-cost:  267
c ---[ 268]---> BDD-cost:  293
c ---[ 266]---> BDD-cost:  297
c ---[ 264]---> BDD-cost:  251
c ---[ 262]---> BDD-cost:  271
c ---[ 260]---> BDD-cost:  301
c ---[ 258]---> BDD-cost:  147
c ---[ 256]---> BDD-cost:  269
c ---[ 254]---> BDD-cost:  307
c ---[ 252]---> BDD-cost:  305
c ---[ 250]---> BDD-cost:  309
c ---[ 248]---> BDD-cost:  309
c ---[ 246]---> BDD-cost:  289
c ---[ 244]---> BDD-cost:  283
c ---[ 242]---> BDD-cost:  307
c ---[ 240]---> BDD-cost:  287
c ---[ 238]---> BDD-cost:  315
c ---[ 236]---> BDD-cost:  245
c ---[ 234]---> BDD-cost:  247
c ---[ 232]---> BDD-cost:  317
c ---[ 230]---> BDD-cost:  315
c ---[ 226]---> BDD-cost:  321
c ---[ 224]---> BDD-cost:  277
c ---[ 222]---> BDD-cost:  301
c ---[ 220]---> BDD-cost:  245
c ---[ 218]---> BDD-cost:  323
c ---[ 216]---> BDD-cost:  263
c ---[ 214]---> BDD-cost:  329
c ---[ 212]---> BDD-cost:  313
c ---[ 210]---> BDD-cost:  331
c ---[ 208]---> BDD-cost:  329
c ---[ 206]---> BDD-cost:  337
c ---[ 204]---> BDD-cost:  243
c ---[ 202]---> BDD-cost:  295
c ---[ 200]---> BDD-cost:  339
c ---[ 198]---> BDD-cost:  339
c ---[ 196]---> BDD-cost:  339
c ---[ 194]---> BDD-cost:  341
c ---[ 192]---> BDD-cost:  341
c ---[ 190]---> BDD-cost:  343
c ---[ 188]---> BDD-cost:  225
c ---[ 186]---> BDD-cost:  323
c ---[ 184]---> BDD-cost:  351
c ---[ 182]---> BDD-cost:  351
c ---[ 180]---> BDD-cost:  357
c ---[ 178]---> BDD-cost:  307
c ---[ 176]---> BDD-cost:  361
c ---[ 174]---> BDD-cost:  339
c ---[ 172]---> BDD-cost:  297
c ---[ 170]---> BDD-cost:  363
c ---[ 168]---> BDD-cost:  369
c ---[ 166]---> BDD-cost:  357
c ---[ 164]---> BDD-cost:  371
c ---[ 162]---> BDD-cost:  373
c ---[ 160]---> BDD-cost:  375
c ---[ 158]---> BDD-cost:  355
c ---[ 156]---> BDD-cost:  377
c ---[ 154]---> BDD-cost:  339
c ---[ 152]---> BDD-cost:  381
c ---[ 150]---> BDD-cost:  253
c ---[ 148]---> BDD-cost:  387
c ---[ 146]---> BDD-cost:  395
c ---[ 144]---> BDD-cost:  331
c ---[ 142]---> BDD-cost:  405
c ---[ 140]---> BDD-cost:  411
c ---[ 138]---> BDD-cost:  415
c ---[ 136]---> BDD-cost:  409
c ---[ 134]---> BDD-cost:  397
c ---[ 132]---> BDD-cost:  421
c ---[ 130]---> BDD-cost:  413
c ---[ 128]---> BDD-cost:  427
c ---[ 126]---> BDD-cost:  431
c ---[ 124]---> BDD-cost:  405
c ---[ 122]---> BDD-cost:  433
c ---[ 120]---> BDD-cost:  437
c ---[ 118]---> BDD-cost:  403
c ---[ 116]---> BDD-cost:  439
c ---[ 114]---> BDD-cost:  437
c ---[ 112]---> BDD-cost:  329
c ---[ 110]---> BDD-cost:  417
c ---[ 108]---> BDD-cost:  447
c ---[ 106]---> BDD-cost:  455
c ---[ 104]---> BDD-cost:  455
c ---[ 102]---> BDD-cost:  431
c ---[ 100]---> BDD-cost:  455
c ---[  98]---> BDD-cost:  443
c ---[  96]---> BDD-cost:  463
c ---[  94]---> BDD-cost:  453
c ---[  92]---> BDD-cost:  465
c ---[  90]---> BDD-cost:  475
c ---[  88]---> BDD-cost:  479
c ---[  86]---> BDD-cost:  423
c ---[  84]---> BDD-cost:  471
c ---[  82]---> BDD-cost:  501
c ---[  80]---> BDD-cost:  501
c ---[  78]---> BDD-cost:  509
c ---[  76]---> BDD-cost:  517
c ---[  74]---> BDD-cost:  521
c ---[  72]---> BDD-cost:  523
c ---[  70]---> BDD-cost:  523
c ---[  68]---> BDD-cost:  499
c ---[  67]---> BDD-cost:  531
c ---[  65]---> BDD-cost:  533
c ---[  62]---> BDD-cost:  535
c ---[  60]---> BDD-cost:  541
c ---[  58]---> BDD-cost:  543
c ---[  56]---> BDD-cost:  545
c ---[  54]---> BDD-cost:  545
c ---[  52]---> BDD-cost:  495
c ---[  50]---> BDD-cost:  549
c ---[  48]---> BDD-cost:  563
c ---[  46]---> BDD-cost:  565
c ---[  44]---> BDD-cost:  565
c ---[  42]---> BDD-cost:  563
c ---[  40]---> BDD-cost:  331
c ---[  38]---> BDD-cost:  577
c ---[  36]---> BDD-cost:  557
c ---[  34]---> BDD-cost:  581
c ---[  32]---> BDD-cost:  601
c ---[  30]---> BDD-cost:  591
c ---[  28]---> BDD-cost:  641
c ---[  24]---> BDD-cost:  643
c ---[  22]---> BDD-cost:  635
c ---[  20]---> BDD-cost:  663
c ---[  18]---> BDD-cost:  665
c ---[  16]---> BDD-cost:  685
c ---[  14]---> BDD-cost:  679
c ---[  12]---> BDD-cost:  495
c ---[  10]---> BDD-cost:  693
c ---[   8]---> BDD-cost:  731
c ---[   6]---> BDD-cost:  519
c ---[   4]---> BDD-cost:  745
c ---[   2]---> BDD-cost:  743
c ---[   0]---> BDD-cost:  799
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  234650   611110 |   78216       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 21182[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 59722   maxlim: 3887266   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        16 |  652590  2103768 |  217530      16      273    17.1 |  0.000 % |
c |       116 |  652590  2103768 |  239283     116     7501    64.7 |  0.262 % |
c |       266 |  652590  2103768 |  263211     266    16467    61.9 |  0.262 % |
c |       491 |  652590  2103768 |  289532     491    28747    58.5 |  0.262 % |
c |       829 |  652590  2103768 |  318485     829   119948   144.7 |  0.262 % |
c |      1335 |  651460  2099794 |  350334    1174   121251   103.3 |  0.382 % |
c |      2094 |  651435  2099713 |  385367    1930   256035   132.7 |  0.385 % |
c |      3233 |  651435  2099713 |  423904    3069   448872   146.3 |  0.385 % |
c |      4941 |  651303  2099249 |  466294    4756   663123   139.4 |  0.399 % |
c |      7505 |  651251  2099073 |  512924    7313  1247698   170.6 |  0.405 % |
c |     11349 |  651190  2098860 |  564216   11150  2086392   187.1 |  0.412 % |
c |     17117 |  651190  2098860 |  620638   16918  4990941   295.0 |  0.412 % |
c ==============================================================================
c [1mFound solution: 18251[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3890197   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18762 |  651203  2098941 |  217067   18563  5164095   278.2 |  0.412 % |
c |     18862 |  651203  2098941 |  238773   18663  5190403   278.1 |  0.415 % |
c |     19012 |  651203  2098941 |  262651   18813  5194854   276.1 |  0.415 % |
c |     19237 |  651203  2098941 |  288916   19038  5244426   275.5 |  0.415 % |
c |     19574 |  651203  2098941 |  317807   19375  5266740   271.8 |  0.415 % |
c |     20080 |  651203  2098941 |  349588   19881  5379214   270.6 |  0.415 % |
c |     20841 |  651192  2098898 |  384547   20641  5428639   263.0 |  0.417 % |
c |     21980 |  651192  2098898 |  423002   21780  5789731   265.8 |  0.417 % |
c |     23691 |  651192  2098898 |  465302   23491  6106489   260.0 |  0.417 % |
c |     26253 |  651192  2098898 |  511832   26053  6379992   244.9 |  0.417 % |
c |     30097 |  651171  2098829 |  563015   29891  7197939   240.8 |  0.418 % |
c |     35863 |  651155  2098777 |  619317   35655  9279954   260.3 |  0.420 % |
c |     44512 |  651069  2098483 |  681249   44293 13701527   309.3 |  0.430 % |
c |     57488 |  651053  2098431 |  749374   57266 20593650   359.6 |  0.432 % |
c ==============================================================================
c [1mFound solution: 17920[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3890528   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64468 |  651040  2098431 |  217013   64243 22663207   352.8 |  0.432 % |
c |     64568 |  650991  2098268 |  238714   64334 22664654   352.3 |  0.443 % |
c |     64718 |  650991  2098268 |  262585   64484 22675962   351.7 |  0.443 % |
c |     64943 |  650991  2098268 |  288844   64709 22687476   350.6 |  0.443 % |
c |     65280 |  650991  2098268 |  317728   65046 22720498   349.3 |  0.443 % |
c |     65786 |  650991  2098268 |  349501   65552 22743978   347.0 |  0.443 % |
c |     66545 |  650991  2098268 |  384451   66311 22947342   346.1 |  0.443 % |
c |     67684 |  650980  2098225 |  422896   67449 22988819   340.8 |  0.444 % |
c |     69392 |  650971  2098196 |  465186   69156 23247535   336.2 |  0.446 % |
c |     71955 |  650971  2098196 |  511705   71719 24329804   339.2 |  0.446 % |
c |     75799 |  650953  2098138 |  562875   75561 25159530   333.0 |  0.448 % |
c |     81567 |  650953  2098138 |  619163   81329 25866658   318.0 |  0.448 % |
c |     90217 |  650921  2098034 |  681079   89975 28835474   320.5 |  0.452 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 x50 -x51 -x52 -x53 -x54 -x55 -x56 x57 x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 x703 -x704 -x705 -x706 -x707 -x708 -x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 -x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 x1132 -x1133 x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 -x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 -x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 -x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 -x2150 -x2151 x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 -x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 -x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 -x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 -x2260 -x2261 -x2262 -x2263 -x2264 -x2265 -x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 -x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 -x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 -x2374 -x2375 -x2376 -x2377 x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 -x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 -x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 -x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 -x2609 -x2610 -x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 -x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 -x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 -x2663 -x2664 -x2665 -x2666 -x2667 -x2668 -x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 -x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 -x2701 -x2702 -x2703 -x2704 -x2705 -x2706 -x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 -x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 -x2759 -x2760 -x2761 -x2762 -x2763 -x2764 -x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 -x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 -x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 -x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 -x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 -x2915 -x2916 -x2917 -x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 -x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 -x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 -x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 -x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 -x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 -x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 -x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 -x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 -x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 -x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 -x3406 -x3407 -x3408 -x3409 -x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 -x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 -x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 -x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 -x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 -x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 -x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 -x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 -x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 -x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 -x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 -x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 -x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x4273 -x4274 -x4275 -x4276 -x4277 -x4278 -x4279 -x4280 -x4281 -x4282 -x4283 -x4284 -x4285 -x4286 -x4287 -x4288 -x4289 -x4290 -x4291 -x4292 -x4293 -x4294 -x4295 -x4296 -x4297 -x4298 -x4299 -x4300 -x4301 -x4302 -x4303 -x4304 -x4305 -x4306 -x4307 -x4308 -x4309 -x4310 -x4311 -x4312 -x4313 -x4314 -x4315 -x4316 -x4317 -x4318 -x4319 -x4320 -x4321 -x4322 -x4323 -x4324 -x4325 -x4326 -x4327 -x4328 x4329 -x4330 -x4331 -x4332 -x4333 -x4334 -x4335 -x4336 -x4337 -x4338 -x4339 -x4340 -x4341 -x4342 -x4343 -x4344 -x4345 -x4346 -x4347 -x4348 -x4349 -x4350 -x4351 -x4352 -x4353 -x4354 -x4355 -x4356 -x4357 -x4358 -x4359 -x4360 -x4361 -x4362 -x4363 -x4364 -x4365 -x4366 -x4367 -x4368 -x4369 -x4370 -x4371 -x4372 -x4373 -x4374 -x4375 -x4376 -x4377 -x4378 -x4379 -x4380 -x4381 -x4382 -x4383 -x4384 -x4385 -x4386 -x4387 -x4388 -x4389 -x4390 -x4391 -x4392 -x4393 -x4394 -x4395 -x4396 -x4397 -x4398 -x4399 -x4400 -x4401 -x4402 -x4403 -x4404 -x4405 -x4406 -x4407 -x4408 -x4409 -x4410 -x4411 -x4412 -x4413 -x4414 -x4415 -x4416 -x4417 -x4418 -x4419 -x4420 -x4421 -x4422 -x4423 -x4424 -x4425 -x4426 -x4427 -x4428 -x4429 -x4430 -x4431 -x4432 -x4433 -x4434 -x4435 -x4436 -x4437 -x4438 -x4439 -x4440 -x4441 -x4442 -x4443 -x4444 -x4445 -x4446 -x4447 -x4448 -x4449 -x4450 -x4451 -x4452 -x4453 -x4454 -x4455 -x4456 -x4457 -x4458 -x4459 -x4460 -x4461 -x4462 -x4463 -x4464 -x4465 -x4466 -x4467 -x4468 -x4469 -x4470 -x4471 -x4472 -x4473 -x4474 -x4475 -x4476 -x4477 -x4478 -x4479 -x4480 -x4481 -x4482 -x4483 -x4484 -x4485 -x4486 -x4487 -x4488 -x4489 -x4490 -x4491 -x4492 -x4493 -x4494 -x4495 -x4496 -x4497 -x4498 -x4499 -x4500 -x4501 -x4502 -x4503 -x4504 -x4505 -x4506 -x4507 -x4508 -x4509 -x4510 -x4511 -x4512 -x4513 -x4514 -x4515 -x4516 -x4517 -x4518 -x4519 -x4520 -x4521 -x4522 -x4523 -x4524 -x4525 -x4526 -x4527 -x4528 -x4529 -x4530 -x4531 -x4532 -x4533 -x4534 -x4535 -x4536 -x4537 -x4538 -x4539 -x4540 -x4541 -x4542 -x4543 -x4544 -x4545 -x4546 -x4547 -x4548 -x4549 -x4550 -x4551 -x4552 -x4553 -x4554 -x4555 -x4556 x4557 -x4558 -x4559 -x4560 -x4561 -x4562 -x4563 -x4564 -x4565 -x4566 -x4567 -x4568 -x4569 -x4570 -x4571 -x4572 -x4573 -x4574 -x4575 -x4576 -x4577 -x4578 -x4579 -x4580 -x4581 -x4582 -x4583 -x4584 -x4585 -x4586 -x4587 -x4588 -x4589 -x4590 -x4591 -x4592 -x4593 -x4594 -x4595 -x4596 -x4597 -x4598 -x4599 -x4600 -x4601 -x4602 -x4603 -x4604 -x4605 -x4606 -x4607 -x4608 -x4609 -x4610 -x4611 -x4612 -x4613 -x4614 -x4615 -x4616 -x4617 -x4618 -x4619 -x4620 -x4621 -x4622 -x4623 -x4624 -x4625 -x4626 -x4627 -x4628 -x4629 -x4630 -x4631 -x4632 -x4633 -x4634 -x4635 -x4636 -x4637 -x4638 -x4639 -x4640 -x4641 -x4642 -x4643 -x4644 -x4645 -x4646 -x4647 -x4648 -x4649 -x4650 -x4651 -x4652 -x4653 -x4654 -x4655 -x4656 -x4657 -x4658 -x4659 -x4660 -x4661 -x4662 -x4663 -x4664 -x4665 -x4666 -x4667 -x4668 -x4669 -x4670 -x4671 -x4672 -x4673 -x4674 -x4675 -x4676 -x4677 -x4678 -x4679 -x4680 -x4681 -x4682 -x4683 -x4684 -x4685 -x4686 -x4687 -x4688 -x4689 -x4690 -x4691 -x4692 -x4693 -x4694 -x4695 -x4696 -x4697 -x4698 -x4699 -x4700 -x4701 -x4702 -x4703 -x4704 -x4705 -x4706 -x4707 -x4708 -x4709 -x4710 -x4711 -x4712 -x4713 -x4714 -x4715 -x4716 -x4717 -x4718 -x4719 -x4720 -x4721 -x4722 -x4723 -x4724 -x4725 -x4726 -x4727 -x4728 -x4729 -x4730 -x4731 -x4732 -x4733 -x4734 -x4735 -x4736 -x4737 -x4738 -x4739 -x4740 -x4741 -x4742 -x4743 -x4744 -x4745 -x4746 -x4747 -x4748 -x4749 -x4750 -x4751 -x4752 -x4753 -x4754 -x4755 -x4756 -x4757 -x4758 -x4759 -x4760 -x4761 -x4762 -x4763 -x4764 -x4765 -x4766 -x4767 -x4768 -x4769 -x4770 -x4771 -x4772 -x4773 -x4774 -x4775 -x4776 -x4777 -x4778 -x4779 -x4780 -x4781 -x4782 -x4783 -x4784 -x4785 -x4786 -x4787 -x4788 -x4789 -x4790 -x4791 -x4792 -x4793 -x4794 -x4795 -x4796 -x4797 -x4798 -x4799 -x4800 -x4801 -x4802 -x4803 -x4804 -x4805 -x4806 -x4807 -x4808 -x4809 -x4810 -x4811 -x4812 -x4813 -x4814 -x4815 -x4816 -x4817 -x4818 -x4819 -x4820 -x4821 -x4822 -x4823 -x4824 -x4825 -x4826 -x4827 -x4828 -x4829 -x4830 -x4831 -x4832 -x4833 -x4834 -x4835 -x4836 -x4837 -x4838 -x4839 -x4840 -x4841 -x4842 -x4843 -x4844 -x4845 -x4846 -x4847 -x4848 -x4849 -x4850 -x4851 -x4852 -x4853 -x4854 -x4855 -x4856 -x4857 -x4858 -x4859 -x4860 -x4861 -x4862 -x4863 -x4864 -x4865 -x4866 -x4867 -x4868 -x4869 -x4870 -x4871 -x4872 -x4873 -x4874 -x4875 -x4876 -x4877 -x4878 -x4879 -x4880 -x4881 -x4882 -x4883 -x4884 -x4885 -x4886 -x4887 -x4888 -x4889 -x4890 -x4891 -x4892 -x4893 -x4894 -x4895 -x4896 -x4897 -x4898 -x4899 -x4900 -x4901 -x4902 -x4903 -x4904 -x4905 -x4906 -x4907 -x4908 -x4909 -x4910 -x4911 -x4912 -x4913 -x4914 -x4915 -x4916 -x4917 -x4918 -x4919 -x4920 -x4921 -x4922 -x4923 -x4924 -x4925 -x4926 -x4927 -x4928 -x4929 -x4930 -x4931 -x4932 -x4933 -x4934 -x4935 -x4936 -x4937 -x4938 -x4939 -x4940 -x4941 -x4942 -x4943 -x4944 -x4945 -x4946 -x4947 -x4948 -x4949 -x4950 -x4951 -x4952 -x4953 -x4954 -x4955 -x4956 -x4957 -x4958 -x4959 -x4960 -x4961 -x4962 -x4963 -x4964 -x4965 -x4966 -x4967 -x4968 -x4969 -x4970 -x4971 -x4972 -x4973 -x4974 -x4975 -x4976 -x4977 -x4978 -x4979 -x4980 -x4981 -x4982 -x4983 -x4984 -x4985 -x4986 -x4987 -x4988 -x4989 -x4990 -x4991 -x4992 -x4993 -x4994 -x4995 -x4996 -x4997 -x4998 -x4999 -x5000 -x5001 -x5002 -x5003 -x5004 -x5005 -x5006 -x5007 -x5008 -x5009 -x5010 -x5011 -x5012 -x5013 -x5014 -x5015 -x5016 -x5017 -x5018 -x5019 -x5020 -x5021 -x5022 -x5023 -x5024 -x5025 -x5026 -x5027 -x5028 -x5029 -x5030 -x5031 -x5032 -x5033 -x5034 -x5035 -x5036 -x5037 -x5038 -x5039 -x5040 -x5041 -x5042 -x5043 -x5044 -x5045 -x5046 -x5047 -x5048 -x5049 -x5050 -x5051 -x5052 -x5053 -x5054 -x5055 -x5056 -x5057 -x5058 -x5059 -x5060 -x5061 -x5062 -x5063 -x5064 -x5065 -x5066 -x5067 -x5068 -x5069 -x5070 -x5071 -x5072 -x5073 -x5074 -x5075 -x5076 -x5077 -x5078 -x5079 -x5080 -x5081 -x5082 -x5083 -x5084 -x5085 -x5086 -x5087 -x5088 -x5089 -x5090 -x5091 -x5092 -x5093 -x5094 -x5095 -x5096 -x5097 -x5098 -x5099 -x5100 -x5101 -x5102 -x5103 -x5104 -x5105 -x5106 -x5107 -x5108 -x5109 -x5110 -x5111 -x5112 -x5113 -x5114 -x5115 -x5116 -x5117 -x5118 -x5119 -x5120 -x5121 -x5122 -x5123 -x5124 -x5125 -x5126 -x5127 -x5128 -x5129 -x5130 -x5131 -x5132 -x5133 -x5134 -x5135 -x5136 -x5137 -x5138 -x5139 -x5140 -x5141 -x5142 -x5143 -x5144 -x5145 -x5146 -x5147 -x5148 -x5149 -x5150 -x5151 -x5152 -x5153 -x5154 -x5155 -x5156 -x5157 -x5158 -x5159 -x5160 -x5161 -x5162 -x5163 -x5164 -x5165 -x5166 -x5167 -x5168 -x5169 -x5170 -x5171 -x5172 -x5173 -x5174 -x5175 -x5176 -x5177 -x5178 -x5179 -x5180 -x5181 -x5182 -x5183 -x5184 -x5185 -x5186 -x5187 -x5188 -x5189 -x5190 -x5191 -x5192 -x5193 -x5194 -x5195 -x5196 -x5197 -x5198 -x5199 -x5200 -x5201 -x5202 -x5203 -x5204 -x5205 -x5206 -x5207 -x5208 -x5209 -x5210 -x5211 -x5212 -x5213 -x5214 -x5215 -x5216 -x5217 -x5218 -x5219 -x5220 -x5221 -x5222 -x5223 -x5224 -x5225 -x5226 -x5227 -x5228 -x5229 -x5230 -x5231 -x5232 -x5233 -x5234 -x5235 -x5236 -x5237 -x5238 -x5239 -x5240 -x5241 -x5242 -x5243 -x5244 -x5245 -x5246 -x5247 -x5248 -x5249 -x5250 -x5251 -x5252 -x5253 -x5254 -x5255 -x5256 -x5257 -x5258 -x5259 -x5260 -x5261 -x5262 -x5263 -x5264 -x5265 -x5266 -x5267 -x5268 -x5269 -x5270 -x5271 -x5272 -x5273 -x5274 -x5275 -x5276 -x5277 -x5278 -x5279 -x5280 -x5281 -x5282 -x5283 -x5284 -x5285 -x5286 -x5287 -x5288 -x5289 -x5290 -x5291 -x5292 -x5293 -x5294 -x5295 -x5296 -x5297 -x5298 -x5299 -x5300 -x5301 -x5302 -x5303 -x5304 -x5305 -x5306 -x5307 -x5308 -x5309 -x5310 -x5311 -x5312 -x5313 -x5314 -x5315 -x5316 -x5317 -x5318 -x5319 -x5320 -x5321 -x5322 -x5323 -x5324 -x5325 -x5326 -x5327 -x5328 -x5329 -x5330 -x5331 -x5332 -x5333 -x5334 -x5335 -x5336 -x5337 -x5338 -x5339 -x5340 -x5341 -x5342 -x5343 -x5344 -x5345 -x5346 -x5347 -x5348 -x5349 -x5350 -x5351 -x5352 -x5353 -x5354 -x5355 -x5356 -x5357 -x5358 -x5359 -x5360 -x5361 -x5362 -x5363 -x5364 -x5365 -x5366 -x5367 -x5368 -x5369 -x5370 -x5371 -x5372 -x5373 -x5374 -x5375 -x5376 -x5377 -x5378 -x5379 -x5380 -x5381 -x5382 -x5383 -x5384 -x5385 -x5386 -x5387 -x5388 -x5389 -x5390 -x5391 -x5392 -x5393 -x5394 -x5395 -x5396 -x5397 -x5398 -x5399 -x5400 -x5401 -x5402 -x5403 -x5404 -x5405 -x5406 -x5407 -x5408 -x5409 -x5410 -x5411 -x5412 -x5413 -x5414 -x5415 -x5416 -x5417 -x5418 -x5419 -x5420 -x5421 -x5422 -x5423 -x5424 -x5425 -x5426 -x5427 -x5428 -x5429 -x5430 -x5431 -x5432 -x5433 -x5434 -x5435 -x5436 -x5437 -x5438 -x5439 -x5440 -x5441 -x5442 -x5443 -x5444 -x5445 -x5446 -x5447 -x5448 -x5449 -x5450 -x5451 -x5452 -x5453 -x5454 -x5455 -x5456 -x5457 -x5458 -x5459 -x5460 -x5461 -x5462 -x5463 -x5464 -x5465 -x5466 -x5467 -x5468 -x5469 -x5470 -x5471 -x5472 -x5473 -x5474 -x5475 -x5476 -x5477 -x5478 -x5479 -x5480 -x5481 -x5482 -x5483 -x5484 -x5485 -x5486 -x5487 -x5488 -x5489 -x5490 -x5491 -x5492 -x5493 -x5494 -x5495 -x5496 -x5497 -x5498 -x5499 -x5500 -x5501 -x5502 -x5503 -x5504 -x5505 -x5506 -x5507 -x5508 -x5509 -x5510 -x5511 -x5512 -x5513 -x5514 -x5515 -x5516 -x5517 -x5518 -x5519 -x5520 -x5521 -x5522 -x5523 -x5524 -x5525 -x5526 -x5527 -x5528 -x5529 -x5530 -x5531 -x5532 -x5533 -x5534 -x5535 -x5536 -x5537 -x5538 -x5539 -x5540 -x5541 -x5542 -x5543 -x5544 -x5545 -x5546 -x5547 -x5548 -x5549 -x5550 -x5551 -x5552 -x5553 -x5554 -x5555 -x5556 -x5557 -x5558 -x5559 -x5560 -x5561 -x5562 -x5563 -x5564 -x5565 -x5566 -x5567 -x5568 -x5569 -x5570 -x5571 -x5572 -x5573 -x5574 -x5575 -x5576 -x5577 -x5578 -x5579 -x5580 -x5581 -x5582 -x5583 -x5584 -x5585 -x5586 -x5587 -x5588 -x5589 -x5590 -x5591 -x5592 -x5593 -x5594 -x5595 -x5596 -x5597 -x5598 -x5599 -x5600 -x5601 -x5602 -x5603 -x5604 -x5605 -x5606 -x5607 -x5608 -x5609 -x5610 -x5611 -x5612 -x5613 -x5614 -x5615 -x5616 -x5617 -x5618 -x5619 -x5620 -x5621 -x5622 -x5623 -x5624 -x5625 -x5626 -x5627 -x5628 -x5629 -x5630 -x5631 -x5632 -x5633 -x5634 -x5635 -x5636 -x5637 -x5638 -x5639 -x5640 -x5641 -x5642 -x5643 -x5644 -x5645 -x5646 -x5647 -x5648 -x5649 -x5650 -x5651 -x5652 -x5653 -x5654 -x5655 -x5656 -x5657 -x5658 -x5659 -x5660 -x5661 -x5662 -x5663 -x5664 -x5665 -x5666 -x5667 -x5668 -x5669 -x5670 -x5671 -x5672 -x5673 -x5674 -x5675 -x5676 -x5677 -x5678 -x5679 -x5680 -x5681 -x5682 -x5683 -x5684 -x5685 -x5686 -x5687 -x5688 -x5689 -x5690 -x5691 -x5692 -x5693 -x5694 -x5695 -x5696 -x5697 -x5698 -x5699 -x5700 -x5701 -x5702 -x5703 -x5704 -x5705 -x5706 -x5707 -x5708 -x5709 -x5710 -x5711 -x5712 -x5713 -x5714 -x5715 -x5716 -x5717 -x5718 -x5719 -x5720 -x5721 -x5722 -x5723 -x5724 -x5725 -x5726 -x5727 -x5728 -x5729 -x5730 -x5731 -x5732 -x5733 -x5734 -x5735 -x5736 -x5737 -x5738 -x5739 -x5740 -x5741 -x5742 -x5743 -x5744 -x5745 -x5746 -x5747 -x5748 -x5749 -x5750 -x5751 -x5752 -x5753 -x5754 -x5755 -x5756 -x5757 x5758 -x5759 -x5760 -x5761 -x5762 -x5763 -x5764 -x5765 -x5766 -x5767 -x5768 -x5769 -x5770 -x5771 -x5772 -x5773 -x5774 -x5775 -x5776 -x5777 -x5778 -x5779 -x5780 -x5781 -x5782 -x5783 -x5784 -x5785 -x5786 -x5787 -x5788 -x5789 -x5790 -x5791 -x5792 -x5793 -x5794 -x5795 -x5796 -x5797 -x5798 -x5799 -x5800 -x5801 -x5802 -x5803 -x5804 -x5805 -x5806 -x5807 -x5808 -x5809 -x5810 -x5811 -x5812 -x5813 -x5814 -x5815 -x5816 -x5817 -x5818 -x5819 -x5820 -x5821 -x5822 -x5823 -x5824 -x5825 -x5826 -x5827 -x5828 -x5829 -x5830 -x5831 -x5832 -x5833 -x5834 -x5835 -x5836 -x5837 -x5838 -x5839 -x5840 -x5841 -x5842 -x5843 -x5844 -x5845 -x5846 -x5847 -x5848 -x5849 -x5850 -x5851 -x5852 -x5853 -x5854 -x5855 -x5856 -x5857 -x5858 -x5859 -x5860 -x5861 -x5862 -x5863 -x5864 -x5865 -x5866 -x5867 -x5868 -x5869 -x5870 -x5871 -x5872 -x5873 -x5874 -x5875 -x5876 -x5877 -x5878 -x5879 -x5880 -x5881 -x5882 -x5883 -x5884 -x5885 -x5886 -x5887 -x5888 -x5889 -x5890 -x5891 -x5892 -x5893 -x5894 -x5895 -x5896 -x5897 -x5898 -x5899 -x5900 -x5901 -x5902 -x5903 -x5904 -x5905 -x5906 -x5907 -x5908 -x5909 -x5910 -x5911 -x5912 -x5913 -x5914 -x5915 -x5916 -x5917 -x5918 -x5919 -x5920 -x5921 -x5922 -x5923 -x5924 -x5925 -x5926 -x5927 -x5928 -x5929 -x5930 -x5931 -x5932 -x5933 -x5934 -x5935 -x5936 -x5937 -x5938 -x5939 -x5940 -x5941 -x5942 -x5943 -x5944 -x5945 -x5946 -x5947 -x5948 -x5949 -x5950 -x5951 -x5952 -x5953 -x5954 -x5955 -x5956 -x5957 -x5958 -x5959 -x5960 -x5961 -x5962 -x5963 -x5964 -x5965 -x5966 -x5967 -x5968 -x5969 -x5970 -x5971 -x5972 -x5973 -x5974 -x5975 -x5976 -x5977 -x5978 -x5979 -x5980 -x5981 -x5982 -x5983 -x5984 -x5985 -x5986 x5987 -x5988 -x5989 -x5990 -x5991 -x5992 -x5993 -x5994 -x5995 -x5996 -x5997 -x5998 -x5999 -x6000 -x6001 -x6002 -x6003 -x6004 -x6005 -x6006 -x6007 -x6008 -x6009 -x6010 -x6011 -x6012 -x6013 -x6014 -x6015 -x6016 -x6017 -x6018 -x6019 -x6020 -x6021 -x6022 -x6023 -x6024 -x6025 -x6026 -x6027 -x6028 -x6029 -x6030 -x6031 -x6032 -x6033 -x6034 -x6035 -x6036 -x6037 -x6038 -x6039 -x6040 -x6041 -x6042 -x6043 -x6044 -x6045 -x6046 -x6047 -x6048 -x6049 -x6050 -x6051 -x6052 -x6053 -x6054 -x6055 -x6056 -x6057 -x6058 -x6059 -x6060 -x6061 -x6062 -x6063 -x6064 -x6065 -x6066 -x6067 -x6068 -x6069 -x6070 -x6071 -x6072 -x6073 -x6074 -x6075 -x6076 -x6077 -x6078 -x6079 -x6080 -x6081 -x6082 -x6083 -x6084 -x6085 -x6086 -x6087 -x6088 -x6089 -x6090 -x6091 -x6092 -x6093 -x6094 -x6095 -x6096 -x6097 -x6098 -x6099 -x6100 -x6101 -x6102 -x6103 -x6104 -x6105 -x6106 -x6107 -x6108 x6109 -x6110 -x6111 -x6112 -x6113 -x6114 -x6115 -x6116 -x6117 -x6118 -x6119 -x6120 -x6121 -x6122 -x6123 -x6124 -x6125 -x6126 -x6127 -x6128 -x6129 -x6130 -x6131 -x6132 -x6133 -x6134 -x6135 -x6136 -x6137 -x6138 -x6139 -x6140 -x6141 -x6142 -x6143 -x6144 -x6145 -x6146 -x6147 -x6148 -x6149 -x6150 -x6151 -x6152 -x6153 -x6154 -x6155 -x6156 -x6157 -x6158 -x6159 -x6160 -x6161 -x6162 -x6163 -x6164 -x6165 -x6166 -x6167 -x6168 -x6169 -x6170 -x6171 -x6172 -x6173 -x6174 -x6175 -x6176 -x6177 -x6178 -x6179 -x6180 -x6181 -x6182 -x6183 -x6184 -x6185 -x6186 -x6187 -x6188 -x6189 -x6190 -x6191 -x6192 -x6193 -x6194 -x6195 -x6196 -x6197 -x6198 -x6199 -x6200 -x6201 -x6202 -x6203 -x6204 -x6205 -x6206 -x6207 x6208 -x6209 -x6210 -x6211 -x6212 -x6213 -x6214 -x6215 -x6216 -x6217 -x6218 -x6219 -x6220 -x6221 -x6222 -x6223 -x6224 -x6225 -x6226 -x6227 -x6228 -x6229 -x6230 -x6231 -x6232 -x6233 -x6234 -x6235 -x6236 -x6237 -x6238 -x6239 -x6240 -x6241 -x6242 -x6243 -x6244 -x6245 -x6246 -x6247 -x6248 -x6249 -x6250 -x6251 -x6252 -x6253 -x6254 -x6255 -x6256 -x6257 -x6258 -x6259 -x6260 -x6261 -x6262 -x6263 -x6264 -x6265 -x6266 -x6267 -x6268 -x6269 -x6270 -x6271 -x6272 -x6273 -x6274 -x6275 -x6276 -x6277 -x6278 -x6279 -x6280 -x6281 -x6282 -x6283 -x6284 -x6285 -x6286 -x6287 -x6288 -x6289 -x6290 -x6291 -x6292 -x6293 -x6294 -x6295 -x6296 x6297 -x6298 -x6299 -x6300 -x6301 -x6302 -x6303 -x6304 -x6305 -x6306 -x6307 -x6308 -x6309 -x6310 -x6311 -x6312 -x6313 -x6314 -x6315 -x6316 -x6317 -x6318 -x6319 -x6320 -x6321 -x6322 -x6323 -x6324 -x6325 -x6326 -x6327 -x6328 -x6329 -x6330 -x6331 -x6332 -x6333 -x6334 -x6335 -x6336 -x6337 -x6338 -x6339 -x6340 -x6341 -x6342 -x6343 -x6344 -x6345 -x6346 -x6347 -x6348 -x6349 -x6350 -x6351 -x6352 -x6353 -x6354 -x6355 -x6356 -x6357 -x6358 -x6359 -x6360 -x6361 -x6362 -x6363 -x6364 -x6365 -x6366 -x6367 -x6368 -x6369 -x6370 -x6371 -x6372 -x6373 -x6374 -x6375 -x6376 -x6377 -x6378 -x6379 -x6380 -x6381 -x6382 -x6383 -x6384 -x6385 -x6386 -x6387 -x6388 -x6389 -x6390 -x6391 -x6392 -x6393 -x6394 -x6395 -x6396 -x6397 -x6398 -x6399 -x6400 -x6401 -x6402 -x6403 -x6404 -x6405 -x6406 -x6407 -x6408 -x6409 -x6410 -x6411 -x6412 -x6413 -x6414 -x6415 -x6416 -x6417 -x6418 -x6419 -x6420 -x6421 -x6422 -x6423 -x6424 -x6425 -x6426 -x6427 -x6428 -x6429 -x6430 -x6431 -x6432 -x6433 -x6434 -x6435 -x6436 -x6437 -x6438 -x6439 -x6440 -x6441 -x6442 -x6443 -x6444 -x6445 -x6446 -x6447 -x6448 -x6449 -x6450 -x6451 -x6452 -x6453 -x6454 -x6455 -x6456 -x6457 -x6458 -x6459 -x6460 -x6461 -x6462 -x6463 -x6464 -x6465 -x6466 -x6467 -x6468 -x6469 -x6470 -x6471 -x6472 -x6473 -x6474 -x6475 -x6476 -x6477 -x6478 -x6479 -x6480 -x6481 -x6482 -x6483 -x6484 -x6485 -x6486 -x6487 -x6488 -x6489 -x6490 -x6491 -x6492 -x6493 -x6494 -x6495 -x6496 -x6497 -x6498 -x6499 -x6500 -x6501 -x6502 -x6503 -x6504 -x6505 -x6506 -x6507 -x6508 -x6509 -x6510 -x6511 -x6512 -x6513 -x6514 -x6515 -x6516 -x6517 -x6518 -x6519 -x6520 -x6521 -x6522 -x6523 -x6524 -x6525 -x6526 -x6527 -x6528 -x6529 -x6530 -x6531 -x6532 -x6533 -x6534 -x6535 -x6536 -x6537 -x6538 -x6539 -x6540 -x6541 -x6542 -x6543 -x6544 -x6545 -x6546 -x6547 -x6548 -x6549 -x6550 -x6551 -x6552 -x6553 -x6554 -x6555 -x6556 -x6557 -x6558 -x6559 -x6560 -x6561 -x6562 -x6563 -x6564 -x6565 -x6566 -x6567 -x6568 -x6569 -x6570 -x6571 -x6572 -x6573 -x6574 -x6575 -x6576 -x6577 -x6578 -x6579 -x6580 -x6581 -x6582 -x6583 -x6584 -x6585 -x6586 -x6587 -x6588 -x6589 -x6590 -x6591 -x6592 -x6593 -x6594 -x6595 -x6596 -x6597 -x6598 -x6599 -x6600 -x6601 -x6602 -x6603 -x6604 -x6605 -x6606 -x6607 -x6608 -x6609 -x6610 -x6611 -x6612 -x6613 -x6614 -x6615 -x6616 -x6617 -x6618 -x6619 -x6620 -x6621 -x6622 -x6623 -x6624 -x6625 -x6626 -x6627 -x6628 -x6629 -x6630 -x6631 -x6632 x6633 -x6634 -x6635 -x6636 -x6637 -x6638 -x6639 -x6640 -x6641 -x6642 -x6643 -x6644 -x6645 -x6646 -x6647 -x6648 -x6649 -x6650 -x6651 -x6652 -x6653 -x6654 -x6655 -x6656 -x6657 -x6658 -x6659 -x6660 -x6661 -x6662 -x6663 -x6664 -x6665 -x6666 -x6667 -x6668 -x6669 -x6670 -x6671 -x6672 -x6673 -x6674 -x6675 -x6676 -x6677 -x6678 -x6679 -x6680 -x6681 -x6682 -x6683 -x6684 -x6685 -x6686 -x6687 -x6688 -x6689 -x6690 -x6691 -x6692 -x6693 -x6694 -x6695 -x6696 -x6697 -x6698 x6699 -x6700 -x6701 -x6702 -x6703 -x6704 -x6705 -x6706 -x6707 -x6708 -x6709 -x6710 -x6711 -x6712 -x6713 -x6714 -x6715 -x6716 -x6717 -x6718 -x6719 -x6720 -x6721 -x6722 -x6723 -x6724 -x6725 -x6726 -x6727 -x6728 -x6729 -x6730 -x6731 -x6732 -x6733 -x6734 -x6735 -x6736 -x6737 -x6738 -x6739 -x6740 -x6741 -x6742 -x6743 -x6744 -x6745 -x6746 -x6747 -x6748 -x6749 -x6750 -x6751 -x6752 -x6753 -x6754 -x6755 -x6756 -x6757 -x6758 -x6759 -x6760 -x6761 -x6762 -x6763 -x6764 -x6765 -x6766 -x6767 -x6768 -x6769 -x6770 -x6771 -x6772 -x6773 -x6774 -x6775 -x6776 -x6777 -x6778 -x6779 -x6780 -x6781 -x6782 -x6783 -x6784 -x6785 -x6786 -x6787 x6788 -x6789 -x6790 -x6791 -x6792 -x6793 -x6794 -x6795 -x6796 -x6797 -x6798 -x6799 -x6800 x6801 -x6802 -x6803 -x6804 -x6805 -x6806 -x6807 -x6808 -x6809 -x6810 -x6811 -x6812 -x6813 -x6814 -x6815 -x6816 -x6817 -x6818 -x6819 -x6820 -x6821 -x6822 -x6823 -x6824 -x6825 -x6826 -x6827 -x6828 -x6829 -x6830 -x6831 -x6832 -x6833 -x6834 -x6835 -x6836 -x6837 -x6838 -x6839 x6840 -x6841 -x6842 -x6843 -x6844 -x6845 -x6846 -x6847 -x6848 -x6849 -x6850 -x6851 -x6852 -x6853 -x6854 -x6855 -x6856 -x6857 -x6858 -x6859 -x6860 -x6861 -x6862 -x6863 -x6864 -x6865 -x6866 -x6867 -x6868 -x6869 -x6870 -x6871 -x6872 -x6873 -x6874 -x6875 -x6876 -x6877 -x6878 -x6879 -x6880 -x6881 -x6882 -x6883 -x6884 -x6885 -x6886 -x6887 -x6888 -x6889 -x6890 -x6891 -x6892 -x6893 -x6894 -x6895 -x6896 -x6897 -x6898 -x6899 -x6900 -x6901 -x6902 -x6903 -x6904 -x6905 -x6906 -x6907 -x6908 -x6909 -x6910 -x6911 -x6912 -x6913 -x6914 -x6915 -x6916 -x6917 -x6918 -x6919 -x6920 -x6921 -x6922 -x6923 -x6924 -x6925 -x6926 -x6927 -x6928 -x6929 -x6930 -x6931 -x6932 -x6933 -x6934 -x6935 x6936 -x6937 -x6938 -x6939 -x6940 -x6941 -x6942 -x6943 -x6944 -x6945 -x6946 -x6947 -x6948 -x6949 -x6950 -x6951 -x6952 -x6953 -x6954 -x6955 -x6956 -x6957 -x6958 -x6959 -x6960 -x6961 -x6962 -x6963 -x6964 -x6965 -x6966 -x6967 -x6968 -x6969 -x6970 -x6971 -x6972 -x6973 -x6974 -x6975 -x6976 -x6977 -x6978 -x6979 -x6980 -x6981 -x6982 -x6983 -x6984 -x6985 -x6986 -x6987 -x6988 -x6989 -x6990 -x6991 -x6992 -x6993 -x6994 -x6995 -x6996 -x6997 -x6998 -x6999 -x7000 -x7001 -x7002 -x7003 -x7004 -x7005 -x7006 -x7007 -x7008 -x7009 -x7010 -x7011 -x7012 -x7013 -x7014 -x7015 -x7016 -x7017 -x7018 -x7019 -x7020 -x7021 -x7022 -x7023 -x7024 -x7025 -x7026 -x7027 -x7028 -x7029 -x7030 -x7031 -x7032 -x7033 -x7034 -x7035 -x7036 -x7037 -x7038 -x7039 -x7040 -x7041 -x7042 -x7043 -x7044 -x7045 -x7046 -x7047 -x7048 -x7049 -x7050 -x7051 -x7052 -x7053 x7054 -x7055 -x7056 -x7057 -x7058 -x7059 -x7060 -x7061 -x7062 -x7063 -x7064 -x7065 -x7066 -x7067 -x7068 -x7069 -x7070 -x7071 -x7072 -x7073 -x7074 -x7075 -x7076 -x7077 -x7078 -x7079 -x7080 -x7081 -x7082 -x7083 -x7084 -x7085 -x7086 -x7087 -x7088 -x7089 -x7090 -x7091 -x7092 -x7093 -x7094 -x7095 -x7096 -x7097 -x7098 -x7099 -x7100 -x7101 -x7102 -x7103 -x7104 -x7105 -x7106 -x7107 -x7108 -x7109 -x7110 -x7111 -x7112 -x7113 -x7114 -x7115 -x7116 -x7117 -x7118 -x7119 -x7120 -x7121 -x7122 x7123 -x7124 -x7125 -x7126 -x7127 -x7128 -x7129 -x7130 -x7131 -x7132 -x7133 -x7134 -x7135 -x7136 -x7137 -x7138 -x7139 -x7140 -x7141 -x7142 -x7143 -x7144 -x7145 -x7146 -x7147 -x7148 -x7149 -x7150 -x7151 -x7152 -x7153 -x7154 x7155 -x7156 -x7157 -x7158 -x7159 -x7160 -x7161 -x7162 -x7163 -x7164 -x7165 -x7166 -x7167 -x7168 -x7169 -x7170 x7171 -x7172 -x7173 -x7174 -x7175 -x7176 -x7177 -x7178 -x7179#### 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.00 0.00 0.00 2/54 12351
Raw data (stat): 12351 (runsolver) R 12350 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429230734 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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+9.99953 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 30748 0 0 0 927 70 0 0 25 0 1 0 429230734 113344512 24785 4294967295 134512640 134672761 3221224640 3221221880 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27672 24785 603 41 0 27631 0
vsize: 110688
[startup+20.0009 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 43593 0 0 0 1900 98 0 0 25 0 1 0 429230734 186671104 37615 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45574 37615 603 41 0 45533 0
vsize: 182296
[startup+30.0016 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 43704 0 0 0 2899 98 0 0 25 0 1 0 429230734 187076608 37726 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45673 37726 603 41 0 45632 0
vsize: 182692
[startup+40.0019 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 43706 0 0 0 3898 98 0 0 25 0 1 0 429230734 187076608 37728 4294967295 134512640 134672761 3221224640 3221223812 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45673 37728 603 41 0 45632 0
vsize: 182692
[startup+50.003 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 43848 0 0 0 4898 99 0 0 25 0 1 0 429230734 187756544 37870 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45839 37870 603 41 0 45798 0
vsize: 183356
[startup+60.0028 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44043 0 0 0 5898 99 0 0 25 0 1 0 429230734 188424192 38065 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46002 38065 603 41 0 45961 0
vsize: 184008
[startup+70.0035 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44136 0 0 0 6897 100 0 0 25 0 1 0 429230734 188829696 38158 4294967295 134512640 134672761 3221224640 3221223824 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46101 38158 603 41 0 46060 0
vsize: 184404
[startup+80.0043 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44183 0 0 0 7897 100 0 0 25 0 1 0 429230734 189124608 38205 4294967295 134512640 134672761 3221224640 3221223776 134560606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46173 38205 603 41 0 46132 0
vsize: 184692
[startup+90.0051 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44273 0 0 0 8897 100 0 0 25 0 1 0 429230734 189382656 38295 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46236 38295 603 41 0 46195 0
vsize: 184944
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44468 0 0 0 9897 101 0 0 25 0 1 0 429230734 190197760 38490 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46435 38490 603 41 0 46394 0
vsize: 185740
[startup+110.005 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44806 0 0 0 10897 101 0 0 25 0 1 0 429230734 191557632 38828 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46767 38828 603 41 0 46726 0
vsize: 187068
[startup+120.005 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44902 0 0 0 11897 102 0 0 25 0 1 0 429230734 191967232 38924 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46867 38924 603 41 0 46826 0
vsize: 187468
[startup+130.005 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 44972 0 0 0 12897 102 0 0 25 0 1 0 429230734 192237568 38994 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46933 38994 603 41 0 46892 0
vsize: 187732
[startup+140.006 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 45091 0 0 0 13897 102 0 0 25 0 1 0 429230734 192823296 39113 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47076 39113 603 41 0 47035 0
vsize: 188304
[startup+150.007 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 45348 0 0 0 14896 103 0 0 25 0 1 0 429230734 193773568 39370 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47308 39370 603 41 0 47267 0
vsize: 189232
[startup+160.006 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 45737 0 0 0 15895 104 0 0 25 0 1 0 429230734 195399680 39759 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47705 39759 603 41 0 47664 0
vsize: 190820
[startup+170.006 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 45999 0 0 0 16894 104 0 0 25 0 1 0 429230734 196489216 40021 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47971 40021 603 41 0 47930 0
vsize: 191884
[startup+180.007 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 46436 0 0 0 17893 105 0 0 25 0 1 0 429230734 198275072 40458 4294967295 134512640 134672761 3221224640 3221223744 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48407 40458 603 41 0 48366 0
vsize: 193628
[startup+190.008 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 46903 0 0 0 18893 106 0 0 25 0 1 0 429230734 200220672 40925 4294967295 134512640 134672761 3221224640 3221223744 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48882 40925 603 41 0 48841 0
vsize: 195528
[startup+200.008 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 47341 0 0 0 19892 107 0 0 25 0 1 0 429230734 201961472 41363 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49307 41363 603 41 0 49266 0
vsize: 197228
[startup+210.007 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 47777 0 0 0 20891 108 0 0 25 0 1 0 429230734 203747328 41799 4294967295 134512640 134672761 3221224640 3221223744 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49743 41799 603 41 0 49702 0
vsize: 198972
[startup+220.008 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 48215 0 0 0 21891 109 0 0 25 0 1 0 429230734 205512704 42237 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50174 42237 603 41 0 50133 0
vsize: 200696
[startup+230.008 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 48643 0 0 0 22890 110 0 0 25 0 1 0 429230734 207372288 42665 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50628 42665 603 41 0 50587 0
vsize: 202512
[startup+240.009 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 48700 0 0 0 23890 110 0 0 25 0 1 0 429230734 207642624 42722 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50694 42722 603 41 0 50653 0
vsize: 202776
[startup+250.01 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 48743 0 0 0 24890 110 0 0 25 0 1 0 429230734 207777792 42765 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50727 42765 603 41 0 50686 0
vsize: 202908
[startup+260.009 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 48814 0 0 0 25890 110 0 0 25 0 1 0 429230734 208048128 42836 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50793 42836 603 41 0 50752 0
vsize: 203172
[startup+270.01 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 51500 0 0 0 26884 117 0 0 25 0 1 0 429230734 209702912 43126 4294967295 134512640 134672761 3221224640 3221222608 134544291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51197 43126 603 41 0 51156 0
vsize: 204788
[startup+280.01 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52016 0 0 0 27882 118 0 0 25 0 1 0 429230734 210685952 43627 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51437 43627 603 41 0 51396 0
vsize: 205748
[startup+290.011 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52022 0 0 0 28883 118 0 0 25 0 1 0 429230734 210685952 43633 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51437 43633 603 41 0 51396 0
vsize: 205748
[startup+300.011 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52047 0 0 0 29883 118 0 0 25 0 1 0 429230734 210821120 43658 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51470 43658 603 41 0 51429 0
vsize: 205880
[startup+310.01 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52105 0 0 0 30883 118 0 0 25 0 1 0 429230734 211091456 43716 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51536 43716 603 41 0 51495 0
vsize: 206144
[startup+320.011 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52229 0 0 0 31883 118 0 0 25 0 1 0 429230734 211496960 43840 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51635 43840 603 41 0 51594 0
vsize: 206540
[startup+330.011 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52348 0 0 0 32883 119 0 0 25 0 1 0 429230734 212029440 43959 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51765 43959 603 41 0 51724 0
vsize: 207060
[startup+340.011 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52473 0 0 0 33883 119 0 0 25 0 1 0 429230734 212570112 44084 4294967295 134512640 134672761 3221224640 3221223744 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51897 44084 603 41 0 51856 0
vsize: 207588
[startup+350.011 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 52789 0 0 0 34882 120 0 0 25 0 1 0 429230734 213786624 44400 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52194 44400 603 41 0 52153 0
vsize: 208776
[startup+360.011 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 53088 0 0 0 35881 121 0 0 25 0 1 0 429230734 214990848 44699 4294967295 134512640 134672761 3221224640 3221223812 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52488 44699 603 41 0 52447 0
vsize: 209952
[startup+370.011 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 53436 0 0 0 36881 121 0 0 25 0 1 0 429230734 216469504 45047 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52849 45047 603 41 0 52808 0
vsize: 211396
[startup+380.011 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 53827 0 0 0 37880 122 0 0 25 0 1 0 429230734 218087424 45438 4294967295 134512640 134672761 3221224640 3221223744 134559939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53244 45438 603 41 0 53203 0
vsize: 212976
[startup+390.011 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 54056 0 0 0 38880 122 0 0 25 0 1 0 429230734 219021312 45667 4294967295 134512640 134672761 3221224640 3221223744 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53472 45667 603 41 0 53431 0
vsize: 213888
[startup+400.011 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 54160 0 0 0 39880 123 0 0 25 0 1 0 429230734 219430912 45771 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53572 45771 603 41 0 53531 0
vsize: 214288
[startup+410.011 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 54239 0 0 0 40880 123 0 0 25 0 1 0 429230734 219705344 45850 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53639 45850 603 41 0 53598 0
vsize: 214556
[startup+420.012 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 54391 0 0 0 41880 123 0 0 25 0 1 0 429230734 220381184 46002 4294967295 134512640 134672761 3221224640 3221223744 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53804 46002 603 41 0 53763 0
vsize: 215216
[startup+430.012 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 54799 0 0 0 42879 124 0 0 25 0 1 0 429230734 222130176 46410 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54231 46410 603 41 0 54190 0
vsize: 216924
[startup+440.012 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 55219 0 0 0 43879 125 0 0 25 0 1 0 429230734 223911936 46830 4294967295 134512640 134672761 3221224640 3221223744 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54666 46830 603 41 0 54625 0
vsize: 218664
[startup+450.012 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 55621 0 0 0 44878 126 0 0 25 0 1 0 429230734 225558528 47232 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55068 47232 603 41 0 55027 0
vsize: 220272
[startup+460.012 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56019 0 0 0 45877 127 0 0 25 0 1 0 429230734 227188736 47630 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55466 47630 603 41 0 55425 0
vsize: 221864
[startup+470.012 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56121 0 0 0 46877 127 0 0 25 0 1 0 429230734 227586048 47732 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55563 47732 603 41 0 55522 0
vsize: 222252
[startup+480.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56223 0 0 0 47877 127 0 0 25 0 1 0 429230734 227999744 47834 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55664 47834 603 41 0 55623 0
vsize: 222656
[startup+490.011 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56240 0 0 0 48877 127 0 0 25 0 1 0 429230734 227999744 47851 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55664 47851 603 41 0 55623 0
vsize: 222656
[startup+500.012 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56285 0 0 0 49878 127 0 0 25 0 1 0 429230734 228274176 47896 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55731 47896 603 41 0 55690 0
vsize: 222924
[startup+510.012 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 56653 0 0 0 50877 127 0 0 25 0 1 0 429230734 229752832 48265 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56092 48265 603 41 0 56051 0
vsize: 224368
[startup+520.011 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 57035 0 0 0 51877 128 0 0 25 0 1 0 429230734 231251968 48646 4294967295 134512640 134672761 3221224640 3221223744 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56458 48646 603 41 0 56417 0
vsize: 225832
[startup+530.012 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 57405 0 0 0 52875 130 0 0 25 0 1 0 429230734 232742912 49016 4294967295 134512640 134672761 3221224640 3221223744 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56822 49016 603 41 0 56781 0
vsize: 227288
[startup+540.012 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 57768 0 0 0 53875 130 0 0 25 0 1 0 429230734 234348544 49379 4294967295 134512640 134672761 3221224640 3221223744 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57214 49379 603 41 0 57173 0
vsize: 228856
[startup+550.012 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 58128 0 0 0 54874 131 0 0 25 0 1 0 429230734 235696128 49739 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57543 49739 603 41 0 57502 0
vsize: 230172
[startup+560.012 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 58500 0 0 0 55874 131 0 0 25 0 1 0 429230734 237314048 50111 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57938 50111 603 41 0 57897 0
vsize: 231752
[startup+570.012 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 58864 0 0 0 56873 132 0 0 25 0 1 0 429230734 238821376 50475 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58306 50475 603 41 0 58265 0
vsize: 233224
[startup+580.012 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 59232 0 0 0 57873 133 0 0 25 0 1 0 429230734 240336896 50843 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58676 50843 603 41 0 58635 0
vsize: 234704
[startup+590.012 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 59589 0 0 0 58872 134 0 0 25 0 1 0 429230734 241700864 51200 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59009 51200 603 41 0 58968 0
vsize: 236036
[startup+600.013 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 59956 0 0 0 59872 134 0 0 25 0 1 0 429230734 243224576 51567 4294967295 134512640 134672761 3221224640 3221223744 134559976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59381 51567 603 41 0 59340 0
vsize: 237524
[startup+610.013 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 60330 0 0 0 60871 136 0 0 25 0 1 0 429230734 244695040 51941 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59740 51941 603 41 0 59699 0
vsize: 238960
[startup+620.014 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 60512 0 0 0 61870 136 0 0 25 0 1 0 429230734 245526528 52123 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59943 52123 603 41 0 59902 0
vsize: 239772
[startup+630.013 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 60866 0 0 0 62869 137 0 0 25 0 1 0 429230734 246906880 52477 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60280 52477 603 41 0 60239 0
vsize: 241120
[startup+640.014 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 61265 0 0 0 63868 138 0 0 25 0 1 0 429230734 248524800 52876 4294967295 134512640 134672761 3221224640 3221223744 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60675 52876 603 41 0 60634 0
vsize: 242700
[startup+650.014 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 61685 0 0 0 64867 140 0 0 25 0 1 0 429230734 250257408 53296 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61098 53296 603 41 0 61057 0
vsize: 244392
[startup+660.013 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 62075 0 0 0 65866 141 0 0 25 0 1 0 429230734 251895808 53686 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61498 53686 603 41 0 61457 0
vsize: 245992
[startup+670.015 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 62476 0 0 0 66865 142 0 0 25 0 1 0 429230734 253526016 54087 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61896 54087 603 41 0 61855 0
vsize: 247584
[startup+680.014 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 62866 0 0 0 67864 143 0 0 25 0 1 0 429230734 255135744 54477 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62289 54477 603 41 0 62248 0
vsize: 249156
[startup+690.015 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 63265 0 0 0 68864 143 0 0 25 0 1 0 429230734 256749568 54876 4294967295 134512640 134672761 3221224640 3221223744 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62683 54876 603 41 0 62642 0
vsize: 250732
[startup+700.015 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 63656 0 0 0 69863 144 0 0 25 0 1 0 429230734 258387968 55267 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63083 55267 603 41 0 63042 0
vsize: 252332
[startup+710.015 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 64062 0 0 0 70863 145 0 0 25 0 1 0 429230734 260038656 55673 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63486 55673 603 41 0 63445 0
vsize: 253944
[startup+720.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 64432 0 0 0 71861 146 0 0 25 0 1 0 429230734 261525504 56043 4294967295 134512640 134672761 3221224640 3221223776 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63849 56043 603 41 0 63808 0
vsize: 255396
[startup+730.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 64798 0 0 0 72861 147 0 0 25 0 1 0 429230734 263012352 56409 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64212 56409 603 41 0 64171 0
vsize: 256848
[startup+740.016 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 65185 0 0 0 73860 148 0 0 25 0 1 0 429230734 264646656 56796 4294967295 134512640 134672761 3221224640 3221223744 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64611 56796 603 41 0 64570 0
vsize: 258444
[startup+750.015 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 65552 0 0 0 74860 149 0 0 25 0 1 0 429230734 266162176 57163 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64981 57163 603 41 0 64940 0
vsize: 259924
[startup+760.015 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 65934 0 0 0 75859 149 0 0 25 0 1 0 429230734 267661312 57545 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65347 57545 603 41 0 65306 0
vsize: 261388
[startup+770.015 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 66323 0 0 0 76859 150 0 0 25 0 1 0 429230734 269307904 57934 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65749 57934 603 41 0 65708 0
vsize: 262996
[startup+780.016 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 66731 0 0 0 77858 151 0 0 25 0 1 0 429230734 270974976 58342 4294967295 134512640 134672761 3221224640 3221223744 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66156 58342 603 41 0 66115 0
vsize: 264624
[startup+790.016 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 67133 0 0 0 78857 152 0 0 25 0 1 0 429230734 272621568 58744 4294967295 134512640 134672761 3221224640 3221223744 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66558 58744 603 41 0 66517 0
vsize: 266232
[startup+800.016 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 67400 0 0 0 79856 153 0 0 25 0 1 0 429230734 273707008 59011 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66823 59011 603 41 0 66782 0
vsize: 267292
[startup+810.016 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 67751 0 0 0 80855 154 0 0 25 0 1 0 429230734 275062784 59362 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67154 59362 603 41 0 67113 0
vsize: 268616
[startup+820.016 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 68118 0 0 0 81853 155 0 0 25 0 1 0 429230734 276541440 59729 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67515 59729 603 41 0 67474 0
vsize: 270060
[startup+830.016 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 68490 0 0 0 82853 156 0 0 25 0 1 0 429230734 278163456 60101 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67911 60101 603 41 0 67870 0
vsize: 271644
[startup+840.017 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 68876 0 0 0 83852 157 0 0 25 0 1 0 429230734 279658496 60487 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68276 60487 603 41 0 68235 0
vsize: 273104
[startup+850.018 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 69030 0 0 0 84852 157 0 0 25 0 1 0 429230734 280338432 60641 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68442 60641 603 41 0 68401 0
vsize: 273768
[startup+860.017 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 69068 0 0 0 85852 157 0 0 25 0 1 0 429230734 280473600 60679 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68475 60679 603 41 0 68434 0
vsize: 273900
[startup+870.018 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 69185 0 0 0 86852 157 0 0 25 0 1 0 429230734 281022464 60796 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68609 60796 603 41 0 68568 0
vsize: 274436
[startup+880.018 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 69473 0 0 0 87852 158 0 0 25 0 1 0 429230734 282103808 61084 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68873 61084 603 41 0 68832 0
vsize: 275492
[startup+890.019 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74260 0 0 0 88838 172 0 0 25 0 1 0 429230734 282509312 61193 4294967295 134512640 134672761 3221224640 3221223940 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68972 61193 603 41 0 68931 0
vsize: 275888
[startup+900.018 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74261 0 0 0 89839 172 0 0 25 0 1 0 429230734 282509312 61194 4294967295 134512640 134672761 3221224640 3221223840 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68972 61194 603 41 0 68931 0
vsize: 275888
[startup+910.018 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74261 0 0 0 90839 172 0 0 25 0 1 0 429230734 282509312 61194 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68972 61194 603 41 0 68931 0
vsize: 275888
[startup+920.019 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74347 0 0 0 91839 172 0 0 25 0 1 0 429230734 283193344 61280 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69139 61280 603 41 0 69098 0
vsize: 276556
[startup+930.019 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74471 0 0 0 92838 172 0 0 25 0 1 0 429230734 283738112 61404 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69272 61404 603 41 0 69231 0
vsize: 277088
[startup+940.019 s]
Raw data (loadavg): 1.07 0.96 0.61 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74509 0 0 0 93839 172 0 0 25 0 1 0 429230734 283873280 61442 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69305 61442 603 41 0 69264 0
vsize: 277220
[startup+950.02 s]
Raw data (loadavg): 1.06 0.96 0.62 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74576 0 0 0 94839 172 0 0 25 0 1 0 429230734 284143616 61509 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69371 61509 603 41 0 69330 0
vsize: 277484
[startup+960.02 s]
Raw data (loadavg): 1.05 0.96 0.62 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 74821 0 0 0 95838 173 0 0 25 0 1 0 429230734 285081600 61754 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69600 61754 603 41 0 69559 0
vsize: 278400
[startup+970.021 s]
Raw data (loadavg): 1.04 0.96 0.63 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 75199 0 0 0 96837 174 0 0 25 0 1 0 429230734 286703616 62132 4294967295 134512640 134672761 3221224640 3221223744 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69996 62132 603 41 0 69955 0
vsize: 279984
[startup+980.021 s]
Raw data (loadavg): 1.03 0.96 0.63 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 75576 0 0 0 97837 175 0 0 25 0 1 0 429230734 288190464 62509 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70359 62509 603 41 0 70318 0
vsize: 281436
[startup+990.022 s]
Raw data (loadavg): 1.03 0.96 0.63 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 75875 0 0 0 98836 176 0 0 25 0 1 0 429230734 289402880 62808 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70655 62808 603 41 0 70614 0
vsize: 282620
[startup+1000.02 s]
Raw data (loadavg): 1.02 0.97 0.64 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 75979 0 0 0 99836 177 0 0 25 0 1 0 429230734 289812480 62912 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70755 62912 603 41 0 70714 0
vsize: 283020
[startup+1010.02 s]
Raw data (loadavg): 1.02 0.97 0.64 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76046 0 0 0 100835 177 0 0 25 0 1 0 429230734 290082816 62979 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70821 62979 603 41 0 70780 0
vsize: 283284
[startup+1020.02 s]
Raw data (loadavg): 1.02 0.97 0.64 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76134 0 0 0 101836 177 0 0 25 0 1 0 429230734 290492416 63067 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70921 63067 603 41 0 70880 0
vsize: 283684
[startup+1030.02 s]
Raw data (loadavg): 1.01 0.97 0.65 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76298 0 0 0 102835 177 0 0 25 0 1 0 429230734 291168256 63231 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71086 63231 603 41 0 71045 0
vsize: 284344
[startup+1040.02 s]
Raw data (loadavg): 1.01 0.97 0.65 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76645 0 0 0 103835 178 0 0 25 0 1 0 429230734 292511744 63578 4294967295 134512640 134672761 3221224640 3221223744 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71414 63578 603 41 0 71373 0
vsize: 285656
[startup+1050.02 s]
Raw data (loadavg): 1.08 0.99 0.66 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76779 0 0 0 104834 179 0 0 25 0 1 0 429230734 293052416 63712 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71546 63712 603 41 0 71505 0
vsize: 286184
[startup+1060.02 s]
Raw data (loadavg): 1.07 0.99 0.66 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76843 0 0 0 105834 179 0 0 25 0 1 0 429230734 293322752 63776 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71612 63776 603 41 0 71571 0
vsize: 286448
[startup+1070.02 s]
Raw data (loadavg): 1.06 0.99 0.66 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 76942 0 0 0 106834 179 0 0 25 0 1 0 429230734 293728256 63875 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71711 63875 603 41 0 71670 0
vsize: 286844
[startup+1080.02 s]
Raw data (loadavg): 1.05 0.99 0.67 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 77309 0 0 0 107832 181 0 0 25 0 1 0 429230734 295202816 64242 4294967295 134512640 134672761 3221224640 3221223744 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72071 64242 603 41 0 72030 0
vsize: 288284
[startup+1090.02 s]
Raw data (loadavg): 1.04 0.99 0.67 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 77495 0 0 0 108832 182 0 0 25 0 1 0 429230734 296001536 64428 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72266 64428 603 41 0 72225 0
vsize: 289064
[startup+1100.02 s]
Raw data (loadavg): 1.03 0.99 0.67 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 77586 0 0 0 109832 182 0 0 25 0 1 0 429230734 296407040 64519 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72365 64519 603 41 0 72324 0
vsize: 289460
[startup+1110.02 s]
Raw data (loadavg): 1.03 0.99 0.67 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 77763 0 0 0 110832 182 0 0 25 0 1 0 429230734 297078784 64696 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72529 64696 603 41 0 72488 0
vsize: 290116
[startup+1120.02 s]
Raw data (loadavg): 1.02 0.99 0.68 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 78119 0 0 0 111831 183 0 0 25 0 1 0 429230734 298569728 65052 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72893 65052 603 41 0 72852 0
vsize: 291572
[startup+1130.02 s]
Raw data (loadavg): 1.02 0.99 0.68 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 78478 0 0 0 112830 184 0 0 25 0 1 0 429230734 300056576 65411 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73256 65411 603 41 0 73215 0
vsize: 293024
[startup+1140.02 s]
Raw data (loadavg): 1.02 0.99 0.68 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 78823 0 0 0 113830 185 0 0 25 0 1 0 429230734 301408256 65756 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73586 65756 603 41 0 73545 0
vsize: 294344
[startup+1150.02 s]
Raw data (loadavg): 1.01 0.99 0.69 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 79164 0 0 0 114829 186 0 0 25 0 1 0 429230734 302870528 66097 4294967295 134512640 134672761 3221224640 3221223744 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73943 66097 603 41 0 73902 0
vsize: 295772
[startup+1160.02 s]
Raw data (loadavg): 1.01 0.99 0.69 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 79507 0 0 0 115829 186 0 0 25 0 1 0 429230734 304218112 66440 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74272 66440 603 41 0 74231 0
vsize: 297088
[startup+1170.02 s]
Raw data (loadavg): 1.01 0.99 0.69 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 79831 0 0 0 116828 188 0 0 25 0 1 0 429230734 305561600 66764 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74600 66764 603 41 0 74559 0
vsize: 298400
[startup+1180.02 s]
Raw data (loadavg): 1.01 0.99 0.70 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 80165 0 0 0 117827 188 0 0 25 0 1 0 429230734 306925568 67098 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74933 67098 603 41 0 74892 0
vsize: 299732
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.70 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 80481 0 0 0 118827 189 0 0 25 0 1 0 429230734 308256768 67414 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75258 67414 603 41 0 75217 0
vsize: 301032
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.70 2/54 12351
Raw data (stat): 12351 (minisat+) R 12350 32461 32460 0 -1 0 80770 0 0 0 119826 190 0 0 25 0 1 0 429230734 309334016 67703 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75521 67703 603 41 0 75480 0
vsize: 302084
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.70 1/54 12351
Raw data (stat): 12351 (minisat+) Z 12350 32461 32460 0 -1 12 80773 0 0 0 119827 203 0 0 25 0 1 0 429230734 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): 1200.17
CPU time (s): 1200.31
CPU user time (s): 1198.27
CPU system time (s): 2.03269
CPU usage (%): 100.011
Max. virtual memory (Kb): 302084
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####