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/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-air05.opb
MD5SUM	a0fff131fa124ee4d61d9b3bf266a4ba
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	29628
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	1175.13
Number of variables	7195
Total number of constraints	7621
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	7621
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	404
Trace number 21846

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        167992 kB
Buffers:         36196 kB
Cached:         808024 kB
SwapCached:          0 kB
Active:         383420 kB
Inactive:       463548 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        167740 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6820 kB
Slab:            14008 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:38:33 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 12454 7 1200.35 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): (none)
c ---[ 850]---> BDD-cost:  233
c ---[ 848]---> BDD-cost:  459
c ---[ 846]---> BDD-cost:  253
c ---[ 844]---> BDD-cost:  191
c ---[ 842]---> BDD-cost:  109
c ---[ 840]---> BDD-cost:  277
c ---[ 838]---> BDD-cost:  147
c ---[ 836]---> BDD-cost:   87
c ---[ 834]---> BDD-cost:   85
c ---[ 832]---> BDD-cost:  127
c ---[ 830]---> BDD-cost:  167
c ---[ 828]---> BDD-cost:  191
c ---[ 826]---> BDD-cost:  663
c ---[ 822]---> BDD-cost:  123
c ---[ 820]---> BDD-cost:  405
c ---[ 818]---> BDD-cost:  443
c ---[ 816]---> BDD-cost:  465
c ---[ 814]---> BDD-cost:  425
c ---[ 812]---> BDD-cost:  253
c ---[ 810]---> BDD-cost:  177
c ---[ 808]---> BDD-cost:  415
c ---[ 806]---> BDD-cost:  413
c ---[ 804]---> BDD-cost:  693
c ---[ 802]---> BDD-cost:  103
c ---[ 800]---> BDD-cost:  119
c ---[ 798]---> BDD-cost:  309
c ---[ 796]---> BDD-cost:  289
c ---[ 794]---> BDD-cost:  155
c ---[ 786]---> BDD-cost:   39
c ---[ 784]---> BDD-cost:   67
c ---[ 782]---> BDD-cost:  157
c ---[ 780]---> BDD-cost:  253
c ---[ 778]---> BDD-cost:  199
c ---[ 776]---> BDD-cost:  445
c ---[ 774]---> BDD-cost:  315
c ---[ 772]---> BDD-cost:   89
c ---[ 770]---> BDD-cost:  107
c ---[ 768]---> BDD-cost:   67
c ---[ 766]---> BDD-cost:   93
c ---[ 764]---> BDD-cost:  135
c ---[ 762]---> BDD-cost:  163
c ---[ 760]---> BDD-cost:  173
c ---[ 758]---> BDD-cost:   33
c ---[ 756]---> BDD-cost:   13
c ---[ 754]---> BDD-cost:    7
c ---[ 752]---> BDD-cost:   23
c ---[ 750]---> BDD-cost:   37
c ---[ 748]---> BDD-cost:   43
c ---[ 746]---> BDD-cost:   39
c ---[ 744]---> BDD-cost:   95
c ---[ 742]---> BDD-cost:  101
c ---[ 740]---> BDD-cost:  525
c ---[ 738]---> BDD-cost:  121
c ---[ 736]---> BDD-cost:  483
c ---[ 732]---> BDD-cost:    9
c ---[ 730]---> BDD-cost:  193
c ---[ 728]---> BDD-cost:  181
c ---[ 726]---> BDD-cost:   93
c ---[ 724]---> BDD-cost:  325
c ---[ 722]---> BDD-cost:  479
c ---[ 720]---> BDD-cost:  273
c ---[ 718]---> BDD-cost:  269
c ---[ 716]---> BDD-cost:   93
c ---[ 714]---> BDD-cost:  341
c ---[ 712]---> BDD-cost:  299
c ---[ 710]---> BDD-cost:  183
c ---[ 708]---> BDD-cost:  315
c ---[ 706]---> BDD-cost:  289
c ---[ 704]---> BDD-cost:  383
c ---[ 702]---> BDD-cost:  231
c ---[ 700]---> BDD-cost:  205
c ---[ 698]---> BDD-cost:  133
c ---[ 696]---> BDD-cost:  257
c ---[ 694]---> BDD-cost:  331
c ---[ 692]---> BDD-cost:  179
c ---[ 690]---> BDD-cost:  159
c ---[ 688]---> BDD-cost:  185
c ---[ 686]---> BDD-cost:   95
c ---[ 684]---> BDD-cost:   63
c ---[ 682]---> BDD-cost:  547
c ---[ 680]---> BDD-cost:  569
c ---[ 678]---> BDD-cost:  169
c ---[ 676]---> BDD-cost:  115
c ---[ 674]---> BDD-cost:  125
c ---[ 672]---> BDD-cost:  163
c ---[ 670]---> BDD-cost:  119
c ---[ 668]---> BDD-cost:  565
c ---[ 666]---> BDD-cost:  331
c ---[ 664]---> BDD-cost:  255
c ---[ 662]---> BDD-cost:  217
c ---[ 660]---> BDD-cost:  189
c ---[ 658]---> BDD-cost:  237
c ---[ 656]---> BDD-cost:  113
c ---[ 654]---> BDD-cost:   67
c ---[ 652]---> BDD-cost:   71
c ---[ 650]---> BDD-cost:  351
c ---[ 648]---> BDD-cost:  521
c ---[ 646]---> BDD-cost:  535
c ---[ 644]---> BDD-cost:  341
c ---[ 642]---> BDD-cost:  251
c ---[ 640]---> BDD-cost:  293
c ---[ 638]---> BDD-cost:  313
c ---[ 636]---> BDD-cost:  431
c ---[ 634]---> BDD-cost:  395
c ---[ 632]---> BDD-cost:  419
c ---[ 630]---> BDD-cost:  389
c ---[ 628]---> BDD-cost:  169
c ---[ 626]---> BDD-cost:  357
c ---[ 624]---> BDD-cost:  493
c ---[ 622]---> BDD-cost:  285
c ---[ 620]---> BDD-cost:  229
c ---[ 618]---> BDD-cost:   89
c ---[ 616]---> BDD-cost:   79
c ---[ 614]---> BDD-cost:  745
c ---[ 612]---> BDD-cost:  565
c ---[ 610]---> BDD-cost:  799
c ---[ 608]---> BDD-cost:  673
c ---[ 606]---> BDD-cost:  577
c ---[ 604]---> BDD-cost:  179
c ---[ 602]---> BDD-cost:  523
c ---[ 598]---> BDD-cost:  319
c ---[ 596]---> BDD-cost:  377
c ---[ 594]---> BDD-cost:  395
c ---[ 592]---> BDD-cost:  105
c ---[ 590]---> BDD-cost:   71
c ---[ 586]---> BDD-cost:  643
c ---[ 584]---> BDD-cost:  177
c ---[ 582]---> BDD-cost:   83
c ---[ 580]---> BDD-cost:  157
c ---[ 578]---> BDD-cost:  101
c ---[ 574]---> BDD-cost:  269
c ---[ 572]---> BDD-cost:  227
c ---[ 570]---> BDD-cost:  181
c ---[ 568]---> BDD-cost:  119
c ---[ 566]---> BDD-cost:   83
c ---[ 564]---> BDD-cost:  123
c ---[ 562]---> BDD-cost:  101
c ---[ 560]---> BDD-cost:    0
c ---[ 558]---> BDD-cost:   81
c ---[ 556]---> BDD-cost:   75
c ---[ 554]---> BDD-cost:  119
c ---[ 552]---> BDD-cost:  399
c ---[ 550]---> BDD-cost:  139
c ---[ 548]---> BDD-cost:   81
c ---[ 546]---> BDD-cost:  151
c ---[ 544]---> BDD-cost:  533
c ---[ 542]---> BDD-cost:  495
c ---[ 540]---> BDD-cost:  323
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   37
c ---[ 532]---> BDD-cost:   27
c ---[ 530]---> BDD-cost:   21
c ---[ 528]---> BDD-cost:   23
c ---[ 526]---> BDD-cost:  225
c ---[ 524]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:  155
c ---[ 520]---> BDD-cost:   27
c ---[ 518]---> BDD-cost:   97
c ---[ 516]---> BDD-cost:   47
c ---[ 514]---> BDD-cost:  169
c ---[ 512]---> BDD-cost:  155
c ---[ 510]---> BDD-cost:  129
c ---[ 508]---> BDD-cost:  363
c ---[ 506]---> BDD-cost:  241
c ---[ 504]---> BDD-cost:  245
c ---[ 502]---> BDD-cost:  193
c ---[ 496]---> BDD-cost:  149
c ---[ 494]---> BDD-cost:   63
c ---[ 492]---> BDD-cost:  125
c ---[ 490]---> BDD-cost:   69
c ---[ 488]---> BDD-cost:   17
c ---[ 486]---> BDD-cost:   25
c ---[ 484]---> BDD-cost:   13
c ---[ 482]---> BDD-cost:   67
c ---[ 480]---> BDD-cost:   33
c ---[ 478]---> BDD-cost:   49
c ---[ 476]---> BDD-cost:   45
c ---[ 474]---> BDD-cost:   67
c ---[ 472]---> BDD-cost:  213
c ---[ 470]---> BDD-cost:   47
c ---[ 468]---> BDD-cost:   67
c ---[ 466]---> BDD-cost:   55
c ---[ 464]---> BDD-cost:   49
c ---[ 462]---> BDD-cost:   17
c ---[ 460]---> BDD-cost:   23
c ---[ 458]---> BDD-cost:  129
c ---[ 456]---> BDD-cost:   43
c ---[ 454]---> BDD-cost:   81
c ---[ 452]---> BDD-cost:   57
c ---[ 450]---> BDD-cost:  115
c ---[ 448]---> BDD-cost:  137
c ---[ 446]---> BDD-cost:   87
c ---[ 444]---> BDD-cost:   59
c ---[ 442]---> BDD-cost:   45
c ---[ 440]---> BDD-cost:  113
c ---[ 438]---> BDD-cost:   47
c ---[ 436]---> BDD-cost:  135
c ---[ 434]---> BDD-cost:  341
c ---[ 432]---> BDD-cost:  213
c ---[ 430]---> BDD-cost:  165
c ---[ 428]---> BDD-cost:  223
c ---[ 426]---> BDD-cost:  107
c ---[ 424]---> BDD-cost:  363
c ---[ 420]---> BDD-cost:   45
c ---[ 418]---> BDD-cost:   25
c ---[ 416]---> BDD-cost:   29
c ---[ 414]---> BDD-cost:   51
c ---[ 412]---> BDD-cost:   53
c ---[ 410]---> BDD-cost:   49
c ---[ 408]---> BDD-cost:  189
c ---[ 406]---> BDD-cost:  177
c ---[ 404]---> BDD-cost:  147
c ---[ 402]---> BDD-cost:  133
c ---[ 400]---> BDD-cost:   69
c ---[ 398]---> BDD-cost:   53
c ---[ 396]---> BDD-cost:  341
c ---[ 394]---> BDD-cost:  193
c ---[ 392]---> BDD-cost:  187
c ---[ 390]---> BDD-cost:  541
c ---[ 388]---> BDD-cost:  543
c ---[ 386]---> BDD-cost:  435
c ---[ 384]---> BDD-cost:  341
c ---[ 382]---> BDD-cost:   85
c ---[ 380]---> BDD-cost:  243
c ---[ 378]---> BDD-cost:   91
c ---[ 376]---> BDD-cost:  137
c ---[ 374]---> BDD-cost:  273
c ---[ 372]---> BDD-cost:  173
c ---[ 370]---> BDD-cost:  125
c ---[ 368]---> BDD-cost:  143
c ---[ 366]---> BDD-cost:   87
c ---[ 364]---> BDD-cost:  167
c ---[ 362]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:    0
c ---[ 358]---> BDD-cost:  119
c ---[ 356]---> BDD-cost:   89
c ---[ 354]---> BDD-cost:  149
c ---[ 352]---> BDD-cost:   11
c ---[ 350]---> BDD-cost:  151
c ---[ 348]---> BDD-cost:   93
c ---[ 346]---> BDD-cost:  213
c ---[ 344]---> BDD-cost:  215
c ---[ 342]---> BDD-cost:  455
c ---[ 340]---> BDD-cost:  465
c ---[ 338]---> BDD-cost:   73
c ---[ 336]---> BDD-cost:  207
c ---[ 334]---> BDD-cost:  223
c ---[ 332]---> BDD-cost:   83
c ---[ 330]---> BDD-cost:  153
c ---[ 328]---> BDD-cost:  313
c ---[ 326]---> BDD-cost:  199
c ---[ 324]---> BDD-cost:  121
c ---[ 322]---> BDD-cost:  351
c ---[ 320]---> BDD-cost:  307
c ---[ 318]---> BDD-cost:   71
c ---[ 316]---> BDD-cost:   57
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:  657
c ---[ 310]---> BDD-cost:  621
c ---[ 308]---> BDD-cost:  169
c ---[ 306]---> BDD-cost:  191
c ---[ 304]---> BDD-cost:  343
c ---[ 302]---> BDD-cost:  521
c ---[ 300]---> BDD-cost:    3
c ---[ 298]---> BDD-cost:   17
c ---[ 296]---> BDD-cost:   93
c ---[ 294]---> BDD-cost:   49
c ---[ 292]---> BDD-cost:   25
c ---[ 290]---> BDD-cost:  207
c ---[ 286]---> BDD-cost:  283
c ---[ 284]---> BDD-cost:  503
c ---[ 282]---> BDD-cost:  329
c ---[ 280]---> BDD-cost:  251
c ---[ 278]---> BDD-cost:  247
c ---[ 276]---> BDD-cost:  307
c ---[ 274]---> BDD-cost:  369
c ---[ 272]---> BDD-cost:    0
c ---[ 270]---> BDD-cost:  591
c ---[ 268]---> BDD-cost:  279
c ---[ 266]---> BDD-cost:  217
c ---[ 264]---> BDD-cost:  201
c ---[ 262]---> BDD-cost:  341
c ---[ 260]---> BDD-cost:  307
c ---[ 258]---> BDD-cost:  225
c ---[ 256]---> BDD-cost:  457
c ---[ 254]---> BDD-cost:  413
c ---[ 252]---> BDD-cost:  299
c ---[ 250]---> BDD-cost:   31
c ---[ 248]---> BDD-cost:  223
c ---[ 246]---> BDD-cost:  375
c ---[ 244]---> BDD-cost:  341
c ---[ 242]---> BDD-cost:  371
c ---[ 240]---> BDD-cost:  437
c ---[ 238]---> BDD-cost:  293
c ---[ 236]---> BDD-cost:  409
c ---[ 234]---> BDD-cost:  293
c ---[ 232]---> BDD-cost:  173
c ---[ 230]---> BDD-cost:  119
c ---[ 228]---> BDD-cost:   55
c ---[ 226]---> BDD-cost:  143
c ---[ 224]---> BDD-cost:  103
c ---[ 222]---> BDD-cost:  337
c ---[ 220]---> BDD-cost:  243
c ---[ 218]---> BDD-cost:  109
c ---[ 216]---> BDD-cost:   65
c ---[ 214]---> BDD-cost:   21
c ---[ 212]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:  213
c ---[ 208]---> BDD-cost:  187
c ---[ 206]---> BDD-cost:  111
c ---[ 204]---> BDD-cost:  329
c ---[ 202]---> BDD-cost:  341
c ---[ 200]---> BDD-cost:  297
c ---[ 198]---> BDD-cost:  253
c ---[ 196]---> BDD-cost:  463
c ---[ 194]---> BDD-cost:  381
c ---[ 192]---> BDD-cost:  281
c ---[ 190]---> BDD-cost:  249
c ---[ 188]---> BDD-cost:  197
c ---[ 186]---> BDD-cost:  263
c ---[ 184]---> BDD-cost:  209
c ---[ 182]---> BDD-cost:  175
c ---[ 180]---> BDD-cost:  583
c ---[ 178]---> BDD-cost:  539
c ---[ 176]---> BDD-cost:    5
c ---[ 174]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:  185
c ---[ 170]---> BDD-cost:  233
c ---[ 168]---> BDD-cost:  175
c ---[ 166]---> BDD-cost:   87
c ---[ 164]---> BDD-cost:   97
c ---[ 162]---> BDD-cost:  129
c ---[ 160]---> BDD-cost:   81
c ---[ 158]---> BDD-cost:  167
c ---[ 156]---> BDD-cost:  223
c ---[ 154]---> BDD-cost:  417
c ---[ 152]---> BDD-cost:  347
c ---[ 150]---> BDD-cost:  291
c ---[ 148]---> BDD-cost:  501
c ---[ 146]---> BDD-cost:  275
c ---[ 144]---> BDD-cost:  279
c ---[ 142]---> BDD-cost:  255
c ---[ 140]---> BDD-cost:  125
c ---[ 138]---> BDD-cost:  207
c ---[ 136]---> BDD-cost:  107
c ---[ 134]---> BDD-cost:  203
c ---[ 132]---> BDD-cost:  237
c ---[ 130]---> BDD-cost:  183
c ---[ 128]---> BDD-cost:  137
c ---[ 126]---> BDD-cost:  211
c ---[ 124]---> BDD-cost:  159
c ---[ 122]---> BDD-cost:  189
c ---[ 120]---> BDD-cost:  211
c ---[ 118]---> BDD-cost:  447
c ---[ 116]---> BDD-cost:  281
c ---[ 114]---> BDD-cost:  295
c ---[ 112]---> BDD-cost:  433
c ---[ 110]---> BDD-cost:  185
c ---[ 108]---> BDD-cost:  159
c ---[ 106]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   65
c ---[ 100]---> BDD-cost:   19
c ---[  98]---> BDD-cost:   39
c ---[  94]---> BDD-cost:  133
c ---[  92]---> BDD-cost:   75
c ---[  90]---> BDD-cost:   83
c ---[  88]---> BDD-cost:  281
c ---[  86]---> BDD-cost:  235
c ---[  84]---> BDD-cost:  257
c ---[  82]---> BDD-cost:  387
c ---[  80]---> BDD-cost:   89
c ---[  76]---> BDD-cost:  111
c ---[  74]---> BDD-cost:  217
c ---[  72]---> BDD-cost:  271
c ---[  70]---> BDD-cost:  271
c ---[  68]---> BDD-cost:  303
c ---[  66]---> BDD-cost:  227
c ---[  64]---> BDD-cost:  489
c ---[  62]---> BDD-cost:  193
c ---[  60]---> BDD-cost:  245
c ---[  58]---> BDD-cost:  145
c ---[  56]---> BDD-cost:  129
c ---[  54]---> BDD-cost:  317
c ---[  52]---> BDD-cost:  263
c ---[  50]---> BDD-cost:  297
c ---[  48]---> BDD-cost:  275
c ---[  46]---> BDD-cost:  381
c ---[  44]---> BDD-cost:  475
c ---[  42]---> BDD-cost:  389
c ---[  40]---> BDD-cost:  289
c ---[  38]---> BDD-cost:  285
c ---[  36]---> BDD-cost:  223
c ---[  34]---> BDD-cost:   99
c ---[  32]---> BDD-cost:  563
c ---[  30]---> BDD-cost:  517
c ---[  28]---> BDD-cost:  531
c ---[  26]---> BDD-cost:  687
c ---[  24]---> BDD-cost:  495
c ---[  22]---> BDD-cost:  599
c ---[  20]---> BDD-cost:  423
c ---[  18]---> BDD-cost:  375
c ---[  16]---> BDD-cost:  731
c ---[  14]---> BDD-cost:  519
c ---[  12]---> BDD-cost:  755
c ---[  10]---> BDD-cost:  511
c ---[   8]---> BDD-cost:  581
c ---[   6]---> BDD-cost:  679
c ---[   4]---> BDD-cost:  157
c ---[   2]---> BDD-cost:  197
c ---[   0]---> BDD-cost:  241
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  421681  1171525 |  140560       0        0     nan |  0.000 % |
c |       100 |  421681  1171525 |  154616     100     9633    96.3 |  0.403 % |
c |       250 |  421681  1171525 |  170077     250    22884    91.5 |  0.403 % |
c |       478 |  421681  1171525 |  187085     478   101502   212.3 |  0.403 % |
c |       815 |  421607  1171312 |  205793     814   127929   157.2 |  0.416 % |
c |      1324 |  421607  1171312 |  226373    1323   214289   162.0 |  0.416 % |
c |      2083 |  421602  1171297 |  249010    2077   412436   198.6 |  0.417 % |
c ==============================================================================
c [1mFound solution: 44192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 59618   maxlim: 3862736   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3183 |  838863  2661546 |  279621    3177   600276   188.9 |  0.417 % |
c |      3284 |  838863  2661546 |  307583    3278   612163   186.7 |  0.271 % |
c |      3434 |  838863  2661546 |  338341    3428   622426   181.6 |  0.271 % |
c |      3659 |  838863  2661546 |  372175    3653   703559   192.6 |  0.271 % |
c |      3996 |  838830  2661442 |  409393    3989   750574   188.2 |  0.273 % |
c |      4502 |  838830  2661442 |  450332    4495   842036   187.3 |  0.273 % |
c |      5261 |  838825  2661427 |  495365    5250   997681   190.0 |  0.274 % |
c |      6400 |  838784  2661299 |  544902    6386  1518468   237.8 |  0.276 % |
c |      8108 |  838452  2660276 |  599392    8088  1982481   245.1 |  0.288 % |
c |     10675 |  838154  2659357 |  659331   10634  2994808   281.6 |  0.300 % |
c ==============================================================================
c [1mFound solution: 44077[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 41048   maxlim: 3853150   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12825 | 1125295  3685009 |  375098   12768  4034824   316.0 |  0.300 % |
c |     12926 | 1125295  3685009 |  412607   12869  4042894   314.2 |  0.252 % |
c |     13078 | 1125249  3684855 |  453868   13017  4073209   312.9 |  0.253 % |
c |     13303 | 1125204  3684711 |  499255   13238  4129007   311.9 |  0.253 % |
c |     13640 | 1125204  3684711 |  549180   13575  4180533   308.0 |  0.253 % |
c |     14151 | 1125204  3684711 |  604099   14086  4411343   313.2 |  0.253 % |
c |     14916 | 1125204  3684711 |  664508   14851  4560707   307.1 |  0.253 % |
c |     16055 | 1124971  3683973 |  730959   15976  4815486   301.4 |  0.258 % |
c ==============================================================================
c [1mFound solution: 43625[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 35236   maxlim: 3849913   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17701 | 1371507  4564534 |  457169   17621  5488691   311.5 |  0.258 % |
c |     17801 | 1371507  4564534 |  502885   17721  5499789   310.4 |  0.227 % |
c |     17951 | 1371502  4564519 |  553174   17868  5619461   314.5 |  0.228 % |
c |     18177 | 1371328  4563942 |  608491   18082  5653518   312.7 |  0.232 % |
c |     18516 | 1371328  4563942 |  669341   18421  5756230   312.5 |  0.232 % |
c |     19025 | 1371328  4563942 |  736275   18930  5885709   310.9 |  0.232 % |
c |     19784 | 1371328  4563942 |  809902   19689  6952691   353.1 |  0.232 % |
c |     20924 | 1371181  4563478 |  890893   20812  7700324   370.0 |  0.235 % |
c |     22632 | 1370882  4562527 |  979982   22471  8183651   364.2 |  0.240 % |
c ==============================================================================
c [1mFound solution: 42844[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 34140   maxlim: 3844469   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23747 | 1609776  5415761 |  536592   23586  8810047   373.5 |  0.240 % |
c |     23847 | 1609614  5415188 |  590251   23665  8811445   372.3 |  0.226 % |
c |     23997 | 1609192  5413728 |  649276   23751  8811663   371.0 |  0.253 % |
c |     24222 | 1609084  5413354 |  714203   23959  8812370   367.8 |  0.260 % |
c |     24559 | 1608928  5412856 |  785624   24276  8824787   363.5 |  0.266 % |
c ==============================================================================
c [1mFound solution: 41772[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32094   maxlim: 3844101   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24747 | 1833455  6214756 |  611151   24463  8867031   362.5 |  0.266 % |
c |     24848 | 1833455  6214756 |  672266   24564  8889717   361.9 |  0.242 % |
c |     25000 | 1833455  6214756 |  739492   24716  8904717   360.3 |  0.242 % |
c |     25225 | 1833455  6214756 |  813441   24941  9029961   362.1 |  0.242 % |
c |     25564 | 1833455  6214756 |  894786   25280  9165197   362.5 |  0.242 % |
c |     26071 | 1833455  6214756 |  984264   25787  9308015   361.0 |  0.242 % |
c |     26830 | 1833374  6214504 | 1082691   26543  9535850   359.3 |  0.243 % |
c |     27970 | 1833374  6214504 | 1190960   27683 11531690   416.6 |  0.243 % |
c |     29678 | 1833367  6214481 | 1310056   29390 14784633   503.0 |  0.243 % |
c |     32241 | 1833260  6214140 | 1441062   31939 16539936   517.9 |  0.244 % |
c ==============================================================================
c [1mFound solution: 41670[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 29766   maxlim: 3841553   bits: 22/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34928 | 2041508  6957906 |  680502   34612 18482433   534.0 |  0.244 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1_bit0 -x2_bit0 -x3_bit0 -x4_bit0 x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 x13_bit0 -x14_bit0 -x15_bit0 -x16_bit0 -x17_bit0 -x18_bit0 x19_bit0 x20_bit0 -x21_bit0 -x22_bit0 -x23_bit0 -x24_bit0 -x25_bit0 -x26_bit0 -x27_bit0 -x28_bit0 -x29_bit0 -x30_bit0 -x31_bit0 -x32_bit0 -x33_bit0 x34_bit0 -x35_bit0 x36_bit0 -x37_bit0 -x38_bit0 -x39_bit0 -x40_bit0 x41_bit0 -x42_bit0 x43_bit0 x44_bit0 x45_bit0 -x46_bit0 -x47_bit0 x48_bit0 -x49_bit0 -x50_bit0 -x51_bit0 -x52_bit0 -x53_bit0 x54_bit0 x55_bit0 x56_bit0 -x57_bit0 x58_bit0 -x59_bit0 -x60_bit0 -x61_bit0 -x62_bit0 -x63_bit0 x64_bit0 -x65_bit0 -x66_bit0 x67_bit0 x68_bit0 -x69_bit0 -x70_bit0 -x71_bit0 -x72_bit0 -x73_bit0 -x74_bit0 -x75_bit0 -x76_bit0 -x77_bit0 -x78_bit0 -x79_bit0 -x80_bit0 -x81_bit0 -x82_bit0 -x83_bit0 -x84_bit0 -x85_bit0 -x86_bit0 -x87_bit0 -x88_bit0 -x89_bit0 -x90_bit0 -x91_bit0 -x92_bit0 -x93_bit0 -x94_bit0 -x95_bit0 -x96_bit0 -x97_bit0 -x98_bit0 -x99_bit0 -x100_bit0 -x101_bit0 -x102_bit0 -x103_bit0 -x104_bit0 -x105_bit0 -x106_bit0 -x107_bit0 -x108_bit0 -x109_bit0 -x110_bit0 -x111_bit0 -x112_bit0 -x113_bit0 -x114_bit0 -x115_bit0 -x116_bit0 -x117_bit0 -x118_bit0 -x119_bit0 -x120_bit0 -x121_bit0 -x122_bit0 -x123_bit0 x124_bit0 -x125_bit0 -x126_bit0 -x127_bit0 x128_bit0 -x129_bit0 x130_bit0 -x131_bit0 -x132_bit0 -x133_bit0 -x134_bit0 -x135_bit0 -x136_bit0 -x137_bit0 -x138_bit0 -x139_bit0 -x140_bit0 -x141_bit0 -x142_bit0 -x143_bit0 -x144_bit0 -x145_bit0 -x146_bit0 -x147_bit0 -x148_bit0 -x149_bit0 -x150_bit0 -x151_bit0 -x152_bit0 -x153_bit0 -x154_bit0 -x155_bit0 -x156_bit0 -x157_bit0 -x158_bit0 -x159_bit0 -x160_bit0 -x161_bit0 -x162_bit0 -x163_bit0 -x164_bit0 -x165_bit0 -x166_bit0 -x167_bit0 -x168_bit0 -x169_bit0 -x170_bit0 -x171_bit0 -x172_bit0 -x173_bit0 -x174_bit0 -x175_bit0 -x176_bit0 -x177_bit0 -x178_bit0 -x179_bit0 -x180_bit0 -x181_bit0 -x182_bit0 -x183_bit0 -x184_bit0 -x185_bit0 -x186_bit0 -x187_bit0 -x188_bit0 -x189_bit0 -x190_bit0 -x191_bit0 -x192_bit0 -x193_bit0 -x194_bit0 x195_bit0 -x196_bit0 -x197_bit0 -x198_bit0 -x199_bit0 -x200_bit0 -x201_bit0 -x202_bit0 -x203_bit0 -x204_bit0 -x205_bit0 -x206_bit0 -x207_bit0 -x208_bit0 -x209_bit0 -x210_bit0 -x211_bit0 -x212_bit0 -x213_bit0 -x214_bit0 -x215_bit0 -x216_bit0 -x217_bit0 -x218_bit0 -x219_bit0 -x220_bit0 -x221_bit0 -x222_bit0 -x223_bit0 -x224_bit0 -x225_bit0 -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -x242_bit0 -x243_bit0 x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 -x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 -x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 -x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 -x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 -x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 -x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 -x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 x857_bit0 -x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 -x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 -x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 -x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 -x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 -x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 -x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 -x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 -x1154_bit0 x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 -x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 -x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 x1266_bit0 -x1267_bit0 -x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 x1273_bit0 -x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 -x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 -x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 -x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 -x1443_bit0 -x1444_bit0 -x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 x1518_bit0 -x1519_bit0 -x1520_bit0 -x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 -x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 -x1537_bit0 -x1538_bit0 -x1539_bit0 -x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 -x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 -x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 -x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 -x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 -x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 -x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 -x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 -x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 -x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 -x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 -x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 -x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 -x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 -x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 -x1931_bit0 -x1932_bit0 -x1933_bit0 -x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 -x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 -x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 -x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 -x1997_bit0 -x1998_bit0 -x1999_bit0 -x2000_bit0 x2001_bit0 -x2002_bit0 -x2003_bit0 -x2004_bit0 -x2005_bit0 -x2006_bit0 -x2007_bit0 -x2008_bit0 -x2009_bit0 -x2010_bit0 -x2011_bit0 -x2012_bit0 -x2013_bit0 -x2014_bit0 -x2015_bit0 -x2016_bit0 -x2017_bit0 -x2018_bit0 -x2019_bit0 -x2020_bit0 -x2021_bit0 -x2022_bit0 -x2023_bit0 -x2024_bit0 -x2025_bit0 -x2026_bit0 -x2027_bit0 -x2028_bit0 -x2029_bit0 -x2030_bit0 -x2031_bit0 -x2032_bit0 -x2033_bit0 -x2034_bit0 -x2035_bit0 -x2036_bit0 -x2037_bit0 -x2038_bit0 -x2039_bit0 -x2040_bit0 -x2041_bit0 -x2042_bit0 -x2043_bit0 -x2044_bit0 -x2045_bit0 -x2046_bit0 -x2047_bit0 -x2048_bit0 -x2049_bit0 -x2050_bit0 -x2051_bit0 -x2052_bit0 -x2053_bit0 -x2054_bit0 -x2055_bit0 -x2056_bit0 -x2057_bit0 -x2058_bit0 -x2059_bit0 -x2060_bit0 -x2061_bit0 -x2062_bit0 -x2063_bit0 -x2064_bit0 -x2065_bit0 -x2066_bit0 -x2067_bit0 -x2068_bit0 -x2069_bit0 -x2070_bit0 -x2071_bit0 -x2072_bit0 -x2073_bit0 -x2074_bit0 -x2075_bit0 -x2076_bit0 -x2077_bit0 -x2078_bit0 -x2079_bit0 -x2080_bit0 -x2081_bit0 -x2082_bit0 -x2083_bit0 -x2084_bit0 -x2085_bit0 -x2086_bit0 -x2087_bit0 -x2088_bit0 -x2089_bit0 -x2090_bit0 -x2091_bit0 -x2092_bit0 -x2093_bit0 -x2094_bit0 -x2095_bit0 -x2096_bit0 -x2097_bit0 -x2098_bit0 -x2099_bit0 -x2100_bit0 -x2101_bit0 -x2102_bit0 -x2103_bit0 -x2104_bit0 x2105_bit0 -x2106_bit0 -x2107_bit0 -x2108_bit0 -x2109_bit0 -x2110_bit0 -x2111_bit0 -x2112_bit0 -x2113_bit0 -x2114_bit0 -x2115_bit0 -x2116_bit0 -x2117_bit0 -x2118_bit0 -x2119_bit0 -x2120_bit0 -x2121_bit0 -x2122_bit0 -x2123_bit0 -x2124_bit0 -x2125_bit0 -x2126_bit0 -x2127_bit0 -x2128_bit0 -x2129_bit0 -x2130_bit0 -x2131_bit0 -x2132_bit0 -x2133_bit0 -x2134_bit0 -x2135_bit0 -x2136_bit0 -x2137_bit0 -x2138_bit0 -x2139_bit0 -x2140_bit0 -x2141_bit0 -x2142_bit0 -x2143_bit0 -x2144_bit0 -x2145_bit0 -x2146_bit0 -x2147_bit0 -x2148_bit0 -x2149_bit0 -x2150_bit0 -x2151_bit0 -x2152_bit0 -x2153_bit0 -x2154_bit0 -x2155_bit0 -x2156_bit0 -x2157_bit0 -x2158_bit0 -x2159_bit0 -x2160_bit0 -x2161_bit0 -x2162_bit0 -x2163_bit0 -x2164_bit0 -x2165_bit0 -x2166_bit0 -x2167_bit0 -x2168_bit0 -x2169_bit0 -x2170_bit0 -x2171_bit0 -x2172_bit0 -x2173_bit0 -x2174_bit0 -x2175_bit0 -x2176_bit0 -x2177_bit0 -x2178_bit0 -x2179_bit0 -x2180_bit0 -x2181_bit0 -x2182_bit0 -x2183_bit0 -x2184_bit0 -x2185_bit0 -x2186_bit0 -x2187_bit0 -x2188_bit0 -x2189_bit0 -x2190_bit0 -x2191_bit0 -x2192_bit0 -x2193_bit0 -x2194_bit0 -x2195_bit0 -x2196_bit0 -x2197_bit0 -x2198_bit0 -x2199_bit0 -x2200_bit0 -x2201_bit0 -x2202_bit0 -x2203_bit0 -x2204_bit0 -x2205_bit0 -x2206_bit0 -x2207_bit0 -x2208_bit0 -x2209_bit0 -x2210_bit0 -x2211_bit0 -x2212_bit0 -x2213_bit0 -x2214_bit0 -x2215_bit0 -x2216_bit0 -x2217_bit0 -x2218_bit0 -x2219_bit0 -x2220_bit0 -x2221_bit0 -x2222_bit0 -x2223_bit0 -x2224_bit0 -x2225_bit0 -x2226_bit0 -x2227_bit0 -x2228_bit0 -x2229_bit0 -x2230_bit0 -x2231_bit0 -x2232_bit0 -x2233_bit0 -x2234_bit0 -x2235_bit0 -x2236_bit0 -x2237_bit0 -x2238_bit0 -x2239_bit0 -x2240_bit0 -x2241_bit0 -x2242_bit0 -x2243_bit0 -x2244_bit0 -x2245_bit0 -x2246_bit0 -x2247_bit0 -x2248_bit0 -x2249_bit0 -x2250_bit0 -x2251_bit0 -x2252_bit0 -x2253_bit0 -x2254_bit0 -x2255_bit0 -x2256_bit0 -x2257_bit0 -x2258_bit0 -x2259_bit0 -x2260_bit0 -x2261_bit0 -x2262_bit0 -x2263_bit0 -x2264_bit0 -x2265_bit0 -x2266_bit0 -x2267_bit0 -x2268_bit0 -x2269_bit0 -x2270_bit0 -x2271_bit0 -x2272_bit0 -x2273_bit0 -x2274_bit0 -x2275_bit0 -x2276_bit0 -x2277_bit0 -x2278_bit0 -x2279_bit0 -x2280_bit0 -x2281_bit0 -x2282_bit0 -x2283_bit0 -x2284_bit0 -x2285_bit0 -x2286_bit0 -x2287_bit0 -x2288_bit0 -x2289_bit0 -x2290_bit0 -x2291_bit0 -x2292_bit0 -x2293_bit0 -x2294_bit0 -x2295_bit0 -x2296_bit0 -x2297_bit0 -x2298_bit0 -x2299_bit0 -x2300_bit0 -x2301_bit0 -x2302_bit0 -x2303_bit0 -x2304_bit0 -x2305_bit0 -x2306_bit0 -x2307_bit0 -x2308_bit0 -x2309_bit0 -x2310_bit0 -x2311_bit0 -x2312_bit0 -x2313_bit0 -x2314_bit0 -x2315_bit0 -x2316_bit0 -x2317_bit0 -x2318_bit0 -x2319_bit0 -x2320_bit0 -x2321_bit0 -x2322_bit0 -x2323_bit0 -x2324_bit0 -x2325_bit0 -x2326_bit0 -x2327_bit0 -x2328_bit0 -x2329_bit0 -x2330_bit0 -x2331_bit0 -x2332_bit0 -x2333_bit0 -x2334_bit0 -x2335_bit0 -x2336_bit0 -x2337_bit0 -x2338_bit0 -x2339_bit0 -x2340_bit0 -x2341_bit0 -x2342_bit0 -x2343_bit0 -x2344_bit0 -x2345_bit0 -x2346_bit0 -x2347_bit0 -x2348_bit0 -x2349_bit0 -x2350_bit0 -x2351_bit0 -x2352_bit0 -x2353_bit0 -x2354_bit0 -x2355_bit0 -x2356_bit0 -x2357_bit0 -x2358_bit0 -x2359_bit0 -x2360_bit0 -x2361_bit0 -x2362_bit0 -x2363_bit0 -x2364_bit0 -x2365_bit0 -x2366_bit0 -x2367_bit0 -x2368_bit0 -x2369_bit0 -x2370_bit0 -x2371_bit0 -x2372_bit0 -x2373_bit0 -x2374_bit0 -x2375_bit0 -x2376_bit0 -x2377_bit0 -x2378_bit0 -x2379_bit0 -x2380_bit0 -x2381_bit0 -x2382_bit0 -x2383_bit0 -x2384_bit0 -x2385_bit0 -x2386_bit0 -x2387_bit0 -x2388_bit0 -x2389_bit0 -x2390_bit0 -x2391_bit0 -x2392_bit0 -x2393_bit0 -x2394_bit0 -x2395_bit0 -x2396_bit0 -x2397_bit0 -x2398_bit0 -x2399_bit0 -x2400_bit0 -x2401_bit0 -x2402_bit0 -x2403_bit0 -x2404_bit0 -x2405_bit0 -x2406_bit0 -x2407_bit0 -x2408_bit0 -x2409_bit0 -x2410_bit0 -x2411_bit0 -x2412_bit0 -x2413_bit0 -x2414_bit0 -x2415_bit0 -x2416_bit0 -x2417_bit0 -x2418_bit0 -x2419_bit0 -x2420_bit0 -x2421_bit0 -x2422_bit0 -x2423_bit0 -x2424_bit0 -x2425_bit0 -x2426_bit0 -x2427_bit0 x2428_bit0 -x2429_bit0 -x2430_bit0 -x2431_bit0 -x2432_bit0 -x2433_bit0 -x2434_bit0 -x2435_bit0 -x2436_bit0 -x2437_bit0 -x2438_bit0 -x2439_bit0 -x2440_bit0 -x2441_bit0 -x2442_bit0 -x2443_bit0 -x2444_bit0 -x2445_bit0 -x2446_bit0 -x2447_bit0 -x2448_bit0 -x2449_bit0 -x2450_bit0 -x2451_bit0 -x2452_bit0 -x2453_bit0 -x2454_bit0 -x2455_bit0 -x2456_bit0 x2457_bit0 -x2458_bit0 -x2459_bit0 -x2460_bit0 -x2461_bit0 -x2462_bit0 -x2463_bit0 -x2464_bit0 -x2465_bit0 -x2466_bit0 -x2467_bit0 -x2468_bit0 -x2469_bit0 -x2470_bit0 -x2471_bit0 -x2472_bit0 -x2473_bit0 -x2474_bit0 -x2475_bit0 -x2476_bit0 -x2477_bit0 -x2478_bit0 -x2479_bit0 -x2480_bit0 -x2481_bit0 -x2482_bit0 -x2483_bit0 -x2484_bit0 -x2485_bit0 -x2486_bit0 -x2487_bit0 -x2488_bit0 -x2489_bit0 -x2490_bit0 -x2491_bit0 -x2492_bit0 -x2493_bit0 -x2494_bit0 -x2495_bit0 -x2496_bit0 -x2497_bit0 -x2498_bit0 -x2499_bit0 -x2500_bit0 -x2501_bit0 -x2502_bit0 -x2503_bit0 -x2504_bit0 -x2505_bit0 -x2506_bit0 -x2507_bit0 -x2508_bit0 -x2509_bit0 -x2510_bit0 -x2511_bit0 -x2512_bit0 -x2513_bit0 -x2514_bit0 -x2515_bit0 -x2516_bit0 -x2517_bit0 -x2518_bit0 -x2519_bit0 -x2520_bit0 -x2521_bit0 -x2522_bit0 -x2523_bit0 -x2524_bit0 -x2525_bit0 -x2526_bit0 -x2527_bit0 -x2528_bit0 -x2529_bit0 -x2530_bit0 -x2531_bit0 -x2532_bit0 -x2533_bit0 -x2534_bit0 -x2535_bit0 -x2536_bit0 -x2537_bit0 -x2538_bit0 -x2539_bit0 -x2540_bit0 -x2541_bit0 -x2542_bit0 -x2543_bit0 -x2544_bit0 -x2545_bit0 -x2546_bit0 -x2547_bit0 -x2548_bit0 -x2549_bit0 -x2550_bit0 -x2551_bit0 -x2552_bit0 -x2553_bit0 -x2554_bit0 -x2555_bit0 -x2556_bit0 -x2557_bit0 -x2558_bit0 -x2559_bit0 -x2560_bit0 -x2561_bit0 -x2562_bit0 -x2563_bit0 -x2564_bit0 -x2565_bit0 -x2566_bit0 -x2567_bit0 -x2568_bit0 -x2569_bit0 -x2570_bit0 -x2571_bit0 -x2572_bit0 -x2573_bit0 -x2574_bit0 -x2575_bit0 -x2576_bit0 -x2577_bit0 -x2578_bit0 -x2579_bit0 -x2580_bit0 -x2581_bit0 -x2582_bit0 -x2583_bit0 -x2584_bit0 -x2585_bit0 -x2586_bit0 -x2587_bit0 -x2588_bit0 -x2589_bit0 -x2590_bit0 -x2591_bit0 -x2592_bit0 -x2593_bit0 -x2594_bit0 -x2595_bit0 -x2596_bit0 -x2597_bit0 -x2598_bit0 -x2599_bit0 -x2600_bit0 -x2601_bit0 -x2602_bit0 -x2603_bit0 -x2604_bit0 -x2605_bit0 -x2606_bit0 -x2607_bit0 -x2608_bit0 -x2609_bit0 -x2610_bit0 -x2611_bit0 x2612_bit0 -x2613_bit0 -x2614_bit0 -x2615_bit0 -x2616_bit0 -x2617_bit0 -x2618_bit0 -x2619_bit0 -x2620_bit0 -x2621_bit0 -x2622_bit0 -x2623_bit0 -x2624_bit0 -x2625_bit0 -x2626_bit0 -x2627_bit0 -x2628_bit0 -x2629_bit0 -x2630_bit0 -x2631_bit0 -x2632_bit0 -x2633_bit0 -x2634_bit0 -x2635_bit0 -x2636_bit0 -x2637_bit0 -x2638_bit0 -x2639_bit0 -x2640_bit0 -x2641_bit0 -x2642_bit0 -x2643_bit0 -x2644_bit0 -x2645_bit0 -x2646_bit0 -x2647_bit0 -x2648_bit0 -x2649_bit0 -x2650_bit0 -x2651_bit0 -x2652_bit0 -x2653_bit0 -x2654_bit0 -x2655_bit0 -x2656_bit0 -x2657_bit0 -x2658_bit0 -x2659_bit0 -x2660_bit0 -x2661_bit0 -x2662_bit0 -x2663_bit0 -x2664_bit0 -x2665_bit0 -x2666_bit0 -x2667_bit0 -x2668_bit0 -x2669_bit0 -x2670_bit0 -x2671_bit0 -x2672_bit0 -x2673_bit0 -x2674_bit0 -x2675_bit0 -x2676_bit0 -x2677_bit0 -x2678_bit0 -x2679_bit0 -x2680_bit0 -x2681_bit0 -x2682_bit0 -x2683_bit0 -x2684_bit0 -x2685_bit0 -x2686_bit0 -x2687_bit0 -x2688_bit0 -x2689_bit0 -x2690_bit0 -x2691_bit0 -x2692_bit0 -x2693_bit0 -x2694_bit0 -x2695_bit0 -x2696_bit0 -x2697_bit0 -x2698_bit0 -x2699_bit0 -x2700_bit0 -x2701_bit0 -x2702_bit0 -x2703_bit0 -x2704_bit0 -x2705_bit0 -x2706_bit0 -x2707_bit0 -x2708_bit0 -x2709_bit0 -x2710_bit0 -x2711_bit0 -x2712_bit0 -x2713_bit0 -x2714_bit0 -x2715_bit0 -x2716_bit0 -x2717_bit0 -x2718_bit0 -x2719_bit0 -x2720_bit0 -x2721_bit0 -x2722_bit0 -x2723_bit0 -x2724_bit0 -x2725_bit0 -x2726_bit0 -x2727_bit0 -x2728_bit0 -x2729_bit0 -x2730_bit0 -x2731_bit0 -x2732_bit0 -x2733_bit0 -x2734_bit0 -x2735_bit0 -x2736_bit0 -x2737_bit0 -x2738_bit0 -x2739_bit0 -x2740_bit0 -x2741_bit0 -x2742_bit0 -x2743_bit0 -x2744_bit0 -x2745_bit0 -x2746_bit0 -x2747_bit0 -x2748_bit0 -x2749_bit0 -x2750_bit0 -x2751_bit0 -x2752_bit0 -x2753_bit0 -x2754_bit0 -x2755_bit0 -x2756_bit0 -x2757_bit0 -x2758_bit0 -x2759_bit0 -x2760_bit0 -x2761_bit0 -x2762_bit0 -x2763_bit0 -x2764_bit0 -x2765_bit0 -x2766_bit0 -x2767_bit0 -x2768_bit0 -x2769_bit0 -x2770_bit0 -x2771_bit0 -x2772_bit0 -x2773_bit0 -x2774_bit0 -x2775_bit0 -x2776_bit0 -x2777_bit0 -x2778_bit0 -x2779_bit0 -x2780_bit0 -x2781_bit0 -x2782_bit0 -x2783_bit0 -x2784_bit0 -x2785_bit0 -x2786_bit0 -x2787_bit0 -x2788_bit0 -x2789_bit0 -x2790_bit0 -x2791_bit0 -x2792_bit0 -x2793_bit0 -x2794_bit0 -x2795_bit0 -x2796_bit0 -x2797_bit0 -x2798_bit0 -x2799_bit0 -x2800_bit0 -x2801_bit0 -x2802_bit0 -x2803_bit0 -x2804_bit0 -x2805_bit0 -x2806_bit0 -x2807_bit0 -x2808_bit0 -x2809_bit0 -x2810_bit0 -x2811_bit0 -x2812_bit0 -x2813_bit0 -x2814_bit0 -x2815_bit0 -x2816_bit0 -x2817_bit0 -x2818_bit0 -x2819_bit0 -x2820_bit0 -x2821_bit0 -x2822_bit0 -x2823_bit0 -x2824_bit0 -x2825_bit0 -x2826_bit0 -x2827_bit0 -x2828_bit0 -x2829_bit0 -x2830_bit0 -x2831_bit0 -x2832_bit0 -x2833_bit0 -x2834_bit0 -x2835_bit0 -x2836_bit0 -x2837_bit0 -x2838_bit0 -x2839_bit0 -x2840_bit0 -x2841_bit0 -x2842_bit0 -x2843_bit0 -x2844_bit0 -x2845_bit0 -x2846_bit0 -x2847_bit0 -x2848_bit0 -x2849_bit0 -x2850_bit0 -x2851_bit0 -x2852_bit0 -x2853_bit0 -x2854_bit0 -x2855_bit0 -x2856_bit0 -x2857_bit0 -x2858_bit0 -x2859_bit0 -x2860_bit0 -x2861_bit0 -x2862_bit0 -x2863_bit0 -x2864_bit0 -x2865_bit0 -x2866_bit0 -x2867_bit0 -x2868_bit0 -x2869_bit0 -x2870_bit0 -x2871_bit0 -x2872_bit0 -x2873_bit0 -x2874_bit0 -x2875_bit0 -x2876_bit0 -x2877_bit0 -x2878_bit0 -x2879_bit0 -x2880_bit0 -x2881_bit0 -x2882_bit0 -x2883_bit0 -x2884_bit0 -x2885_bit0 -x2886_bit0 -x2887_bit0 -x2888_bit0 -x2889_bit0 -x2890_bit0 -x2891_bit0 -x2892_bit0 -x2893_bit0 -x2894_bit0 -x2895_bit0 -x2896_bit0 -x2897_bit0 -x2898_bit0 -x2899_bit0 -x2900_bit0 -x2901_bit0 -x2902_bit0 -x2903_bit0 -x2904_bit0 -x2905_bit0 -x2906_bit0 -x2907_bit0 -x2908_bit0 -x2909_bit0 -x2910_bit0 -x2911_bit0 -x2912_bit0 -x2913_bit0 -x2914_bit0 -x2915_bit0 -x2916_bit0 -x2917_bit0 -x2918_bit0 -x2919_bit0 -x2920_bit0 -x2921_bit0 -x2922_bit0 -x2923_bit0 -x2924_bit0 -x2925_bit0 -x2926_bit0 -x2927_bit0 -x2928_bit0 -x2929_bit0 -x2930_bit0 -x2931_bit0 -x2932_bit0 -x2933_bit0 -x2934_bit0 -x2935_bit0 -x2936_bit0 -x2937_bit0 -x2938_bit0 -x2939_bit0 -x2940_bit0 -x2941_bit0 -x2942_bit0 -x2943_bit0 -x2944_bit0 -x2945_bit0 -x2946_bit0 -x2947_bit0 -x2948_bit0 -x2949_bit0 -x2950_bit0 -x2951_bit0 -x2952_bit0 -x2953_bit0 -x2954_bit0 -x2955_bit0 -x2956_bit0 -x2957_bit0 -x2958_bit0 -x2959_bit0 -x2960_bit0 -x2961_bit0 -x2962_bit0 -x2963_bit0 -x2964_bit0 -x2965_bit0 -x2966_bit0 -x2967_bit0 -x2968_bit0 -x2969_bit0 -x2970_bit0 -x2971_bit0 -x2972_bit0 -x2973_bit0 -x2974_bit0 -x2975_bit0 -x2976_bit0 -x2977_bit0 -x2978_bit0 -x2979_bit0 -x2980_bit0 -x2981_bit0 -x2982_bit0 -x2983_bit0 -x2984_bit0 -x2985_bit0 -x2986_bit0 -x2987_bit0 -x2988_bit0 -x2989_bit0 -x2990_bit0 -x2991_bit0 -x2992_bit0 -x2993_bit0 -x2994_bit0 -x2995_bit0 -x2996_bit0 -x2997_bit0 -x2998_bit0 -x2999_bit0 -x3000_bit0 -x3001_bit0 -x3002_bit0 -x3003_bit0 -x3004_bit0 -x3005_bit0 -x3006_bit0 x3007_bit0 -x3008_bit0 -x3009_bit0 -x3010_bit0 -x3011_bit0 -x3012_bit0 -x3013_bit0 -x3014_bit0 -x3015_bit0 -x3016_bit0 -x3017_bit0 -x3018_bit0 -x3019_bit0 -x3020_bit0 -x3021_bit0 -x3022_bit0 -x3023_bit0 -x3024_bit0 -x3025_bit0 -x3026_bit0 -x3027_bit0 -x3028_bit0 -x3029_bit0 -x3030_bit0 -x3031_bit0 -x3032_bit0 -x3033_bit0 -x3034_bit0 -x3035_bit0 -x3036_bit0 -x3037_bit0 -x3038_bit0 -x3039_bit0 -x3040_bit0 -x3041_bit0 -x3042_bit0 -x3043_bit0 -x3044_bit0 -x3045_bit0 -x3046_bit0 -x3047_bit0 -x3048_bit0 -x3049_bit0 -x3050_bit0 -x3051_bit0 -x3052_bit0 -x3053_bit0 -x3054_bit0 -x3055_bit0 -x3056_bit0 -x3057_bit0 -x3058_bit0 -x3059_bit0 -x3060_bit0 -x3061_bit0 -x3062_bit0 -x3063_bit0 -x3064_bit0 -x3065_bit0 -x3066_bit0 -x3067_bit0 -x3068_bit0 -x3069_bit0 -x3070_bit0 -x3071_bit0 -x3072_bit0 -x3073_bit0 -x3074_bit0 x3075_bit0 -x3076_bit0 -x3077_bit0 -x3078_bit0 -x3079_bit0 -x3080_bit0 -x3081_bit0 -x3082_bit0 -x3083_bit0 -x3084_bit0 -x3085_bit0 -x3086_bit0 -x3087_bit0 -x3088_bit0 -x3089_bit0 -x3090_bit0 -x3091_bit0 -x3092_bit0 -x3093_bit0 -x3094_bit0 -x3095_bit0 -x3096_bit0 -x3097_bit0 -x3098_bit0 -x3099_bit0 -x3100_bit0 -x3101_bit0 -x3102_bit0 -x3103_bit0 -x3104_bit0 -x3105_bit0 -x3106_bit0 -x3107_bit0 -x3108_bit0 -x3109_bit0 -x3110_bit0 -x3111_bit0 -x3112_bit0 -x3113_bit0 -x3114_bit0 -x3115_bit0 -x3116_bit0 -x3117_bit0 -x3118_bit0 -x3119_bit0 -x3120_bit0 -x3121_bit0 -x3122_bit0 -x3123_bit0 -x3124_bit0 -x3125_bit0 -x3126_bit0 -x3127_bit0 -x3128_bit0 -x3129_bit0 -x3130_bit0 -x3131_bit0 -x3132_bit0 -x3133_bit0 -x3134_bit0 -x3135_bit0 -x3136_bit0 -x3137_bit0 -x3138_bit0 -x3139_bit0 -x3140_bit0 -x3141_bit0 -x3142_bit0 -x3143_bit0 -x3144_bit0 -x3145_bit0 -x3146_bit0 -x3147_bit0 -x3148_bit0 -x3149_bit0 -x3150_bit0 -x3151_bit0 -x3152_bit0 -x3153_bit0 -x3154_bit0 -x3155_bit0 -x3156_bit0 -x3157_bit0 -x3158_bit0 -x3159_bit0 -x3160_bit0 -x3161_bit0 -x3162_bit0 -x3163_bit0 -x3164_bit0 -x3165_bit0 -x3166_bit0 -x3167_bit0 -x3168_bit0 -x3169_bit0 -x3170_bit0 -x3171_bit0 -x3172_bit0 -x3173_bit0 -x3174_bit0 -x3175_bit0 -x3176_bit0 -x3177_bit0 -x3178_bit0 -x3179_bit0 -x3180_bit0 -x3181_bit0 -x3182_bit0 -x3183_bit0 -x3184_bit0 -x3185_bit0 -x3186_bit0 -x3187_bit0 -x3188_bit0 -x3189_bit0 -x3190_bit0 -x3191_bit0 -x3192_bit0 -x3193_bit0 -x3194_bit0 -x3195_bit0 -x3196_bit0 -x3197_bit0 -x3198_bit0 -x3199_bit0 -x3200_bit0 -x3201_bit0 -x3202_bit0 -x3203_bit0 -x3204_bit0 -x3205_bit0 -x3206_bit0 -x3207_bit0 -x3208_bit0 -x3209_bit0 -x3210_bit0 -x3211_bit0 -x3212_bit0 -x3213_bit0 -x3214_bit0 -x3215_bit0 -x3216_bit0 -x3217_bit0 -x3218_bit0 -x3219_bit0 -x3220_bit0 -x3221_bit0 -x3222_bit0 -x3223_bit0 -x3224_bit0 -x3225_bit0 -x3226_bit0 -x3227_bit0 -x3228_bit0 -x3229_bit0 -x3230_bit0 -x3231_bit0 -x3232_bit0 -x3233_bit0 -x3234_bit0 -x3235_bit0 -x3236_bit0 -x3237_bit0 -x3238_bit0 -x3239_bit0 -x3240_bit0 -x3241_bit0 -x3242_bit0 -x3243_bit0 -x3244_bit0 -x3245_bit0 -x3246_bit0 -x3247_bit0 -x3248_bit0 -x3249_bit0 -x3250_bit0 -x3251_bit0 -x3252_bit0 -x3253_bit0 -x3254_bit0 -x3255_bit0 -x3256_bit0 -x3257_bit0 -x3258_bit0 -x3259_bit0 -x3260_bit0 -x3261_bit0 -x3262_bit0 -x3263_bit0 -x3264_bit0 x3265_bit0 -x3266_bit0 -x3267_bit0 -x3268_bit0 -x3269_bit0 -x3270_bit0 -x3271_bit0 -x3272_bit0 -x3273_bit0 -x3274_bit0 -x3275_bit0 -x3276_bit0 -x3277_bit0 -x3278_bit0 -x3279_bit0 -x3280_bit0 -x3281_bit0 -x3282_bit0 -x3283_bit0 -x3284_bit0 -x3285_bit0 -x3286_bit0 -x3287_bit0 -x3288_bit0 -x3289_bit0 -x3290_bit0 -x3291_bit0 -x3292_bit0 -x3293_bit0 -x3294_bit0 -x3295_bit0 -x3296_bit0 -x3297_bit0 -x3298_bit0 -x3299_bit0 -x3300_bit0 -x3301_bit0 -x3302_bit0 -x3303_bit0 -x3304_bit0 -x3305_bit0 -x3306_bit0 -x3307_bit0 -x3308_bit0 -x3309_bit0 -x3310_bit0 -x3311_bit0 -x3312_bit0 -x3313_bit0 -x3314_bit0 -x3315_bit0 -x3316_bit0 -x3317_bit0 -x3318_bit0 -x3319_bit0 -x3320_bit0 -x3321_bit0 -x3322_bit0 -x3323_bit0 -x3324_bit0 -x3325_bit0 -x3326_bit0 -x3327_bit0 -x3328_bit0 -x3329_bit0 -x3330_bit0 -x3331_bit0 -x3332_bit0 -x3333_bit0 -x3334_bit0 -x3335_bit0 -x3336_bit0 -x3337_bit0 -x3338_bit0 -x3339_bit0 -x3340_bit0 -x3341_bit0 -x3342_bit0 -x3343_bit0 -x3344_bit0 -x3345_bit0 -x3346_bit0 -x3347_bit0 -x3348_bit0 -x3349_bit0 -x3350_bit0 -x3351_bit0 -x3352_bit0 -x3353_bit0 -x3354_bit0 -x3355_bit0 -x3356_bit0 -x3357_bit0 -x3358_bit0 -x3359_bit0 -x3360_bit0 -x3361_bit0 -x3362_bit0 -x3363_bit0 -x3364_bit0 -x3365_bit0 -x3366_bit0 -x3367_bit0 -x3368_bit0 -x3369_bit0 -x3370_bit0 -x3371_bit0 -x3372_bit0 -x3373_bit0 -x3374_bit0 -x3375_bit0 -x3376_bit0 -x3377_bit0 -x3378_bit0 -x3379_bit0 -x3380_bit0 -x3381_bit0 -x3382_bit0 -x3383_bit0 -x3384_bit0 -x3385_bit0 -x3386_bit0 -x3387_bit0 -x3388_bit0 -x3389_bit0 -x3390_bit0 -x3391_bit0 -x3392_bit0 -x3393_bit0 -x3394_bit0 -x3395_bit0 -x3396_bit0 -x3397_bit0 -x3398_bit0 -x3399_bit0 -x3400_bit0 -x3401_bit0 -x3402_bit0 -x3403_bit0 -x3404_bit0 -x3405_bit0 -x3406_bit0 -x3407_bit0 -x3408_bit0 -x3409_bit0 -x3410_bit0 -x3411_bit0 -x3412_bit0 -x3413_bit0 -x3414_bit0 -x3415_bit0 -x3416_bit0 -x3417_bit0 -x3418_bit0 -x3419_bit0 -x3420_bit0 -x3421_bit0 -x3422_bit0 -x3423_bit0 -x3424_bit0 -x3425_bit0 -x3426_bit0 -x3427_bit0 -x3428_bit0 -x3429_bit0 -x3430_bit0 -x3431_bit0 -x3432_bit0 -x3433_bit0 -x3434_bit0 -x3435_bit0 -x3436_bit0 -x3437_bit0 -x3438_bit0 -x3439_bit0 -x3440_bit0 -x3441_bit0 -x3442_bit0 -x3443_bit0 -x3444_bit0 -x3445_bit0 -x3446_bit0 -x3447_bit0 -x3448_bit0 -x3449_bit0 -x3450_bit0 -x3451_bit0 -x3452_bit0 -x3453_bit0 -x3454_bit0 -x3455_bit0 -x3456_bit0 -x3457_bit0 -x3458_bit0 -x3459_bit0 -x3460_bit0 -x3461_bit0 -x3462_bit0 -x3463_bit0 -x3464_bit0 -x3465_bit0 -x3466_bit0 -x3467_bit0 -x3468_bit0 -x3469_bit0 -x3470_bit0 -x3471_bit0 -x3472_bit0 -x3473_bit0 -x3474_bit0 -x3475_bit0 -x3476_bit0 -x3477_bit0 -x3478_bit0 -x3479_bit0 -x3480_bit0 -x3481_bit0 -x3482_bit0 -x3483_bit0 -x3484_bit0 -x3485_bit0 -x3486_bit0 -x3487_bit0 -x3488_bit0 -x3489_bit0 -x3490_bit0 -x3491_bit0 -x3492_bit0 -x3493_bit0 -x3494_bit0 -x3495_bit0 -x3496_bit0 -x3497_bit0 -x3498_bit0 -x3499_bit0 -x3500_bit0 -x3501_bit0 -x3502_bit0 -x3503_bit0 -x3504_bit0 -x3505_bit0 -x3506_bit0 -x3507_bit0 -x3508_bit0 -x3509_bit0 -x3510_bit0 -x3511_bit0 -x3512_bit0 -x3513_bit0 -x3514_bit0 -x3515_bit0 -x3516_bit0 -x3517_bit0 -x3518_bit0 -x3519_bit0 -x3520_bit0 x3521_bit0 -x3522_bit0 -x3523_bit0 -x3524_bit0 -x3525_bit0 -x3526_bit0 -x3527_bit0 -x3528_bit0 -x3529_bit0 -x3530_bit0 -x3531_bit0 -x3532_bit0 -x3533_bit0 -x3534_bit0 -x3535_bit0 -x3536_bit0 -x3537_bit0 -x3538_bit0 -x3539_bit0 -x3540_bit0 -x3541_bit0 -x3542_bit0 -x3543_bit0 -x3544_bit0 -x3545_bit0 -x3546_bit0 -x3547_bit0 -x3548_bit0 -x3549_bit0 -x3550_bit0 -x3551_bit0 -x3552_bit0 -x3553_bit0 -x3554_bit0 -x3555_bit0 -x3556_bit0 -x3557_bit0 -x3558_bit0 -x3559_bit0 -x3560_bit0 -x3561_bit0 -x3562_bit0 -x3563_bit0 -x3564_bit0 -x3565_bit0 -x3566_bit0 -x3567_bit0 -x3568_bit0 -x3569_bit0 -x3570_bit0 -x3571_bit0 -x3572_bit0 -x3573_bit0 -x3574_bit0 -x3575_bit0 -x3576_bit0 -x3577_bit0 -x3578_bit0 -x3579_bit0 -x3580_bit0 -x3581_bit0 -x3582_bit0 -x3583_bit0 -x3584_bit0 -x3585_bit0 -x3586_bit0 -x3587_bit0 -x3588_bit0 -x3589_bit0 -x3590_bit0 -x3591_bit0 -x3592_bit0 -x3593_bit0 -x3594_bit0 -x3595_bit0 -x3596_bit0 -x3597_bit0 -x3598_bit0 -x3599_bit0 -x3600_bit0 -x3601_bit0 -x3602_bit0 -x3603_bit0 -x3604_bit0 -x3605_bit0 -x3606_bit0 -x3607_bit0 -x3608_bit0 -x3609_bit0 -x3610_bit0 -x3611_bit0 -x3612_bit0 -x3613_bit0 -x3614_bit0 -x3615_bit0 -x3616_bit0 -x3617_bit0 -x3618_bit0 -x3619_bit0 -x3620_bit0 -x3621_bit0 -x3622_bit0 -x3623_bit0 -x3624_bit0 -x3625_bit0 -x3626_bit0 -x3627_bit0 -x3628_bit0 -x3629_bit0 -x3630_bit0 -x3631_bit0 -x3632_bit0 -x3633_bit0 -x3634_bit0 -x3635_bit0 -x3636_bit0 -x3637_bit0 -x3638_bit0 -x3639_bit0 -x3640_bit0 -x3641_bit0 -x3642_bit0 -x3643_bit0 -x3644_bit0 -x3645_bit0 -x3646_bit0 -x3647_bit0 -x3648_bit0 -x3649_bit0 -x3650_bit0 -x3651_bit0 -x3652_bit0 -x3653_bit0 -x3654_bit0 -x3655_bit0 -x3656_bit0 -x3657_bit0 -x3658_bit0 -x3659_bit0 -x3660_bit0 -x3661_bit0 -x3662_bit0 -x3663_bit0 -x3664_bit0 -x3665_bit0 -x3666_bit0 -x3667_bit0 -x3668_bit0 -x3669_bit0 -x3670_bit0 -x3671_bit0 -x3672_bit0 -x3673_bit0 -x3674_bit0 -x3675_bit0 -x3676_bit0 -x3677_bit0 -x3678_bit0 -x3679_bit0 -x3680_bit0 -x3681_bit0 -x3682_bit0 -x3683_bit0 -x3684_bit0 -x3685_bit0 -x3686_bit0 -x3687_bit0 -x3688_bit0 -x3689_bit0 -x3690_bit0 -x3691_bit0 -x3692_bit0 -x3693_bit0 -x3694_bit0 -x3695_bit0 -x3696_bit0 -x3697_bit0 -x3698_bit0 -x3699_bit0 -x3700_bit0 -x3701_bit0 -x3702_bit0 -x3703_bit0 -x3704_bit0 -x3705_bit0 -x3706_bit0 -x3707_bit0 x3708_bit0 -x3709_bit0 -x3710_bit0 -x3711_bit0 -x3712_bit0 -x3713_bit0 -x3714_bit0 -x3715_bit0 -x3716_bit0 -x3717_bit0 -x3718_bit0 -x3719_bit0 -x3720_bit0 -x3721_bit0 -x3722_bit0 -x3723_bit0 -x3724_bit0 -x3725_bit0 -x3726_bit0 -x3727_bit0 -x3728_bit0 -x3729_bit0 -x3730_bit0 -x3731_bit0 -x3732_bit0 -x3733_bit0 -x3734_bit0 -x3735_bit0 -x3736_bit0 -x3737_bit0 -x3738_bit0 -x3739_bit0 -x3740_bit0 -x3741_bit0 -x3742_bit0 -x3743_bit0 -x3744_bit0 -x3745_bit0 -x3746_bit0 -x3747_bit0 -x3748_bit0 -x3749_bit0 -x3750_bit0 -x3751_bit0 -x3752_bit0 -x3753_bit0 -x3754_bit0 -x3755_bit0 -x3756_bit0 -x3757_bit0 -x3758_bit0 -x3759_bit0 -x3760_bit0 -x3761_bit0 -x3762_bit0 -x3763_bit0 -x3764_bit0 -x3765_bit0 -x3766_bit0 -x3767_bit0 -x3768_bit0 -x3769_bit0 -x3770_bit0 -x3771_bit0 -x3772_bit0 -x3773_bit0 -x3774_bit0 -x3775_bit0 -x3776_bit0 -x3777_bit0 -x3778_bit0 -x3779_bit0 -x3780_bit0 -x3781_bit0 -x3782_bit0 -x3783_bit0 -x3784_bit0 -x3785_bit0 -x3786_bit0 -x3787_bit0 -x3788_bit0 -x3789_bit0 -x3790_bit0 -x3791_bit0 -x3792_bit0 -x3793_bit0 -x3794_bit0 -x3795_bit0 -x3796_bit0 -x3797_bit0 -x3798_bit0 -x3799_bit0 -x3800_bit0 -x3801_bit0 -x3802_bit0 -x3803_bit0 -x3804_bit0 -x3805_bit0 -x3806_bit0 -x3807_bit0 -x3808_bit0 x3809_bit0 -x3810_bit0 -x3811_bit0 -x3812_bit0 -x3813_bit0 -x3814_bit0 -x3815_bit0 -x3816_bit0 -x3817_bit0 -x3818_bit0 -x3819_bit0 -x3820_bit0 -x3821_bit0 -x3822_bit0 -x3823_bit0 -x3824_bit0 -x3825_bit0 -x3826_bit0 -x3827_bit0 -x3828_bit0 -x3829_bit0 -x3830_bit0 -x3831_bit0 -x3832_bit0 -x3833_bit0 -x3834_bit0 -x3835_bit0 -x3836_bit0 -x3837_bit0 -x3838_bit0 -x3839_bit0 -x3840_bit0 -x3841_bit0 -x3842_bit0 -x3843_bit0 -x3844_bit0 -x3845_bit0 -x3846_bit0 -x3847_bit0 -x3848_bit0 -x3849_bit0 -x3850_bit0 -x3851_bit0 -x3852_bit0 -x3853_bit0 -x3854_bit0 -x3855_bit0 -x3856_bit0 -x3857_bit0 -x3858_bit0 -x3859_bit0 -x3860_bit0 -x3861_bit0 -x3862_bit0 -x3863_bit0 -x3864_bit0 -x3865_bit0 -x3866_bit0 -x3867_bit0 -x3868_bit0 -x3869_bit0 -x3870_bit0 -x3871_bit0 -x3872_bit0 -x3873_bit0 -x3874_bit0 -x3875_bit0 -x3876_bit0 -x3877_bit0 -x3878_bit0 -x3879_bit0 -x3880_bit0 -x3881_bit0 -x3882_bit0 -x3883_bit0 -x3884_bit0 -x3885_bit0 -x3886_bit0 -x3887_bit0 -x3888_bit0 -x3889_bit0 -x3890_bit0 -x3891_bit0 -x3892_bit0 -x3893_bit0 -x3894_bit0 -x3895_bit0 -x3896_bit0 -x3897_bit0 -x3898_bit0 -x3899_bit0 -x3900_bit0 -x3901_bit0 -x3902_bit0 -x3903_bit0 -x3904_bit0 -x3905_bit0 -x3906_bit0 -x3907_bit0 -x3908_bit0 -x3909_bit0 -x3910_bit0 -x3911_bit0 -x3912_bit0 -x3913_bit0 -x3914_bit0 -x3915_bit0 -x3916_bit0 -x3917_bit0 -x3918_bit0 -x3919_bit0 -x3920_bit0 -x3921_bit0 -x3922_bit0 -x3923_bit0 -x3924_bit0 -x3925_bit0 -x3926_bit0 -x3927_bit0 -x3928_bit0 -x3929_bit0 -x3930_bit0 -x3931_bit0 -x3932_bit0 -x3933_bit0 -x3934_bit0 -x3935_bit0 -x3936_bit0 -x3937_bit0 -x3938_bit0 -x3939_bit0 -x3940_bit0 -x3941_bit0 -x3942_bit0 -x3943_bit0 -x3944_bit0 -x3945_bit0 -x3946_bit0 -x3947_bit0 -x3948_bit0 -x3949_bit0 -x3950_bit0 -x3951_bit0 -x3952_bit0 -x3953_bit0 -x3954_bit0 -x3955_bit0 -x3956_bit0 -x3957_bit0 -x3958_bit0 -x3959_bit0 -x3960_bit0 -x3961_bit0 -x3962_bit0 -x3963_bit0 -x3964_bit0 -x3965_bit0 -x3966_bit0 -x3967_bit0 -x3968_bit0 -x3969_bit0 -x3970_bit0 -x3971_bit0 -x3972_bit0 -x3973_bit0 -x3974_bit0 -x3975_bit0 -x3976_bit0 -x3977_bit0 -x3978_bit0 -x3979_bit0 -x3980_bit0 -x3981_bit0 -x3982_bit0 -x3983_bit0 -x3984_bit0 -x3985_bit0 -x3986_bit0 -x3987_bit0 -x3988_bit0 -x3989_bit0 -x3990_bit0 -x3991_bit0 -x3992_bit0 -x3993_bit0 -x3994_bit0 -x3995_bit0 -x3996_bit0 -x3997_bit0 -x3998_bit0 -x3999_bit0 -x4000_bit0 -x4001_bit0 -x4002_bit0 -x4003_bit0 -x4004_bit0 -x4005_bit0 -x4006_bit0 -x4007_bit0 -x4008_bit0 -x4009_bit0 -x4010_bit0 -x4011_bit0 -x4012_bit0 -x4013_bit0 -x4014_bit0 -x4015_bit0 -x4016_bit0 -x4017_bit0 -x4018_bit0 -x4019_bit0 -x4020_bit0 -x4021_bit0 -x4022_bit0 -x4023_bit0 -x4024_bit0 -x4025_bit0 -x4026_bit0 -x4027_bit0 -x4028_bit0 -x4029_bit0 -x4030_bit0 -x4031_bit0 -x4032_bit0 -x4033_bit0 -x4034_bit0 -x4035_bit0 -x4036_bit0 x4037_bit0 -x4038_bit0 -x4039_bit0 -x4040_bit0 -x4041_bit0 -x4042_bit0 -x4043_bit0 -x4044_bit0 -x4045_bit0 -x4046_bit0 -x4047_bit0 -x4048_bit0 -x4049_bit0 -x4050_bit0 -x4051_bit0 -x4052_bit0 -x4053_bit0 -x4054_bit0 -x4055_bit0 -x4056_bit0 -x4057_bit0 -x4058_bit0 -x4059_bit0 -x4060_bit0 -x4061_bit0 -x4062_bit0 -x4063_bit0 -x4064_bit0 -x4065_bit0 -x4066_bit0 -x4067_bit0 -x4068_bit0 -x4069_bit0 -x4070_bit0 -x4071_bit0 -x4072_bit0 -x4073_bit0 -x4074_bit0 -x4075_bit0 -x4076_bit0 -x4077_bit0 -x4078_bit0 -x4079_bit0 -x4080_bit0 -x4081_bit0 -x4082_bit0 -x4083_bit0 -x4084_bit0 -x4085_bit0 -x4086_bit0 -x4087_bit0 -x4088_bit0 -x4089_bit0 -x4090_bit0 -x4091_bit0 -x4092_bit0 -x4093_bit0 -x4094_bit0 -x4095_bit0 -x4096_bit0 -x4097_bit0 -x4098_bit0 -x4099_bit0 -x4100_bit0 -x4101_bit0 -x4102_bit0 -x4103_bit0 -x4104_bit0 -x4105_bit0 -x4106_bit0 -x4107_bit0 -x4108_bit0 -x4109_bit0 -x4110_bit0 -x4111_bit0 -x4112_bit0 -x4113_bit0 -x4114_bit0 -x4115_bit0 -x4116_bit0 -x4117_bit0 -x4118_bit0 -x4119_bit0 -x4120_bit0 -x4121_bit0 -x4122_bit0 -x4123_bit0 -x4124_bit0 -x4125_bit0 -x4126_bit0 -x4127_bit0 -x4128_bit0 -x4129_bit0 -x4130_bit0 -x4131_bit0 -x4132_bit0 -x4133_bit0 -x4134_bit0 -x4135_bit0 -x4136_bit0 -x4137_bit0 -x4138_bit0 -x4139_bit0 -x4140_bit0 -x4141_bit0 -x4142_bit0 -x4143_bit0 -x4144_bit0 -x4145_bit0 -x4146_bit0 -x4147_bit0 -x4148_bit0 -x4149_bit0 -x4150_bit0 -x4151_bit0 -x4152_bit0 -x4153_bit0 -x4154_bit0 -x4155_bit0 -x4156_bit0 -x4157_bit0 -x4158_bit0 -x4159_bit0 -x4160_bit0 -x4161_bit0 -x4162_bit0 -x4163_bit0 -x4164_bit0 -x4165_bit0 -x4166_bit0 -x4167_bit0 -x4168_bit0 -x4169_bit0 -x4170_bit0 -x4171_bit0 -x4172_bit0 -x4173_bit0 -x4174_bit0 -x4175_bit0 -x4176_bit0 -x4177_bit0 -x4178_bit0 -x4179_bit0 -x4180_bit0 -x4181_bit0 -x4182_bit0 -x4183_bit0 -x4184_bit0 -x4185_bit0 -x4186_bit0 -x4187_bit0 -x4188_bit0 -x4189_bit0 -x4190_bit0 -x4191_bit0 -x4192_bit0 -x4193_bit0 -x4194_bit0 -x4195_bit0 -x4196_bit0 -x4197_bit0 -x4198_bit0 -x4199_bit0 -x4200_bit0 -x4201_bit0 -x4202_bit0 -x4203_bit0 -x4204_bit0 -x4205_bit0 -x4206_bit0 -x4207_bit0 -x4208_bit0 -x4209_bit0 -x4210_bit0 -x4211_bit0 -x4212_bit0 -x4213_bit0 -x4214_bit0 -x4215_bit0 -x4216_bit0 -x4217_bit0 -x4218_bit0 -x4219_bit0 -x4220_bit0 -x4221_bit0 -x4222_bit0 -x4223_bit0 -x4224_bit0 -x4225_bit0 -x4226_bit0 -x4227_bit0 -x4228_bit0 -x4229_bit0 -x4230_bit0 -x4231_bit0 -x4232_bit0 -x4233_bit0 -x4234_bit0 -x4235_bit0 -x4236_bit0 -x4237_bit0 -x4238_bit0 -x4239_bit0 -x4240_bit0 -x4241_bit0 -x4242_bit0 -x4243_bit0 -x4244_bit0 -x4245_bit0 -x4246_bit0 -x4247_bit0 -x4248_bit0 -x4249_bit0 -x4250_bit0 -x4251_bit0 -x4252_bit0 -x4253_bit0 -x4254_bit0 -x4255_bit0 -x4256_bit0 -x4257_bit0 -x4258_bit0 -x4259_bit0 -x4260_bit0 -x4261_bit0 -x4262_bit0 -x4263_bit0 -x4264_bit0 -x4265_bit0 -x4266_bit0 -x4267_bit0 -x4268_bit0 -x4269_bit0 -x4270_bit0 -x4271_bit0 -x4272_bit0 -x4273_bit0 -x4274_bit0 -x4275_bit0 -x4276_bit0 -x4277_bit0 -x4278_bit0 -x4279_bit0 -x4280_bit0 -x4281_bit0 -x4282_bit0 -x4283_bit0 -x4284_bit0 x4285_bit0 -x4286_bit0 -x4287_bit0 -x4288_bit0 -x4289_bit0 -x4290_bit0 -x4291_bit0 -x4292_bit0 -x4293_bit0 -x4294_bit0 -x4295_bit0 -x4296_bit0 -x4297_bit0 -x4298_bit0 -x4299_bit0 x4300_bit0 -x4301_bit0 -x4302_bit0 -x4303_bit0 -x4304_bit0 -x4305_bit0 -x4306_bit0 -x4307_bit0 -x4308_bit0 -x4309_bit0 -x4310_bit0 -x4311_bit0 -x4312_bit0 -x4313_bit0 -x4314_bit0 -x4315_bit0 -x4316_bit0 -x4317_bit0 -x4318_bit0 -x4319_bit0 -x4320_bit0 -x4321_bit0 -x4322_bit0 -x4323_bit0 -x4324_bit0 -x4325_bit0 -x4326_bit0 -x4327_bit0 -x4328_bit0 -x4329_bit0 -x4330_bit0 -x4331_bit0 -x4332_bit0 -x4333_bit0 -x4334_bit0 -x4335_bit0 -x4336_bit0 -x4337_bit0 -x4338_bit0 -x4339_bit0 -x4340_bit0 -x4341_bit0 -x4342_bit0 -x4343_bit0 -x4344_bit0 -x4345_bit0 -x4346_bit0 -x4347_bit0 -x4348_bit0 -x4349_bit0 -x4350_bit0 -x4351_bit0 -x4352_bit0 -x4353_bit0 -x4354_bit0 -x4355_bit0 -x4356_bit0 -x4357_bit0 -x4358_bit0 -x4359_bit0 -x4360_bit0 -x4361_bit0 -x4362_bit0 -x4363_bit0 -x4364_bit0 -x4365_bit0 -x4366_bit0 -x4367_bit0 -x4368_bit0 -x4369_bit0 -x4370_bit0 -x4371_bit0 -x4372_bit0 -x4373_bit0 -x4374_bit0 -x4375_bit0 -x4376_bit0 -x4377_bit0 -x4378_bit0 -x4379_bit0 -x4380_bit0 -x4381_bit0 -x4382_bit0 -x4383_bit0 -x4384_bit0 -x4385_bit0 -x4386_bit0 -x4387_bit0 -x4388_bit0 -x4389_bit0 -x4390_bit0 -x4391_bit0 -x4392_bit0 -x4393_bit0 -x4394_bit0 -x4395_bit0 -x4396_bit0 -x4397_bit0 -x4398_bit0 -x4399_bit0 -x4400_bit0 -x4401_bit0 -x4402_bit0 -x4403_bit0 -x4404_bit0 -x4405_bit0 -x4406_bit0 -x4407_bit0 -x4408_bit0 -x4409_bit0 -x4410_bit0 -x4411_bit0 -x4412_bit0 -x4413_bit0 -x4414_bit0 -x4415_bit0 -x4416_bit0 -x4417_bit0 -x4418_bit0 -x4419_bit0 -x4420_bit0 -x4421_bit0 -x4422_bit0 -x4423_bit0 -x4424_bit0 -x4425_bit0 -x4426_bit0 -x4427_bit0 -x4428_bit0 -x4429_bit0 -x4430_bit0 -x4431_bit0 -x4432_bit0 -x4433_bit0 -x4434_bit0 -x4435_bit0 -x4436_bit0 -x4437_bit0 -x4438_bit0 -x4439_bit0 -x4440_bit0 -x4441_bit0 -x4442_bit0 -x4443_bit0 -x4444_bit0 -x4445_bit0 -x4446_bit0 -x4447_bit0 -x4448_bit0 -x4449_bit0 -x4450_bit0 -x4451_bit0 -x4452_bit0 -x4453_bit0 -x4454_bit0 -x4455_bit0 -x4456_bit0 -x4457_bit0 -x4458_bit0 -x4459_bit0 -x4460_bit0 -x4461_bit0 -x4462_bit0 -x4463_bit0 -x4464_bit0 -x4465_bit0 -x4466_bit0 -x4467_bit0 -x4468_bit0 -x4469_bit0 -x4470_bit0 -x4471_bit0 -x4472_bit0 -x4473_bit0 -x4474_bit0 -x4475_bit0 -x4476_bit0 -x4477_bit0 -x4478_bit0 -x4479_bit0 -x4480_bit0 -x4481_bit0 -x4482_bit0 -x4483_bit0 -x4484_bit0 -x4485_bit0 -x4486_bit0 -x4487_bit0 -x4488_bit0 -x4489_bit0 -x4490_bit0 -x4491_bit0 -x4492_bit0 -x4493_bit0 -x4494_bit0 -x4495_bit0 -x4496_bit0 -x4497_bit0 -x4498_bit0 -x4499_bit0 -x4500_bit0 -x4501_bit0 -x4502_bit0 -x4503_bit0 -x4504_bit0 -x4505_bit0 -x4506_bit0 -x4507_bit0 -x4508_bit0 -x4509_bit0 -x4510_bit0 -x4511_bit0 -x4512_bit0 -x4513_bit0 -x4514_bit0 -x4515_bit0 -x4516_bit0 -x4517_bit0 -x4518_bit0 -x4519_bit0 -x4520_bit0 -x4521_bit0 -x4522_bit0 -x4523_bit0 -x4524_bit0 -x4525_bit0 -x4526_bit0 -x4527_bit0 -x4528_bit0 -x4529_bit0 -x4530_bit0 -x4531_bit0 -x4532_bit0 -x4533_bit0 -x4534_bit0 -x4535_bit0 -x4536_bit0 -x4537_bit0 -x4538_bit0 -x4539_bit0 -x4540_bit0 -x4541_bit0 -x4542_bit0 -x4543_bit0 -x4544_bit0 -x4545_bit0 -x4546_bit0 -x4547_bit0 -x4548_bit0 -x4549_bit0 -x4550_bit0 -x4551_bit0 -x4552_bit0 -x4553_bit0 -x4554_bit0 -x4555_bit0 -x4556_bit0 -x4557_bit0 -x4558_bit0 -x4559_bit0 -x4560_bit0 -x4561_bit0 -x4562_bit0 -x4563_bit0 -x4564_bit0 -x4565_bit0 -x4566_bit0 -x4567_bit0 -x4568_bit0 -x4569_bit0 -x4570_bit0 -x4571_bit0 -x4572_bit0 -x4573_bit0 -x4574_bit0 -x4575_bit0 -x4576_bit0 -x4577_bit0 -x4578_bit0 -x4579_bit0 -x4580_bit0 -x4581_bit0 -x4582_bit0 -x4583_bit0 -x4584_bit0 -x4585_bit0 -x4586_bit0 -x4587_bit0 -x4588_bit0 -x4589_bit0 -x4590_bit0 -x4591_bit0 -x4592_bit0 -x4593_bit0 -x4594_bit0 -x4595_bit0 -x4596_bit0 -x4597_bit0 -x4598_bit0 -x4599_bit0 -x4600_bit0 -x4601_bit0 -x4602_bit0 -x4603_bit0 -x4604_bit0 -x4605_bit0 -x4606_bit0 -x4607_bit0 -x4608_bit0 -x4609_bit0 -x4610_bit0 -x4611_bit0 -x4612_bit0 -x4613_bit0 -x4614_bit0 -x4615_bit0 -x4616_bit0 -x4617_bit0 -x4618_bit0 -x4619_bit0 -x4620_bit0 -x4621_bit0 -x4622_bit0 -x4623_bit0 -x4624_bit0 -x4625_bit0 -x4626_bit0 -x4627_bit0 -x4628_bit0 -x4629_bit0 -x4630_bit0 -x4631_bit0 -x4632_bit0 -x4633_bit0 -x4634_bit0 -x4635_bit0 -x4636_bit0 -x4637_bit0 -x4638_bit0 -x4639_bit0 -x4640_bit0 -x4641_bit0 -x4642_bit0 -x4643_bit0 -x4644_bit0 -x4645_bit0 -x4646_bit0 -x4647_bit0 -x4648_bit0 -x4649_bit0 -x4650_bit0 -x4651_bit0 -x4652_bit0 -x4653_bit0 -x4654_bit0 -x4655_bit0 -x4656_bit0 -x4657_bit0 -x4658_bit0 -x4659_bit0 -x4660_bit0 -x4661_bit0 -x4662_bit0 -x4663_bit0 -x4664_bit0 -x4665_bit0 -x4666_bit0 -x4667_bit0 -x4668_bit0 -x4669_bit0 -x4670_bit0 -x4671_bit0 -x4672_bit0 -x4673_bit0 -x4674_bit0 -x4675_bit0 -x4676_bit0 -x4677_bit0 -x4678_bit0 -x4679_bit0 -x4680_bit0 -x4681_bit0 -x4682_bit0 -x4683_bit0 -x4684_bit0 -x4685_bit0 -x4686_bit0 -x4687_bit0 -x4688_bit0 -x4689_bit0 -x4690_bit0 -x4691_bit0 -x4692_bit0 -x4693_bit0 -x4694_bit0 -x4695_bit0 -x4696_bit0 -x4697_bit0 -x4698_bit0 -x4699_bit0 -x4700_bit0 -x4701_bit0 -x4702_bit0 -x4703_bit0 -x4704_bit0 -x4705_bit0 -x4706_bit0 -x4707_bit0 -x4708_bit0 -x4709_bit0 -x4710_bit0 -x4711_bit0 -x4712_bit0 -x4713_bit0 -x4714_bit0 -x4715_bit0 -x4716_bit0 -x4717_bit0 -x4718_bit0 -x4719_bit0 -x4720_bit0 -x4721_bit0 -x4722_bit0 -x4723_bit0 -x4724_bit0 -x4725_bit0 -x4726_bit0 -x4727_bit0 -x4728_bit0 -x4729_bit0 -x4730_bit0 -x4731_bit0 -x4732_bit0 -x4733_bit0 -x4734_bit0 -x4735_bit0 -x4736_bit0 -x4737_bit0 -x4738_bit0 -x4739_bit0 -x4740_bit0 -x4741_bit0 -x4742_bit0 -x4743_bit0 -x4744_bit0 -x4745_bit0 -x4746_bit0 -x4747_bit0 -x4748_bit0 -x4749_bit0 -x4750_bit0 -x4751_bit0 -x4752_bit0 -x4753_bit0 -x4754_bit0 -x4755_bit0 -x4756_bit0 -x4757_bit0 -x4758_bit0 -x4759_bit0 -x4760_bit0 -x4761_bit0 -x4762_bit0 -x4763_bit0 -x4764_bit0 -x4765_bit0 -x4766_bit0 -x4767_bit0 -x4768_bit0 -x4769_bit0 -x4770_bit0 -x4771_bit0 -x4772_bit0 -x4773_bit0 -x4774_bit0 -x4775_bit0 -x4776_bit0 -x4777_bit0 -x4778_bit0 -x4779_bit0 -x4780_bit0 -x4781_bit0 -x4782_bit0 -x4783_bit0 -x4784_bit0 -x4785_bit0 -x4786_bit0 -x4787_bit0 -x4788_bit0 -x4789_bit0 -x4790_bit0 -x4791_bit0 -x4792_bit0 -x4793_bit0 -x4794_bit0 -x4795_bit0 -x4796_bit0 -x4797_bit0 -x4798_bit0 -x4799_bit0 -x4800_bit0 -x4801_bit0 -x4802_bit0 -x4803_bit0 -x4804_bit0 -x4805_bit0 -x4806_bit0 -x4807_bit0 -x4808_bit0 -x4809_bit0 -x4810_bit0 -x4811_bit0 -x4812_bit0 -x4813_bit0 -x4814_bit0 -x4815_bit0 -x4816_bit0 -x4817_bit0 -x4818_bit0 -x4819_bit0 -x4820_bit0 -x4821_bit0 -x4822_bit0 -x4823_bit0 -x4824_bit0 -x4825_bit0 -x4826_bit0 -x4827_bit0 -x4828_bit0 -x4829_bit0 -x4830_bit0 -x4831_bit0 -x4832_bit0 -x4833_bit0 -x4834_bit0 -x4835_bit0 -x4836_bit0 -x4837_bit0 -x4838_bit0 -x4839_bit0 -x4840_bit0 -x4841_bit0 -x4842_bit0 -x4843_bit0 -x4844_bit0 -x4845_bit0 -x4846_bit0 -x4847_bit0 -x4848_bit0 -x4849_bit0 -x4850_bit0 -x4851_bit0 -x4852_bit0 -x4853_bit0 -x4854_bit0 -x4855_bit0 -x4856_bit0 -x4857_bit0 -x4858_bit0 -x4859_bit0 -x4860_bit0 -x4861_bit0 -x4862_bit0 -x4863_bit0 -x4864_bit0 -x4865_bit0 -x4866_bit0 -x4867_bit0 -x4868_bit0 -x4869_bit0 -x4870_bit0 -x4871_bit0 -x4872_bit0 -x4873_bit0 -x4874_bit0 -x4875_bit0 -x4876_bit0 -x4877_bit0 -x4878_bit0 -x4879_bit0 -x4880_bit0 -x4881_bit0 x4882_bit0 -x4883_bit0 -x4884_bit0 -x4885_bit0 -x4886_bit0 -x4887_bit0 -x4888_bit0 -x4889_bit0 -x4890_bit0 -x4891_bit0 -x4892_bit0 -x4893_bit0 -x4894_bit0 -x4895_bit0 -x4896_bit0 -x4897_bit0 -x4898_bit0 -x4899_bit0 -x4900_bit0 -x4901_bit0 -x4902_bit0 -x4903_bit0 -x4904_bit0 -x4905_bit0 -x4906_bit0 -x4907_bit0 -x4908_bit0 -x4909_bit0 -x4910_bit0 -x4911_bit0 -x4912_bit0 -x4913_bit0 -x4914_bit0 -x4915_bit0 -x4916_bit0 -x4917_bit0 -x4918_bit0 -x4919_bit0 -x4920_bit0 -x4921_bit0 -x4922_bit0 -x4923_bit0 -x4924_bit0 -x4925_bit0 -x4926_bit0 -x4927_bit0 -x4928_bit0 -x4929_bit0 -x4930_bit0 -x4931_bit0 -x4932_bit0 -x4933_bit0 -x4934_bit0 -x4935_bit0 -x4936_bit0 x4937_bit0 -x4938_bit0 -x4939_bit0 -x4940_bit0 -x4941_bit0 -x4942_bit0 -x4943_bit0 -x4944_bit0 -x4945_bit0 -x4946_bit0 -x4947_bit0 -x4948_bit0 -x4949_bit0 -x4950_bit0 -x4951_bit0 -x4952_bit0 -x4953_bit0 -x4954_bit0 -x4955_bit0 -x4956_bit0 -x4957_bit0 -x4958_bit0 -x4959_bit0 -x4960_bit0 -x4961_bit0 -x4962_bit0 -x4963_bit0 -x4964_bit0 -x4965_bit0 -x4966_bit0 -x4967_bit0 -x4968_bit0 -x4969_bit0 -x4970_bit0 -x4971_bit0 -x4972_bit0 -x4973_bit0 -x4974_bit0 -x4975_bit0 -x4976_bit0 -x4977_bit0 -x4978_bit0 -x4979_bit0 -x4980_bit0 -x4981_bit0 -x4982_bit0 -x4983_bit0 -x4984_bit0 -x4985_bit0 -x4986_bit0 -x4987_bit0 -x4988_bit0 -x4989_bit0 -x4990_bit0 -x4991_bit0 -x4992_bit0 -x4993_bit0 -x4994_bit0 -x4995_bit0 -x4996_bit0 -x4997_bit0 -x4998_bit0 -x4999_bit0 -x5000_bit0 -x5001_bit0 -x5002_bit0 -x5003_bit0 -x5004_bit0 -x5005_bit0 -x5006_bit0 -x5007_bit0 -x5008_bit0 -x5009_bit0 -x5010_bit0 -x5011_bit0 -x5012_bit0 -x5013_bit0 -x5014_bit0 -x5015_bit0 -x5016_bit0 -x5017_bit0 -x5018_bit0 -x5019_bit0 -x5020_bit0 -x5021_bit0 -x5022_bit0 -x5023_bit0 -x5024_bit0 -x5025_bit0 -x5026_bit0 -x5027_bit0 -x5028_bit0 -x5029_bit0 -x5030_bit0 -x5031_bit0 -x5032_bit0 -x5033_bit0 -x5034_bit0 -x5035_bit0 -x5036_bit0 -x5037_bit0 -x5038_bit0 -x5039_bit0 -x5040_bit0 -x5041_bit0 -x5042_bit0 -x5043_bit0 -x5044_bit0 -x5045_bit0 -x5046_bit0 -x5047_bit0 -x5048_bit0 -x5049_bit0 -x5050_bit0 -x5051_bit0 -x5052_bit0 -x5053_bit0 -x5054_bit0 -x5055_bit0 -x5056_bit0 -x5057_bit0 -x5058_bit0 -x5059_bit0 -x5060_bit0 -x5061_bit0 -x5062_bit0 -x5063_bit0 -x5064_bit0 -x5065_bit0 -x5066_bit0 -x5067_bit0 -x5068_bit0 -x5069_bit0 -x5070_bit0 -x5071_bit0 -x5072_bit0 -x5073_bit0 -x5074_bit0 -x5075_bit0 -x5076_bit0 -x5077_bit0 -x5078_bit0 -x5079_bit0 -x5080_bit0 -x5081_bit0 -x5082_bit0 -x5083_bit0 -x5084_bit0 -x5085_bit0 -x5086_bit0 -x5087_bit0 -x5088_bit0 -x5089_bit0 -x5090_bit0 -x5091_bit0 -x5092_bit0 -x5093_bit0 -x5094_bit0 -x5095_bit0 -x5096_bit0 -x5097_bit0 -x5098_bit0 -x5099_bit0 -x5100_bit0 -x5101_bit0 -x5102_bit0 -x5103_bit0 -x5104_bit0 -x5105_bit0 -x5106_bit0 -x5107_bit0 -x5108_bit0 -x5109_bit0 -x5110_bit0 -x5111_bit0 -x5112_bit0 -x5113_bit0 -x5114_bit0 -x5115_bit0 -x5116_bit0 -x5117_bit0 -x5118_bit0 -x5119_bit0 -x5120_bit0 -x5121_bit0 -x5122_bit0 -x5123_bit0 -x5124_bit0 -x5125_bit0 -x5126_bit0 -x5127_bit0 -x5128_bit0 -x5129_bit0 -x5130_bit0 -x5131_bit0 -x5132_bit0 -x5133_bit0 -x5134_bit0 -x5135_bit0 -x5136_bit0 -x5137_bit0 -x5138_bit0 -x5139_bit0 -x5140_bit0 -x5141_bit0 -x5142_bit0 -x5143_bit0 -x5144_bit0 -x5145_bit0 -x5146_bit0 -x5147_bit0 -x5148_bit0 -x5149_bit0 -x5150_bit0 -x5151_bit0 -x5152_bit0 -x5153_bit0 -x5154_bit0 -x5155_bit0 -x5156_bit0 -x5157_bit0 -x5158_bit0 -x5159_bit0 -x5160_bit0 -x5161_bit0 -x5162_bit0 -x5163_bit0 -x5164_bit0 -x5165_bit0 -x5166_bit0 -x5167_bit0 -x5168_bit0 -x5169_bit0 -x5170_bit0 -x5171_bit0 -x5172_bit0 -x5173_bit0 -x5174_bit0 -x5175_bit0 x5176_bit0 -x5177_bit0 -x5178_bit0 -x5179_bit0 -x5180_bit0 -x5181_bit0 -x5182_bit0 -x5183_bit0 -x5184_bit0 -x5185_bit0 -x5186_bit0 -x5187_bit0 -x5188_bit0 -x5189_bit0 -x5190_bit0 -x5191_bit0 -x5192_bit0 -x5193_bit0 -x5194_bit0 -x5195_bit0 -x5196_bit0 -x5197_bit0 -x5198_bit0 -x5199_bit0 -x5200_bit0 -x5201_bit0 -x5202_bit0 -x5203_bit0 -x5204_bit0 -x5205_bit0 -x5206_bit0 -x5207_bit0 -x5208_bit0 -x5209_bit0 -x5210_bit0 -x5211_bit0 -x5212_bit0 -x5213_bit0 -x5214_bit0 -x5215_bit0 -x5216_bit0 -x5217_bit0 -x5218_bit0 -x5219_bit0 -x5220_bit0 -x5221_bit0 -x5222_bit0 -x5223_bit0 -x5224_bit0 -x5225_bit0 -x5226_bit0 -x5227_bit0 -x5228_bit0 -x5229_bit0 -x5230_bit0 -x5231_bit0 -x5232_bit0 -x5233_bit0 -x5234_bit0 -x5235_bit0 -x5236_bit0 -x5237_bit0 -x5238_bit0 -x5239_bit0 -x5240_bit0 -x5241_bit0 -x5242_bit0 -x5243_bit0 -x5244_bit0 -x5245_bit0 -x5246_bit0 -x5247_bit0 -x5248_bit0 -x5249_bit0 -x5250_bit0 -x5251_bit0 -x5252_bit0 -x5253_bit0 -x5254_bit0 -x5255_bit0 -x5256_bit0 -x5257_bit0 -x5258_bit0 -x5259_bit0 -x5260_bit0 -x5261_bit0 -x5262_bit0 -x5263_bit0 -x5264_bit0 -x5265_bit0 -x5266_bit0 -x5267_bit0 -x5268_bit0 -x5269_bit0 -x5270_bit0 -x5271_bit0 -x5272_bit0 -x5273_bit0 -x5274_bit0 -x5275_bit0 -x5276_bit0 -x5277_bit0 -x5278_bit0 -x5279_bit0 -x5280_bit0 -x5281_bit0 -x5282_bit0 -x5283_bit0 -x5284_bit0 -x5285_bit0 -x5286_bit0 -x5287_bit0 -x5288_bit0 -x5289_bit0 -x5290_bit0 -x5291_bit0 -x5292_bit0 -x5293_bit0 -x5294_bit0 -x5295_bit0 -x5296_bit0 -x5297_bit0 -x5298_bit0 -x5299_bit0 -x5300_bit0 -x5301_bit0 -x5302_bit0 -x5303_bit0 -x5304_bit0 -x5305_bit0 -x5306_bit0 -x5307_bit0 -x5308_bit0 -x5309_bit0 -x5310_bit0 -x5311_bit0 -x5312_bit0 -x5313_bit0 -x5314_bit0 -x5315_bit0 -x5316_bit0 -x5317_bit0 -x5318_bit0 -x5319_bit0 -x5320_bit0 -x5321_bit0 -x5322_bit0 -x5323_bit0 -x5324_bit0 x5325_bit0 -x5326_bit0 -x5327_bit0 -x5328_bit0 -x5329_bit0 -x5330_bit0 -x5331_bit0 -x5332_bit0 -x5333_bit0 -x5334_bit0 -x5335_bit0 -x5336_bit0 -x5337_bit0 -x5338_bit0 -x5339_bit0 -x5340_bit0 -x5341_bit0 -x5342_bit0 -x5343_bit0 -x5344_bit0 -x5345_bit0 -x5346_bit0 -x5347_bit0 -x5348_bit0 -x5349_bit0 -x5350_bit0 -x5351_bit0 -x5352_bit0 -x5353_bit0 -x5354_bit0 -x5355_bit0 -x5356_bit0 -x5357_bit0 -x5358_bit0 -x5359_bit0 -x5360_bit0 -x5361_bit0 -x5362_bit0 -x5363_bit0 -x5364_bit0 -x5365_bit0 -x5366_bit0 -x5367_bit0 -x5368_bit0 -x5369_bit0 -x5370_bit0 -x5371_bit0 -x5372_bit0 -x5373_bit0 -x5374_bit0 -x5375_bit0 -x5376_bit0 -x5377_bit0 -x5378_bit0 -x5379_bit0 -x5380_bit0 -x5381_bit0 -x5382_bit0 -x5383_bit0 -x5384_bit0 -x5385_bit0 -x5386_bit0 -x5387_bit0 -x5388_bit0 -x5389_bit0 -x5390_bit0 -x5391_bit0 -x5392_bit0 -x5393_bit0 -x5394_bit0 -x5395_bit0 -x5396_bit0 -x5397_bit0 -x5398_bit0 -x5399_bit0 -x5400_bit0 -x5401_bit0 -x5402_bit0 -x5403_bit0 -x5404_bit0 -x5405_bit0 -x5406_bit0 -x5407_bit0 -x5408_bit0 -x5409_bit0 -x5410_bit0 -x5411_bit0 -x5412_bit0 -x5413_bit0 -x5414_bit0 -x5415_bit0 -x5416_bit0 -x5417_bit0 -x5418_bit0 -x5419_bit0 -x5420_bit0 -x5421_bit0 -x5422_bit0 -x5423_bit0 -x5424_bit0 -x5425_bit0 -x5426_bit0 -x5427_bit0 -x5428_bit0 -x5429_bit0 -x5430_bit0 -x5431_bit0 -x5432_bit0 -x5433_bit0 -x5434_bit0 -x5435_bit0 -x5436_bit0 -x5437_bit0 -x5438_bit0 -x5439_bit0 -x5440_bit0 -x5441_bit0 -x5442_bit0 -x5443_bit0 -x5444_bit0 -x5445_bit0 -x5446_bit0 -x5447_bit0 -x5448_bit0 -x5449_bit0 -x5450_bit0 -x5451_bit0 -x5452_bit0 -x5453_bit0 -x5454_bit0 -x5455_bit0 -x5456_bit0 -x5457_bit0 -x5458_bit0 -x5459_bit0 -x5460_bit0 -x5461_bit0 -x5462_bit0 -x5463_bit0 -x5464_bit0 -x5465_bit0 -x5466_bit0 -x5467_bit0 -x5468_bit0 -x5469_bit0 -x5470_bit0 -x5471_bit0 -x5472_bit0 -x5473_bit0 -x5474_bit0 -x5475_bit0 -x5476_bit0 -x5477_bit0 -x5478_bit0 -x5479_bit0 -x5480_bit0 -x5481_bit0 -x5482_bit0 -x5483_bit0 -x5484_bit0 -x5485_bit0 -x5486_bit0 -x5487_bit0 -x5488_bit0 -x5489_bit0 -x5490_bit0 -x5491_bit0 -x5492_bit0 -x5493_bit0 -x5494_bit0 -x5495_bit0 -x5496_bit0 -x5497_bit0 -x5498_bit0 -x5499_bit0 -x5500_bit0 -x5501_bit0 -x5502_bit0 -x5503_bit0 -x5504_bit0 -x5505_bit0 -x5506_bit0 -x5507_bit0 -x5508_bit0 -x5509_bit0 -x5510_bit0 -x5511_bit0 -x5512_bit0 -x5513_bit0 -x5514_bit0 -x5515_bit0 -x5516_bit0 -x5517_bit0 -x5518_bit0 -x5519_bit0 -x5520_bit0 -x5521_bit0 -x5522_bit0 -x5523_bit0 -x5524_bit0 -x5525_bit0 -x5526_bit0 -x5527_bit0 -x5528_bit0 -x5529_bit0 -x5530_bit0 -x5531_bit0 -x5532_bit0 -x5533_bit0 -x5534_bit0 -x5535_bit0 -x5536_bit0 -x5537_bit0 -x5538_bit0 -x5539_bit0 -x5540_bit0 -x5541_bit0 -x5542_bit0 -x5543_bit0 -x5544_bit0 -x5545_bit0 -x5546_bit0 -x5547_bit0 -x5548_bit0 -x5549_bit0 -x5550_bit0 -x5551_bit0 -x5552_bit0 -x5553_bit0 -x5554_bit0 -x5555_bit0 -x5556_bit0 -x5557_bit0 -x5558_bit0 -x5559_bit0 -x5560_bit0 -x5561_bit0 -x5562_bit0 -x5563_bit0 -x5564_bit0 -x5565_bit0 -x5566_bit0 -x5567_bit0 -x5568_bit0 -x5569_bit0 -x5570_bit0 -x5571_bit0 -x5572_bit0 -x5573_bit0 -x5574_bit0 -x5575_bit0 -x5576_bit0 -x5577_bit0 -x5578_bit0 -x5579_bit0 -x5580_bit0 -x5581_bit0 -x5582_bit0 -x5583_bit0 -x5584_bit0 -x5585_bit0 -x5586_bit0 -x5587_bit0 -x5588_bit0 -x5589_bit0 -x5590_bit0 -x5591_bit0 -x5592_bit0 -x5593_bit0 -x5594_bit0 -x5595_bit0 -x5596_bit0 -x5597_bit0 -x5598_bit0 -x5599_bit0 -x5600_bit0 -x5601_bit0 -x5602_bit0 -x5603_bit0 -x5604_bit0 -x5605_bit0 -x5606_bit0 -x5607_bit0 -x5608_bit0 -x5609_bit0 -x5610_bit0 -x5611_bit0 -x5612_bit0 -x5613_bit0 -x5614_bit0 -x5615_bit0 -x5616_bit0 -x5617_bit0 -x5618_bit0 -x5619_bit0 -x5620_bit0 -x5621_bit0 -x5622_bit0 -x5623_bit0 -x5624_bit0 -x5625_bit0 -x5626_bit0 -x5627_bit0 -x5628_bit0 -x5629_bit0 -x5630_bit0 -x5631_bit0 -x5632_bit0 -x5633_bit0 -x5634_bit0 -x5635_bit0 -x5636_bit0 -x5637_bit0 -x5638_bit0 -x5639_bit0 -x5640_bit0 -x5641_bit0 -x5642_bit0 -x5643_bit0 -x5644_bit0 -x5645_bit0 -x5646_bit0 -x5647_bit0 -x5648_bit0 -x5649_bit0 -x5650_bit0 -x5651_bit0 -x5652_bit0 -x5653_bit0 -x5654_bit0 -x5655_bit0 -x5656_bit0 -x5657_bit0 -x5658_bit0 -x5659_bit0 -x5660_bit0 -x5661_bit0 -x5662_bit0 x5663_bit0 -x5664_bit0 -x5665_bit0 -x5666_bit0 -x5667_bit0 -x5668_bit0 -x5669_bit0 -x5670_bit0 -x5671_bit0 -x5672_bit0 -x5673_bit0 -x5674_bit0 -x5675_bit0 -x5676_bit0 -x5677_bit0 -x5678_bit0 -x5679_bit0 -x5680_bit0 -x5681_bit0 -x5682_bit0 -x5683_bit0 -x5684_bit0 -x5685_bit0 -x5686_bit0 -x5687_bit0 -x5688_bit0 -x5689_bit0 -x5690_bit0 -x5691_bit0 x5692_bit0 -x5693_bit0 -x5694_bit0 -x5695_bit0 -x5696_bit0 -x5697_bit0 -x5698_bit0 -x5699_bit0 -x5700_bit0 -x5701_bit0 -x5702_bit0 -x5703_bit0 -x5704_bit0 -x5705_bit0 -x5706_bit0 -x5707_bit0 -x5708_bit0 -x5709_bit0 -x5710_bit0 -x5711_bit0 -x5712_bit0 -x5713_bit0 -x5714_bit0 -x5715_bit0 -x5716_bit0 -x5717_bit0 -x5718_bit0 -x5719_bit0 -x5720_bit0 -x5721_bit0 -x5722_bit0 -x5723_bit0 -x5724_bit0 -x5725_bit0 -x5726_bit0 -x5727_bit0 -x5728_bit0 -x5729_bit0 -x5730_bit0 -x5731_bit0 -x5732_bit0 -x5733_bit0 -x5734_bit0 -x5735_bit0 -x5736_bit0 -x5737_bit0 -x5738_bit0 -x5739_bit0 -x5740_bit0 -x5741_bit0 -x5742_bit0 -x5743_bit0 -x5744_bit0 -x5745_bit0 -x5746_bit0 -x5747_bit0 -x5748_bit0 -x5749_bit0 -x5750_bit0 -x5751_bit0 -x5752_bit0 -x5753_bit0 -x5754_bit0 -x5755_bit0 -x5756_bit0 -x5757_bit0 -x5758_bit0 -x5759_bit0 -x5760_bit0 -x5761_bit0 -x5762_bit0 -x5763_bit0 -x5764_bit0 -x5765_bit0 -x5766_bit0 -x5767_bit0 -x5768_bit0 -x5769_bit0 -x5770_bit0 -x5771_bit0 -x5772_bit0 -x5773_bit0 -x5774_bit0 -x5775_bit0 -x5776_bit0 -x5777_bit0 -x5778_bit0 -x5779_bit0 -x5780_bit0 -x5781_bit0 -x5782_bit0 -x5783_bit0 -x5784_bit0 x5785_bit0 -x5786_bit0 -x5787_bit0 -x5788_bit0 -x5789_bit0 -x5790_bit0 -x5791_bit0 -x5792_bit0 -x5793_bit0 -x5794_bit0 -x5795_bit0 -x5796_bit0 -x5797_bit0 -x5798_bit0 -x5799_bit0 -x5800_bit0 -x5801_bit0 -x5802_bit0 -x5803_bit0 -x5804_bit0 -x5805_bit0 -x5806_bit0 -x5807_bit0 -x5808_bit0 -x5809_bit0 -x5810_bit0 -x5811_bit0 -x5812_bit0 -x5813_bit0 -x5814_bit0 -x5815_bit0 -x5816_bit0 -x5817_bit0 -x5818_bit0 -x5819_bit0 -x5820_bit0 -x5821_bit0 -x5822_bit0 -x5823_bit0 -x5824_bit0 -x5825_bit0 -x5826_bit0 -x5827_bit0 -x5828_bit0 -x5829_bit0 -x5830_bit0 -x5831_bit0 -x5832_bit0 -x5833_bit0 -x5834_bit0 -x5835_bit0 -x5836_bit0 -x5837_bit0 -x5838_bit0 -x5839_bit0 -x5840_bit0 -x5841_bit0 -x5842_bit0 -x5843_bit0 -x5844_bit0 -x5845_bit0 -x5846_bit0 -x5847_bit0 -x5848_bit0 -x5849_bit0 -x5850_bit0 -x5851_bit0 -x5852_bit0 -x5853_bit0 -x5854_bit0 -x5855_bit0 -x5856_bit0 -x5857_bit0 -x5858_bit0 -x5859_bit0 -x5860_bit0 -x5861_bit0 -x5862_bit0 -x5863_bit0 -x5864_bit0 -x5865_bit0 -x5866_bit0 -x5867_bit0 -x5868_bit0 -x5869_bit0 -x5870_bit0 -x5871_bit0 -x5872_bit0 -x5873_bit0 -x5874_bit0 -x5875_bit0 -x5876_bit0 -x5877_bit0 -x5878_bit0 -x5879_bit0 -x5880_bit0 -x5881_bit0 -x5882_bit0 -x5883_bit0 -x5884_bit0 -x5885_bit0 -x5886_bit0 -x5887_bit0 -x5888_bit0 -x5889_bit0 -x5890_bit0 -x5891_bit0 -x5892_bit0 -x5893_bit0 -x5894_bit0 -x5895_bit0 -x5896_bit0 -x5897_bit0 -x5898_bit0 -x5899_bit0 -x5900_bit0 -x5901_bit0 -x5902_bit0 -x5903_bit0 -x5904_bit0 -x5905_bit0 -x5906_bit0 -x5907_bit0 -x5908_bit0 -x5909_bit0 -x5910_bit0 -x5911_bit0 -x5912_bit0 -x5913_bit0 -x5914_bit0 -x5915_bit0 -x5916_bit0 -x5917_bit0 -x5918_bit0 -x5919_bit0 -x5920_bit0 -x5921_bit0 -x5922_bit0 -x5923_bit0 -x5924_bit0 -x5925_bit0 -x5926_bit0 -x5927_bit0 -x5928_bit0 -x5929_bit0 -x5930_bit0 -x5931_bit0 -x5932_bit0 -x5933_bit0 -x5934_bit0 -x5935_bit0 -x5936_bit0 -x5937_bit0 -x5938_bit0 -x5939_bit0 -x5940_bit0 -x5941_bit0 -x5942_bit0 -x5943_bit0 -x5944_bit0 -x5945_bit0 -x5946_bit0 -x5947_bit0 -x5948_bit0 -x5949_bit0 -x5950_bit0 -x5951_bit0 -x5952_bit0 -x5953_bit0 -x5954_bit0 -x5955_bit0 -x5956_bit0 -x5957_bit0 -x5958_bit0 -x5959_bit0 -x5960_bit0 -x5961_bit0 -x5962_bit0 -x5963_bit0 -x5964_bit0 -x5965_bit0 -x5966_bit0 -x5967_bit0 -x5968_bit0 -x5969_bit0 -x5970_bit0 -x5971_bit0 -x5972_bit0 -x5973_bit0 -x5974_bit0 -x5975_bit0 -x5976_bit0 -x5977_bit0 -x5978_bit0 -x5979_bit0 -x5980_bit0 -x5981_bit0 -x5982_bit0 -x5983_bit0 -x5984_bit0 -x5985_bit0 -x5986_bit0 -x5987_bit0 -x5988_bit0 -x5989_bit0 -x5990_bit0 -x5991_bit0 -x5992_bit0 -x5993_bit0 -x5994_bit0 -x5995_bit0 -x5996_bit0 -x5997_bit0 -x5998_bit0 -x5999_bit0 -x6000_bit0 -x6001_bit0 -x6002_bit0 -x6003_bit0 -x6004_bit0 -x6005_bit0 -x6006_bit0 -x6007_bit0 -x6008_bit0 -x6009_bit0 -x6010_bit0 -x6011_bit0 -x6012_bit0 -x6013_bit0 -x6014_bit0 -x6015_bit0 -x6016_bit0 -x6017_bit0 -x6018_bit0 -x6019_bit0 -x6020_bit0 -x6021_bit0 -x6022_bit0 -x6023_bit0 -x6024_bit0 -x6025_bit0 -x6026_bit0 -x6027_bit0 -x6028_bit0 -x6029_bit0 -x6030_bit0 -x6031_bit0 -x6032_bit0 -x6033_bit0 -x6034_bit0 -x6035_bit0 -x6036_bit0 -x6037_bit0 -x6038_bit0 -x6039_bit0 -x6040_bit0 -x6041_bit0 -x6042_bit0 -x6043_bit0 -x6044_bit0 -x6045_bit0 -x6046_bit0 -x6047_bit0 -x6048_bit0 -x6049_bit0 -x6050_bit0 -x6051_bit0 -x6052_bit0 -x6053_bit0 -x6054_bit0 -x6055_bit0 -x6056_bit0 -x6057_bit0 -x6058_bit0 -x6059_bit0 -x6060_bit0 -x6061_bit0 -x6062_bit0 -x6063_bit0 -x6064_bit0 -x6065_bit0 -x6066_bit0 -x6067_bit0 -x6068_bit0 -x6069_bit0 -x6070_bit0 -x6071_bit0 -x6072_bit0 -x6073_bit0 -x6074_bit0 -x6075_bit0 -x6076_bit0 -x6077_bit0 -x6078_bit0 x6079_bit0 -x6080_bit0 -x6081_bit0 -x6082_bit0 -x6083_bit0 -x6084_bit0 -x6085_bit0 -x6086_bit0 -x6087_bit0 -x6088_bit0 -x6089_bit0 -x6090_bit0 -x6091_bit0 -x6092_bit0 -x6093_bit0 -x6094_bit0 -x6095_bit0 -x6096_bit0 -x6097_bit0 -x6098_bit0 -x6099_bit0 -x6100_bit0 -x6101_bit0 -x6102_bit0 -x6103_bit0 -x6104_bit0 -x6105_bit0 -x6106_bit0 -x6107_bit0 -x6108_bit0 -x6109_bit0 -x6110_bit0 -x6111_bit0 -x6112_bit0 -x6113_bit0 -x6114_bit0 -x6115_bit0 -x6116_bit0 -x6117_bit0 -x6118_bit0 -x6119_bit0 -x6120_bit0 -x6121_bit0 -x6122_bit0 -x6123_bit0 -x6124_bit0 -x6125_bit0 -x6126_bit0 -x6127_bit0 -x6128_bit0 -x6129_bit0 -x6130_bit0 -x6131_bit0 -x6132_bit0 -x6133_bit0 -x6134_bit0 -x6135_bit0 -x6136_bit0 -x6137_bit0 -x6138_bit0 -x6139_bit0 -x6140_bit0 -x6141_bit0 -x6142_bit0 -x6143_bit0 -x6144_bit0 -x6145_bit0 -x6146_bit0 -x6147_bit0 -x6148_bit0 -x6149_bit0 -x6150_bit0 -x6151_bit0 -x6152_bit0 -x6153_bit0 -x6154_bit0 -x6155_bit0 -x6156_bit0 -x6157_bit0 -x6158_bit0 -x6159_bit0 -x6160_bit0 -x6161_bit0 -x6162_bit0 -x6163_bit0 -x6164_bit0 -x6165_bit0 -x6166_bit0 -x6167_bit0 -x6168_bit0 -x6169_bit0 -x6170_bit0 -x6171_bit0 -x6172_bit0 -x6173_bit0 -x6174_bit0 -x6175_bit0 -x6176_bit0 -x6177_bit0 -x6178_bit0 -x6179_bit0 -x6180_bit0 -x6181_bit0 -x6182_bit0 -x6183_bit0 -x6184_bit0 -x6185_bit0 -x6186_bit0 -x6187_bit0 -x6188_bit0 -x6189_bit0 -x6190_bit0 -x6191_bit0 -x6192_bit0 -x6193_bit0 -x6194_bit0 -x6195_bit0 -x6196_bit0 -x6197_bit0 -x6198_bit0 -x6199_bit0 -x6200_bit0 -x6201_bit0 -x6202_bit0 -x6203_bit0 -x6204_bit0 -x6205_bit0 -x6206_bit0 -x6207_bit0 -x6208_bit0 -x6209_bit0 -x6210_bit0 -x6211_bit0 -x6212_bit0 -x6213_bit0 -x6214_bit0 -x6215_bit0 -x6216_bit0 -x6217_bit0 -x6218_bit0 -x6219_bit0 -x6220_bit0 -x6221_bit0 -x6222_bit0 x6223_bit0 -x6224_bit0 -x6225_bit0 -x6226_bit0 -x6227_bit0 -x6228_bit0 -x6229_bit0 -x6230_bit0 -x6231_bit0 -x6232_bit0 -x6233_bit0 -x6234_bit0 -x6235_bit0 -x6236_bit0 -x6237_bit0 -x6238_bit0 -x6239_bit0 -x6240_bit0 -x6241_bit0 -x6242_bit0 -x6243_bit0 -x6244_bit0 -x6245_bit0 -x6246_bit0 -x6247_bit0 -x6248_bit0 -x6249_bit0 -x6250_bit0 -x6251_bit0 -x6252_bit0 -x6253_bit0 -x6254_bit0 -x6255_bit0 -x6256_bit0 -x6257_bit0 -x6258_bit0 -x6259_bit0 -x6260_bit0 -x6261_bit0 -x6262_bit0 -x6263_bit0 -x6264_bit0 -x6265_bit0 -x6266_bit0 -x6267_bit0 -x6268_bit0 -x6269_bit0 -x6270_bit0 -x6271_bit0 -x6272_bit0 -x6273_bit0 -x6274_bit0 -x6275_bit0 -x6276_bit0 -x6277_bit0 -x6278_bit0 -x6279_bit0 -x6280_bit0 -x6281_bit0 -x6282_bit0 -x6283_bit0 -x6284_bit0 -x6285_bit0 -x6286_bit0 -x6287_bit0 -x6288_bit0 -x6289_bit0 -x6290_bit0 -x6291_bit0 -x6292_bit0 -x6293_bit0 -x6294_bit0 -x6295_bit0 -x6296_bit0 -x6297_bit0 x6298_bit0 -x6299_bit0 -x6300_bit0 -x6301_bit0 -x6302_bit0 -x6303_bit0 -x6304_bit0 -x6305_bit0 -x6306_bit0 -x6307_bit0 -x6308_bit0 -x6309_bit0 -x6310_bit0 -x6311_bit0 -x6312_bit0 -x6313_bit0 -x6314_bit0 -x6315_bit0 -x6316_bit0 -x6317_bit0 -x6318_bit0 -x6319_bit0 -x6320_bit0 -x6321_bit0 -x6322_bit0 -x6323_bit0 -x6324_bit0 -x6325_bit0 -x6326_bit0 -x6327_bit0 -x6328_bit0 -x6329_bit0 -x6330_bit0 -x6331_bit0 -x6332_bit0 -x6333_bit0 -x6334_bit0 -x6335_bit0 -x6336_bit0 -x6337_bit0 -x6338_bit0 -x6339_bit0 -x6340_bit0 -x6341_bit0 -x6342_bit0 -x6343_bit0 -x6344_bit0 -x6345_bit0 -x6346_bit0 -x6347_bit0 -x6348_bit0 -x6349_bit0 -x6350_bit0 -x6351_bit0 -x6352_bit0 -x6353_bit0 -x6354_bit0 -x6355_bit0 -x6356_bit0 -x6357_bit0 -x6358_bit0 -x6359_bit0 -x6360_bit0 -x6361_bit0 -x6362_bit0 -x6363_bit0 -x6364_bit0 -x6365_bit0 -x6366_bit0 -x6367_bit0 -x6368_bit0 -x6369_bit0 -x6370_bit0 -x6371_bit0 -x6372_bit0 -x6373_bit0 -x6374_bit0 -x6375_bit0 -x6376_bit0 -x6377_bit0 -x6378_bit0 -x6379_bit0 -x6380_bit0 -x6381_bit0 -x6382_bit0 -x6383_bit0 -x6384_bit0 -x6385_bit0 -x6386_bit0 -x6387_bit0 -x6388_bit0 -x6389_bit0 -x6390_bit0 -x6391_bit0 -x6392_bit0 -x6393_bit0 -x6394_bit0 -x6395_bit0 -x6396_bit0 -x6397_bit0 -x6398_bit0 -x6399_bit0 -x6400_bit0 -x6401_bit0 -x6402_bit0 -x6403_bit0 -x6404_bit0 -x6405_bit0 -x6406_bit0 -x6407_bit0 -x6408_bit0 -x6409_bit0 -x6410_bit0 -x6411_bit0 -x6412_bit0 -x6413_bit0 -x6414_bit0 -x6415_bit0 -x6416_bit0 -x6417_bit0 -x6418_bit0 -x6419_bit0 -x6420_bit0 -x6421_bit0 -x6422_bit0 -x6423_bit0 -x6424_bit0 -x6425_bit0 -x6426_bit0 -x6427_bit0 -x6428_bit0 -x6429_bit0 -x6430_bit0 -x6431_bit0 -x6432_bit0 -x6433_bit0 -x6434_bit0 -x6435_bit0 -x6436_bit0 -x6437_bit0 -x6438_bit0 -x6439_bit0 -x6440_bit0 -x6441_bit0 -x6442_bit0 -x6443_bit0 -x6444_bit0 -x6445_bit0 -x6446_bit0 -x6447_bit0 -x6448_bit0 -x6449_bit0 -x6450_bit0 -x6451_bit0 -x6452_bit0 -x6453_bit0 -x6454_bit0 -x6455_bit0 -x6456_bit0 -x6457_bit0 -x6458_bit0 -x6459_bit0 -x6460_bit0 -x6461_bit0 -x6462_bit0 -x6463_bit0 -x6464_bit0 -x6465_bit0 -x6466_bit0 -x6467_bit0 -x6468_bit0 -x6469_bit0 -x6470_bit0 -x6471_bit0 -x6472_bit0 -x6473_bit0 -x6474_bit0 -x6475_bit0 -x6476_bit0 -x6477_bit0 -x6478_bit0 -x6479_bit0 -x6480_bit0 -x6481_bit0 -x6482_bit0 -x6483_bit0 -x6484_bit0 -x6485_bit0 -x6486_bit0 -x6487_bit0 -x6488_bit0 -x6489_bit0 -x6490_bit0 -x6491_bit0 x6492_bit0 -x6493_bit0 -x6494_bit0 -x6495_bit0 -x6496_bit0 -x6497_bit0 -x6498_bit0 -x6499_bit0 -x6500_bit0 -x6501_bit0 -x6502_bit0 -x6503_bit0 -x6504_bit0 x6505_bit0 -x6506_bit0 -x6507_bit0 -x6508_bit0 -x6509_bit0 -x6510_bit0 -x6511_bit0 -x6512_bit0 -x6513_bit0 -x6514_bit0 -x6515_bit0 -x6516_bit0 -x6517_bit0 -x6518_bit0 -x6519_bit0 -x6520_bit0 -x6521_bit0 -x6522_bit0 -x6523_bit0 -x6524_bit0 -x6525_bit0 -x6526_bit0 -x6527_bit0 -x6528_bit0 -x6529_bit0 -x6530_bit0 -x6531_bit0 -x6532_bit0 -x6533_bit0 -x6534_bit0 -x6535_bit0 -x6536_bit0 -x6537_bit0 -x6538_bit0 -x6539_bit0 -x6540_bit0 -x6541_bit0 -x6542_bit0 -x6543_bit0 -x6544_bit0 -x6545_bit0 -x6546_bit0 -x6547_bit0 -x6548_bit0 -x6549_bit0 -x6550_bit0 -x6551_bit0 -x6552_bit0 -x6553_bit0 -x6554_bit0 -x6555_bit0 -x6556_bit0 -x6557_bit0 -x6558_bit0 -x6559_bit0 -x6560_bit0 -x6561_bit0 -x6562_bit0 -x6563_bit0 -x6564_bit0 -x6565_bit0 -x6566_bit0 -x6567_bit0 -x6568_bit0 -x6569_bit0 -x6570_bit0 -x6571_bit0 -x6572_bit0 -x6573_bit0 -x6574_bit0 -x6575_bit0 -x6576_bit0 -x6577_bit0 -x6578_bit0 -x6579_bit0 -x6580_bit0 -x6581_bit0 -x6582_bit0 -x6583_bit0 -x6584_bit0 -x6585_bit0 -x6586_bit0 -x6587_bit0 -x6588_bit0 -x6589_bit0 -x6590_bit0 -x6591_bit0 -x6592_bit0 -x6593_bit0 -x6594_bit0 x6595_bit0 -x6596_bit0 -x6597_bit0 -x6598_bit0 x6599_bit0 -x6600_bit0 -x6601_bit0 -x6602_bit0 -x6603_bit0 -x6604_bit0 -x6605_bit0 -x6606_bit0 -x6607_bit0 -x6608_bit0 -x6609_bit0 -x6610_bit0 -x6611_bit0 -x6612_bit0 -x6613_bit0 -x6614_bit0 -x6615_bit0 -x6616_bit0 -x6617_bit0 -x6618_bit0 -x6619_bit0 -x6620_bit0 -x6621_bit0 -x6622_bit0 -x6623_bit0 -x6624_bit0 -x6625_bit0 -x6626_bit0 -x6627_bit0 -x6628_bit0 -x6629_bit0 -x6630_bit0 -x6631_bit0 -x6632_bit0 -x6633_bit0 x6634_bit0 -x6635_bit0 -x6636_bit0 -x6637_bit0 -x6638_bit0 -x6639_bit0 -x6640_bit0 -x6641_bit0 -x6642_bit0 -x6643_bit0 -x6644_bit0 -x6645_bit0 -x6646_bit0 -x6647_bit0 -x6648_bit0 -x6649_bit0 -x6650_bit0 -x6651_bit0 -x6652_bit0 -x6653_bit0 -x6654_bit0 -x6655_bit0 -x6656_bit0 -x6657_bit0 -x6658_bit0 -x6659_bit0 -x6660_bit0 -x6661_bit0 -x6662_bit0 -x6663_bit0 -x6664_bit0 -x6665_bit0 -x6666_bit0 -x6667_bit0 -x6668_bit0 -x6669_bit0 -x6670_bit0 -x6671_bit0 -x6672_bit0 -x6673_bit0 -x6674_bit0 -x6675_bit0 -x6676_bit0 -x6677_bit0 -x6678_bit0 -x6679_bit0 -x6680_bit0 -x6681_bit0 -x6682_bit0 -x6683_bit0 -x6684_bit0 -x6685_bit0 -x6686_bit0 -x6687_bit0 -x6688_bit0 -x6689_bit0 -x6690_bit0 -x6691_bit0 -x6692_bit0 -x6693_bit0 -x6694_bit0 -x6695_bit0 -x6696_bit0 -x6697_bit0 -x6698_bit0 -x6699_bit0 -x6700_bit0 -x6701_bit0 -x6702_bit0 -x6703_bit0 -x6704_bit0 -x6705_bit0 -x6706_bit0 -x6707_bit0 -x6708_bit0 -x6709_bit0 -x6710_bit0 -x6711_bit0 -x6712_bit0 -x6713_bit0 -x6714_bit0 -x6715_bit0 -x6716_bit0 -x6717_bit0 -x6718_bit0 -x6719_bit0 -x6720_bit0 -x6721_bit0 -x6722_bit0 -x6723_bit0 -x6724_bit0 -x6725_bit0 -x6726_bit0 -x6727_bit0 -x6728_bit0 -x6729_bit0 -x6730_bit0 -x6731_bit0 -x6732_bit0 -x6733_bit0 -x6734_bit0 -x6735_bit0 -x6736_bit0 -x6737_bit0 -x6738_bit0 -x6739_bit0 -x6740_bit0 -x6741_bit0 -x6742_bit0 -x6743_bit0 -x6744_bit0 -x6745_bit0 -x6746_bit0 -x6747_bit0 -x6748_bit0 -x6749_bit0 -x6750_bit0 -x6751_bit0 -x6752_bit0 -x6753_bit0 -x6754_bit0 -x6755_bit0 -x6756_bit0 -x6757_bit0 -x6758_bit0 -x6759_bit0 -x6760_bit0 -x6761_bit0 -x6762_bit0 -x6763_bit0 -x6764_bit0 -x6765_bit0 -x6766_bit0 -x6767_bit0 -x6768_bit0 -x6769_bit0 -x6770_bit0 -x6771_bit0 -x6772_bit0 -x6773_bit0 -x6774_bit0 -x6775_bit0 -x6776_bit0 -x6777_bit0 -x6778_bit0 -x6779_bit0 -x6780_bit0 -x6781_bit0 x6782_bit0 -x6783_bit0 -x6784_bit0 -x6785_bit0 -x6786_bit0 -x6787_bit0 -x6788_bit0 -x6789_bit0 -x6790_bit0 -x6791_bit0 -x6792_bit0 -x6793_bit0 -x6794_bit0 -x6795_bit0 -x6796_bit0 -x6797_bit0 -x6798_bit0 -x6799_bit0 x6800_bit0 -x6801_bit0 -x6802_bit0 -x6803_bit0 -x6804_bit0 -x6805_bit0 -x6806_bit0 -x6807_bit0 -x6808_bit0 -x6809_bit0 -x6810_bit0 -x6811_bit0 -x6812_bit0 -x6813_bit0 -x6814_bit0 -x6815_bit0 -x6816_bit0 -x6817_bit0 -x6818_bit0 -x6819_bit0 -x6820_bit0 -x6821_bit0 -x6822_bit0 -x6823_bit0 -x6824_bit0 -x6825_bit0 -x6826_bit0 -x6827_bit0 -x6828_bit0 -x6829_bit0 -x6830_bit0 -x6831_bit0 -x6832_bit0 -x6833_bit0 -x6834_bit0 -x6835_bit0 -x6836_bit0 -x6837_bit0 -x6838_bit0 -x6839_bit0 -x6840_bit0 -x6841_bit0 -x6842_bit0 -x6843_bit0 -x6844_bit0 -x6845_bit0 -x6846_bit0 -x6847_bit0 -x6848_bit0 -x6849_bit0 -x6850_bit0 -x6851_bit0 -x6852_bit0 -x6853_bit0 -x6854_bit0 -x6855_bit0 -x6856_bit0 -x6857_bit0 -x6858_bit0 -x6859_bit0 -x6860_bit0 -x6861_bit0 -x6862_bit0 -x6863_bit0 -x6864_bit0 -x6865_bit0 -x6866_bit0 -x6867_bit0 -x6868_bit0 -x6869_bit0 -x6870_bit0 -x6871_bit0 -x6872_bit0 -x6873_bit0 -x6874_bit0 -x6875_bit0 -x6876_bit0 -x6877_bit0 -x6878_bit0 -x6879_bit0 -x6880_bit0 -x6881_bit0 -x6882_bit0 -x6883_bit0 -x6884_bit0 -x6885_bit0 -x6886_bit0 -x6887_bit0 -x6888_bit0 -x6889_bit0 -x6890_bit0 -x6891_bit0 -x6892_bit0 -x6893_bit0 -x6894_bit0 -x6895_bit0 -x6896_bit0 -x6897_bit0 -x6898_bit0 -x6899_bit0 -x6900_bit0 -x6901_bit0 -x6902_bit0 -x6903_bit0 -x6904_bit0 -x6905_bit0 -x6906_bit0 -x6907_bit0 -x6908_bit0 -x6909_bit0 -x6910_bit0 -x6911_bit0 -x6912_bit0 -x6913_bit0 -x6914_bit0 -x6915_bit0 -x6916_bit0 -x6917_bit0 -x6918_bit0 -x6919_bit0 -x6920_bit0 -x6921_bit0 -x6922#### 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.91 0.96 0.91 2/54 15525
Raw data (stat): 15525 (runsolver) R 15524 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491478144 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0013 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 10271 0 0 0 974 24 0 0 25 0 1 0 491478144 44793856 9874 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10936 9874 603 41 0 10895 0
vsize: 43744
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 10460 0 0 0 1973 25 0 0 25 0 1 0 491478144 45600768 10063 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11133 10063 603 41 0 11092 0
vsize: 44532
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 10688 0 0 0 2972 26 0 0 25 0 1 0 491478144 46538752 10291 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11362 10291 603 41 0 11321 0
vsize: 45448
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 26759 0 0 0 3937 61 0 0 25 0 1 0 491478144 103673856 21385 4294967295 134512640 134672761 3221224544 3221221752 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25311 21387 603 41 0 25270 0
vsize: 101244
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 47406 0 0 0 4886 113 0 0 25 0 1 0 491478144 192806912 39379 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47072 39379 603 41 0 47031 0
vsize: 188288
[startup+60.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 47596 0 0 0 5885 113 0 0 25 0 1 0 491478144 193482752 39569 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47237 39569 603 41 0 47196 0
vsize: 188948
[startup+70.0047 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 47717 0 0 0 6885 114 0 0 25 0 1 0 491478144 193888256 39690 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47336 39690 603 41 0 47295 0
vsize: 189344
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 47836 0 0 0 7884 115 0 0 25 0 1 0 491478144 194424832 39809 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47467 39809 603 41 0 47426 0
vsize: 189868
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 47998 0 0 0 8884 116 0 0 25 0 1 0 491478144 195100672 39971 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47632 39971 603 41 0 47591 0
vsize: 190528
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48213 0 0 0 9883 116 0 0 25 0 1 0 491478144 196046848 40186 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47863 40186 603 41 0 47822 0
vsize: 191452
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48411 0 0 0 10883 117 0 0 25 0 1 0 491478144 196734976 40384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48031 40384 603 41 0 47990 0
vsize: 192124
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48567 0 0 0 11883 117 0 0 25 0 1 0 491478144 197406720 40540 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48195 40540 603 41 0 48154 0
vsize: 192780
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48715 0 0 0 12882 118 0 0 25 0 1 0 491478144 197947392 40688 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48327 40688 603 41 0 48286 0
vsize: 193308
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48866 0 0 0 13882 118 0 0 25 0 1 0 491478144 198623232 40839 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48492 40839 603 41 0 48451 0
vsize: 193968
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 48961 0 0 0 14882 119 0 0 25 0 1 0 491478144 199024640 40934 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48590 40934 603 41 0 48549 0
vsize: 194360
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 49093 0 0 0 15881 120 0 0 25 0 1 0 491478144 199565312 41066 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48722 41066 603 41 0 48681 0
vsize: 194888
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 49357 0 0 0 16881 121 0 0 25 0 1 0 491478144 200634368 41330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48983 41330 603 41 0 48942 0
vsize: 195932
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 49627 0 0 0 17880 121 0 0 25 0 1 0 491478144 201707520 41600 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49245 41600 603 41 0 49204 0
vsize: 196980
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 49935 0 0 0 18879 122 0 0 25 0 1 0 491478144 202932224 41908 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49544 41908 603 41 0 49503 0
vsize: 198176
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 50008 0 0 0 19879 122 0 0 25 0 1 0 491478144 203202560 41981 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49610 41981 603 41 0 49569 0
vsize: 198440
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 50217 0 0 0 20878 123 0 0 25 0 1 0 491478144 204156928 42190 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49843 42190 603 41 0 49802 0
vsize: 199372
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 50557 0 0 0 21878 124 0 0 25 0 1 0 491478144 205533184 42530 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50179 42530 603 41 0 50138 0
vsize: 200716
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 50870 0 0 0 22877 124 0 0 25 0 1 0 491478144 206807040 42843 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50490 42843 603 41 0 50449 0
vsize: 201960
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 55400 0 0 0 23865 135 0 0 25 0 1 0 491478144 208490496 43157 4294967295 134512640 134672761 3221224544 3221222624 134523140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50901 43157 603 41 0 50860 0
vsize: 203604
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 59913 0 0 0 24856 144 0 0 25 0 1 0 491478144 226500608 47655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55298 47655 603 41 0 55257 0
vsize: 221192
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60025 0 0 0 25856 144 0 0 25 0 1 0 491478144 226902016 47767 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55396 47767 603 41 0 55355 0
vsize: 221584
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60153 0 0 0 26856 145 0 0 25 0 1 0 491478144 227442688 47895 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55528 47895 603 41 0 55487 0
vsize: 222112
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60333 0 0 0 27855 145 0 0 25 0 1 0 491478144 228126720 48075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55695 48075 603 41 0 55654 0
vsize: 222780
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60398 0 0 0 28855 146 0 0 25 0 1 0 491478144 228401152 48140 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55762 48140 603 41 0 55721 0
vsize: 223048
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60523 0 0 0 29855 146 0 0 25 0 1 0 491478144 228941824 48265 4294967295 134512640 134672761 3221224544 3221223728 134558423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55894 48265 603 41 0 55853 0
vsize: 223576
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60626 0 0 0 30855 146 0 0 25 0 1 0 491478144 229208064 48368 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55959 48368 603 41 0 55918 0
vsize: 223836
[startup+320.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60763 0 0 0 31855 146 0 0 25 0 1 0 491478144 229752832 48505 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56092 48505 603 41 0 56051 0
vsize: 224368
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60868 0 0 0 32855 146 0 0 25 0 1 0 491478144 230158336 48610 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56191 48610 603 41 0 56150 0
vsize: 224764
[startup+340.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 60943 0 0 0 33855 147 0 0 25 0 1 0 491478144 230572032 48685 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56292 48685 603 41 0 56251 0
vsize: 225168
[startup+350.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 61132 0 0 0 34855 148 0 0 25 0 1 0 491478144 231251968 48874 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56458 48874 603 41 0 56417 0
vsize: 225832
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 61332 0 0 0 35854 148 0 0 25 0 1 0 491478144 232206336 49074 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56691 49074 603 41 0 56650 0
vsize: 226764
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 63016 0 0 0 36850 152 0 0 25 0 1 0 491478144 233431040 49381 4294967295 134512640 134672761 3221224544 3221222920 1075347113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56990 49381 603 41 0 56949 0
vsize: 227960
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 66822 0 0 0 37843 160 0 0 25 0 1 0 491478144 245035008 53172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59823 53172 603 41 0 59782 0
vsize: 239292
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 67047 0 0 0 38841 161 0 0 25 0 1 0 491478144 245846016 53397 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60021 53397 603 41 0 59980 0
vsize: 240084
[startup+400.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 67155 0 0 0 39841 161 0 0 25 0 1 0 491478144 246247424 53505 4294967295 134512640 134672761 3221224544 3221223700 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60119 53505 603 41 0 60078 0
vsize: 240476
[startup+410.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 67250 0 0 0 40841 161 0 0 25 0 1 0 491478144 246661120 53600 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60220 53600 603 41 0 60179 0
vsize: 240880
[startup+420.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 67348 0 0 0 41841 161 0 0 25 0 1 0 491478144 247070720 53698 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60320 53698 603 41 0 60279 0
vsize: 241280
[startup+430.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 67636 0 0 0 42840 163 0 0 25 0 1 0 491478144 248328192 53986 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60627 53986 603 41 0 60586 0
vsize: 242508
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68041 0 0 0 43840 163 0 0 25 0 1 0 491478144 250036224 54391 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61044 54391 603 41 0 61003 0
vsize: 244176
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68401 0 0 0 44840 164 0 0 25 0 1 0 491478144 251490304 54751 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61399 54751 603 41 0 61358 0
vsize: 245596
[startup+460.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68465 0 0 0 45840 164 0 0 25 0 1 0 491478144 251629568 54815 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61433 54815 603 41 0 61392 0
vsize: 245732
[startup+470.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68640 0 0 0 46839 165 0 0 25 0 1 0 491478144 252452864 54990 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61634 54990 603 41 0 61593 0
vsize: 246536
[startup+480.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68825 0 0 0 47839 165 0 0 25 0 1 0 491478144 253145088 55175 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61803 55175 603 41 0 61762 0
vsize: 247212
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 68973 0 0 0 48838 166 0 0 25 0 1 0 491478144 253693952 55323 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61937 55323 603 41 0 61896 0
vsize: 247748
[startup+500.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69146 0 0 0 49838 166 0 0 25 0 1 0 491478144 254398464 55496 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62109 55496 603 41 0 62068 0
vsize: 248436
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69214 0 0 0 50838 167 0 0 25 0 1 0 491478144 254668800 55564 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62175 55564 603 41 0 62134 0
vsize: 248700
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69375 0 0 0 51837 167 0 0 25 0 1 0 491478144 255320064 55725 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62334 55725 603 41 0 62293 0
vsize: 249336
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69444 0 0 0 52837 167 0 0 25 0 1 0 491478144 255725568 55794 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62433 55794 603 41 0 62392 0
vsize: 249732
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69541 0 0 0 53838 168 0 0 25 0 1 0 491478144 256126976 55891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62531 55891 603 41 0 62490 0
vsize: 250124
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69630 0 0 0 54838 168 0 0 25 0 1 0 491478144 256397312 55980 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62597 55980 603 41 0 62556 0
vsize: 250388
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69768 0 0 0 55837 169 0 0 25 0 1 0 491478144 256933888 56118 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62728 56118 603 41 0 62687 0
vsize: 250912
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 69914 0 0 0 56837 169 0 0 25 0 1 0 491478144 257601536 56264 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62891 56264 603 41 0 62850 0
vsize: 251564
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 70108 0 0 0 57836 170 0 0 25 0 1 0 491478144 258424832 56458 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63092 56458 603 41 0 63051 0
vsize: 252368
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 72920 0 0 0 58830 176 0 0 25 0 1 0 491478144 267956224 58589 4294967295 134512640 134672761 3221224544 3221187968 134592600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65419 58589 603 41 0 65378 0
vsize: 261676
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 77937 0 0 0 59815 191 0 0 25 0 1 0 491478144 287035392 60125 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70077 60125 603 41 0 70036 0
vsize: 280308
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 77938 0 0 0 60815 191 0 0 25 0 1 0 491478144 287035392 60126 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70077 60126 603 41 0 70036 0
vsize: 280308
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 77939 0 0 0 61816 191 0 0 25 0 1 0 491478144 287035392 60127 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70077 60127 603 41 0 70036 0
vsize: 280308
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 77941 0 0 0 62816 191 0 0 25 0 1 0 491478144 287035392 60129 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70077 60129 603 41 0 70036 0
vsize: 280308
[startup+640.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 77968 0 0 0 63816 191 0 0 25 0 1 0 491478144 287170560 60156 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70110 60156 603 41 0 70069 0
vsize: 280440
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 78100 0 0 0 64816 192 0 0 25 0 1 0 491478144 287711232 60288 4294967295 134512640 134672761 3221224544 3221223648 134560028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70242 60288 603 41 0 70201 0
vsize: 280968
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 78282 0 0 0 65815 193 0 0 25 0 1 0 491478144 288522240 60470 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70440 60470 603 41 0 70399 0
vsize: 281760
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83067 0 0 0 66804 204 0 0 25 0 1 0 491478144 299773952 63854 4294967295 134512640 134672761 3221224544 3221223844 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73187 63854 603 41 0 73146 0
vsize: 292748
[startup+680.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83397 0 0 0 67803 205 0 0 25 0 1 0 491478144 301125632 64184 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73517 64184 603 41 0 73476 0
vsize: 294068
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83522 0 0 0 68803 206 0 0 25 0 1 0 491478144 301674496 64309 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73651 64309 603 41 0 73610 0
vsize: 294604
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83624 0 0 0 69803 206 0 0 25 0 1 0 491478144 302080000 64411 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73750 64411 603 41 0 73709 0
vsize: 295000
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83703 0 0 0 70803 206 0 0 25 0 1 0 491478144 302485504 64490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73849 64490 603 41 0 73808 0
vsize: 295396
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83811 0 0 0 71802 207 0 0 25 0 1 0 491478144 302764032 64598 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73917 64598 603 41 0 73876 0
vsize: 295668
[startup+730.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83897 0 0 0 72802 207 0 0 25 0 1 0 491478144 303063040 64684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73990 64684 603 41 0 73949 0
vsize: 295960
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 83979 0 0 0 73802 207 0 0 25 0 1 0 491478144 303472640 64766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74090 64766 603 41 0 74049 0
vsize: 296360
[startup+750.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 84072 0 0 0 74802 207 0 0 25 0 1 0 491478144 303742976 64859 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74156 64859 603 41 0 74115 0
vsize: 296624
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 84133 0 0 0 75802 208 0 0 25 0 1 0 491478144 304005120 64920 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74220 64920 603 41 0 74179 0
vsize: 296880
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 84213 0 0 0 76802 208 0 0 25 0 1 0 491478144 304414720 65000 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74320 65000 603 41 0 74279 0
vsize: 297280
[startup+780.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 84441 0 0 0 77801 209 0 0 25 0 1 0 491478144 305336320 65228 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 65228 603 41 0 74504 0
vsize: 298180
[startup+790.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 84767 0 0 0 78801 210 0 0 25 0 1 0 491478144 306692096 65554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74876 65554 603 41 0 74835 0
vsize: 299504
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 85089 0 0 0 79800 210 0 0 25 0 1 0 491478144 308101120 65876 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75220 65876 603 41 0 75179 0
vsize: 300880
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 85379 0 0 0 80800 211 0 0 25 0 1 0 491478144 309207040 66166 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75490 66166 603 41 0 75449 0
vsize: 301960
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 85684 0 0 0 81800 211 0 0 25 0 1 0 491478144 310476800 66471 4294967295 134512640 134672761 3221224544 3221223728 134559604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75800 66471 603 41 0 75759 0
vsize: 303200
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 86010 0 0 0 82800 212 0 0 25 0 1 0 491478144 311758848 66797 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76113 66797 603 41 0 76072 0
vsize: 304452
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 86138 0 0 0 83799 212 0 0 25 0 1 0 491478144 312225792 66925 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76227 66925 603 41 0 76186 0
vsize: 304908
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 86311 0 0 0 84799 212 0 0 25 0 1 0 491478144 313028608 67098 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76423 67098 603 41 0 76382 0
vsize: 305692
[startup+860.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 86449 0 0 0 85799 213 0 0 25 0 1 0 491478144 313597952 67236 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76562 67236 603 41 0 76521 0
vsize: 306248
[startup+870.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 86753 0 0 0 86798 214 0 0 25 0 1 0 491478144 314814464 67540 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76859 67540 603 41 0 76818 0
vsize: 307436
[startup+880.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 87042 0 0 0 87797 215 0 0 25 0 1 0 491478144 315998208 67829 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77148 67829 603 41 0 77107 0
vsize: 308592
[startup+890.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 87323 0 0 0 88797 215 0 0 25 0 1 0 491478144 317149184 68110 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77429 68110 603 41 0 77388 0
vsize: 309716
[startup+900.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 87622 0 0 0 89797 216 0 0 25 0 1 0 491478144 318345216 68409 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77721 68409 603 41 0 77680 0
vsize: 310884
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 87936 0 0 0 90796 216 0 0 25 0 1 0 491478144 319631360 68723 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78035 68723 603 41 0 77994 0
vsize: 312140
[startup+920.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 88225 0 0 0 91796 217 0 0 25 0 1 0 491478144 320778240 69012 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78315 69012 603 41 0 78274 0
vsize: 313260
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 88555 0 0 0 92795 218 0 0 25 0 1 0 491478144 322117632 69342 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78642 69342 603 41 0 78601 0
vsize: 314568
[startup+940.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 88853 0 0 0 93795 218 0 0 25 0 1 0 491478144 323440640 69640 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78965 69640 603 41 0 78924 0
vsize: 315860
[startup+950.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89154 0 0 0 94794 219 0 0 25 0 1 0 491478144 324689920 69941 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79270 69941 603 41 0 79229 0
vsize: 317080
[startup+960.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89343 0 0 0 95793 220 0 0 25 0 1 0 491478144 325390336 70130 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79441 70130 603 41 0 79400 0
vsize: 317764
[startup+970.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89448 0 0 0 96793 220 0 0 25 0 1 0 491478144 325795840 70235 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79540 70235 603 41 0 79499 0
vsize: 318160
[startup+980.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89516 0 0 0 97793 220 0 0 25 0 1 0 491478144 326066176 70303 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79606 70303 603 41 0 79565 0
vsize: 318424
[startup+990.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89649 0 0 0 98793 221 0 0 25 0 1 0 491478144 326598656 70436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79736 70436 603 41 0 79695 0
vsize: 318944
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89794 0 0 0 99793 221 0 0 25 0 1 0 491478144 327258112 70581 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79897 70581 603 41 0 79856 0
vsize: 319588
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 89962 0 0 0 100793 222 0 0 25 0 1 0 491478144 327970816 70749 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80071 70749 603 41 0 80030 0
vsize: 320284
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 90289 0 0 0 101792 223 0 0 25 0 1 0 491478144 329203712 71076 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80372 71076 603 41 0 80331 0
vsize: 321488
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 90703 0 0 0 102791 224 0 0 25 0 1 0 491478144 331042816 71490 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80821 71490 603 41 0 80780 0
vsize: 323284
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 90857 0 0 0 103791 224 0 0 25 0 1 0 491478144 331608064 71644 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80959 71644 603 41 0 80918 0
vsize: 323836
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 90943 0 0 0 104791 224 0 0 25 0 1 0 491478144 331882496 71730 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81026 71730 603 41 0 80985 0
vsize: 324104
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91072 0 0 0 105791 224 0 0 25 0 1 0 491478144 332423168 71859 4294967295 134512640 134672761 3221224544 3221223792 134562574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81158 71859 603 41 0 81117 0
vsize: 324632
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91171 0 0 0 106791 225 0 0 25 0 1 0 491478144 332840960 71958 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81260 71958 603 41 0 81219 0
vsize: 325040
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91225 0 0 0 107791 225 0 0 25 0 1 0 491478144 333111296 72012 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81326 72012 603 41 0 81285 0
vsize: 325304
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91409 0 0 0 108791 225 0 0 25 0 1 0 491478144 333795328 72196 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81493 72196 603 41 0 81452 0
vsize: 325972
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91623 0 0 0 109791 226 0 0 25 0 1 0 491478144 334950400 72410 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81775 72410 603 41 0 81734 0
vsize: 327100
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91869 0 0 0 110790 226 0 0 25 0 1 0 491478144 335818752 72656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81987 72656 603 41 0 81946 0
vsize: 327948
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 91953 0 0 0 111791 226 0 0 25 0 1 0 491478144 336224256 72740 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82086 72740 603 41 0 82045 0
vsize: 328344
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92187 0 0 0 112790 227 0 0 25 0 1 0 491478144 337186816 72974 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82321 72974 603 41 0 82280 0
vsize: 329284
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92424 0 0 0 113790 227 0 0 25 0 1 0 491478144 338202624 73211 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82569 73211 603 41 0 82528 0
vsize: 330276
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92676 0 0 0 114790 228 0 0 25 0 1 0 491478144 339132416 73463 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82796 73463 603 41 0 82755 0
vsize: 331184
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92795 0 0 0 115790 228 0 0 25 0 1 0 491478144 339632128 73582 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82918 73582 603 41 0 82877 0
vsize: 331672
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92874 0 0 0 116790 228 0 0 25 0 1 0 491478144 340033536 73661 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83016 73661 603 41 0 82975 0
vsize: 332064
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 92980 0 0 0 117790 228 0 0 25 0 1 0 491478144 340439040 73767 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83115 73767 603 41 0 83074 0
vsize: 332460
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 94552 0 0 0 118786 232 0 0 25 0 1 0 491478144 341663744 74038 4294967295 134512640 134672761 3221224544 3221222096 134523140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83414 74038 603 41 0 83373 0
vsize: 333656
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15525
Raw data (stat): 15525 (minisat+) R 15524 32461 32460 0 -1 0 97401 0 0 0 119779 238 0 0 25 0 1 0 491478144 349888512 76873 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 85422 76873 603 41 0 85381 0
vsize: 341688
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 15525
Raw data (stat): 15525 (minisat+) Z 15524 32461 32460 0 -1 12 97404 0 0 0 119781 253 0 0 25 0 1 0 491478144 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.22
CPU time (s): 1200.35
CPU user time (s): 1197.81
CPU system time (s): 2.53761
CPU usage (%): 100.011
Max. virtual memory (Kb): 341688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####