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 6919

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        713232 kB
Buffers:         38492 kB
Cached:         242008 kB
SwapCached:          0 kB
Active:          86336 kB
Inactive:       196980 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        712980 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32536 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:45:31 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 4990 7 1200.24 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  234650   611110 |   70394       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/100597          
c   -- var.elim.:  2000/100597          
c   -- var.elim.:  3000/100597          
c   -- var.elim.:  4000/100597          
c   -- var.elim.:  5000/100597          
c   -- var.elim.:  6000/100597          
c   -- var.elim.:  7000/100597          
c   -- var.elim.:  8000/100597          
c   -- var.elim.:  9000/100597          
c   -- var.elim.:  10000/100597          
c   -- var.elim.:  11000/100597          
c   -- var.elim.:  12000/100597          
c   -- var.elim.:  13000/100597          
c   -- var.elim.:  14000/100597          
c   -- var.elim.:  15000/100597          
c   -- var.elim.:  16000/100597          
c   -- var.elim.:  17000/100597          
c   -- var.elim.:  18000/100597          
c   -- var.elim.:  19000/100597          
c   -- var.elim.:  20000/100597          
c   -- var.elim.:  21000/100597          
c   -- var.elim.:  22000/100597          
c   -- var.elim.:  23000/100597          
c   -- var.elim.:  24000/100597          
c   -- var.elim.:  25000/100597          
c   -- var.elim.:  26000/100597          
c   -- var.elim.:  27000/100597          
c   -- var.elim.:  28000/100597          
c   -- var.elim.:  29000/100597          
c   -- var.elim.:  30000/100597          
c   -- var.elim.:  31000/100597          
c   -- var.elim.:  32000/100597          
c   -- var.elim.:  33000/100597          
c   -- var.elim.:  34000/100597          
c   -- var.elim.:  35000/100597          
c   -- var.elim.:  36000/100597          
c   -- var.elim.:  37000/100597          
c   -- var.elim.:  38000/100597          
c   -- var.elim.:  39000/100597          
c   -- var.elim.:  40000/100597          
c   -- var.elim.:  41000/100597          
c   -- var.elim.:  42000/100597          
c   -- var.elim.:  43000/100597          
c   -- var.elim.:  44000/100597          
c   -- var.elim.:  45000/100597          
c   -- var.elim.:  46000/100597          
c   -- var.elim.:  47000/100597          
c   -- var.elim.:  48000/100597          
c   -- var.elim.:  49000/100597          
c   -- var.elim.:  50000/100597          
c   -- var.elim.:  51000/100597          
c   -- var.elim.:  52000/100597          
c   -- var.elim.:  53000/100597          
c   -- var.elim.:  54000/100597          
c   -- var.elim.:  55000/100597          
c   -- var.elim.:  56000/100597          
c   -- var.elim.:  57000/100597          
c   -- var.elim.:  58000/100597          
c   -- var.elim.:  59000/100597          
c   -- var.elim.:  60000/100597          
c   -- var.elim.:  61000/100597          
c   -- var.elim.:  62000/100597          
c   -- var.elim.:  63000/100597          
c   -- var.elim.:  64000/100597          
c   -- var.elim.:  65000/100597          
c   -- var.elim.:  66000/100597          
c   -- var.elim.:  67000/100597          
c   -- var.elim.:  68000/100597          
c   -- var.elim.:  69000/100597          
c   -- var.elim.:  70000/100597          
c   -- var.elim.:  71000/100597          
c   -- var.elim.:  72000/100597          
c   -- var.elim.:  73000/100597          
c   -- var.elim.:  74000/100597          
c   -- var.elim.:  75000/100597          
c   -- var.elim.:  76000/100597          
c   -- var.elim.:  77000/100597          
c   -- var.elim.:  78000/100597          
c   -- var.elim.:  79000/100597          
c   -- var.elim.:  80000/100597          
c   -- var.elim.:  81000/100597          
c   -- var.elim.:  82000/100597          
c   -- var.elim.:  83000/100597          
c   -- var.elim.:  84000/100597          
c   -- var.elim.:  85000/100597          
c   -- var.elim.:  86000/100597          
c   -- var.elim.:  87000/100597          
c   -- var.elim.:  88000/100597          
c   -- var.elim.:  89000/100597          
c   -- var.elim.:  90000/100597          
c   -- var.elim.:  91000/100597          
c   -- var.elim.:  92000/100597          
c   -- var.elim.:  93000/100597          
c   -- var.elim.:  94000/100597          
c   -- var.elim.:  95000/100597          
c   -- var.elim.:  96000/100597          
c   -- var.elim.:  97000/100597          
c   -- var.elim.:  98000/100597          
c   -- var.elim.:  99000/100597          
c   -- var.elim.:  100000/100597          
c   -- var.elim.:  100597/100597          
c   -- var.elim.:  1000/2536          
c   -- var.elim.:  2000/2536          
c   -- var.elim.:  2536/2536          
c   -- subsuming                       
c   -- var.elim.:  1000/2067          
c   -- var.elim.:  2000/2067          
c   -- var.elim.:  2067/2067          
c   -- var.elim.:  1000/2241          
c   -- var.elim.:  2000/2241          
c   -- var.elim.:  2241/2241          
c   -- subsuming                       
c   -- var.elim.:  1000/1916          
c   -- var.elim.:  1916/1916          
c   -- var.elim.:  517/517          
c   -- subsuming                       
c   -- var.elim.:  417/417          
c |         0 |  232505   603647 |      --       0       --      -- |     --   | -2144/-6236
c |         0 |  232505   603647 |   93002       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 6.04508 s)
c ==============================================================================
c [1mFound solution: 20352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 59722   maxlim: 3888096   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        63 |  650470  2096419 |  195140      63     1079    17.1 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/66751          
c   -- var.elim.:  2000/66751          
c   -- var.elim.:  3000/66751          
c   -- var.elim.:  4000/66751          
c   -- var.elim.:  5000/66751          
c   -- var.elim.:  6000/66751          
c   -- var.elim.:  7000/66751          
c   -- var.elim.:  8000/66751          
c   -- var.elim.:  9000/66751          
c   -- var.elim.:  10000/66751          
c   -- var.elim.:  11000/66751          
c   -- var.elim.:  12000/66751          
c   -- var.elim.:  13000/66751          
c   -- var.elim.:  14000/66751          
c   -- var.elim.:  15000/66751          
c   -- var.elim.:  16000/66751          
c   -- var.elim.:  17000/66751          
c   -- var.elim.:  18000/66751          
c   -- var.elim.:  19000/66751          
c   -- var.elim.:  20000/66751          
c   -- var.elim.:  21000/66751          
c   -- var.elim.:  22000/66751          
c   -- var.elim.:  23000/66751          
c   -- var.elim.:  24000/66751          
c   -- var.elim.:  25000/66751          
c   -- var.elim.:  26000/66751          
c   -- var.elim.:  27000/66751          
c   -- var.elim.:  28000/66751          
c   -- var.elim.:  29000/66751          
c   -- var.elim.:  30000/66751          
c   -- var.elim.:  31000/66751          
c   -- var.elim.:  32000/66751          
c   -- var.elim.:  33000/66751          
c   -- var.elim.:  34000/66751          
c   -- var.elim.:  35000/66751          
c   -- var.elim.:  36000/66751          
c   -- var.elim.:  37000/66751          
c   -- var.elim.:  38000/66751          
c   -- var.elim.:  39000/66751          
c   -- var.elim.:  40000/66751          
c   -- var.elim.:  41000/66751          
c   -- var.elim.:  42000/66751          
c   -- var.elim.:  43000/66751          
c   -- var.elim.:  44000/66751          
c   -- var.elim.:  45000/66751          
c   -- var.elim.:  46000/66751          
c   -- var.elim.:  47000/66751          
c   -- var.elim.:  48000/66751          
c   -- var.elim.:  49000/66751          
c   -- var.elim.:  50000/66751          
c   -- var.elim.:  51000/66751          
c   -- var.elim.:  52000/66751          
c   -- var.elim.:  53000/66751          
c   -- var.elim.:  54000/66751          
c   -- var.elim.:  55000/66751          
c   -- var.elim.:  56000/66751          
c   -- var.elim.:  57000/66751          
c   -- var.elim.:  58000/66751          
c   -- var.elim.:  59000/66751          
c   -- var.elim.:  60000/66751          
c   -- var.elim.:  61000/66751          
c   -- var.elim.:  62000/66751          
c   -- var.elim.:  63000/66751          
c   -- var.elim.:  64000/66751          
c   -- var.elim.:  65000/66751          
c   -- var.elim.:  66000/66751          
c   -- var.elim.:  66751/66751          
c   -- var.elim.:  36/36          
c |        63 |  649245  2091456 |      --      63       --      -- |     --   | -1211/-4861
c |        63 |  649245  2091456 |  259698      63     1079    17.1 |  0.000 % |
c |       163 |  649245  2091456 |  285667     163    13167    80.8 |  0.368 % |
c |       313 |  649245  2091456 |  314234     313    24812    79.3 |  0.368 % |
c |       539 |  649245  2091456 |  345658     539    76906   142.7 |  0.368 % |
c |       877 |  648931  2090379 |  380039     875   101618   116.1 |  0.396 % |
c |      1384 |  648931  2090379 |  418043    1382   206055   149.1 |  0.396 % |
c |      2146 |  648931  2090379 |  459848    2144   609934   284.5 |  0.396 % |
c |      3285 |  648901  2090274 |  505809    3282   659355   200.9 |  0.398 % |
c |      4993 |  648619  2089306 |  556148    4988  1139205   228.4 |  0.423 % |
c |      7555 |  648608  2089269 |  611753    7548  1299520   172.2 |  0.424 % |
c |     11399 |  648608  2089269 |  672928   11392  3303283   290.0 |  0.424 % |
c |     17165 |  648608  2089269 |  740221   17158  5011670   292.1 |  0.424 % |
c |     25815 |  648325  2088298 |  813888   25807  8020782   310.8 |  0.449 % |
c |     38789 |  648043  2087329 |  894888   38778  9424942   243.0 |  0.474 % |
c |     58250 |  648043  2087329 |  984376   58239 20041767   344.1 |  0.474 % |
c ==============================================================================
c (current CPU-time: 610.508 s)
c ==============================================================================
c [1mFound solution: 20350[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3888098   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     60052 |  648073  2087462 |  194421   60041 20701454   344.8 |  0.474 % |
c   -- subsuming                       
c   -- var.elim.:  389/389          
c   -- var.elim.:  34/34          
c |     60052 |  648035  2086660 |      --   60041       --      -- |     --   | -38/-800
c |     60052 |  648035  2086660 |  259214   59959 20685274   345.0 |  0.474 % |
c |     60152 |  648035  2086660 |  285135   60059 20688023   344.5 |  0.478 % |
c |     60303 |  648035  2086660 |  313648   60210 20689807   343.6 |  0.478 % |
c |     60528 |  648035  2086660 |  345013   60435 20698551   342.5 |  0.478 % |
c |     60866 |  648035  2086660 |  379515   60773 20719981   340.9 |  0.478 % |
c |     61372 |  648035  2086660 |  417466   61279 20732836   338.3 |  0.478 % |
c |     62131 |  648035  2086660 |  459213   62038 20771260   334.8 |  0.478 % |
c |     63270 |  648035  2086660 |  505134   63177 20936237   331.4 |  0.478 % |
c ==============================================================================
c (current CPU-time: 676.563 s)
c ==============================================================================
c [1mFound solution: 19960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3888488   bits: 22/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     63328 |  648066  2086820 |  194419   63235 20940773   331.2 |  0.478 % |
c   -- subsuming                       
c   -- var.elim.:  51/51          
c   -- var.elim.:  25/25          
c |     63328 |  648046  2086734 |      --   63235       --      -- |     --   | -17/-33
c |     63328 |  648046  2086734 |  259218   63225 20940409   331.2 |  0.478 % |
c |     63428 |  648046  2086734 |  285140   63325 20942246   330.7 |  0.482 % |
c |     63579 |  648046  2086734 |  313654   63476 20952509   330.1 |  0.482 % |
c |     63805 |  648046  2086734 |  345019   63702 20966279   329.1 |  0.482 % |
c |     64144 |  648046  2086734 |  379521   64041 21009009   328.1 |  0.482 % |
c |     64652 |  648046  2086734 |  417473   64549 21159787   327.8 |  0.482 % |
c |     65412 |  648046  2086734 |  459221   65309 21273266   325.7 |  0.482 % |
c |     66551 |  648046  2086734 |  505143   66448 21440180   322.7 |  0.482 % |
c |     68259 |  648046  2086734 |  555657   68156 21683258   318.1 |  0.482 % |
c |     70821 |  648046  2086734 |  611223   70718 21906785   309.8 |  0.482 % |
c |     74666 |  648046  2086734 |  672345   74563 23337306   313.0 |  0.482 % |
c |     80432 |  648046  2086734 |  739580   80329 26378837   328.4 |  0.482 % |
c |     89081 |  648046  2086734 |  813538   88978 30138436   338.7 |  0.482 % |
c |    102055 |  648022  2086633 |  894859  101947 35127509   344.6 |  0.482 % |
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#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.00 0.00 0.00 2/54 22738
Raw data (stat): 22738 (runsolver) R 22737 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487452845 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.9998 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 23115 0 0 0 933 55 0 0 25 0 1 0 487452845 73969664 16558 4294967295 134512640 134672761 3221224576 3221223280 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18059 16558 603 41 0 18018 0
vsize: 72236
[startup+20.0006 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 58124 0 0 0 1853 134 0 0 25 0 1 0 487452845 231440384 46938 4294967295 134512640 134672761 3221224576 3221218780 134530405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56504 46938 603 41 0 56463 0
vsize: 226016
[startup+30.0019 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61054 0 0 0 2846 141 0 0 25 0 1 0 487452845 239894528 48937 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58568 48937 603 41 0 58527 0
vsize: 234272
[startup+40.001 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61172 0 0 0 3846 142 0 0 25 0 1 0 487452845 240824320 49055 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58795 49055 603 41 0 58754 0
vsize: 235180
[startup+50.0018 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61517 0 0 0 4845 143 0 0 25 0 1 0 487452845 242155520 49400 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59120 49400 603 41 0 59079 0
vsize: 236480
[startup+60.0016 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61702 0 0 0 5845 143 0 0 25 0 1 0 487452845 242962432 49585 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59317 49585 603 41 0 59276 0
vsize: 237268
[startup+70.0025 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61747 0 0 0 6844 143 0 0 25 0 1 0 487452845 243097600 49630 4294967295 134512640 134672761 3221224576 3221223568 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59350 49630 603 41 0 59309 0
vsize: 237400
[startup+80.0032 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 61813 0 0 0 7844 144 0 0 25 0 1 0 487452845 243359744 49696 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59414 49696 603 41 0 59373 0
vsize: 237656
[startup+90.0032 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62242 0 0 0 8843 145 0 0 25 0 1 0 487452845 245084160 50125 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59835 50125 603 41 0 59794 0
vsize: 239340
[startup+100.004 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62285 0 0 0 9843 145 0 0 25 0 1 0 487452845 245616640 50168 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59965 50168 603 41 0 59924 0
vsize: 239860
[startup+110.003 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62369 0 0 0 10843 145 0 0 25 0 1 0 487452845 245874688 50252 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60028 50252 603 41 0 59987 0
vsize: 240112
[startup+120.004 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62416 0 0 0 11843 145 0 0 25 0 1 0 487452845 246009856 50299 4294967295 134512640 134672761 3221224576 3221223744 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60061 50299 603 41 0 60020 0
vsize: 240244
[startup+130.004 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62444 0 0 0 12843 145 0 0 25 0 1 0 487452845 246140928 50327 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60093 50327 603 41 0 60052 0
vsize: 240372
[startup+140.004 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62485 0 0 0 13843 145 0 0 25 0 1 0 487452845 246272000 50368 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60125 50368 603 41 0 60084 0
vsize: 240500
[startup+150.004 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62710 0 0 0 14843 146 0 0 25 0 1 0 487452845 247197696 50593 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60351 50593 603 41 0 60310 0
vsize: 241404
[startup+160.003 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62802 0 0 0 15843 146 0 0 25 0 1 0 487452845 247611392 50685 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60452 50685 603 41 0 60411 0
vsize: 241808
[startup+170.004 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 62946 0 0 0 16842 147 0 0 25 0 1 0 487452845 248139776 50829 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60581 50829 603 41 0 60540 0
vsize: 242324
[startup+180.005 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 63429 0 0 0 17841 148 0 0 25 0 1 0 487452845 250089472 51312 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61057 51312 603 41 0 61016 0
vsize: 244228
[startup+190.005 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 64297 0 0 0 18840 150 0 0 25 0 1 0 487452845 253698048 52180 4294967295 134512640 134672761 3221224576 3221223616 134613118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61938 52180 603 41 0 61897 0
vsize: 247752
[startup+200.004 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 64438 0 0 0 19839 150 0 0 25 0 1 0 487452845 254242816 52321 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62071 52321 603 41 0 62030 0
vsize: 248284
[startup+210.004 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 64833 0 0 0 20838 151 0 0 25 0 1 0 487452845 255836160 52716 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62460 52716 603 41 0 62419 0
vsize: 249840
[startup+220.005 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 66263 0 0 0 21835 155 0 0 25 0 1 0 487452845 261775360 54146 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63910 54146 603 41 0 63869 0
vsize: 255640
[startup+230.005 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 66337 0 0 0 22835 155 0 0 25 0 1 0 487452845 262049792 54220 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63977 54220 603 41 0 63936 0
vsize: 255908
[startup+240.005 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 66416 0 0 0 23835 155 0 0 25 0 1 0 487452845 262447104 54299 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64074 54299 603 41 0 64033 0
vsize: 256296
[startup+250.005 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 66674 0 0 0 24834 156 0 0 25 0 1 0 487452845 263495680 54557 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64330 54557 603 41 0 64289 0
vsize: 257320
[startup+260.005 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 67020 0 0 0 25834 157 0 0 25 0 1 0 487452845 264888320 54903 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64670 54903 603 41 0 64629 0
vsize: 258680
[startup+270.006 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 67503 0 0 0 26834 157 0 0 25 0 1 0 487452845 266833920 55386 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65145 55386 603 41 0 65104 0
vsize: 260580
[startup+280.007 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 67904 0 0 0 27832 159 0 0 25 0 1 0 487452845 268443648 55787 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65538 55787 603 41 0 65497 0
vsize: 262152
[startup+290.007 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 67964 0 0 0 28832 159 0 0 25 0 1 0 487452845 268709888 55847 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65603 55847 603 41 0 65562 0
vsize: 262412
[startup+300.007 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 68284 0 0 0 29832 160 0 0 25 0 1 0 487452845 270045184 56167 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65929 56167 603 41 0 65888 0
vsize: 263716
[startup+310.007 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69351 0 0 0 30829 163 0 0 25 0 1 0 487452845 274395136 57234 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66991 57234 603 41 0 66950 0
vsize: 267964
[startup+320.008 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69391 0 0 0 31829 163 0 0 25 0 1 0 487452845 274526208 57274 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67023 57274 603 41 0 66982 0
vsize: 268092
[startup+330.008 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69562 0 0 0 32828 164 0 0 25 0 1 0 487452845 275320832 57445 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67217 57445 603 41 0 67176 0
vsize: 268868
[startup+340.007 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69608 0 0 0 33828 164 0 0 25 0 1 0 487452845 275451904 57491 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67249 57491 603 41 0 67208 0
vsize: 268996
[startup+350.008 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69653 0 0 0 34828 164 0 0 25 0 1 0 487452845 275582976 57536 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67281 57536 603 41 0 67240 0
vsize: 269124
[startup+360.008 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69677 0 0 0 35829 164 0 0 25 0 1 0 487452845 275718144 57560 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67314 57560 603 41 0 67273 0
vsize: 269256
[startup+370.009 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69709 0 0 0 36829 164 0 0 25 0 1 0 487452845 275849216 57592 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67346 57592 603 41 0 67305 0
vsize: 269384
[startup+380.009 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69748 0 0 0 37829 164 0 0 25 0 1 0 487452845 275984384 57631 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67379 57631 603 41 0 67338 0
vsize: 269516
[startup+390.01 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69771 0 0 0 38829 164 0 0 25 0 1 0 487452845 276119552 57654 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67412 57654 603 41 0 67371 0
vsize: 269648
[startup+400.01 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 69963 0 0 0 39829 165 0 0 25 0 1 0 487452845 276779008 57846 4294967295 134512640 134672761 3221224576 3221223828 134618559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67573 57846 603 41 0 67532 0
vsize: 270292
[startup+410.01 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70009 0 0 0 40829 165 0 0 25 0 1 0 487452845 277041152 57892 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67637 57892 603 41 0 67596 0
vsize: 270548
[startup+420.011 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70081 0 0 0 41829 165 0 0 25 0 1 0 487452845 277434368 57964 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67733 57964 603 41 0 67692 0
vsize: 270932
[startup+430.011 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70081 0 0 0 42829 165 0 0 25 0 1 0 487452845 277434368 57964 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67733 57964 603 41 0 67692 0
vsize: 270932
[startup+440.01 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70188 0 0 0 43829 166 0 0 25 0 1 0 487452845 277827584 58071 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67829 58071 603 41 0 67788 0
vsize: 271316
[startup+450.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70245 0 0 0 44829 166 0 0 25 0 1 0 487452845 278106112 58128 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67897 58128 603 41 0 67856 0
vsize: 271588
[startup+460.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70569 0 0 0 45828 166 0 0 25 0 1 0 487452845 279429120 58452 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68220 58452 603 41 0 68179 0
vsize: 272880
[startup+470.011 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70726 0 0 0 46828 167 0 0 25 0 1 0 487452845 280104960 58609 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68385 58609 603 41 0 68344 0
vsize: 273540
[startup+480.011 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70787 0 0 0 47828 167 0 0 25 0 1 0 487452845 280236032 58670 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68417 58670 603 41 0 68376 0
vsize: 273668
[startup+490.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70814 0 0 0 48828 167 0 0 25 0 1 0 487452845 280367104 58697 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68449 58697 603 41 0 68408 0
vsize: 273796
[startup+500.012 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70850 0 0 0 49828 167 0 0 25 0 1 0 487452845 280502272 58733 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68482 58733 603 41 0 68441 0
vsize: 273928
[startup+510.012 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70876 0 0 0 50828 167 0 0 25 0 1 0 487452845 280633344 58759 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68514 58759 603 41 0 68473 0
vsize: 274056
[startup+520.013 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 70944 0 0 0 51828 167 0 0 25 0 1 0 487452845 280903680 58827 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68580 58827 603 41 0 68539 0
vsize: 274320
[startup+530.013 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 72365 0 0 0 52826 170 0 0 25 0 1 0 487452845 286683136 60248 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69991 60248 603 41 0 69950 0
vsize: 279964
[startup+540.013 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 73182 0 0 0 53825 172 0 0 25 0 1 0 487452845 290041856 61065 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70811 61065 603 41 0 70770 0
vsize: 283244
[startup+550.013 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 74275 0 0 0 54822 174 0 0 25 0 1 0 487452845 294551552 62158 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71912 62158 603 41 0 71871 0
vsize: 287648
[startup+560.014 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 75828 0 0 0 55818 178 0 0 25 0 1 0 487452845 300855296 63711 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73451 63711 603 41 0 73410 0
vsize: 293804
[startup+570.015 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 77530 0 0 0 56815 181 0 0 25 0 1 0 487452845 307888128 65413 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75168 65413 603 41 0 75127 0
vsize: 300672
[startup+580.014 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 79052 0 0 0 57812 185 0 0 25 0 1 0 487452845 314056704 66935 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76674 66935 603 41 0 76633 0
vsize: 306696
[startup+590.014 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 80569 0 0 0 58809 188 0 0 25 0 1 0 487452845 320253952 68452 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78187 68452 603 41 0 78146 0
vsize: 312748
[startup+600.014 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 81561 0 0 0 59808 190 0 0 25 0 1 0 487452845 324304896 69444 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79176 69444 603 41 0 79135 0
vsize: 316704
[startup+610.014 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 82017 0 0 0 60806 191 0 0 25 0 1 0 487452845 326144000 69900 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79625 69900 603 41 0 79584 0
vsize: 318500
[startup+620.013 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 89125 0 0 0 61789 208 0 0 25 0 1 0 487452845 328646656 70486 4294967295 134512640 134672761 3221224576 3221221424 134523531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80236 70486 603 41 0 80195 0
vsize: 320944
[startup+630.013 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 90854 0 0 0 62784 213 0 0 25 0 1 0 487452845 329715712 70943 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80497 70943 603 41 0 80456 0
vsize: 321988
[startup+640.013 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 90855 0 0 0 63784 213 0 0 25 0 1 0 487452845 329715712 70944 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80497 70944 603 41 0 80456 0
vsize: 321988
[startup+650.014 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 90855 0 0 0 64785 213 0 0 25 0 1 0 487452845 329715712 70944 4294967295 134512640 134672761 3221224576 3221223776 134619634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80497 70944 603 41 0 80456 0
vsize: 321988
[startup+660.014 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 90859 0 0 0 65784 213 0 0 25 0 1 0 487452845 329715712 70948 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80497 70948 603 41 0 80456 0
vsize: 321988
[startup+670.014 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 90864 0 0 0 66784 213 0 0 25 0 1 0 487452845 329715712 70953 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80497 70953 603 41 0 80456 0
vsize: 321988
[startup+680.015 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 96548 0 0 0 67771 226 0 0 25 0 1 0 487452845 333459456 71832 4294967295 134512640 134672761 3221224576 3220963552 134592600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 81411 71832 603 41 0 81370 0
vsize: 325644
[startup+690.015 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101398 0 0 0 68756 240 0 0 25 0 1 0 487452845 329846784 70997 4294967295 134512640 134672761 3221224576 3221223832 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 80529 70997 603 41 0 80488 0
vsize: 322116
[startup+700.016 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101399 0 0 0 69756 240 0 0 25 0 1 0 487452845 329846784 70998 4294967295 134512640 134672761 3221224576 3221223776 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80529 70998 603 41 0 80488 0
vsize: 322116
[startup+710.015 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101450 0 0 0 70756 241 0 0 25 0 1 0 487452845 330108928 71049 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80593 71049 603 41 0 80552 0
vsize: 322372
[startup+720.015 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101577 0 0 0 71755 241 0 0 25 0 1 0 487452845 330629120 71176 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80720 71176 603 41 0 80679 0
vsize: 322880
[startup+730.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101707 0 0 0 72755 241 0 0 25 0 1 0 487452845 331427840 71306 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80915 71306 603 41 0 80874 0
vsize: 323660
[startup+740.015 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 101824 0 0 0 73755 242 0 0 25 0 1 0 487452845 331960320 71423 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81045 71423 603 41 0 81004 0
vsize: 324180
[startup+750.015 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102140 0 0 0 74754 242 0 0 25 0 1 0 487452845 333152256 71739 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81336 71739 603 41 0 81295 0
vsize: 325344
[startup+760.016 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102165 0 0 0 75754 243 0 0 25 0 1 0 487452845 333287424 71764 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81369 71764 603 41 0 81328 0
vsize: 325476
[startup+770.015 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102191 0 0 0 76754 243 0 0 25 0 1 0 487452845 333418496 71790 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81401 71790 603 41 0 81360 0
vsize: 325604
[startup+780.015 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102291 0 0 0 77754 243 0 0 25 0 1 0 487452845 333815808 71890 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81498 71890 603 41 0 81457 0
vsize: 325992
[startup+790.015 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102349 0 0 0 78754 243 0 0 25 0 1 0 487452845 334077952 71948 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81562 71948 603 41 0 81521 0
vsize: 326248
[startup+800.015 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 102795 0 0 0 79754 243 0 0 25 0 1 0 487452845 335794176 72394 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81981 72394 603 41 0 81940 0
vsize: 327924
[startup+810.016 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 103832 0 0 0 80752 246 0 0 25 0 1 0 487452845 340148224 73431 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83044 73431 603 41 0 83003 0
vsize: 332176
[startup+820.015 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 103878 0 0 0 81751 246 0 0 25 0 1 0 487452845 340283392 73477 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83077 73477 603 41 0 83036 0
vsize: 332308
[startup+830.016 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 103990 0 0 0 82752 246 0 0 25 0 1 0 487452845 340680704 73589 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83174 73589 603 41 0 83133 0
vsize: 332696
[startup+840.016 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 104111 0 0 0 83751 247 0 0 25 0 1 0 487452845 341196800 73710 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83300 73710 603 41 0 83259 0
vsize: 333200
[startup+850.016 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 104235 0 0 0 84751 247 0 0 25 0 1 0 487452845 341721088 73834 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83428 73834 603 41 0 83387 0
vsize: 333712
[startup+860.016 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 104455 0 0 0 85750 248 0 0 25 0 1 0 487452845 342634496 74054 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83651 74054 603 41 0 83610 0
vsize: 334604
[startup+870.016 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 104876 0 0 0 86750 249 0 0 25 0 1 0 487452845 344367104 74475 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84074 74475 603 41 0 84033 0
vsize: 336296
[startup+880.017 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 105382 0 0 0 87749 250 0 0 25 0 1 0 487452845 346415104 74981 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84574 74981 603 41 0 84533 0
vsize: 338296
[startup+890.017 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 105570 0 0 0 88749 250 0 0 25 0 1 0 487452845 347201536 75169 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84766 75169 603 41 0 84725 0
vsize: 339064
[startup+900.017 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 105791 0 0 0 89749 250 0 0 25 0 1 0 487452845 348110848 75390 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84988 75390 603 41 0 84947 0
vsize: 339952
[startup+910.018 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 106146 0 0 0 90748 251 0 0 25 0 1 0 487452845 349585408 75745 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85348 75745 603 41 0 85307 0
vsize: 341392
[startup+920.017 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 106555 0 0 0 91748 252 0 0 25 0 1 0 487452845 351252480 76154 4294967295 134512640 134672761 3221224576 3221223680 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85755 76154 603 41 0 85714 0
vsize: 343020
[startup+930.018 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 106894 0 0 0 92747 253 0 0 25 0 1 0 487452845 352669696 76493 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86101 76493 603 41 0 86060 0
vsize: 344404
[startup+940.018 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 107228 0 0 0 93746 253 0 0 25 0 1 0 487452845 353984512 76827 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86422 76827 603 41 0 86381 0
vsize: 345688
[startup+950.018 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 107637 0 0 0 94745 255 0 0 25 0 1 0 487452845 355704832 77236 4294967295 134512640 134672761 3221224576 3221223700 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86842 77236 603 41 0 86801 0
vsize: 347368
[startup+960.018 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 108682 0 0 0 95743 257 0 0 25 0 1 0 487452845 359907328 78281 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87868 78281 603 41 0 87827 0
vsize: 351472
[startup+970.018 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 109135 0 0 0 96741 259 0 0 25 0 1 0 487452845 361771008 78734 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88323 78734 603 41 0 88282 0
vsize: 353292
[startup+980.018 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 110297 0 0 0 97740 261 0 0 25 0 1 0 487452845 366460928 79896 4294967295 134512640 134672761 3221224576 3221223760 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89468 79896 603 41 0 89427 0
vsize: 357872
[startup+990.018 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 110719 0 0 0 98739 262 0 0 25 0 1 0 487452845 368287744 80318 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89914 80318 603 41 0 89873 0
vsize: 359656
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 110829 0 0 0 99739 262 0 0 25 0 1 0 487452845 368693248 80428 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90013 80428 603 41 0 89972 0
vsize: 360052
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 111130 0 0 0 100738 263 0 0 25 0 1 0 487452845 369905664 80729 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90309 80729 603 41 0 90268 0
vsize: 361236
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 112250 0 0 0 101736 266 0 0 25 0 1 0 487452845 374468608 81849 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91423 81849 603 41 0 91382 0
vsize: 365692
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 112523 0 0 0 102735 266 0 0 25 0 1 0 487452845 375627776 82122 4294967295 134512640 134672761 3221224576 3221223700 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91706 82122 603 41 0 91665 0
vsize: 366824
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 112744 0 0 0 103735 267 0 0 25 0 1 0 487452845 376512512 82343 4294967295 134512640 134672761 3221224576 3221223776 134610688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91922 82343 603 41 0 91881 0
vsize: 367688
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 113108 0 0 0 104734 268 0 0 25 0 1 0 487452845 377970688 82707 4294967295 134512640 134672761 3221224576 3221223712 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92278 82707 603 41 0 92237 0
vsize: 369112
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 113515 0 0 0 105733 269 0 0 25 0 1 0 487452845 379691008 83114 4294967295 134512640 134672761 3221224576 3221223760 134615557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92698 83114 603 41 0 92657 0
vsize: 370792
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 114275 0 0 0 106731 271 0 0 25 0 1 0 487452845 382717952 83874 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93437 83874 603 41 0 93396 0
vsize: 373748
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 114569 0 0 0 107730 272 0 0 25 0 1 0 487452845 383922176 84168 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93731 84168 603 41 0 93690 0
vsize: 374924
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 114848 0 0 0 108729 273 0 0 25 0 1 0 487452845 385134592 84447 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94027 84447 603 41 0 93986 0
vsize: 376108
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 114970 0 0 0 109730 273 0 0 25 0 1 0 487452845 385650688 84569 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94153 84569 603 41 0 94112 0
vsize: 376612
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 115529 0 0 0 110728 275 0 0 25 0 1 0 487452845 387919872 85128 4294967295 134512640 134672761 3221224576 3221223760 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94707 85128 603 41 0 94666 0
vsize: 378828
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 115798 0 0 0 111727 275 0 0 25 0 1 0 487452845 388980736 85397 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94966 85397 603 41 0 94925 0
vsize: 379864
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 115830 0 0 0 112727 275 0 0 25 0 1 0 487452845 389115904 85429 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94999 85429 603 41 0 94958 0
vsize: 379996
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 116378 0 0 0 113727 276 0 0 25 0 1 0 487452845 391413760 85977 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95560 85977 603 41 0 95519 0
vsize: 382240
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 116607 0 0 0 114726 277 0 0 25 0 1 0 487452845 392327168 86206 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 95783 86206 603 41 0 95742 0
vsize: 383132
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 117433 0 0 0 115724 279 0 0 25 0 1 0 487452845 395681792 87032 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 96602 87032 603 41 0 96561 0
vsize: 386408
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 118949 0 0 0 116720 283 0 0 25 0 1 0 487452845 401899520 88548 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 98120 88548 603 41 0 98079 0
vsize: 392480
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 120345 0 0 0 117718 285 0 0 25 0 1 0 487452845 407547904 89944 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 99499 89944 603 41 0 99458 0
vsize: 397996
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 121478 0 0 0 118716 288 0 0 25 0 1 0 487452845 412200960 91077 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100635 91077 603 41 0 100594 0
vsize: 402540
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22738
Raw data (stat): 22738 (minisat+) R 22737 11931 11930 0 -1 0 122828 0 0 0 119712 292 0 0 25 0 1 0 487452845 417701888 92427 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101978 92427 603 41 0 101937 0
vsize: 407912
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 22738
Raw data (stat): 22738 (minisat+) Z 22737 11931 11930 0 -1 12 122829 0 0 0 119713 310 0 0 25 0 1 0 487452845 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.21
CPU time (s): 1200.24
CPU user time (s): 1197.14
CPU system time (s): 3.10053
CPU usage (%): 100.002
Max. virtual memory (Kb): 407912
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####