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 6921

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        825808 kB
Buffers:         35620 kB
Cached:         135776 kB
SwapCached:       3160 kB
Active:          75704 kB
Inactive:       101728 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        825556 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25884 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:45:35 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4992 7 1200.22 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 |  421499  1171283 |  140499       0        0     nan |  0.000 % |
c |       100 |  421444  1171118 |  154548      71     1471    20.7 |  0.415 % |
c |       250 |  421439  1171103 |  170003     219     5209    23.8 |  0.415 % |
c |       475 |  421320  1170746 |  187004     369     8499    23.0 |  0.439 % |
c |       813 |  421248  1170530 |  205704     634    22965    36.2 |  0.452 % |
c |      1322 |  421157  1170259 |  226275    1040    38589    37.1 |  0.470 % |
c |      2081 |  420994  1169772 |  248902    1618    52958    32.7 |  0.501 % |
c ==============================================================================
c [1mFound solution: 34417[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 59722   maxlim: 3874031   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2707 |  838781  2661995 |  279593    2046    64940    31.7 |  0.501 % |
c |      2807 |  838701  2661755 |  307552    2086    63876    30.6 |  0.355 % |
c |      2957 |  838685  2661709 |  338307    2222    68826    31.0 |  0.357 % |
c |      3182 |  838640  2661574 |  372138    2408    76973    32.0 |  0.362 % |
c |      3521 |  838595  2661439 |  409352    2709    83655    30.9 |  0.369 % |
c |      4027 |  838437  2660967 |  450287    3078    98975    32.2 |  0.388 % |
c ==============================================================================
c [1mFound solution: 32001[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3876447   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4182 |  838412  2660934 |  279470    3203   105318    32.9 |  0.388 % |
c |      4282 |  838402  2660904 |  307417    3296   107233    32.5 |  0.395 % |
c |      4432 |  838362  2660784 |  338158    3407   108997    32.0 |  0.400 % |
c |      4658 |  838272  2660514 |  371974    3541   113733    32.1 |  0.412 % |
c |      4995 |  838160  2660178 |  409172    3767   123395    32.8 |  0.425 % |
c |      5501 |  838065  2659893 |  450089    4146   135730    32.7 |  0.437 % |
c |      6260 |  837843  2659227 |  495098    4693   158753    33.8 |  0.464 % |
c |      7399 |  837656  2658670 |  544607    5598   259941    46.4 |  0.487 % |
c |      9110 |  836483  2654912 |  599068    6610   284342    43.0 |  0.625 % |
c |     11672 |  836099  2653760 |  658975    8770  1152043   131.4 |  0.673 % |
c ==============================================================================
c [1mFound solution: 30408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3878040   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14924 |  834807  2649912 |  278269   10830  1366553   126.2 |  0.673 % |
c |     15024 |  834711  2649600 |  306095   10890  1367362   125.6 |  0.849 % |
c |     15175 |  834627  2649346 |  336705   10978  1367784   124.6 |  0.860 % |
c |     15400 |  834454  2648821 |  370376   11106  1369226   123.3 |  0.881 % |
c |     15738 |  834275  2648262 |  407413   11296  1373464   121.6 |  0.903 % |
c |     16245 |  833969  2647340 |  448155   11463  1375164   120.0 |  0.941 % |
c |     17004 |  833471  2645824 |  492970   11865  1385634   116.8 |  1.000 % |
c |     18144 |  833038  2644523 |  542267   12708  1417657   111.6 |  1.054 % |
c |     19852 |  832400  2642611 |  596494   13775  1443173   104.8 |  1.133 % |
c |     22414 |  831596  2640199 |  656143   15478  1957827   126.5 |  1.231 % |
c |     26259 |  829259  2633180 |  721758   17173  2000099   116.5 |  1.518 % |
c ==============================================================================
c [1mFound solution: 29351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3879097   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27516 |  828825  2631927 |  276275   18030  2136932   118.5 |  1.518 % |
c |     27616 |  828715  2631597 |  303902   18021  2135360   118.5 |  1.589 % |
c |     27766 |  828530  2631042 |  334292   18022  2134683   118.4 |  1.612 % |
c |     27992 |  828379  2630587 |  367722   18148  2135725   117.7 |  1.631 % |
c |     28331 |  828120  2629810 |  404494   18250  2137760   117.1 |  1.663 % |
c |     28837 |  827726  2628628 |  444943   18395  2139397   116.3 |  1.711 % |
c |     29596 |  827362  2627536 |  489438   18713  2165238   115.7 |  1.756 % |
c |     30735 |  826609  2625277 |  538381   19125  2171140   113.5 |  1.849 % |
c |     32443 |  825692  2622512 |  592219   19949  2449327   122.8 |  1.961 % |
c |     35005 |  823848  2616974 |  651441   20969  2468896   117.7 |  2.188 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x0 -x1 -x2 -x3 -x4 -x5 -x6 x7 x8 x9 -x10 -x11 x12 -x13 x14 -x15 -x16 -x17 x18 x19 -x20 x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 x29 -x30 -x31 -x32 -x33 x34 -x35 x36 x37 -x38 x39 x40 -x41 -x42 x43 x44 -x45 -x46 x47 x48 -x49 x50 -x51 -x52 -x53 -x54 x55 -x56 -x57 x58 -x59 -x60 -x61 x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 x73 x74 x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 x126 x127 -x128 x129 x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 x195 -x196 -x197 -x198 -x199 -x200 x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 x248 x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 x272 x273 x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 x298 x299 x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 x336 -x337 -x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 -x391 -x392 -x393 -x394 -x395 -x396 x397 -x398 -x399 x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 -x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 -x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 -x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 x571 -x572 -x573 -x574 -x575 x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 -x594 -x595 -x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 -x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 -x662 -x663 -x664 -x665 -x666 -x667 x668 -x669 x670 -x671 -x672 -x673 -x674 -x675 -x676 -x677 -x678 -x679 x680 -x681 -x682 -x683 -x684 -x685 -x686 -x687 -x688 -x689 -x690 x691 -x692 -x693 -x694 -x695 -x696 -x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 -x705 -x706 -x707 x708 -x709 -x710 x711 -x712 -x713 -x714 -x715 -x716 -x717 -x718 -x719 -x720 -x721 -x722 -x723 -x724 -x725 -x726 -x727 -x728 -x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x737 -x738 -x739 -x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 -x748 -x749 -x750 -x751 -x752 -x753 -x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 -x762 -x763 -x764 -x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 -x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 x802 -x803 -x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 x820 -x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 -x862 -x863 -x864 -x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 -x881 -x882 -x883 -x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 -x902 -x903 -x904 -x905 -x906 -x907 -x908 -x909 -x910 -x911 -x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 -x942 -x943 -x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 -x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x978 -x979 -x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 -x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 -x1008 -x1009 -x1010 -x1011 -x1012 -x1013 -x1014 -x1015 x1016 -x1017 -x1018 -x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 -x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 -x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 -x1048 -x1049 -x1050 -x1051 -x1052 -x1053 -x1054 -x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 -x1068 -x1069 -x1070 -x1071 -x1072 -x1073 -x1074 -x1075 -x1076 -x1077 -x1078 -x1079 -x1080 -x1081 -x1082 -x1083 -x1084 -x1085 -x1086 -x1087 -x1088 -x1089 -x1090 -x1091 -x1092 x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 -x1102 -x1103 -x1104 -x1105 -x1106 -x1107 -x1108 -x1109 -x1110 -x1111 -x1112 -x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 -x1120 -x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 -x1143 -x1144 -x1145 -x1146 -x1147 -x1148 -x1149 -x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 -x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 -x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 -x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 -x1208 -x1209 -x1210 -x1211 -x1212 -x1213 -x1214 -x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 -x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 -x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 -x1248 -x1249 -x1250 -x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 -x1263 -x1264 -x1265 -x1266 -x1267 -x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 -x1282 -x1283 -x1284 -x1285 -x1286 -x1287 -x1288 -x1289 -x1290 -x1291 -x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 -x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 -x1310 -x1311 -x1312 -x1313 -x1314 x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 -x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 -x1334 -x1335 -x1336 -x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 -x1346 -x1347 -x1348 -x1349 -x1350 -x1351 -x1352 -x1353 -x1354 -x1355 -x1356 -x1357 -x1358 -x1359 -x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 -x1379 -x1380 -x1381 -x1382 -x1383 -x1384 -x1385 -x1386 -x1387 -x1388 -x1389 -x1390 -x1391 -x1392 -x1393 -x1394 -x1395 -x1396 -x1397 -x1398 -x1399 -x1400 -x1401 -x1402 -x1403 -x1404 -x1405 -x1406 -x1407 -x1408 -x1409 -x1410 -x1411 -x1412 -x1413 -x1414 -x1415 -x1416 -x1417 -x1418 -x1419 -x1420 -x1421 -x1422 -x1423 -x1424 -x1425 -x1426 -x1427 -x1428 -x1429 -x1430 -x1431 -x1432 -x1433 -x1434 -x1435 -x1436 -x1437 -x1438 -x1439 -x1440 -x1441 -x1442 -x1443 -x1444 -x1445 -x1446 -x1447 -x1448 -x1449 -x1450 -x1451 -x1452 -x1453 -x1454 -x1455 -x1456 -x1457 -x1458 -x1459 -x1460 -x1461 -x1462 -x1463 -x1464 -x1465 -x1466 -x1467 -x1468 -x1469 -x1470 -x1471 -x1472 -x1473 -x1474 -x1475 -x1476 -x1477 -x1478 -x1479 -x1480 -x1481 -x1482 -x1483 -x1484 -x1485 -x1486 -x1487 -x1488 -x1489 -x1490 -x1491 -x1492 -x1493 -x1494 -x1495 -x1496 -x1497 -x1498 -x1499 -x1500 -x1501 -x1502 -x1503 -x1504 -x1505 -x1506 -x1507 -x1508 -x1509 -x1510 -x1511 -x1512 -x1513 -x1514 -x1515 -x1516 -x1517 -x1518 -x1519 -x1520 -x1521 -x1522 -x1523 -x1524 -x1525 -x1526 -x1527 -x1528 -x1529 -x1530 -x1531 -x1532 -x1533 -x1534 -x1535 -x1536 -x1537 -x1538 -x1539 -x1540 -x1541 -x1542 -x1543 -x1544 -x1545 -x1546 -x1547 -x1548 -x1549 -x1550 -x1551 -x1552 -x1553 -x1554 -x1555 -x1556 -x1557 -x1558 -x1559 -x1560 -x1561 -x1562 -x1563 -x1564 -x1565 -x1566 -x1567 -x1568 -x1569 -x1570 x1571 -x1572 -x1573 -x1574 -x1575 -x1576 -x1577 -x1578 -x1579 -x1580 -x1581 -x1582 -x1583 -x1584 -x1585 -x1586 -x1587 -x1588 -x1589 -x1590 -x1591 -x1592 -x1593 -x1594 -x1595 -x1596 -x1597 -x1598 -x1599 -x1600 -x1601 -x1602 -x1603 -x1604 -x1605 -x1606 -x1607 -x1608 -x1609 -x1610 -x1611 -x1612 -x1613 -x1614 -x1615 -x1616 -x1617 -x1618 -x1619 -x1620 -x1621 -x1622 -x1623 -x1624 -x1625 -x1626 -x1627 -x1628 -x1629 -x1630 -x1631 -x1632 -x1633 -x1634 -x1635 -x1636 -x1637 -x1638 -x1639 -x1640 -x1641 -x1642 -x1643 -x1644 -x1645 -x1646 -x1647 -x1648 -x1649 -x1650 -x1651 -x1652 -x1653 -x1654 -x1655 -x1656 -x1657 -x1658 -x1659 -x1660 -x1661 -x1662 -x1663 -x1664 -x1665 -x1666 -x1667 -x1668 -x1669 -x1670 -x1671 -x1672 -x1673 -x1674 -x1675 -x1676 -x1677 -x1678 -x1679 -x1680 -x1681 -x1682 -x1683 -x1684 -x1685 -x1686 -x1687 -x1688 -x1689 -x1690 -x1691 -x1692 -x1693 -x1694 -x1695 -x1696 -x1697 -x1698 -x1699 -x1700 -x1701 -x1702 -x1703 -x1704 -x1705 -x1706 -x1707 -x1708 -x1709 -x1710 -x1711 -x1712 -x1713 -x1714 -x1715 -x1716 -x1717 -x1718 -x1719 -x1720 -x1721 -x1722 -x1723 -x1724 -x1725 -x1726 -x1727 -x1728 -x1729 -x1730 -x1731 -x1732 -x1733 -x1734 -x1735 -x1736 -x1737 -x1738 -x1739 -x1740 -x1741 -x1742 -x1743 -x1744 -x1745 -x1746 -x1747 -x1748 -x1749 -x1750 -x1751 -x1752 -x1753 -x1754 -x1755 -x1756 -x1757 -x1758 -x1759 -x1760 -x1761 -x1762 -x1763 -x1764 -x1765 -x1766 -x1767 -x1768 -x1769 -x1770 -x1771 -x1772 -x1773 -x1774 -x1775 -x1776 -x1777 -x1778 -x1779 -x1780 -x1781 -x1782 -x1783 -x1784 -x1785 -x1786 -x1787 -x1788 -x1789 -x1790 -x1791 -x1792 -x1793 -x1794 -x1795 -x1796 -x1797 -x1798 -x1799 -x1800 -x1801 -x1802 -x1803 -x1804 -x1805 -x1806 -x1807 -x1808 -x1809 -x1810 -x1811 -x1812 -x1813 -x1814 -x1815 -x1816 -x1817 -x1818 -x1819 -x1820 -x1821 -x1822 -x1823 -x1824 -x1825 -x1826 -x1827 -x1828 -x1829 -x1830 -x1831 -x1832 -x1833 -x1834 -x1835 -x1836 -x1837 -x1838 -x1839 -x1840 -x1841 -x1842 -x1843 -x1844 -x1845 -x1846 -x1847 -x1848 -x1849 -x1850 -x1851 -x1852 -x1853 -x1854 -x1855 -x1856 -x1857 -x1858 -x1859 -x1860 -x1861 -x1862 -x1863 -x1864 -x1865 -x1866 -x1867 -x1868 -x1869 -x1870 -x1871 -x1872 -x1873 -x1874 -x1875 -x1876 -x1877 -x1878 -x1879 -x1880 -x1881 -x1882 -x1883 -x1884 -x1885 -x1886 -x1887 -x1888 -x1889 -x1890 -x1891 -x1892 -x1893 -x1894 -x1895 -x1896 -x1897 -x1898 -x1899 -x1900 -x1901 -x1902 -x1903 -x1904 -x1905 -x1906 -x1907 -x1908 -x1909 -x1910 -x1911 -x1912 -x1913 -x1914 -x1915 -x1916 -x1917 -x1918 -x1919 -x1920 -x1921 -x1922 -x1923 -x1924 -x1925 -x1926 -x1927 -x1928 -x1929 -x1930 -x1931 -x1932 -x1933 -x1934 -x1935 -x1936 -x1937 -x1938 -x1939 -x1940 -x1941 -x1942 -x1943 -x1944 -x1945 -x1946 -x1947 -x1948 -x1949 -x1950 -x1951 -x1952 -x1953 -x1954 -x1955 -x1956 -x1957 -x1958 -x1959 -x1960 -x1961 -x1962 -x1963 -x1964 -x1965 -x1966 -x1967 -x1968 -x1969 -x1970 -x1971 -x1972 -x1973 -x1974 -x1975 -x1976 -x1977 -x1978 -x1979 -x1980 -x1981 -x1982 -x1983 -x1984 -x1985 -x1986 -x1987 -x1988 -x1989 -x1990 -x1991 -x1992 -x1993 -x1994 -x1995 -x1996 -x1997 -x1998 -x1999 -x2000 -x2001 -x2002 -x2003 -x2004 -x2005 -x2006 -x2007 -x2008 -x2009 -x2010 -x2011 -x2012 -x2013 -x2014 -x2015 -x2016 -x2017 -x2018 -x2019 -x2020 -x2021 -x2022 -x2023 -x2024 -x2025 -x2026 -x2027 -x2028 -x2029 -x2030 -x2031 -x2032 -x2033 -x2034 -x2035 -x2036 -x2037 -x2038 -x2039 -x2040 -x2041 -x2042 -x2043 -x2044 -x2045 -x2046 -x2047 -x2048 -x2049 -x2050 -x2051 -x2052 -x2053 -x2054 -x2055 -x2056 -x2057 -x2058 -x2059 -x2060 -x2061 -x2062 -x2063 -x2064 -x2065 -x2066 -x2067 -x2068 -x2069 -x2070 -x2071 -x2072 -x2073 -x2074 -x2075 -x2076 -x2077 -x2078 -x2079 -x2080 -x2081 -x2082 -x2083 -x2084 -x2085 -x2086 -x2087 -x2088 -x2089 -x2090 -x2091 -x2092 -x2093 -x2094 -x2095 -x2096 -x2097 -x2098 -x2099 -x2100 -x2101 -x2102 -x2103 -x2104 -x2105 -x2106 -x2107 -x2108 -x2109 -x2110 -x2111 -x2112 -x2113 -x2114 -x2115 -x2116 -x2117 -x2118 -x2119 -x2120 -x2121 -x2122 -x2123 -x2124 -x2125 -x2126 -x2127 -x2128 -x2129 -x2130 -x2131 -x2132 -x2133 -x2134 -x2135 -x2136 -x2137 -x2138 -x2139 -x2140 -x2141 -x2142 -x2143 -x2144 -x2145 -x2146 -x2147 -x2148 -x2149 -x2150 -x2151 -x2152 -x2153 -x2154 -x2155 -x2156 -x2157 -x2158 -x2159 -x2160 -x2161 -x2162 -x2163 -x2164 -x2165 -x2166 -x2167 -x2168 -x2169 -x2170 -x2171 -x2172 -x2173 -x2174 -x2175 -x2176 -x2177 -x2178 -x2179 -x2180 -x2181 -x2182 -x2183 -x2184 -x2185 -x2186 -x2187 -x2188 -x2189 -x2190 -x2191 -x2192 -x2193 -x2194 -x2195 -x2196 -x2197 -x2198 -x2199 -x2200 -x2201 -x2202 -x2203 -x2204 -x2205 -x2206 -x2207 -x2208 -x2209 -x2210 -x2211 -x2212 -x2213 -x2214 -x2215 -x2216 -x2217 -x2218 -x2219 x2220 -x2221 -x2222 -x2223 -x2224 -x2225 -x2226 -x2227 -x2228 -x2229 -x2230 -x2231 -x2232 -x2233 -x2234 -x2235 -x2236 -x2237 -x2238 -x2239 -x2240 -x2241 -x2242 -x2243 -x2244 -x2245 -x2246 -x2247 -x2248 -x2249 -x2250 -x2251 -x2252 -x2253 -x2254 -x2255 -x2256 -x2257 -x2258 -x2259 -x2260 -x2261 -x2262 -x2263 -x2264 -x2265 -x2266 -x2267 -x2268 -x2269 -x2270 -x2271 -x2272 -x2273 -x2274 -x2275 -x2276 -x2277 -x2278 -x2279 -x2280 -x2281 -x2282 -x2283 -x2284 -x2285 -x2286 -x2287 -x2288 -x2289 -x2290 -x2291 -x2292 -x2293 -x2294 -x2295 -x2296 -x2297 -x2298 -x2299 -x2300 -x2301 -x2302 -x2303 -x2304 -x2305 -x2306 -x2307 -x2308 -x2309 -x2310 -x2311 -x2312 -x2313 -x2314 -x2315 -x2316 -x2317 -x2318 -x2319 -x2320 -x2321 -x2322 -x2323 -x2324 -x2325 -x2326 -x2327 -x2328 -x2329 -x2330 -x2331 -x2332 x2333 -x2334 -x2335 -x2336 -x2337 -x2338 -x2339 -x2340 -x2341 -x2342 -x2343 -x2344 -x2345 -x2346 -x2347 -x2348 -x2349 -x2350 -x2351 -x2352 -x2353 -x2354 -x2355 -x2356 -x2357 -x2358 -x2359 -x2360 -x2361 -x2362 -x2363 -x2364 -x2365 -x2366 -x2367 -x2368 -x2369 -x2370 -x2371 -x2372 -x2373 -x2374 -x2375 -x2376 -x2377 -x2378 -x2379 -x2380 -x2381 -x2382 -x2383 -x2384 -x2385 -x2386 -x2387 -x2388 -x2389 -x2390 -x2391 -x2392 -x2393 -x2394 -x2395 -x2396 -x2397 -x2398 -x2399 -x2400 -x2401 -x2402 -x2403 -x2404 -x2405 -x2406 -x2407 -x2408 -x2409 -x2410 -x2411 -x2412 -x2413 -x2414 -x2415 -x2416 -x2417 -x2418 -x2419 -x2420 -x2421 -x2422 -x2423 -x2424 -x2425 -x2426 -x2427 -x2428 -x2429 -x2430 -x2431 -x2432 -x2433 -x2434 -x2435 -x2436 -x2437 -x2438 -x2439 -x2440 -x2441 -x2442 -x2443 -x2444 -x2445 -x2446 -x2447 -x2448 -x2449 -x2450 -x2451 -x2452 -x2453 -x2454 -x2455 -x2456 -x2457 -x2458 -x2459 -x2460 -x2461 -x2462 -x2463 -x2464 -x2465 -x2466 -x2467 -x2468 -x2469 -x2470 -x2471 -x2472 -x2473 -x2474 -x2475 -x2476 -x2477 -x2478 -x2479 -x2480 -x2481 -x2482 -x2483 -x2484 -x2485 -x2486 -x2487 -x2488 -x2489 -x2490 -x2491 -x2492 -x2493 -x2494 -x2495 -x2496 -x2497 -x2498 -x2499 -x2500 -x2501 -x2502 -x2503 -x2504 -x2505 -x2506 -x2507 -x2508 -x2509 -x2510 -x2511 -x2512 -x2513 -x2514 -x2515 -x2516 -x2517 -x2518 -x2519 -x2520 -x2521 -x2522 -x2523 -x2524 -x2525 -x2526 -x2527 -x2528 -x2529 -x2530 -x2531 -x2532 -x2533 -x2534 -x2535 -x2536 -x2537 -x2538 -x2539 -x2540 -x2541 -x2542 -x2543 -x2544 -x2545 -x2546 -x2547 -x2548 -x2549 -x2550 -x2551 -x2552 -x2553 -x2554 -x2555 -x2556 -x2557 -x2558 -x2559 -x2560 -x2561 -x2562 -x2563 -x2564 -x2565 -x2566 -x2567 -x2568 -x2569 -x2570 -x2571 -x2572 -x2573 -x2574 -x2575 -x2576 -x2577 -x2578 -x2579 -x2580 -x2581 -x2582 -x2583 -x2584 -x2585 -x2586 -x2587 -x2588 -x2589 -x2590 -x2591 -x2592 -x2593 -x2594 -x2595 -x2596 -x2597 -x2598 -x2599 -x2600 -x2601 -x2602 -x2603 -x2604 -x2605 -x2606 -x2607 -x2608 -x2609 -x2610 -x2611 -x2612 -x2613 -x2614 -x2615 -x2616 -x2617 -x2618 -x2619 -x2620 -x2621 -x2622 -x2623 -x2624 -x2625 -x2626 -x2627 -x2628 -x2629 -x2630 -x2631 -x2632 -x2633 -x2634 -x2635 -x2636 -x2637 -x2638 -x2639 -x2640 -x2641 -x2642 -x2643 -x2644 -x2645 -x2646 -x2647 -x2648 -x2649 -x2650 -x2651 -x2652 -x2653 -x2654 -x2655 -x2656 -x2657 -x2658 -x2659 -x2660 -x2661 -x2662 -x2663 -x2664 -x2665 -x2666 -x2667 -x2668 -x2669 -x2670 -x2671 -x2672 -x2673 -x2674 -x2675 -x2676 -x2677 -x2678 -x2679 -x2680 -x2681 -x2682 -x2683 -x2684 -x2685 -x2686 -x2687 -x2688 -x2689 -x2690 -x2691 -x2692 -x2693 -x2694 -x2695 -x2696 -x2697 -x2698 -x2699 -x2700 -x2701 -x2702 -x2703 -x2704 -x2705 -x2706 -x2707 -x2708 -x2709 -x2710 -x2711 -x2712 -x2713 -x2714 -x2715 -x2716 -x2717 -x2718 -x2719 -x2720 -x2721 -x2722 -x2723 -x2724 -x2725 -x2726 -x2727 -x2728 -x2729 -x2730 -x2731 -x2732 -x2733 -x2734 -x2735 -x2736 -x2737 -x2738 -x2739 -x2740 -x2741 -x2742 -x2743 -x2744 -x2745 -x2746 -x2747 -x2748 -x2749 -x2750 -x2751 -x2752 -x2753 -x2754 -x2755 -x2756 -x2757 -x2758 -x2759 -x2760 -x2761 -x2762 -x2763 -x2764 -x2765 -x2766 -x2767 -x2768 -x2769 -x2770 -x2771 -x2772 -x2773 -x2774 -x2775 -x2776 -x2777 -x2778 -x2779 -x2780 -x2781 -x2782 -x2783 -x2784 -x2785 -x2786 -x2787 -x2788 -x2789 -x2790 -x2791 -x2792 -x2793 -x2794 -x2795 -x2796 -x2797 -x2798 -x2799 -x2800 -x2801 -x2802 -x2803 -x2804 -x2805 -x2806 -x2807 -x2808 -x2809 -x2810 -x2811 -x2812 -x2813 -x2814 -x2815 -x2816 -x2817 -x2818 -x2819 -x2820 -x2821 -x2822 -x2823 -x2824 -x2825 -x2826 -x2827 -x2828 -x2829 -x2830 -x2831 -x2832 -x2833 -x2834 -x2835 -x2836 -x2837 -x2838 -x2839 -x2840 -x2841 -x2842 -x2843 -x2844 -x2845 -x2846 -x2847 -x2848 -x2849 -x2850 -x2851 -x2852 -x2853 -x2854 -x2855 -x2856 -x2857 -x2858 -x2859 -x2860 -x2861 -x2862 -x2863 -x2864 -x2865 -x2866 -x2867 -x2868 -x2869 -x2870 -x2871 -x2872 -x2873 -x2874 -x2875 -x2876 -x2877 -x2878 -x2879 -x2880 -x2881 -x2882 -x2883 -x2884 -x2885 -x2886 -x2887 -x2888 -x2889 -x2890 -x2891 -x2892 -x2893 -x2894 -x2895 -x2896 -x2897 -x2898 -x2899 -x2900 -x2901 -x2902 -x2903 -x2904 -x2905 -x2906 -x2907 -x2908 -x2909 -x2910 -x2911 -x2912 -x2913 -x2914 -x2915 -x2916 -x2917 -x2918 -x2919 -x2920 -x2921 -x2922 -x2923 -x2924 -x2925 -x2926 -x2927 -x2928 -x2929 -x2930 -x2931 -x2932 -x2933 -x2934 -x2935 -x2936 -x2937 -x2938 -x2939 -x2940 -x2941 -x2942 -x2943 -x2944 -x2945 -x2946 -x2947 -x2948 -x2949 -x2950 -x2951 -x2952 -x2953 -x2954 -x2955 -x2956 -x2957 -x2958 -x2959 -x2960 -x2961 -x2962 -x2963 -x2964 -x2965 -x2966 -x2967 -x2968 -x2969 -x2970 -x2971 -x2972 -x2973 -x2974 -x2975 -x2976 -x2977 -x2978 -x2979 -x2980 -x2981 -x2982 -x2983 -x2984 -x2985 -x2986 -x2987 -x2988 -x2989 -x2990 -x2991 -x2992 -x2993 -x2994 -x2995 -x2996 -x2997 -x2998 -x2999 -x3000 -x3001 -x3002 -x3003 -x3004 -x3005 -x3006 -x3007 -x3008 -x3009 -x3010 -x3011 -x3012 -x3013 -x3014 -x3015 -x3016 -x3017 -x3018 -x3019 -x3020 -x3021 -x3022 -x3023 -x3024 -x3025 -x3026 -x3027 -x3028 -x3029 -x3030 -x3031 -x3032 -x3033 -x3034 -x3035 -x3036 -x3037 -x3038 -x3039 -x3040 -x3041 -x3042 -x3043 -x3044 -x3045 -x3046 -x3047 -x3048 -x3049 -x3050 -x3051 -x3052 -x3053 -x3054 -x3055 -x3056 -x3057 -x3058 -x3059 -x3060 -x3061 -x3062 -x3063 -x3064 -x3065 -x3066 -x3067 -x3068 -x3069 -x3070 -x3071 -x3072 -x3073 -x3074 -x3075 -x3076 -x3077 -x3078 -x3079 -x3080 -x3081 -x3082 -x3083 -x3084 -x3085 -x3086 -x3087 -x3088 -x3089 -x3090 -x3091 -x3092 -x3093 -x3094 -x3095 -x3096 -x3097 -x3098 -x3099 -x3100 -x3101 -x3102 -x3103 -x3104 -x3105 -x3106 -x3107 -x3108 -x3109 -x3110 -x3111 -x3112 -x3113 -x3114 -x3115 -x3116 -x3117 -x3118 -x3119 -x3120 -x3121 -x3122 -x3123 -x3124 -x3125 -x3126 -x3127 -x3128 -x3129 -x3130 -x3131 -x3132 -x3133 -x3134 -x3135 -x3136 -x3137 -x3138 -x3139 -x3140 -x3141 -x3142 -x3143 -x3144 -x3145 -x3146 -x3147 -x3148 -x3149 -x3150 -x3151 -x3152 -x3153 -x3154 -x3155 -x3156 -x3157 -x3158 -x3159 -x3160 -x3161 -x3162 -x3163 -x3164 -x3165 -x3166 -x3167 -x3168 -x3169 -x3170 -x3171 -x3172 -x3173 -x3174 -x3175 -x3176 -x3177 -x3178 -x3179 -x3180 -x3181 -x3182 -x3183 -x3184 -x3185 -x3186 -x3187 -x3188 -x3189 -x3190 -x3191 -x3192 -x3193 -x3194 -x3195 -x3196 -x3197 -x3198 -x3199 -x3200 -x3201 -x3202 -x3203 -x3204 -x3205 -x3206 -x3207 -x3208 -x3209 -x3210 -x3211 -x3212 -x3213 -x3214 -x3215 -x3216 -x3217 -x3218 -x3219 -x3220 -x3221 -x3222 -x3223 -x3224 -x3225 -x3226 -x3227 -x3228 -x3229 -x3230 -x3231 -x3232 -x3233 -x3234 -x3235 -x3236 -x3237 -x3238 -x3239 -x3240 -x3241 -x3242 -x3243 -x3244 -x3245 -x3246 -x3247 -x3248 -x3249 -x3250 -x3251 -x3252 -x3253 -x3254 -x3255 -x3256 -x3257 -x3258 -x3259 -x3260 -x3261 -x3262 -x3263 -x3264 -x3265 -x3266 -x3267 -x3268 -x3269 -x3270 -x3271 -x3272 -x3273 -x3274 -x3275 -x3276 -x3277 -x3278 -x3279 -x3280 -x3281 -x3282 -x3283 -x3284 -x3285 -x3286 -x3287 -x3288 -x3289 -x3290 -x3291 -x3292 -x3293 -x3294 -x3295 -x3296 -x3297 -x3298 -x3299 -x3300 -x3301 -x3302 -x3303 -x3304 -x3305 -x3306 -x3307 -x3308 -x3309 -x3310 -x3311 -x3312 -x3313 -x3314 -x3315 -x3316 -x3317 -x3318 -x3319 -x3320 -x3321 -x3322 -x3323 -x3324 -x3325 -x3326 -x3327 -x3328 -x3329 -x3330 -x3331 -x3332 -x3333 -x3334 -x3335 -x3336 -x3337 -x3338 -x3339 -x3340 -x3341 -x3342 -x3343 -x3344 -x3345 -x3346 -x3347 -x3348 -x3349 -x3350 -x3351 -x3352 -x3353 -x3354 -x3355 -x3356 -x3357 -x3358 -x3359 -x3360 -x3361 -x3362 -x3363 -x3364 -x3365 -x3366 -x3367 -x3368 -x3369 -x3370 -x3371 -x3372 -x3373 -x3374 -x3375 -x3376 -x3377 -x3378 -x3379 -x3380 -x3381 -x3382 -x3383 -x3384 -x3385 -x3386 -x3387 -x3388 -x3389 -x3390 -x3391 -x3392 -x3393 -x3394 -x3395 -x3396 -x3397 -x3398 -x3399 -x3400 -x3401 -x3402 -x3403 -x3404 -x3405 -x3406 -x3407 -x3408 -x3409 -x3410 -x3411 -x3412 -x3413 -x3414 -x3415 -x3416 -x3417 -x3418 -x3419 -x3420 -x3421 -x3422 -x3423 -x3424 -x3425 -x3426 -x3427 -x3428 -x3429 -x3430 -x3431 -x3432 -x3433 -x3434 -x3435 -x3436 -x3437 -x3438 -x3439 -x3440 -x3441 -x3442 -x3443 -x3444 -x3445 -x3446 -x3447 -x3448 -x3449 -x3450 -x3451 -x3452 -x3453 -x3454 -x3455 -x3456 -x3457 -x3458 -x3459 -x3460 -x3461 -x3462 -x3463 -x3464 -x3465 -x3466 -x3467 -x3468 -x3469 -x3470 -x3471 -x3472 -x3473 -x3474 -x3475 -x3476 -x3477 -x3478 -x3479 -x3480 -x3481 -x3482 -x3483 -x3484 -x3485 -x3486 -x3487 -x3488 -x3489 -x3490 -x3491 -x3492 -x3493 -x3494 -x3495 -x3496 -x3497 -x3498 -x3499 -x3500 -x3501 -x3502 -x3503 -x3504 -x3505 -x3506 -x3507 -x3508 -x3509 -x3510 -x3511 -x3512 -x3513 -x3514 -x3515 -x3516 -x3517 -x3518 -x3519 -x3520 -x3521 -x3522 -x3523 -x3524 -x3525 -x3526 -x3527 -x3528 -x3529 -x3530 -x3531 -x3532 -x3533 -x3534 -x3535 -x3536 -x3537 -x3538 -x3539 -x3540 -x3541 -x3542 -x3543 -x3544 -x3545 -x3546 -x3547 -x3548 -x3549 -x3550 -x3551 -x3552 -x3553 -x3554 -x3555 -x3556 -x3557 -x3558 -x3559 -x3560 -x3561 -x3562 -x3563 -x3564 -x3565 -x3566 -x3567 -x3568 -x3569 -x3570 -x3571 -x3572 -x3573 -x3574 -x3575 -x3576 -x3577 -x3578 -x3579 -x3580 -x3581 -x3582 -x3583 -x3584 -x3585 -x3586 -x3587 -x3588 -x3589 -x3590 -x3591 -x3592 -x3593 -x3594 -x3595 -x3596 -x3597 -x3598 -x3599 -x3600 -x3601 -x3602 -x3603 -x3604 -x3605 -x3606 -x3607 -x3608 -x3609 -x3610 -x3611 -x3612 -x3613 -x3614 -x3615 -x3616 -x3617 -x3618 -x3619 -x3620 -x3621 -x3622 -x3623 -x3624 -x3625 -x3626 -x3627 -x3628 -x3629 -x3630 -x3631 -x3632 -x3633 -x3634 -x3635 -x3636 -x3637 -x3638 -x3639 -x3640 -x3641 -x3642 -x3643 -x3644 -x3645 -x3646 -x3647 -x3648 -x3649 -x3650 -x3651 -x3652 -x3653 -x3654 -x3655 -x3656 -x3657 -x3658 -x3659 -x3660 -x3661 -x3662 -x3663 -x3664 -x3665 -x3666 -x3667 -x3668 -x3669 -x3670 -x3671 -x3672 -x3673 -x3674 -x3675 -x3676 -x3677 -x3678 -x3679 -x3680 -x3681 -x3682 -x3683 -x3684 -x3685 -x3686 -x3687 -x3688 -x3689 -x3690 -x3691 -x3692 -x3693 -x3694 -x3695 -x3696 -x3697 -x3698 -x3699 -x3700 -x3701 -x3702 -x3703 -x3704 -x3705 -x3706 -x3707 -x3708 -x3709 -x3710 -x3711 -x3712 -x3713 -x3714 -x3715 -x3716 -x3717 -x3718 -x3719 -x3720 -x3721 -x3722 -x3723 -x3724 -x3725 -x3726 -x3727 -x3728 -x3729 -x3730 -x3731 -x3732 -x3733 -x3734 -x3735 -x3736 -x3737 -x3738 -x3739 -x3740 -x3741 -x3742 -x3743 -x3744 -x3745 -x3746 -x3747 -x3748 -x3749 -x3750 -x3751 -x3752 -x3753 -x3754 -x3755 -x3756 -x3757 -x3758 -x3759 -x3760 -x3761 -x3762 -x3763 -x3764 -x3765 -x3766 -x3767 -x3768 -x3769 -x3770 -x3771 -x3772 -x3773 -x3774 -x3775 -x3776 -x3777 -x3778 -x3779 -x3780 -x3781 -x3782 -x3783 -x3784 -x3785 -x3786 -x3787 -x3788 -x3789 -x3790 -x3791 -x3792 -x3793 -x3794 -x3795 -x3796 -x3797 -x3798 -x3799 -x3800 -x3801 -x3802 -x3803 -x3804 -x3805 -x3806 -x3807 -x3808 -x3809 -x3810 -x3811 -x3812 -x3813 -x3814 -x3815 -x3816 -x3817 -x3818 -x3819 -x3820 -x3821 -x3822 -x3823 -x3824 -x3825 -x3826 -x3827 -x3828 -x3829 -x3830 -x3831 -x3832 -x3833 -x3834 -x3835 -x3836 -x3837 -x3838 -x3839 -x3840 -x3841 -x3842 -x3843 -x3844 -x3845 -x3846 -x3847 -x3848 -x3849 -x3850 -x3851 -x3852 -x3853 -x3854 -x3855 -x3856 -x3857 -x3858 -x3859 -x3860 -x3861 -x3862 -x3863 -x3864 -x3865 -x3866 -x3867 -x3868 -x3869 -x3870 -x3871 -x3872 -x3873 -x3874 -x3875 -x3876 -x3877 -x3878 -x3879 -x3880 -x3881 -x3882 -x3883 -x3884 -x3885 -x3886 -x3887 -x3888 -x3889 -x3890 -x3891 -x3892 -x3893 -x3894 -x3895 -x3896 -x3897 -x3898 -x3899 -x3900 -x3901 -x3902 -x3903 -x3904 -x3905 -x3906 -x3907 -x3908 -x3909 -x3910 -x3911 -x3912 -x3913 -x3914 -x3915 -x3916 -x3917 -x3918 -x3919 -x3920 -x3921 -x3922 -x3923 -x3924 -x3925 -x3926 -x3927 -x3928 -x3929 -x3930 -x3931 -x3932 -x3933 -x3934 -x3935 -x3936 -x3937 -x3938 -x3939 -x3940 -x3941 -x3942 -x3943 -x3944 -x3945 -x3946 -x3947 -x3948 -x3949 -x3950 -x3951 -x3952 -x3953 -x3954 -x3955 -x3956 -x3957 -x3958 -x3959 -x3960 -x3961 -x3962 -x3963 -x3964 -x3965 -x3966 -x3967 -x3968 -x3969 -x3970 -x3971 -x3972 -x3973 -x3974 -x3975 -x3976 -x3977 -x3978 -x3979 -x3980 -x3981 -x3982 -x3983 -x3984 -x3985 -x3986 -x3987 -x3988 -x3989 -x3990 -x3991 -x3992 -x3993 -x3994 -x3995 -x3996 -x3997 -x3998 -x3999 -x4000 -x4001 -x4002 -x4003 -x4004 -x4005 -x4006 -x4007 -x4008 -x4009 -x4010 -x4011 -x4012 -x4013 -x4014 -x4015 -x4016 -x4017 -x4018 -x4019 -x4020 -x4021 -x4022 -x4023 -x4024 -x4025 -x4026 -x4027 -x4028 -x4029 -x4030 -x4031 -x4032 -x4033 -x4034 -x4035 -x4036 -x4037 -x4038 -x4039 -x4040 -x4041 -x4042 -x4043 -x4044 -x4045 -x4046 -x4047 -x4048 -x4049 -x4050 -x4051 -x4052 -x4053 -x4054 -x4055 -x4056 -x4057 -x4058 -x4059 -x4060 -x4061 -x4062 -x4063 -x4064 -x4065 -x4066 -x4067 -x4068 -x4069 -x4070 -x4071 -x4072 -x4073 -x4074 -x4075 -x4076 -x4077 -x4078 -x4079 -x4080 -x4081 -x4082 -x4083 -x4084 -x4085 -x4086 -x4087 -x4088 -x4089 -x4090 -x4091 -x4092 -x4093 -x4094 -x4095 -x4096 -x4097 -x4098 -x4099 -x4100 -x4101 -x4102 -x4103 -x4104 -x4105 -x4106 -x4107 -x4108 -x4109 -x4110 -x4111 -x4112 -x4113 -x4114 -x4115 -x4116 -x4117 -x4118 -x4119 -x4120 -x4121 -x4122 -x4123 -x4124 -x4125 -x4126 -x4127 -x4128 -x4129 -x4130 -x4131 -x4132 -x4133 -x4134 -x4135 -x4136 -x4137 -x4138 -x4139 -x4140 -x4141 -x4142 -x4143 -x4144 -x4145 -x4146 -x4147 -x4148 -x4149 -x4150 -x4151 -x4152 -x4153 -x4154 -x4155 -x4156 -x4157 -x4158 -x4159 -x4160 -x4161 -x4162 -x4163 -x4164 -x4165 -x4166 -x4167 -x4168 -x4169 -x4170 -x4171 -x4172 -x4173 -x4174 -x4175 -x4176 -x4177 -x4178 -x4179 -x4180 -x4181 -x4182 -x4183 -x4184 -x4185 -x4186 -x4187 -x4188 -x4189 -x4190 -x4191 -x4192 -x4193 -x4194 -x4195 -x4196 -x4197 -x4198 -x4199 -x4200 -x4201 -x4202 -x4203 -x4204 -x4205 -x4206 -x4207 -x4208 -x4209 -x4210 -x4211 -x4212 -x4213 -x4214 -x4215 -x4216 -x4217 -x4218 -x4219 -x4220 -x4221 -x4222 -x4223 -x4224 -x4225 -x4226 -x4227 -x4228 -x4229 -x4230 -x4231 -x4232 -x4233 -x4234 -x4235 -x4236 -x4237 -x4238 -x4239 -x4240 -x4241 -x4242 -x4243 -x4244 -x4245 -x4246 -x4247 -x4248 -x4249 -x4250 -x4251 -x4252 -x4253 -x4254 -x4255 -x4256 -x4257 -x4258 -x4259 -x4260 -x4261 -x4262 -x4263 -x4264 -x4265 -x4266 -x4267 -x4268 -x4269 -x4270 -x4271 -x4272 -x4273 -x4274 -x4275 -x4276 -x4277 -x4278 -x4279 -x4280 -x4281 -x4282 -x4283 -x4284 -x4285 -x4286 -x4287 -x4288 -x4289 -x4290 -x4291 -x4292 -x4293 -x4294 -x4295 -x4296 -x4297 -x4298 -x4299 -x4300 -x4301 -x4302 -x4303 -x4304 -x4305 -x4306 -x4307 -x4308 -x4309 -x4310 -x4311 -x4312 -x4313 -x4314 -x4315 -x4316 -x4317 -x4318 -x4319 -x4320 -x4321 -x4322 -x4323 -x4324 -x4325 -x4326 -x4327 -x4328 -x4329 -x4330 -x4331 -x4332 -x4333 -x4334 -x4335 -x4336 -x4337 -x4338 -x4339 -x4340 -x4341 -x4342 -x4343 -x4344 -x4345 -x4346 -x4347 -x4348 -x4349 -x4350 -x4351 -x4352 -x4353 -x4354 -x4355 -x4356 -x4357 -x4358 -x4359 -x4360 -x4361 -x4362 -x4363 -x4364 -x4365 -x4366 -x4367 -x4368 -x4369 -x4370 -x4371 -x4372 -x4373 -x4374 -x4375 -x4376 -x4377 -x4378 -x4379 -x4380 -x4381 -x4382 -x4383 -x4384 -x4385 -x4386 -x4387 -x4388 -x4389 -x4390 -x4391 -x4392 -x4393 -x4394 -x4395 -x4396 -x4397 -x4398 -x4399 -x4400 -x4401 -x4402 -x4403 -x4404 -x4405 -x4406 -x4407 -x4408 -x4409 -x4410 -x4411 -x4412 -x4413 -x4414 -x4415 -x4416 -x4417 -x4418 -x4419 -x4420 -x4421 -x4422 -x4423 -x4424 -x4425 -x4426 -x4427 -x4428 -x4429 -x4430 -x4431 -x4432 -x4433 -x4434 -x4435 -x4436 -x4437 -x4438 -x4439 -x4440 -x4441 -x4442 -x4443 -x4444 -x4445 -x4446 -x4447 -x4448 -x4449 -x4450 -x4451 -x4452 -x4453 -x4454 -x4455 -x4456 -x4457 -x4458 -x4459 -x4460 -x4461 -x4462 -x4463 -x4464 -x4465 -x4466 -x4467 -x4468 -x4469 -x4470 -x4471 -x4472 -x4473 -x4474 -x4475 -x4476 -x4477 -x4478 -x4479 -x4480 -x4481 -x4482 -x4483 -x4484 -x4485 -x4486 -x4487 -x4488 -x4489 -x4490 -x4491 -x4492 -x4493 -x4494 -x4495 -x4496 -x4497 -x4498 -x4499 -x4500 -x4501 -x4502 -x4503 -x4504 -x4505 -x4506 -x4507 -x4508 -x4509 -x4510 -x4511 -x4512 -x4513 -x4514 -x4515 -x4516 -x4517 -x4518 -x4519 -x4520 -x4521 -x4522 -x4523 -x4524 -x4525 -x4526 -x4527 -x4528 -x4529 -x4530 -x4531 -x4532 -x4533 -x4534 -x4535 -x4536 -x4537 -x4538 -x4539 -x4540 -x4541 -x4542 -x4543 -x4544 -x4545 -x4546 -x4547 -x4548 -x4549 -x4550 -x4551 -x4552 -x4553 -x4554 -x4555 -x4556 -x4557 -x4558 -x4559 -x4560 -x4561 -x4562 -x4563 -x4564 -x4565 -x4566 -x4567 -x4568 -x4569 -x4570 -x4571 -x4572 -x4573 -x4574 -x4575 -x4576 -x4577 -x4578 -x4579 -x4580 -x4581 -x4582 -x4583 -x4584 -x4585 -x4586 -x4587 -x4588 -x4589 -x4590 -x4591 -x4592 -x4593 -x4594 -x4595 -x4596 -x4597 -x4598 -x4599 -x4600 -x4601 -x4602 -x4603 -x4604 -x4605 -x4606 -x4607 -x4608 -x4609 -x4610 -x4611 -x4612 -x4613 -x4614 -x4615 -x4616 -x4617 -x4618 -x4619 -x4620 -x4621 -x4622 -x4623 -x4624 -x4625 -x4626 -x4627 -x4628 -x4629 -x4630 -x4631 -x4632 -x4633 -x4634 -x4635 -x4636 -x4637 -x4638 -x4639 -x4640 -x4641 -x4642 -x4643 -x4644 -x4645 -x4646 -x4647 -x4648 -x4649 -x4650 -x4651 -x4652 -x4653 -x4654 -x4655 -x4656 -x4657 -x4658 -x4659 -x4660 -x4661 -x4662 -x4663 -x4664 -x4665 -x4666 -x4667 -x4668 -x4669 -x4670 -x4671 -x4672 -x4673 -x4674 -x4675 -x4676 -x4677 -x4678 -x4679 -x4680 -x4681 -x4682 -x4683 -x4684 -x4685 -x4686 -x4687 -x4688 -x4689 -x4690 -x4691 -x4692 -x4693 -x4694 -x4695 -x4696 -x4697 -x4698 -x4699 -x4700 -x4701 -x4702 -x4703 -x4704 -x4705 -x4706 -x4707 -x4708 -x4709 -x4710 -x4711 -x4712 -x4713 -x4714 -x4715 -x4716 -x4717 -x4718 -x4719 -x4720 -x4721 -x4722 -x4723 -x4724 -x4725 -x4726 -x4727 -x4728 -x4729 -x4730 -x4731 -x4732 -x4733 -x4734 -x4735 -x4736 -x4737 -x4738 -x4739 -x4740 -x4741 -x4742 -x4743 -x4744 -x4745 -x4746 -x4747 -x4748 -x4749 -x4750 -x4751 -x4752 -x4753 -x4754 -x4755 -x4756 -x4757 -x4758 -x4759 -x4760 -x4761 -x4762 -x4763 -x4764 -x4765 -x4766 -x4767 -x4768 -x4769 -x4770 -x4771 -x4772 -x4773 -x4774 -x4775 -x4776 -x4777 -x4778 -x4779 -x4780 -x4781 -x4782 -x4783 -x4784 -x4785 -x4786 -x4787 -x4788 -x4789 -x4790 -x4791 -x4792 -x4793 -x4794 -x4795 -x4796 -x4797 -x4798 -x4799 -x4800 -x4801 -x4802 -x4803 -x4804 -x4805 -x4806 -x4807 -x4808 -x4809 -x4810 -x4811 -x4812 -x4813 -x4814 -x4815 -x4816 -x4817 -x4818 -x4819 -x4820 -x4821 -x4822 -x4823 -x4824 -x4825 -x4826 -x4827 -x4828 -x4829 -x4830 -x4831 -x4832 -x4833 -x4834 -x4835 -x4836 -x4837 -x4838 -x4839 -x4840 -x4841 -x4842 -x4843 -x4844 -x4845 -x4846 -x4847 -x4848 -x4849 -x4850 -x4851 -x4852 -x4853 -x4854 -x4855 -x4856 -x4857 -x4858 -x4859 -x4860 -x4861 -x4862 -x4863 -x4864 -x4865 -x4866 -x4867 -x4868 -x4869 -x4870 -x4871 -x4872 -x4873 -x4874 -x4875 -x4876 -x4877 -x4878 -x4879 -x4880 -x4881 -x4882 -x4883 -x4884 -x4885 -x4886 -x4887 -x4888 -x4889 -x4890 -x4891 -x4892 -x4893 -x4894 -x4895 -x4896 -x4897 -x4898 -x4899 -x4900 -x4901 -x4902 -x4903 -x4904 -x4905 -x4906 -x4907 -x4908 -x4909 -x4910 -x4911 -x4912 -x4913 -x4914 -x4915 -x4916 -x4917 -x4918 -x4919 -x4920 -x4921 -x4922 -x4923 -x4924 -x4925 -x4926 -x4927 -x4928 -x4929 -x4930 -x4931 -x4932 -x4933 -x4934 -x4935 -x4936 -x4937 -x4938 -x4939 -x4940 -x4941 -x4942 -x4943 -x4944 -x4945 -x4946 -x4947 -x4948 -x4949 -x4950 -x4951 -x4952 -x4953 -x4954 -x4955 -x4956 -x4957 -x4958 -x4959 -x4960 -x4961 -x4962 -x4963 -x4964 -x4965 -x4966 -x4967 -x4968 -x4969 -x4970 -x4971 -x4972 -x4973 -x4974 -x4975 -x4976 -x4977 -x4978 -x4979 -x4980 -x4981 -x4982 -x4983 -x4984 -x4985 -x4986 -x4987 -x4988 -x4989 -x4990 -x4991 -x4992 -x4993 -x4994 -x4995 -x4996 -x4997 -x4998 -x4999 -x5000 -x5001 -x5002 -x5003 -x5004 -x5005 -x5006 -x5007 -x5008 -x5009 -x5010 -x5011 -x5012 -x5013 -x5014 -x5015 -x5016 -x5017 -x5018 -x5019 -x5020 -x5021 -x5022 -x5023 -x5024 -x5025 -x5026 -x5027 -x5028 -x5029 -x5030 -x5031 -x5032 -x5033 -x5034 -x5035 -x5036 -x5037 -x5038 -x5039 -x5040 -x5041 -x5042 -x5043 -x5044 -x5045 -x5046 -x5047 -x5048 -x5049 -x5050 -x5051 -x5052 -x5053 -x5054 -x5055 -x5056 -x5057 -x5058 -x5059 -x5060 -x5061 -x5062 -x5063 -x5064 -x5065 -x5066 -x5067 -x5068 -x5069 -x5070 -x5071 -x5072 -x5073 -x5074 -x5075 -x5076 -x5077 -x5078 -x5079 -x5080 -x5081 -x5082 -x5083 -x5084 -x5085 -x5086 -x5087 -x5088 -x5089 -x5090 -x5091 -x5092 -x5093 -x5094 -x5095 -x5096 -x5097 -x5098 -x5099 -x5100 -x5101 -x5102 -x5103 -x5104 -x5105 -x5106 -x5107 -x5108 -x5109 -x5110 -x5111 -x5112 -x5113 -x5114 -x5115 -x5116 -x5117 -x5118 -x5119 -x5120 -x5121 -x5122 -x5123 -x5124 -x5125 -x5126 -x5127 -x5128 -x5129 -x5130 -x5131 -x5132 -x5133 -x5134 -x5135 -x5136 -x5137 -x5138 -x5139 -x5140 -x5141 -x5142 -x5143 -x5144 -x5145 -x5146 -x5147 -x5148 -x5149 -x5150 -x5151 -x5152 -x5153 -x5154 -x5155 -x5156 -x5157 -x5158 -x5159 -x5160 -x5161 -x5162 -x5163 -x5164 -x5165 -x5166 -x5167 -x5168 -x5169 -x5170 -x5171 -x5172 -x5173 -x5174 -x5175 -x5176 -x5177 -x5178 -x5179 -x5180 -x5181 -x5182 -x5183 -x5184 -x5185 -x5186 -x5187 -x5188 -x5189 -x5190 -x5191 -x5192 -x5193 -x5194 -x5195 -x5196 -x5197 -x5198 -x5199 -x5200 -x5201 -x5202 -x5203 -x5204 -x5205 -x5206 -x5207 -x5208 -x5209 -x5210 -x5211 -x5212 -x5213 -x5214 -x5215 -x5216 -x5217 -x5218 -x5219 -x5220 -x5221 -x5222 -x5223 -x5224 -x5225 -x5226 -x5227 -x5228 -x5229 -x5230 -x5231 -x5232 -x5233 -x5234 -x5235 -x5236 -x5237 -x5238 -x5239 -x5240 -x5241 -x5242 -x5243 -x5244 -x5245 -x5246 -x5247 -x5248 -x5249 -x5250 -x5251 -x5252 -x5253 -x5254 -x5255 -x5256 -x5257 -x5258 -x5259 -x5260 -x5261 -x5262 -x5263 -x5264 -x5265 -x5266 -x5267 -x5268 -x5269 -x5270 -x5271 -x5272 -x5273 -x5274 -x5275 -x5276 -x5277 -x5278 -x5279 -x5280 -x5281 -x5282 -x5283 -x5284 -x5285 -x5286 -x5287 -x5288 -x5289 -x5290 -x5291 -x5292 -x5293 -x5294 -x5295 -x5296 -x5297 -x5298 -x5299 -x5300 -x5301 -x5302 -x5303 -x5304 -x5305 -x5306 -x5307 -x5308 -x5309 -x5310 -x5311 -x5312 -x5313 -x5314 -x5315 -x5316 -x5317 -x5318 -x5319 -x5320 -x5321 -x5322 -x5323 -x5324 -x5325 -x5326 -x5327 -x5328 -x5329 -x5330 -x5331 -x5332 -x5333 -x5334 -x5335 -x5336 -x5337 -x5338 -x5339 -x5340 -x5341 -x5342 -x5343 -x5344 -x5345 -x5346 -x5347 -x5348 -x5349 -x5350 -x5351 -x5352 -x5353 -x5354 -x5355 -x5356 -x5357 -x5358 -x5359 -x5360 -x5361 -x5362 -x5363 -x5364 -x5365 -x5366 -x5367 -x5368 -x5369 -x5370 -x5371 -x5372 -x5373 -x5374 -x5375 -x5376 -x5377 -x5378 -x5379 -x5380 -x5381 -x5382 -x5383 -x5384 -x5385 -x5386 -x5387 -x5388 -x5389 -x5390 -x5391 -x5392 -x5393 -x5394 -x5395 -x5396 -x5397 -x5398 -x5399 -x5400 -x5401 -x5402 -x5403 -x5404 -x5405 -x5406 -x5407 -x5408 -x5409 -x5410 -x5411 -x5412 -x5413 -x5414 -x5415 -x5416 -x5417 -x5418 -x5419 -x5420 -x5421 -x5422 -x5423 -x5424 -x5425 -x5426 -x5427 -x5428 -x5429 -x5430 -x5431 -x5432 -x5433 -x5434 -x5435 -x5436 -x5437 -x5438 -x5439 -x5440 -x5441 -x5442 -x5443 -x5444 -x5445 -x5446 -x5447 -x5448 -x5449 -x5450 -x5451 -x5452 -x5453 -x5454 -x5455 -x5456 -x5457 -x5458 -x5459 -x5460 -x5461 -x5462 -x5463 -x5464 -x5465 -x5466 -x5467 -x5468 -x5469 -x5470 -x5471 -x5472 -x5473 -x5474 -x5475 -x5476 -x5477 -x5478 -x5479 -x5480 -x5481 -x5482 -x5483 -x5484 -x5485 -x5486 -x5487 -x5488 -x5489 -x5490 -x5491 -x5492 -x5493 -x5494 -x5495 -x5496 -x5497 -x5498 -x5499 -x5500 -x5501 -x5502 -x5503 -x5504 -x5505 -x5506 -x5507 -x5508 -x5509 -x5510 -x5511 -x5512 -x5513 -x5514 -x5515 -x5516 -x5517 -x5518 -x5519 -x5520 -x5521 -x5522 -x5523 -x5524 -x5525 -x5526 -x5527 -x5528 -x5529 -x5530 -x5531 -x5532 -x5533 -x5534 -x5535 -x5536 -x5537 -x5538 -x5539 -x5540 -x5541 -x5542 -x5543 -x5544 -x5545 -x5546 -x5547 -x5548 -x5549 -x5550 -x5551 -x5552 -x5553 -x5554 -x5555 -x5556 -x5557 -x5558 -x5559 -x5560 -x5561 -x5562 -x5563 -x5564 -x5565 -x5566 -x5567 -x5568 -x5569 -x5570 -x5571 -x5572 -x5573 -x5574 -x5575 -x5576 -x5577 -x5578 -x5579 -x5580 -x5581 -x5582 -x5583 -x5584 -x5585 -x5586 -x5587 -x5588 -x5589 -x5590 -x5591 -x5592 -x5593 -x5594 -x5595 -x5596 -x5597 -x5598 -x5599 -x5600 -x5601 -x5602 -x5603 -x5604 -x5605 -x5606 -x5607 -x5608 -x5609 -x5610 -x5611 -x5612 -x5613 -x5614 -x5615 -x5616 -x5617 -x5618 -x5619 -x5620 -x5621 -x5622 -x5623 -x5624 -x5625 -x5626 -x5627 -x5628 -x5629 -x5630 -x5631 -x5632 -x5633 -x5634 -x5635 -x5636 -x5637 -x5638 -x5639 -x5640 -x5641 -x5642 -x5643 -x5644 -x5645 -x5646 -x5647 -x5648 -x5649 -x5650 -x5651 -x5652 -x5653 -x5654 -x5655 -x5656 -x5657 -x5658 -x5659 -x5660 -x5661 -x5662 -x5663 -x5664 -x5665 -x5666 -x5667 -x5668 -x5669 -x5670 -x5671 -x5672 -x5673 -x5674 -x5675 -x5676 -x5677 -x5678 -x5679 -x5680 -x5681 -x5682 -x5683 -x5684 -x5685 -x5686 -x5687 -x5688 -x5689 -x5690 -x5691 -x5692 -x5693 -x5694 -x5695 -x5696 -x5697 -x5698 -x5699 -x5700 -x5701 -x5702 -x5703 -x5704 -x5705 -x5706 -x5707 -x5708 -x5709 -x5710 -x5711 -x5712 -x5713 -x5714 -x5715 -x5716 -x5717 -x5718 -x5719 -x5720 -x5721 -x5722 -x5723 -x5724 -x5725 -x5726 -x5727 -x5728 -x5729 -x5730 -x5731 -x5732 -x5733 -x5734 -x5735 -x5736 -x5737 -x5738 -x5739 -x5740 -x5741 -x5742 -x5743 -x5744 -x5745 -x5746 -x5747 -x5748 -x5749 -x5750 -x5751 -x5752 -x5753 -x5754 -x5755 -x5756 -x5757 -x5758 -x5759 -x5760 -x5761 -x5762 -x5763 -x5764 -x5765 -x5766 -x5767 -x5768 -x5769 -x5770 -x5771 -x5772 -x5773 -x5774 -x5775 -x5776 -x5777 -x5778 -x5779 -x5780 -x5781 -x5782 -x5783 -x5784 -x5785 -x5786 -x5787 -x5788 -x5789 -x5790 -x5791 -x5792 -x5793 -x5794 -x5795 -x5796 -x5797 -x5798 -x5799 -x5800 -x5801 -x5802 -x5803 -x5804 -x5805 -x5806 -x5807 -x5808 -x5809 -x5810 -x5811 -x5812 -x5813 -x5814 -x5815 -x5816 -x5817 -x5818 -x5819 -x5820 -x5821 -x5822 -x5823 -x5824 -x5825 -x5826 -x5827 -x5828 -x5829 -x5830 -x5831 -x5832 -x5833 -x5834 -x5835 -x5836 -x5837 -x5838 -x5839 -x5840 -x5841 -x5842 -x5843 -x5844 -x5845 -x5846 -x5847 -x5848 -x5849 -x5850 -x5851 -x5852 -x5853 -x5854 -x5855 -x5856 -x5857 -x5858 -x5859 -x5860 -x5861 -x5862 -x5863 -x5864 -x5865 -x5866 -x5867 -x5868 -x5869 -x5870 -x5871 -x5872 -x5873 -x5874 -x5875 -x5876 -x5877 -x5878 -x5879 -x5880 -x5881 -x5882 -x5883 -x5884 -x5885 -x5886 -x5887 -x5888 -x5889 -x5890 -x5891 -x5892 -x5893 -x5894 -x5895 -x5896 -x5897 -x5898 -x5899 -x5900 -x5901 -x5902 -x5903 -x5904 -x5905 -x5906 -x5907 -x5908 -x5909 -x5910 -x5911 -x5912 -x5913 -x5914 -x5915 -x5916 -x5917 -x5918 -x5919 -x5920 -x5921 -x5922 -x5923 -x5924 -x5925 -x5926 -x5927 -x5928 -x5929 -x5930 -x5931 -x5932 -x5933 -x5934 -x5935 -x5936 -x5937 -x5938 -x5939 -x5940 -x5941 -x5942 -x5943 -x5944 -x5945 -x5946 -x5947 -x5948 -x5949 -x5950 -x5951 -x5952 -x5953 -x5954 -x5955 -x5956 -x5957 -x5958 -x5959 -x5960 -x5961 -x5962 -x5963 -x5964 -x5965 -x5966 -x5967 -x5968 -x5969 -x5970 -x5971 -x5972 -x5973 -x5974 -x5975 -x5976 -x5977 -x5978 -x5979 -x5980 -x5981 -x5982 -x5983 -x5984 -x5985 -x5986 -x5987 -x5988 -x5989 -x5990 -x5991 -x5992 -x5993 -x5994 -x5995 -x5996 -x5997 -x5998 -x5999 -x6000 -x6001 -x6002 -x6003 -x6004 -x6005 -x6006 -x6007 -x6008 -x6009 -x6010 -x6011 -x6012 -x6013 -x6014 -x6015 -x6016 -x6017 -x6018 -x6019 -x6020 -x6021 -x6022 -x6023 -x6024 -x6025 -x6026 -x6027 -x6028 -x6029 -x6030 -x6031 -x6032 -x6033 -x6034 -x6035 -x6036 -x6037 -x6038 -x6039 -x6040 -x6041 -x6042 -x6043 -x6044 -x6045 -x6046 -x6047 -x6048 -x6049 -x6050 -x6051 -x6052 -x6053 -x6054 -x6055 -x6056 -x6057 -x6058 -x6059 -x6060 -x6061 -x6062 -x6063 -x6064 -x6065 -x6066 -x6067 -x6068 -x6069 -x6070 -x6071 -x6072 -x6073 -x6074 -x6075 -x6076 -x6077 -x6078 -x6079 -x6080 -x6081 -x6082 -x6083 -x6084 -x6085 -x6086 -x6087 -x6088 -x6089 -x6090 -x6091 -x6092 -x6093 -x6094 -x6095 -x6096 -x6097 -x6098 -x6099 -x6100 -x6101 -x6102 -x6103 -x6104 -x6105 -x6106 -x6107 -x6108 -x6109 -x6110 -x6111 -x6112 -x6113 -x6114 -x6115 -x6116 -x6117 -x6118 -x6119 -x6120 -x6121 -x6122 -x6123 -x6124 -x6125 -x6126 -x6127 -x6128 -x6129 -x6130 -x6131 -x6132 -x6133 -x6134 -x6135 -x6136 -x6137 -x6138 -x6139 -x6140 -x6141 -x6142 -x6143 -x6144 -x6145 -x6146 -x6147 -x6148 -x6149 -x6150 -x6151 -x6152 -x6153 -x6154 -x6155 -x6156 -x6157 -x6158 -x6159 -x6160 -x6161 -x6162 -x6163 -x6164 -x6165 -x6166 -x6167 -x6168 -x6169 -x6170 -x6171 -x6172 -x6173 -x6174 -x6175 -x6176 -x6177 -x6178 -x6179 -x6180 -x6181 -x6182 -x6183 -x6184 -x6185 -x6186 -x6187 -x6188 -x6189 -x6190 -x6191 -x6192 -x6193 -x6194 -x6195 -x6196 -x6197 -x6198 -x6199 -x6200 -x6201 -x6202 -x6203 -x6204 -x6205 -x6206 -x6207 -x6208 -x6209 -x6210 -x6211 -x6212 -x6213 -x6214 -x6215 -x6216 -x6217 -x6218 -x6219 -x6220 -x6221 -x6222 -x6223 -x6224 -x6225 -x6226 -x6227 -x6228 -x6229 -x6230 -x6231 -x6232 -x6233 -x6234 -x6235 -x6236 -x6237 -x6238 -x6239 -x6240 -x6241 -x6242 -x6243 -x6244 -x6245 -x6246 -x6247 -x6248 -x6249 -x6250 -x6251 -x6252 -x6253 -x6254 -x6255 -x6256 -x6257 -x6258 -x6259 -x6260 -x6261 -x6262 -x6263 -x6264 -x6265 -x6266 -x6267 -x6268 -x6269 -x6270 -x6271 -x6272 -x6273 -x6274 -x6275 -x6276 -x6277 -x6278 -x6279 -x6280 -x6281 -x6282 -x6283 -x6284 -x6285 -x6286 -x6287 -x6288 -x6289 -x6290 -x6291 -x6292 -x6293 -x6294 -x6295 -x6296 -x6297 -x6298 -x6299 -x6300 -x6301 -x6302 -x6303 -x6304 -x6305 -x6306 -x6307 -x6308 -x6309 -x6310 -x6311 -x6312 -x6313 -x6314 -x6315 -x6316 -x6317 -x6318 -x6319 -x6320 -x6321 -x6322 -x6323 -x6324 -x6325 -x6326 -x6327 -x6328 -x6329 -x6330 -x6331 -x6332 -x6333 -x6334 -x6335 -x6336 -x6337 -x6338 -x6339 -x6340 -x6341 -x6342 -x6343 -x6344 -x6345 -x6346 -x6347 -x6348 -x6349 -x6350 -x6351 -x6352 -x6353 -x6354 -x6355 -x6356 -x6357 -x6358 -x6359 -x6360 -x6361 -x6362 -x6363 -x6364 -x6365 -x6366 -x6367 -x6368 -x6369 -x6370 -x6371 -x6372 -x6373 -x6374 -x6375 -x6376 -x6377 -x6378 -x6379 -x6380 -x6381 -x6382 -x6383 -x6384 -x6385 -x6386 -x6387 -x6388 -x6389 -x6390 -x6391 -x6392 -x6393 -x6394 -x6395 -x6396 -x6397 -x6398 -x6399 -x6400 -x6401 -x6402 -x6403 -x6404 -x6405 -x6406 -x6407 -x6408 -x6409 -x6410 -x6411 -x6412 -x6413 -x6414 -x6415 -x6416 -x6417 -x6418 -x6419 -x6420 -x6421 -x6422 -x6423 -x6424 -x6425 -x6426 -x6427 -x6428 -x6429 -x6430 -x6431 -x6432 -x6433 -x6434 -x6435 -x6436 -x6437 -x6438 -x6439 -x6440 -x6441 -x6442 -x6443 -x6444 -x6445 -x6446 -x6447 -x6448 -x6449 -x6450 -x6451 -x6452 -x6453 -x6454 -x6455 -x6456 -x6457 -x6458 -x6459 -x6460 -x6461 -x6462 -x6463 -x6464 -x6465 -x6466 -x6467 -x6468 -x6469 -x6470 -x6471 -x6472 -x6473 -x6474 -x6475 -x6476 -x6477 -x6478 -x6479 -x6480 -x6481 -x6482 -x6483 -x6484 -x6485 -x6486 -x6487 -x6488 -x6489 -x6490 -x6491 -x6492 -x6493 -x6494 -x6495 -x6496 -x6497 -x6498 -x6499 -x6500 -x6501 -x6502 -x6503 -x6504 -x6505 -x6506 -x6507 -x6508 -x6509 -x6510 -x6511 -x6512 -x6513 -x6514 -x6515 -x6516 -x6517 -x6518 -x6519 -x6520 -x6521 -x6522 -x6523 -x6524 -x6525 -x6526 -x6527 -x6528 -x6529 -x6530 -x6531 -x6532 -x6533 -x6534 -x6535 -x6536 -x6537 -x6538 -x6539 -x6540 -x6541 -x6542 -x6543 -x6544 -x6545 -x6546 -x6547 -x6548 -x6549 -x6550 -x6551 -x6552 -x6553 -x6554 -x6555 -x6556 -x6557 -x6558 -x6559 -x6560 -x6561 -x6562 -x6563 -x6564 -x6565 -x6566 -x6567 -x6568 -x6569 -x6570 -x6571 -x6572 -x6573 -x6574 -x6575 -x6576 -x6577 -x6578 -x6579 -x6580 -x6581 -x6582 -x6583 -x6584 -x6585 -x6586 -x6587 -x6588 -x6589 -x6590 -x6591 -x6592 -x6593 -x6594 -x6595 -x6596 -x6597 -x6598 -x6599 -x6600 -x6601 -x6602 -x6603 -x6604 -x6605 -x6606 -x6607 -x6608 -x6609 -x6610 -x6611 -x6612 -x6613 -x6614 -x6615 -x6616 -x6617 -x6618 -x6619 -x6620 -x6621 -x6622 -x6623 -x6624 -x6625 -x6626 -x6627 -x6628 -x6629 -x6630 -x6631 -x6632 -x6633 -x6634 -x6635 -x6636 -x6637 -x6638 -x6639 -x6640 -x6641 -x6642 -x6643 -x6644 -x6645 -x6646 -x6647 -x6648 -x6649 -x6650 -x6651 -x6652 -x6653 -x6654 -x6655 -x6656 -x6657 -x6658 -x6659 -x6660 -x6661 -x6662 -x6663 -x6664 -x6665 -x6666 -x6667 -x6668 -x6669 -x6670 -x6671 -x6672 -x6673 -x6674 -x6675 -x6676 -x6677 -x6678 -x6679 -x6680 -x6681 -x6682 -x6683 -x6684 -x6685 -x6686 -x6687 -x6688 -x6689 -x6690 -x6691 -x6692 -x6693 -x6694 -x6695 -x6696 -x6697 -x6698 -x6699 -x6700 -x6701 -x6702 -x6703 -x6704 -x6705 -x6706 -x6707 -x6708 -x6709 -x6710 -x6711 -x6712 -x6713 -x6714 -x6715 -x6716 -x6717 -x6718 -x6719 -x6720 -x6721 -x6722 -x6723 -x6724 -x6725 -x6726 -x6727 -x6728 -x6729 -x6730 -x6731 -x6732 -x6733 -x6734 -x6735 -x6736 -x6737 -x6738 -x6739 -x6740 -x6741 -x6742 -x6743 -x6744 -x6745 -x6746 -x6747 -x6748 -x6749 -x6750 -x6751 -x6752 -x6753 -x6754 -x6755 -x6756 -x6757 -x6758 -x6759 -x6760 -x6761 -x6762 -x6763 -x6764 -x6765 -x6766 -x6767 -x6768 -x6769 -x6770 -x6771 -x6772 -x6773 -x6774 -x6775 -x6776 -x6777 -x6778 -x6779 -x6780 -x6781 -x6782 -x6783 -x6784 -x6785 -x6786 -x6787 -x6788 -x6789 -x6790 -x6791 -x6792 -x6793 -x6794 -x6795 -x6796 -x6797 -x6798 -x6799 -x6800 -x6801 -x6802 -x6803 -x6804 -x6805 -x6806 -x6807 -x6808 -x6809 -x6810 -x6811 -x6812 -x6813 -x6814 -x6815 -x6816 -x6817 -x6818 -x6819 -x6820 -x6821 -x6822 -x6823 -x6824 -x6825 -x6826 -x6827 -x6828 -x6829 -x6830 -x6831 -x6832 -x6833 -x6834 -x6835 -x6836 -x6837 -x6838 -x6839 -x6840 -x6841 -x6842 -x6843 -x6844 -x6845 -x6846 -x6847 -x6848 -x6849 -x6850 -x6851 -x6852 -x6853 -x6854 -x6855 -x6856 -x6857 -x6858 -x6859 -x6860 -x6861 -x6862 -x6863 -x6864 -x6865 -x6866 -x6867 -x6868 -x6869 -x6870 -x6871 -x6872 -x6873 -x6874 -x6875 -x6876 -x6877 -x6878 -x6879 -x6880 -x6881 -x6882 -x6883 -x6884 -x6885 -x6886 -x6887 -x6888 -x6889 -x6890 -x6891 -x6892 -x6893 -x6894 -x6895 -x6896 -x6897 -x6898 -x6899 -x6900 -x6901 -x6902 -x6903 -x6904 -x6905 -x6906 -x6907 -x6908 -x6909 -x6910 -x6911 -x6912 -x6913 -x6914 -x6915 -x6916 -x6917 -x6918 -x6919 -x6920 -x6921 -x6922 -x6923 -x6924 -x6925 -x6926 -x6927 -x6928 -x6929 -x6930 -x6931 -x6932 -x6933 -x6934 -x6935 -x6936 -x6937 -x6938 -x6939 -x6940 -x6941 -x6942 -x6943 -x6944 -x6945 -x6946 -x6947 -x6948 -x6949 -x6950 -x6951 -x6952 -x6953 -x6954 -x6955 -x6956 -x6957 -x6958 -x6959 -x6960 -x6961 -x6962 -x6963 -x6964 -x6965 -x6966 -x6967 -x6968 -x6969 -x6970 -x6971 -x6972 -x6973 -x6974 -x6975 -x6976 -x6977 -x6978 -x6979 -x6980 -x6981 -x6982 -x6983 -x6984 -x6985 -x6986 -x6987 -x6988 -x6989 -x6990 -x6991 -x6992 -x6993 -x6994 -x6995 -x6996 -x6997 -x6998 -x6999 -x7000 -x7001 -x7002 -x7003 -x7004 -x7005 -x7006 -x7007 -x7008 -x7009 -x7010 -x7011 -x7012 -x7013 -x7014 -x7015 -x7016 -x7017 -x7018 -x7019 -x7020 -x7021 -x7022 -x7023 -x7024 -x7025 -x7026 -x7027 -x7028 -x7029 -x7030 -x7031 -x7032 -x7033 -x7034 -x7035 -x7036 -x7037 -x7038 -x7039 -x7040 -x7041 -x7042 -x7043 -x7044 -x7045 -x7046 -x7047 -x7048 -x7049 -x7050 -x7051 -x7052 -x7053 -x7054 -x7055 -x7056 -x7057 -x7058 -x7059 -x7060 -x7061 -x7062 -x7063 -x7064 -x7065 -x7066 -x7067 -x7068 -x7069 -x7070 -x7071 -x7072 -x7073 -x7074 -x7075 -x7076 -x7077 -x7078 -x7079 -x7080 -x7081 -x7082 -x7083 -x7084 -x7085 -x7086 -x7087 -x7088 -x7089 -x7090 -x7091 -x7092 -x7093 -x7094 -x7095 -x7096 -x7097 -x7098 -x7099 -x7100 -x7101 -x7102 -x7103 -x7104 -x7105 -x7106 -x7107 -x7108 -x7109 -x7110 -x7111 -x7112 -x7113 -x7114 -x7115 -x7116 -x7117 -x7118 -x7119 -x7120 -x7121 -x7122 -x7123 -x7124 -x7125 -x7126 -x7127 -x7128 -x7129 -x7130 -x7131 -x7132 -x7133 -x7134 -x7135 -x7136 -x7137 -x7138 -x7139 -x7140 -x7141 -x7142 -x7143 -x7144 -x7145 -x7146 -x7147 -x7148 -x7149 -x7150 -x7151 -x7152 -x7153 -x7154 -x7155 -x7156 -x7157 -x7158 -x7159 -x7160 -x7161 -x7162 -x7163 -x7164 -x7165 -x7166 -x7167 -x7168 -x7169 -x7170 -x7171 -x7172 -x7173 -x7174 -x7175 -x7176 -x7177 -x7178 -x7179 -x7180 -x7181 -x7182 -x718#### 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.28 0.06 0.02 2/54 28632
Raw data (stat): 28632 (runsolver) R 28631 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487453497 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99974 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 10101 0 0 0 973 25 0 0 25 0 1 0 487453497 44318720 9769 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10820 9769 603 41 0 10779 0
vsize: 43280
[startup+20.0003 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 10148 0 0 0 1972 25 0 0 25 0 1 0 487453497 44453888 9816 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10853 9816 603 41 0 10812 0
vsize: 43412
[startup+30.0008 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 16019 0 0 0 2958 39 0 0 25 0 1 0 487453497 56680448 12688 4294967295 134512640 134672761 3221224576 3221222848 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13838 12688 603 41 0 13797 0
vsize: 55352
[startup+40.0014 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 41886 0 0 0 3901 96 0 0 25 0 1 0 487453497 164360192 33926 4294967295 134512640 134672761 3221224576 3221219504 134566676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40127 33926 603 41 0 40086 0
vsize: 160508
[startup+50.0017 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 46895 0 0 0 4890 107 0 0 25 0 1 0 487453497 190664704 38935 4294967295 134512640 134672761 3221224576 3221223724 1074754691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46549 38935 603 41 0 46508 0
vsize: 186196
[startup+60.0018 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 46923 0 0 0 5889 108 0 0 25 0 1 0 487453497 190799872 38963 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46582 38963 603 41 0 46541 0
vsize: 186328
[startup+70.0025 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49206 0 0 0 6883 114 0 0 25 0 1 0 487453497 191725568 39114 4294967295 134512640 134672761 3221224576 3221223280 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46808 39114 603 41 0 46767 0
vsize: 187232
[startup+80.003 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 7881 117 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+90.0045 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 8880 117 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+100.005 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 9880 117 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+110.005 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 10880 118 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+120.007 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 11880 118 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223792 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+130.006 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49847 0 0 0 12880 118 0 0 25 0 1 0 487453497 193437696 39733 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39733 603 41 0 47185 0
vsize: 188904
[startup+140.007 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49852 0 0 0 13879 119 0 0 25 0 1 0 487453497 193437696 39738 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39738 603 41 0 47185 0
vsize: 188904
[startup+150.008 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49852 0 0 0 14879 119 0 0 25 0 1 0 487453497 193437696 39738 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39738 603 41 0 47185 0
vsize: 188904
[startup+160.009 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49852 0 0 0 15879 119 0 0 25 0 1 0 487453497 193437696 39738 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39738 603 41 0 47185 0
vsize: 188904
[startup+170.009 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49853 0 0 0 16879 120 0 0 25 0 1 0 487453497 193437696 39739 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39739 603 41 0 47185 0
vsize: 188904
[startup+180.009 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49857 0 0 0 17878 120 0 0 25 0 1 0 487453497 193437696 39743 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39743 603 41 0 47185 0
vsize: 188904
[startup+190.01 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49857 0 0 0 18878 121 0 0 25 0 1 0 487453497 193437696 39743 4294967295 134512640 134672761 3221224576 3221223784 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39743 603 41 0 47185 0
vsize: 188904
[startup+200.011 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49857 0 0 0 19878 121 0 0 25 0 1 0 487453497 193437696 39743 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39743 603 41 0 47185 0
vsize: 188904
[startup+210.011 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 49858 0 0 0 20877 122 0 0 25 0 1 0 487453497 193437696 39744 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47226 39744 603 41 0 47185 0
vsize: 188904
[startup+220.013 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50377 0 0 0 21876 123 0 0 25 0 1 0 487453497 195604480 40263 4294967295 134512640 134672761 3221224576 3221223680 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47755 40263 603 41 0 47714 0
vsize: 191020
[startup+230.012 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50688 0 0 0 22874 125 0 0 25 0 1 0 487453497 196923392 40574 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40574 603 41 0 48036 0
vsize: 192308
[startup+240.013 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50688 0 0 0 23874 125 0 0 25 0 1 0 487453497 196923392 40574 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40574 603 41 0 48036 0
vsize: 192308
[startup+250.014 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50688 0 0 0 24874 126 0 0 25 0 1 0 487453497 196923392 40574 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40574 603 41 0 48036 0
vsize: 192308
[startup+260.013 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50707 0 0 0 25874 126 0 0 25 0 1 0 487453497 196923392 40593 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40593 603 41 0 48036 0
vsize: 192308
[startup+270.014 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50710 0 0 0 26874 126 0 0 25 0 1 0 487453497 196923392 40596 4294967295 134512640 134672761 3221224576 3221223748 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40596 603 41 0 48036 0
vsize: 192308
[startup+280.014 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50711 0 0 0 27873 127 0 0 25 0 1 0 487453497 196923392 40597 4294967295 134512640 134672761 3221224576 3221223760 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48077 40597 603 41 0 48036 0
vsize: 192308
[startup+290.015 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50717 0 0 0 28873 127 0 0 25 0 1 0 487453497 197058560 40603 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48110 40603 603 41 0 48069 0
vsize: 192440
[startup+300.019 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 50883 0 0 0 29873 128 0 0 25 0 1 0 487453497 197738496 40769 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48276 40769 603 41 0 48235 0
vsize: 193104
[startup+310.02 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53729 0 0 0 30865 136 0 0 25 0 1 0 487453497 197873664 40831 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40831 603 41 0 48268 0
vsize: 193236
[startup+320.02 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53729 0 0 0 31865 136 0 0 25 0 1 0 487453497 197873664 40831 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40831 603 41 0 48268 0
vsize: 193236
[startup+330.021 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53729 0 0 0 32865 136 0 0 25 0 1 0 487453497 197873664 40831 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40831 603 41 0 48268 0
vsize: 193236
[startup+340.021 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53729 0 0 0 33864 137 0 0 25 0 1 0 487453497 197873664 40831 4294967295 134512640 134672761 3221224576 3221223768 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40831 603 41 0 48268 0
vsize: 193236
[startup+350.022 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53729 0 0 0 34864 137 0 0 25 0 1 0 487453497 197873664 40831 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40831 603 41 0 48268 0
vsize: 193236
[startup+360.022 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 35864 137 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+370.023 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 36864 138 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+380.022 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 37863 138 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+390.024 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 38863 138 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+400.024 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 39863 139 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+410.024 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53730 0 0 0 40863 139 0 0 25 0 1 0 487453497 197873664 40832 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48309 40832 603 41 0 48268 0
vsize: 193236
[startup+420.025 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53744 0 0 0 41863 139 0 0 25 0 1 0 487453497 198008832 40846 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48342 40846 603 41 0 48301 0
vsize: 193368
[startup+430.025 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53755 0 0 0 42863 139 0 0 25 0 1 0 487453497 198008832 40857 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48342 40857 603 41 0 48301 0
vsize: 193368
[startup+440.026 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53757 0 0 0 43863 139 0 0 25 0 1 0 487453497 198008832 40859 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48342 40859 603 41 0 48301 0
vsize: 193368
[startup+450.026 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53768 0 0 0 44863 139 0 0 25 0 1 0 487453497 198144000 40870 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40870 603 41 0 48334 0
vsize: 193500
[startup+460.027 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53775 0 0 0 45863 140 0 0 25 0 1 0 487453497 198144000 40877 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40877 603 41 0 48334 0
vsize: 193500
[startup+470.027 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53781 0 0 0 46862 140 0 0 25 0 1 0 487453497 198144000 40883 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40883 603 41 0 48334 0
vsize: 193500
[startup+480.028 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53785 0 0 0 47862 140 0 0 25 0 1 0 487453497 198144000 40887 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40887 603 41 0 48334 0
vsize: 193500
[startup+490.028 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53785 0 0 0 48862 141 0 0 25 0 1 0 487453497 198144000 40887 4294967295 134512640 134672761 3221224576 3221223748 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40887 603 41 0 48334 0
vsize: 193500
[startup+500.029 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53786 0 0 0 49862 141 0 0 25 0 1 0 487453497 198144000 40888 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40888 603 41 0 48334 0
vsize: 193500
[startup+510.029 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53786 0 0 0 50862 141 0 0 25 0 1 0 487453497 198144000 40888 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40888 603 41 0 48334 0
vsize: 193500
[startup+520.03 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 53791 0 0 0 51861 142 0 0 25 0 1 0 487453497 198144000 40893 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48375 40893 603 41 0 48334 0
vsize: 193500
[startup+530.03 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54302 0 0 0 52860 143 0 0 25 0 1 0 487453497 200282112 41404 4294967295 134512640 134672761 3221224576 3221223824 134562579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41404 603 41 0 48856 0
vsize: 195588
[startup+540.032 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54303 0 0 0 53861 143 0 0 25 0 1 0 487453497 200282112 41405 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41405 603 41 0 48856 0
vsize: 195588
[startup+550.032 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54303 0 0 0 54860 144 0 0 25 0 1 0 487453497 200282112 41405 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41405 603 41 0 48856 0
vsize: 195588
[startup+560.032 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54306 0 0 0 55860 144 0 0 25 0 1 0 487453497 200282112 41408 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41408 603 41 0 48856 0
vsize: 195588
[startup+570.033 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54306 0 0 0 56860 144 0 0 25 0 1 0 487453497 200282112 41408 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41408 603 41 0 48856 0
vsize: 195588
[startup+580.034 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54310 0 0 0 57860 144 0 0 25 0 1 0 487453497 200282112 41412 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41412 603 41 0 48856 0
vsize: 195588
[startup+590.034 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54312 0 0 0 58859 145 0 0 25 0 1 0 487453497 200282112 41414 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41414 603 41 0 48856 0
vsize: 195588
[startup+600.035 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54320 0 0 0 59859 145 0 0 25 0 1 0 487453497 200282112 41422 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48897 41422 603 41 0 48856 0
vsize: 195588
[startup+610.035 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54342 0 0 0 60859 146 0 0 25 0 1 0 487453497 200560640 41444 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41444 603 41 0 48924 0
vsize: 195860
[startup+620.036 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54342 0 0 0 61859 146 0 0 25 0 1 0 487453497 200560640 41444 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41444 603 41 0 48924 0
vsize: 195860
[startup+630.037 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54358 0 0 0 62859 146 0 0 25 0 1 0 487453497 200560640 41460 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41460 603 41 0 48924 0
vsize: 195860
[startup+640.038 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 63859 147 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+650.038 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 64858 147 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+660.038 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 65858 147 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+670.039 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 66858 148 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+680.038 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 67857 148 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+690.04 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 68857 149 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223776 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+700.041 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 69857 149 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+710.04 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54363 0 0 0 70857 149 0 0 25 0 1 0 487453497 200560640 41465 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48965 41465 603 41 0 48924 0
vsize: 195860
[startup+720.04 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 54413 0 0 0 71857 150 0 0 25 0 1 0 487453497 200826880 41515 4294967295 134512640 134672761 3221224576 3221223680 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49030 41515 603 41 0 48989 0
vsize: 196120
[startup+730.041 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57182 0 0 0 72849 157 0 0 25 0 1 0 487453497 201498624 41665 4294967295 134512640 134672761 3221224576 3221223824 134593754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49194 41665 603 41 0 49153 0
vsize: 196776
[startup+740.041 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 73848 158 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+750.042 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 74848 158 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+760.042 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 75848 159 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+770.043 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 76847 159 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+780.043 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 77847 159 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+790.044 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 78847 160 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+800.044 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 79847 160 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223772 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+810.045 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 80847 160 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+820.045 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57314 0 0 0 81847 161 0 0 25 0 1 0 487453497 201175040 41628 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49115 41628 603 41 0 49074 0
vsize: 196460
[startup+830.045 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57318 0 0 0 82847 161 0 0 25 0 1 0 487453497 201310208 41632 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41632 603 41 0 49107 0
vsize: 196592
[startup+840.046 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57319 0 0 0 83846 161 0 0 25 0 1 0 487453497 201310208 41633 4294967295 134512640 134672761 3221224576 3221223748 134556664 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41633 603 41 0 49107 0
vsize: 196592
[startup+850.047 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57319 0 0 0 84846 162 0 0 25 0 1 0 487453497 201310208 41633 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41633 603 41 0 49107 0
vsize: 196592
[startup+860.046 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57321 0 0 0 85846 162 0 0 25 0 1 0 487453497 201310208 41635 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41635 603 41 0 49107 0
vsize: 196592
[startup+870.047 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57321 0 0 0 86845 162 0 0 25 0 1 0 487453497 201310208 41635 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41635 603 41 0 49107 0
vsize: 196592
[startup+880.047 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57322 0 0 0 87845 163 0 0 25 0 1 0 487453497 201310208 41636 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49148 41636 603 41 0 49107 0
vsize: 196592
[startup+890.048 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57364 0 0 0 88845 163 0 0 25 0 1 0 487453497 201445376 41678 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49181 41678 603 41 0 49140 0
vsize: 196724
[startup+900.048 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57608 0 0 0 89844 164 0 0 25 0 1 0 487453497 202399744 41922 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41922 603 41 0 49373 0
vsize: 197656
[startup+910.048 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57608 0 0 0 90844 164 0 0 25 0 1 0 487453497 202399744 41922 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41922 603 41 0 49373 0
vsize: 197656
[startup+920.048 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57608 0 0 0 91844 165 0 0 25 0 1 0 487453497 202399744 41922 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41922 603 41 0 49373 0
vsize: 197656
[startup+930.049 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57608 0 0 0 92844 165 0 0 25 0 1 0 487453497 202399744 41922 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41922 603 41 0 49373 0
vsize: 197656
[startup+940.049 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57608 0 0 0 93843 165 0 0 25 0 1 0 487453497 202399744 41922 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41922 603 41 0 49373 0
vsize: 197656
[startup+950.05 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57609 0 0 0 94843 166 0 0 25 0 1 0 487453497 202399744 41923 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41923 603 41 0 49373 0
vsize: 197656
[startup+960.05 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57609 0 0 0 95843 166 0 0 25 0 1 0 487453497 202399744 41923 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41923 603 41 0 49373 0
vsize: 197656
[startup+970.051 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57609 0 0 0 96843 166 0 0 25 0 1 0 487453497 202399744 41923 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41923 603 41 0 49373 0
vsize: 197656
[startup+980.05 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57609 0 0 0 97842 167 0 0 25 0 1 0 487453497 202399744 41923 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41923 603 41 0 49373 0
vsize: 197656
[startup+990.052 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57611 0 0 0 98842 167 0 0 25 0 1 0 487453497 202399744 41925 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41925 603 41 0 49373 0
vsize: 197656
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57611 0 0 0 99842 167 0 0 25 0 1 0 487453497 202399744 41925 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41925 603 41 0 49373 0
vsize: 197656
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57611 0 0 0 100842 168 0 0 25 0 1 0 487453497 202399744 41925 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49414 41925 603 41 0 49373 0
vsize: 197656
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57616 0 0 0 101842 168 0 0 25 0 1 0 487453497 202534912 41930 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41930 603 41 0 49406 0
vsize: 197788
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57616 0 0 0 102842 168 0 0 25 0 1 0 487453497 202534912 41930 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41930 603 41 0 49406 0
vsize: 197788
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57616 0 0 0 103842 168 0 0 25 0 1 0 487453497 202534912 41930 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41930 603 41 0 49406 0
vsize: 197788
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57616 0 0 0 104841 169 0 0 25 0 1 0 487453497 202534912 41930 4294967295 134512640 134672761 3221224576 3221223748 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41930 603 41 0 49406 0
vsize: 197788
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57616 0 0 0 105841 169 0 0 25 0 1 0 487453497 202534912 41930 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41930 603 41 0 49406 0
vsize: 197788
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57618 0 0 0 106841 169 0 0 25 0 1 0 487453497 202534912 41932 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41932 603 41 0 49406 0
vsize: 197788
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57623 0 0 0 107840 170 0 0 25 0 1 0 487453497 202534912 41937 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41937 603 41 0 49406 0
vsize: 197788
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57623 0 0 0 108840 170 0 0 25 0 1 0 487453497 202534912 41937 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41937 603 41 0 49406 0
vsize: 197788
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57623 0 0 0 109840 170 0 0 25 0 1 0 487453497 202534912 41937 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41937 603 41 0 49406 0
vsize: 197788
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57623 0 0 0 110840 171 0 0 25 0 1 0 487453497 202534912 41937 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41937 603 41 0 49406 0
vsize: 197788
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57623 0 0 0 111840 171 0 0 25 0 1 0 487453497 202534912 41937 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41937 603 41 0 49406 0
vsize: 197788
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57624 0 0 0 112839 172 0 0 25 0 1 0 487453497 202534912 41938 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41938 603 41 0 49406 0
vsize: 197788
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57625 0 0 0 113839 172 0 0 25 0 1 0 487453497 202534912 41939 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41939 603 41 0 49406 0
vsize: 197788
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57626 0 0 0 114839 172 0 0 25 0 1 0 487453497 202534912 41940 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41940 603 41 0 49406 0
vsize: 197788
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57626 0 0 0 115839 173 0 0 25 0 1 0 487453497 202534912 41940 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41940 603 41 0 49406 0
vsize: 197788
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57627 0 0 0 116839 173 0 0 25 0 1 0 487453497 202534912 41941 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41941 603 41 0 49406 0
vsize: 197788
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57627 0 0 0 117839 173 0 0 25 0 1 0 487453497 202534912 41941 4294967295 134512640 134672761 3221224576 3221223748 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41941 603 41 0 49406 0
vsize: 197788
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57627 0 0 0 118839 173 0 0 25 0 1 0 487453497 202534912 41941 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41941 603 41 0 49406 0
vsize: 197788
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 28632
Raw data (stat): 28632 (minisat+) R 28631 18865 18864 0 -1 0 57633 0 0 0 119839 173 0 0 25 0 1 0 487453497 202534912 41947 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49447 41947 603 41 0 49406 0
vsize: 197788
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 28632
Raw data (stat): 28632 (minisat+) Z 28631 18865 18864 0 -1 12 57636 0 0 0 119840 182 0 0 25 0 1 0 487453497 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.16
CPU time (s): 1200.22
CPU user time (s): 1198.4
CPU system time (s): 1.82172
CPU usage (%): 100.005
Max. virtual memory (Kb): 197788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####