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-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran12x21.opb
MD5SUM	0d744fe957d41a18692933adc6be4af7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1493203
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1511880035
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1511880035
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	5292
Total number of constraints	285
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	285
Minimum length of a constraint	21
Maximum length of a constraint	420
Trace number 14800

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 01:25:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19279 boxname=wulflinc2 idbench=1483 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0d744fe957d41a18692933adc6be4af7  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran12x21.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran12x21.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-ran12x21.opb
IDLAUNCH: 19279
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        629892 kB
Buffers:         33172 kB
Cached:         348036 kB
SwapCached:          0 kB
Active:          32932 kB
Inactive:       351068 kB
HighTotal:      131008 kB
HighFree:         7420 kB
LowTotal:       903652 kB
LowFree:        622472 kB
SwapTotal:     2097136 kB
SwapFree:      2096988 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            15184 kB
Committed_AS:    71748 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:45:52 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19279 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 428   maxlim: 44523   bits: 16/16
c ---[ 314]---> Adder-cost: 428   maxlim: 45163   bits: 16/16
c ---[ 312]---> Adder-cost: 434   maxlim: 55787   bits: 16/16
c ---[ 310]---> Adder-cost: 428   maxlim: 44395   bits: 16/16
c ---[ 308]---> Adder-cost: 428   maxlim: 43627   bits: 16/16
c ---[ 306]---> Adder-cost: 428   maxlim: 43755   bits: 16/16
c ---[ 304]---> Adder-cost: 428   maxlim: 44267   bits: 16/16
c ---[ 302]---> Adder-cost: 412   maxlim: 29419   bits: 15/15
c ---[ 300]---> Adder-cost: 428   maxlim: 44651   bits: 16/16
c ---[ 298]---> Adder-cost: 428   maxlim: 45035   bits: 16/16
c ---[ 296]---> Adder-cost: 434   maxlim: 51819   bits: 16/16
c ---[ 294]---> Adder-cost: 412   maxlim: 29547   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 290]---> Adder-cost: 242   maxlim: 23540   bits: 15/15
c ---[ 288]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 286]---> Adder-cost: 262   maxlim: 42356   bits: 16/16
c ---[ 284]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 282]---> Adder-cost: 262   maxlim: 41332   bits: 16/16
c ---[ 280]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 278]---> Adder-cost: 266   maxlim: 46836   bits: 16/16
c ---[ 276]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 274]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 272]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 270]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 268]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 266]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 264]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 262]---> Adder-cost: 262   maxlim: 42612   bits: 16/16
c ---[ 260]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 258]---> Adder-cost: 242   maxlim: 22644   bits: 15/15
c ---[ 256]---> Adder-cost: 266   maxlim: 48372   bits: 16/16
c ---[ 254]---> Adder-cost: 266   maxlim: 49140   bits: 16/16
c ---[ 252]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   12
c ---[ 241]---> BDD-cost:   10
c ---[ 240]---> BDD-cost:   11
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   14
c ---[ 233]---> BDD-cost:   15
c ---[ 232]---> BDD-cost:   11
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   10
c ---[ 229]---> BDD-cost:   14
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   10
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   10
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   10
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   17
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   11
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   17
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   17
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   17
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   10
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   10
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   15
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   10
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   10
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   17
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   14
c ---[ 164]---> BDD-cost:   15
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:   17
c ---[ 161]---> BDD-cost:   14
c ---[ 160]---> BDD-cost:   10
c ---[ 159]---> BDD-cost:   17
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   17
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   10
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   15
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   10
c ---[ 138]---> BDD-cost:   14
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   15
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost:   10
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   17
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   15
c ---[ 119]---> BDD-cost:   14
c ---[ 118]---> BDD-cost:   14
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   11
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   17
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   17
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   17
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   11
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   15
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   17
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   17
c ---[  88]---> BDD-cost:   13
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:   15
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   17
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   17
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   11
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   13
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   13
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   15
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   15
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   11
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   14
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   73517   256059 |   24505       0        0     nan |  0.000 % |
c |       100 |   73320   255390 |   26955      75      231     3.1 | 21.386 % |
c |       250 |   73230   255084 |   29651     212      661     3.1 | 21.497 % |
c |       475 |   72987   254239 |   32616     409     1322     3.2 | 21.725 % |
c |       812 |   72857   253797 |   35877     727     2372     3.3 | 21.854 % |
c |      1318 |   72623   252993 |   39465    1200     3853     3.2 | 22.082 % |
c |      2077 |   72178   251464 |   43412    1893     6146     3.2 | 22.533 % |
c |      3216 |   71912   250556 |   47753    2991    10032     3.4 | 22.791 % |
c |      4924 |   71582   249416 |   52528    4656    17045     3.7 | 23.124 % |
c |      7486 |   71451   248979 |   57781    7200    30538     4.2 | 23.265 % |
c |     11330 |   71411   248845 |   63559   11035    63963     5.8 | 23.306 % |
c |     17096 |   71385   248757 |   69915   16797   118371     7.0 | 23.335 % |
c |     25746 |   71225   248225 |   76907   25428   191673     7.5 | 23.505 % |
c |     38720 |   71195   248119 |   84597   38397  1164960    30.3 | 23.528 % |
c |     58181 |   71064   247688 |   93057   57840  1460059    25.2 | 23.686 % |
c |     87373 |   70745   246613 |  102363   86990  1886587    21.7 | 24.031 % |
c |    131163 |   70594   246112 |  112599   34067  4725528   138.7 | 24.184 % |
c |    196847 |   70505   245817 |  123859   99740  6284927    63.0 | 24.289 % |
c ==============================================================================
c [1mFound solution: 4859811[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10758   maxlim: 3502528   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203201 |  145757   514619 |   48585  106093  6356071    59.9 | 24.289 % |
c |    203303 |  145757   514619 |   53443   24116   215119     8.9 | 14.945 % |
c |    203453 |  145757   514619 |   58787   24266   216088     8.9 | 14.945 % |
c |    203678 |  145757   514619 |   64666   24491   218207     8.9 | 14.945 % |
c |    204015 |  145757   514619 |   71133   24828   221449     8.9 | 14.945 % |
c |    204521 |  145757   514619 |   78246   25334   225328     8.9 | 14.945 % |
c |    205280 |  145757   514619 |   86071   26093   233063     8.9 | 14.945 % |
c |    206420 |  145748   514590 |   94678   27232   242990     8.9 | 14.952 % |
c |    208128 |  145739   514559 |  104146   28938   264550     9.1 | 14.956 % |
c |    210690 |  145732   514536 |  114560   31498   301371     9.6 | 14.960 % |
c |    214534 |  145732   514536 |  126016   35342   359712    10.2 | 14.960 % |
c |    220300 |  145732   514536 |  138618   41108   439243    10.7 | 14.960 % |
c |    228949 |  145714   514478 |  152480   49755   595270    12.0 | 14.974 % |
c |    241923 |  145696   514420 |  167728   62727   765950    12.2 | 14.988 % |
c |    261384 |  145678   514362 |  184501   82186  1390726    16.9 | 15.003 % |
c ==============================================================================
c [1mFound solution: 4809398[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3552941   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    277660 |  145608   514261 |   48536   98448  1895063    19.2 | 15.003 % |
c |    277761 |  145608   514261 |   53389   25241   259179    10.3 | 15.083 % |
c |    277911 |  145608   514261 |   58728   25391   259920    10.2 | 15.083 % |
c |    278136 |  145599   514232 |   64601   25614   261102    10.2 | 15.091 % |
c |    278474 |  145599   514232 |   71061   25952   263255    10.1 | 15.091 % |
c |    278980 |  145599   514232 |   78167   26458   266115    10.1 | 15.091 % |
c |    279739 |  145599   514232 |   85984   27217   270443     9.9 | 15.091 % |
c |    280881 |  145590   514203 |   94582   28358   279449     9.9 | 15.098 % |
c |    282589 |  145583   514180 |  104041   30065   288882     9.6 | 15.101 % |
c |    285151 |  145560   514101 |  114445   32624   305910     9.4 | 15.116 % |
c |    288995 |  145545   514052 |  125889   36465   335399     9.2 | 15.127 % |
c |    294761 |  145545   514052 |  138478   42231   389287     9.2 | 15.127 % |
c |    303410 |  145545   514052 |  152326   50880  1990096    39.1 | 15.127 % |
c |    316385 |  145407   513582 |  167559   63829  2150015    33.7 | 15.205 % |
c |    335847 |  145389   513522 |  184315   83288  3302885    39.7 | 15.216 % |
c ==============================================================================
c [1mFound solution: 4655889[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3706450   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    362174 |  145356   513519 |   48452  109604  3704209    33.8 | 15.216 % |
c |    362274 |  145356   513519 |   53297   27094   239640     8.8 | 15.262 % |
c |    362424 |  145356   513519 |   58626   27244   240326     8.8 | 15.262 % |
c |    362649 |  145356   513519 |   64489   27469   241806     8.8 | 15.262 % |
c |    362986 |  145356   513519 |   70938   27806   243710     8.8 | 15.262 % |
c |    363492 |  145356   513519 |   78032   28312   246517     8.7 | 15.262 % |
c |    364251 |  145356   513519 |   85835   29071   252992     8.7 | 15.262 % |
c |    365390 |  145356   513519 |   94419   30210   260340     8.6 | 15.262 % |
c |    367098 |  145356   513519 |  103861   31918   272154     8.5 | 15.262 % |
c |    369660 |  145356   513519 |  114247   34480   299338     8.7 | 15.262 % |
c |    373504 |  145356   513519 |  125672   38324   334130     8.7 | 15.262 % |
c |    379270 |  145330   513429 |  138239   44085   699771    15.9 | 15.276 % |
c |    387919 |  145324   513409 |  152063   52732   781850    14.8 | 15.279 % |
c |    400893 |  145309   513358 |  167269   65701  1023070    15.6 | 15.287 % |
c |    420354 |  145309   513358 |  183996   85162  2434044    28.6 | 15.287 % |
c |    449547 |  145300   513329 |  202396  114354  4653627    40.7 | 15.294 % |
c ==============================================================================
c [1mFound solution: 4033059[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4329280   bits: 23/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    456328 |  145296   513040 |   48432  118365  4487806    37.9 | 15.294 % |
c |    456428 |  145296   513040 |   53275   25091   762772    30.4 | 15.316 % |
c |    456578 |  145296   513040 |   58602   25241   763472    30.2 | 15.316 % |
c |    456803 |  145296   513040 |   64462   25466   764679    30.0 | 15.316 % |
c |    457140 |  145296   513040 |   70909   25803   766531    29.7 | 15.316 % |
c |    457647 |  145296   513040 |   78000   26310   769227    29.2 | 15.316 % |
c |    458406 |  145296   513040 |   85800   27069   772716    28.5 | 15.316 % |
c |    459545 |  145296   513040 |   94380   28208   778574    27.6 | 15.316 % |
c |    461253 |  145296   513040 |  103818   29916   788892    26.4 | 15.316 % |
c |    463815 |  145296   513040 |  114200   32478   804616    24.8 | 15.316 % |
c |    467659 |  145296   513040 |  125620   36322   830665    22.9 | 15.316 % |
c |    473426 |  145296   513040 |  138182   42089   890268    21.2 | 15.316 % |
c |    482075 |  145296   513040 |  152000   50738  1010014    19.9 | 15.316 % |
c |    495049 |  145296   513040 |  167200   63712  1187445    18.6 | 15.316 % |
c |    514511 |  145269   512949 |  183920   83167  1521156    18.3 | 15.331 % |
c |    543703 |  145269   512949 |  202312  112359  2445534    21.8 | 15.331 % |
c |    587492 |  145263   512929 |  222543  156146  6380743    40.9 | 15.334 % |
c |    653176 |  145263   512929 |  244798  221830 10997070    49.6 | 15.334 % |
c |    751702 |  145250   512888 |  269277  100885  1961814    19.4 | 15.342 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v X0_bit_7 X0_bit_6 -X0_bit_5 X0_bit_4 X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 X1_bit_6 -X1_bit_5 X1_bit_4 X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 X3_bit_6 X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 X4_bit_6 X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 X6_bit_7 X6_bit_6 -X6_bit_5 -X6_bit_4 X6_bit_3 -X6_bit_2 -X6_bit_1 X6_bit0 X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 X8_bit_6 -X8_bit_5 -X8_bit_4 X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 X9_bit_1 X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 X11_bit_4 -X11_bit_3 X11_bit_2 X11_bit_1 -X11_bit0 X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 X13_bit_5 -X13_bit_4 -X13_bit_3 X13_bit_2 X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 X15_bit_6 X15_bit_5 X15_bit_4 X15_bit_3 -X15_bit_2 -X15_bit_1 X15_bit0 X15_bit1 X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 X16_bit_5 -X16_bit_4 -X16_bit_3 X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 -X24_bit_5 -X24_bit_4 X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 X26_bit_7 -X26_bit_6 -X26_bit_5 X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 -X27_bit_6 -X27_bit_5 X27_bit_4 -X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 X28_bit_7 -X28_bit_6 X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 -X29_bit_5 X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 X30_bit_6 X30_bit_5 -X30_bit_4 X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 -X31_bit_6 X31_bit_5 -X31_bit_4 X31_bit_3 -X31_bit_2 X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 X32_bit_6 X32_bit_5 -X32_bit_4 -X32_bit_3 X32_bit_2 X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 X33_bit_5 -X33_bit_4 -X33_bit_3 X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 X34_bit_5 -X34_bit_4 -X34_bit_3 X34_bit_2 X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 X35_bit_7 -X35_bit_6 X35_bit_5 -X35_bit_4 X35_bit_3 -X35_bit_2 X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 X36_bit_6 -X36_bit_5 -X36_bit_4 X36_bit_3 -X36_bit_2 X36_bit_1 X36_bit0 X36_bit1 X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 X37_bit_5 -X37_bit_4 -X37_bit_3 X37_bit_2 -X37_bit_1 X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 X38_bit_1 -X38_bit0 X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 X40_bit_3 X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 X41_bit_5 -X41_bit_4 X41_bit_3 -X41_bit_2 X41_bit_1 -X41_bit0 X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 -X42_bit_6 -X42_bit_5 X42_bit_4 X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 X45_bit_6 X45_bit_5 -X45_bit_4 X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 X49_bit_5 X49_bit_4 X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 X49_bit1 X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 X50_bit_4 X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 X54_bit_7 -X54_bit_6 X54_bit_5 -X54_bit_4 X54_bit_3 X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 X57_bit_7 -X57_bit_6 X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 X57_bit_1 -X57_bit0 -X57_bit1 X57_bit2 X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 X59_bit_2 X59_bit_1 -X59_bit0 X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 X62_bit_5 -X62_bit_4 -X62_bit_3 X62_bit_2 -X62_bit_1 -X62_bit0 X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 X64_bit_6 X64_bit_5 X64_bit_4 -X64_bit_3 -X64_bit_2 X64_bit_1 -X64_bit0 X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 X66_bit_6 -X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 X67_bit_1 X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 -X69_bit_6 X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 X72_bit_6 -X72_bit_5 -X72_bit_4 X72_bit_3 -X72_bit_2 -X72_bit_1 X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 -X74_bit_6 X74_bit_5 -X74_bit_4 X74_bit_3 X74_bit_2 X74_bit_1 -X74_bit0 X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 X76_bit_6 X76_bit_5 -X76_bit_4 -X76_bit_3 X76_bit_2 -X76_bit_1 X76_bit0 -X76_bit1 X76_bit2 X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 X78_bit_6 -X78_bit_5 -X78_bit_4 X78_bit_3 -X78_bit_2 -X78_bit_1 X78_bit0 -X78_bit1 X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 -X79_bit_6 X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 X82_bit_6 X82_bit_5 -X82_bit_4 X82_bit_3 X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 X84_bit_6 -X84_bit_5 -X84_bit_4 X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 X85_bit_4 -X85_bit_3 -X85_bit_2 X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 X86_bit_6 -X86_bit_5 -X86_bit_4 X86_bit_3 X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 X87_bit_4 X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 X93_bit_3 X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 -X94_bit_6 X94_bit_5 X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 -X95_bit_6 -X95_bit_5 X95_bit_4 -X95_bit_3 X95_bit_2 X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 X96_bit_6 X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 X97_bit_6 X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 X97_bit_1 -X97_bit0 X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bit_6 -X99_bit_5 -X99_bit_4 X99_bit_3 -X99_bit_2 -X99_bit_1 X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 X104_bit_7 -X104_bit_6 X104_bit_5 -X104_bit_4 -X104_bit_3 X104_bit_2 X104_bit_1 -X104_bit0 X104_bit1 -X104_bit2 X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 X106_bit_5 -X106_bit_4 -X106_bit_3 X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 X107_bit_4 X107_bit_3 X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 X109_bit_2 X109_bit_1 X109_bit0 X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 X112_bit_7 -X112_bit_6 X112_bit_5 X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 X116_bit_1 -X116_bit0 X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 X123_bit_5 X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 X125_bit_5 -X125_bit_4 -X125_bit_3 X125_bit_2 -X125_bit_1 -X125_bit0 X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 X126_bit_6 -X126_bit_5 -X126_bit_4 X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 X127_bit_5 X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 X129_bit_6 X129_bit_5 X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 X130_bit_1 -X130_bit0 X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 -X132_bit_6 X132_bit_5 -X132_bit_4 -X132_bit_3 X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 X135_bit_7 X135_bit_6 -X135_bit_5 -X135_bit_4 X135_bit_3 X135_bit_2 X135_bit_1 X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 X136_bit_7 -X136_bit_6 -X136_bit_5 X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 X139_bit_6 X139_bit_5 -X139_bit_4 -X139_bit_3 X139_bit_2 -X139_bit_1 -X139_bit0 X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 X140_bit_1 X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 X141_bit_7 X141_bit_6 X141_bit_5 -X141_bit_4 X141_bit_3 -X141_bit_2 -X141_bit_1 X141_bit0 X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 X142_bit_2 X142_bit_1 X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 X146_bit_6 X146_bit_5 X146_bit_4 -X146_bit_3 -X146_bit_2 X146_bit_1 -X146_bit0 X146_bit1 X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 X147_bit_7 X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 X149_bit_7 X149_bit_6 -X149_bit_5 X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 X150_bit_6 X150_bit_5 X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 X151_bit_1 -X151_bit0 X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 X152_bit_4 X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 X154_bit_7 X154_bit_6 X154_bit_5 X154_bit_4 X154_bit_3 -X154_bit_2 X154_bit_1 X154_bit0 -X154_bit1 -X154_bit2 X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 X155_bit_7 X155_bit_6 -X155_bit_5 X155_bit_4 X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 X156_bit_7 X156_bit_6 X156_bit_5 -X156_bit_4 X156_bit_3 -X156_bit_2 X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 X160_bit_7 -X160_bit_6 X160_bit_5 -X160_bit_4 -X160_bit_3 X160_bit_2 X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 X162_bit_6 X162_bit_5 -X162_bit_4 X162_bit_3 -X162_bit_2 X162_bit_1 X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 X163_bit_7 X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 X163_bit_2 X163_bit_1 X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 X166_bit_7 -X166_bit_6 X166_bit_5 X166_bit_4 -X166_bit_3 X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 X168_bit_7 X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 X170_bit_6 -X170_bit_5 X170_bit_4 -X170_bit_3 X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 X171_bit_7 X171_bit_6 -X171_bit_5 X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 X172_bit_3 X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 X173_bit_4 X173_bit_3 X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 X176_bit_7 X176_bit_6 -X176_bit_5 X176_bit_4 X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 X176_bit2 -X176_bit3 X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 X177_bit_7 X177_bit_6 X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 X179_bit_7 X179_bit_6 X179_bit_5 -X179_bit_4 X179_bit_3 -X179_bit_2 X179_bit_1 X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 X181_bit_5 X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 X182_bit_6 X182_bit_5 X182_bit_4 -X182_bit_3 -X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 X183_bit_7 X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 X185_bit_7 X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 X186_bit_6 X186_bit_5 X186_bit_4 X186_bit_3 X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 X186_bit2 -X186_bit3 X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 X187_bit_5 X187_bit_4 X187_bit_3 X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 -X192_bit_6 -X192_bit_5 X192_bit_4 X192_bit_3 X192_bit_2 -X192_bit_1 X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 X193_bit_7 X193_bit_6 -X193_bit_5 X193_bit_4 X193_bit_3 -X193_bit_2 -X193_bit_1 X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 -X194_bit_5 X194_bit_4 X194_bit_3 X194_bit_2 -X194_bit_1 X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 X196_bit_7 X196_bit_6 -X196_bit_5 X196_bit_4 -X196_bit_3 X196_bit_2 -X196_bit_1 X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 X197_bit_7 X197_bit_6 -X197_bit_5 -X197_bit_4 -X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 X198_bit_5 -X198_bit_4 -X198_bit_3 X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 -X200_bit_5 X200_bit_4 -X200_bit_3 -X200_bit_2 X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 X202_bit_6 -X202_bit_5 X202_bit_4 X202_bit_3 -X202_bit_2 X202_bit_1 X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 X203_bit_5 -X203_bit_4 -X203_bit_3 X203_bit_2 X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 X204_bit_6 X204_bit_5 -X204_bit_4 X204_bit_3 -X204_bit_2 -X204_bit_1 X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 X205_bit_6 -X205_bit_5 -X205_bit_4 X205_bit_3 X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 X206_bit_6 -X206_bit_5 X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 -X208_bit_5 -X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 X211_bit_2 -X211_bit_1 -X211_bit0 X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 -X216_bit_4 X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 -X217_bit_6 -X217_bit_5 X217_bit_4 X217_bit_3 -X217_bit_2 -X217_bit_1 X217_bit0 -X217_bit1 X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 X218_bit_7 -X218_bit_6 -X218_bit_5 X218_bit_4 -X218_bit_3 -X218_bit_2 X218_bit_1 X218_bit0 -X218_bit1 X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 X219_bit_7 X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 X220_bit_5 -X220_bit_4 -X220_bit_3 X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 -X221_bit_6 X221_bit_5 X221_bit_4 -X221_bit_3 X221_bit_2 -X221_bit_1 X221_bit0 -X221_bit1 X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 X222_bit_6 -X222_bit_5 -X222_bit_4 X222_bit_3 X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 X223_bit_6 X223_bit_5 -X223_bit_4 X223_bit_3 X223_bit_2 X223_bit_1 -X223_bit0 -X223_bit1 X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 X224_bit_6 X224_bit_5 -X224_bit_4 -X224_bit_3 X224_bit_2 X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 X225_bit_7 X225_bit_6 X225_bit_5 -X225_bit_4 X225_bit_3 -X225_bit_2 -X225_bit_1 X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 X226_bit_6 -X226_bit_5 -X226_bit_4 X226_bit_3 X226_bit_2 -X226_bit_1 X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 X227_bit_7 -X227_bit_6 -X227_bit_5 X227_bit_4 -X227_bit_3 X227_bit_2 -X227_bit_1 X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 X229_bit_3 -X229_bit_2 X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 -X230_bit_6 -X230_bit_5 X230_bit_4 -X230_bit_3 X230_bit_2 X230_bit_1 X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 X231_bit_6 -X231_bit_5 -X231_bit_4 X231_bit_3 X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 -X233_bit_5 -X233_bit_4 X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 X234_bit_5 X234_bit_4 X234_bit_3 X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 X235_bit0 X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 X236_bit_6 -X236_bit_5 X236_bit_4 X236_bit_3 X236_bit_2 X236_bit_1 X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 X237_bit_4 -X237_bit_3 X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 X238_bit_2 -X238_bit_1 -X238_bit0 X238_bit1 X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 X239_bit_4 -X239_bit_3 -X239_bit_2 X239_bit_1 X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 X241_bit_2 X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 X242_bit_1 X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 -X244_bit_3 X244_bit_2 -X244_bit_1 X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 -X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 X249_bit_3 X249_bit_2 X249_bit_1 X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 -X250_bit_3 -X250_bit_2 X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 X251_bit_4 X251_bit_3 X251_bit_2 -X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 Y0_bit0 Y1_bit0 -Y2_bit0 Y3_bit0 Y4_bit0 Y5_bit0 Y6_bit0 -Y7_bit0 Y8_bit0 Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 Y13_bit0 Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 Y19_bit0 -Y20_bit0 -Y21_bit0 -Y22_bit0 -Y23_bit0 Y24_bit0 -Y25_bit0 Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 -Y43_bit0 Y44_bit0 Y45_bit0 -Y46_bit0 -Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 Y51_bit0 -Y52_bit0 Y53_bit0 Y54_bit0 -Y55_bit0 Y56_bit0 Y57_bit0 -Y58_bit0 Y59_bit0 -Y60_bit0 Y61_bit0 Y62_bit0 -Y63_bit0 Y64_bit0 -Y65_bit0 Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 -Y70_bit0 Y71_bit0 Y72_bit0 -Y73_bit0 Y74_bit0 -Y75_bit0 Y76_bit0 -Y77_bit0 Y78_bit0 Y79_bit0 -Y80_bit0 -Y81_bit0 Y82_bit0 -Y83_bit0 Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 -Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 -Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 -Y108_bit0 Y109_bit0 Y110_bit0 Y111_bit0 Y112_bit0 -Y113_bit0 -Y114_bit0 Y115_bit0 Y116_bit0 -Y117_bit0 Y118_bit0 -Y119_bit0 Y120_bit0 Y121_bit0 -Y122_bit0 Y123_bit0 -Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 -Y128_bit0 Y129_bit0 Y130_bit0 -Y131_bit0 Y132_bit0 -Y133_bit0 -Y134_bit0 Y135_bit0 Y136_bit0 -Y137_bit0 Y138_bit0 Y139_bit0 Y140_bit0 Y141_bit0 Y142_bit0 -Y143_bit0 Y144_bit0 -Y145_bit0 Y146_bit0 Y147_bit0 -Y148_bit0 Y149_bit0 Y150_bit0 Y151_bit0 Y152_bit0 Y153_bit0 Y154_bit0 Y155_bit0 Y156_bit0 Y157_bit0 -Y158_bit0 -Y159_bit0 Y160_bit0 -Y161_bit0 Y162_bit0 Y163_bit0 Y164_bit0 Y165_bit0 Y166_bit0 -Y167_bit0 Y168_bit0 -Y169_bit0 Y170_bit0 Y171_bit0 Y172_bit0 Y173_bit0 Y174_bit0 -Y175_bit0 Y176_bit0 Y177_bit0 -Y178_bit0 Y179_bit0 Y180_bit0 Y181_bit0 Y182_bit0 Y183_bit0 Y184_bit0 Y185_bit0 Y186_bit0 Y187_bit0 -Y188_bit0 -Y189_bit0 Y190_bit0 Y191_bit0 Y192_bit0 Y193_bit0 Y194_bit0 Y195_bit0 Y196_bit0 Y197_bit0 Y198_bit0 -Y199_bit0 Y200_bit0 Y201_bit0 Y202_bit0 Y203_bit0 Y204_bit0 Y205_bit0 Y206_bit0 -Y207_bit0 Y208_bit0 Y209_bit0 Y210_bit0 Y211_bit0 -Y212_bit0 Y213_bit0 -Y214_bit0 Y215_bit0 Y216_bit0 Y217_bit0 Y218_bit0 Y219#### 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.78 0.90 0.94 2/54 16470
Raw data (stat): 16470 (runsolver) R 16469 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482885497 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.82 0.91 0.94 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 1962 0 0 0 993 5 0 0 25 0 1 0 482885497 10641408 1929 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2598 1929 603 41 0 2557 0
vsize: 10392
[startup+19.9997 s]
Raw data (loadavg): 0.84 0.91 0.94 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 2040 0 0 0 1992 6 0 0 25 0 1 0 482885497 11042816 2007 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2696 2007 603 41 0 2655 0
vsize: 10784
[startup+30.001 s]
Raw data (loadavg): 0.87 0.91 0.94 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 2220 0 0 0 2991 7 0 0 25 0 1 0 482885497 11755520 2187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2870 2187 603 41 0 2829 0
vsize: 11480
[startup+40.0002 s]
Raw data (loadavg): 0.89 0.91 0.94 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 2382 0 0 0 3991 7 0 0 25 0 1 0 482885497 12427264 2349 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3034 2349 603 41 0 2993 0
vsize: 12136
[startup+50.0008 s]
Raw data (loadavg): 0.90 0.92 0.94 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 3559 0 0 0 4988 10 0 0 25 0 1 0 482885497 17276928 3526 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4218 3526 603 41 0 4177 0
vsize: 16872
[startup+60.0009 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 3809 0 0 0 5987 11 0 0 25 0 1 0 482885497 18223104 3776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4449 3776 603 41 0 4408 0
vsize: 17796
[startup+70.0002 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 4069 0 0 0 6987 12 0 0 25 0 1 0 482885497 19304448 4036 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4713 4036 603 41 0 4672 0
vsize: 18852
[startup+80.001 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 4338 0 0 0 7987 12 0 0 25 0 1 0 482885497 20639744 4305 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5039 4305 603 41 0 4998 0
vsize: 20156
[startup+90.001 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 4525 0 0 0 8986 13 0 0 25 0 1 0 482885497 21315584 4492 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5204 4492 603 41 0 5163 0
vsize: 20816
[startup+100.001 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 4708 0 0 0 9986 13 0 0 25 0 1 0 482885497 22126592 4675 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5402 4675 603 41 0 5361 0
vsize: 21608
[startup+110.001 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 4889 0 0 0 10985 14 0 0 25 0 1 0 482885497 22802432 4856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5567 4856 603 41 0 5526 0
vsize: 22268
[startup+120.001 s]
Raw data (loadavg): 1.00 0.94 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 5120 0 0 0 11985 15 0 0 25 0 1 0 482885497 23744512 5087 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5797 5087 603 41 0 5756 0
vsize: 23188
[startup+130.001 s]
Raw data (loadavg): 1.00 0.95 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 5748 0 0 0 12983 16 0 0 25 0 1 0 482885497 26292224 5715 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6419 5715 603 41 0 6378 0
vsize: 25676
[startup+140.001 s]
Raw data (loadavg): 1.00 0.95 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 7010 0 0 0 13980 20 0 0 25 0 1 0 482885497 31428608 6977 4294967295 134512640 134672761 3221224544 3221223552 134565819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7673 6977 603 41 0 7632 0
vsize: 30692
[startup+150.002 s]
Raw data (loadavg): 1.08 0.96 0.95 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 7013 0 0 0 14980 20 0 0 25 0 1 0 482885497 31428608 6980 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7673 6980 603 41 0 7632 0
vsize: 30692
[startup+160.002 s]
Raw data (loadavg): 1.14 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 7625 0 0 0 15979 21 0 0 25 0 1 0 482885497 33988608 7592 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7592 603 41 0 8257 0
vsize: 33192
[startup+170.001 s]
Raw data (loadavg): 1.12 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 8116 0 0 0 16978 22 0 0 25 0 1 0 482885497 35872768 8083 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 8083 603 41 0 8717 0
vsize: 35032
[startup+180.001 s]
Raw data (loadavg): 1.10 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 8143 0 0 0 17978 22 0 0 25 0 1 0 482885497 36007936 8110 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8791 8110 603 41 0 8750 0
vsize: 35164
[startup+190.002 s]
Raw data (loadavg): 1.08 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 8164 0 0 0 18978 22 0 0 25 0 1 0 482885497 36143104 8131 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8824 8131 603 41 0 8783 0
vsize: 35296
[startup+200.001 s]
Raw data (loadavg): 1.07 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 8350 0 0 0 19978 23 0 0 25 0 1 0 482885497 36954112 8317 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9022 8317 603 41 0 8981 0
vsize: 36088
[startup+210.001 s]
Raw data (loadavg): 1.06 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 9154 0 0 0 20976 25 0 0 25 0 1 0 482885497 40181760 9121 4294967295 134512640 134672761 3221224544 3221223788 134560736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9121 603 41 0 9769 0
vsize: 39240
[startup+220.001 s]
Raw data (loadavg): 1.05 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 9298 0 0 0 21976 25 0 0 25 0 1 0 482885497 40722432 9265 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9265 603 41 0 9901 0
vsize: 39768
[startup+230.002 s]
Raw data (loadavg): 1.04 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 9650 0 0 0 22975 26 0 0 25 0 1 0 482885497 42205184 9617 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10304 9617 603 41 0 10263 0
vsize: 41216
[startup+240.002 s]
Raw data (loadavg): 1.04 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 9777 0 0 0 23975 26 0 0 25 0 1 0 482885497 42741760 9744 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10435 9744 603 41 0 10394 0
vsize: 41740
[startup+250.002 s]
Raw data (loadavg): 1.03 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16191 0 0 0 24963 39 0 0 25 0 1 0 482885497 65097728 14836 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14836 603 41 0 15852 0
vsize: 63572
[startup+260.003 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16193 0 0 0 25963 39 0 0 25 0 1 0 482885497 65097728 14838 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15893 14838 603 41 0 15852 0
vsize: 63572
[startup+270.003 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16194 0 0 0 26962 39 0 0 25 0 1 0 482885497 65097728 14839 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15893 14839 603 41 0 15852 0
vsize: 63572
[startup+280.003 s]
Raw data (loadavg): 1.02 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16194 0 0 0 27962 39 0 0 25 0 1 0 482885497 65097728 14839 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14839 603 41 0 15852 0
vsize: 63572
[startup+290.004 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16195 0 0 0 28962 39 0 0 25 0 1 0 482885497 65097728 14840 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14840 603 41 0 15852 0
vsize: 63572
[startup+300.004 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16195 0 0 0 29962 39 0 0 25 0 1 0 482885497 65097728 14840 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14840 603 41 0 15852 0
vsize: 63572
[startup+310.003 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16195 0 0 0 30962 39 0 0 25 0 1 0 482885497 65097728 14840 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14840 603 41 0 15852 0
vsize: 63572
[startup+320.003 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16195 0 0 0 31963 39 0 0 25 0 1 0 482885497 65097728 14840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14840 603 41 0 15852 0
vsize: 63572
[startup+330.004 s]
Raw data (loadavg): 1.01 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16195 0 0 0 32963 39 0 0 25 0 1 0 482885497 65097728 14840 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14840 603 41 0 15852 0
vsize: 63572
[startup+340.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16196 0 0 0 33963 39 0 0 25 0 1 0 482885497 65097728 14841 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14841 603 41 0 15852 0
vsize: 63572
[startup+350.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16196 0 0 0 34963 39 0 0 25 0 1 0 482885497 65097728 14841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14841 603 41 0 15852 0
vsize: 63572
[startup+360.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 35963 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+370.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 36963 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+380.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 37964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+390.004 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 38964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+400.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 39964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+410.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 40964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+420.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 41964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+430.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 42964 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+440.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 43965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+450.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 44965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+460.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 45965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+470.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 46965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+480.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 47965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+490.005 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 48965 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+500.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16229 0 0 0 49966 39 0 0 25 0 1 0 482885497 65097728 14874 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14874 603 41 0 15852 0
vsize: 63572
[startup+510.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 50966 39 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+520.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 51966 39 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+530.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 52966 39 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+540.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 53966 39 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+550.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 54966 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+560.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 55966 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+570.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 56967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+580.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 57967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+590.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 58967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+600.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 59967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+610.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 60967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+620.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 61967 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+630.006 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 62968 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+640.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 63968 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+650.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16230 0 0 0 64968 40 0 0 25 0 1 0 482885497 65097728 14875 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14875 603 41 0 15852 0
vsize: 63572
[startup+660.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16236 0 0 0 65968 40 0 0 25 0 1 0 482885497 65097728 14881 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14881 603 41 0 15852 0
vsize: 63572
[startup+670.007 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 66968 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+680.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 67969 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+690.008 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 68969 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+700.013 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 69970 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+710.016 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 70970 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+720.016 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 71970 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+730.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 72970 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+740.016 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 73971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+750.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 74971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+760.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 75971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+770.016 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 76971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+780.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 77971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+790.017 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 78971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+800.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 79971 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+810.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16238 0 0 0 80972 40 0 0 25 0 1 0 482885497 65097728 14883 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14883 603 41 0 15852 0
vsize: 63572
[startup+820.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16243 0 0 0 81972 40 0 0 25 0 1 0 482885497 65097728 14888 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15893 14888 603 41 0 15852 0
vsize: 63572
[startup+830.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16249 0 0 0 82972 40 0 0 25 0 1 0 482885497 65622016 14894 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16021 14894 603 41 0 15980 0
vsize: 64084
[startup+840.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16252 0 0 0 83972 40 0 0 25 0 1 0 482885497 65622016 14897 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16021 14897 603 41 0 15980 0
vsize: 64084
[startup+850.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16254 0 0 0 84972 40 0 0 25 0 1 0 482885497 65622016 14899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16021 14899 603 41 0 15980 0
vsize: 64084
[startup+860.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 16825 0 0 0 85971 42 0 0 25 0 1 0 482885497 67907584 15470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16579 15470 603 41 0 16538 0
vsize: 66316
[startup+870.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 17164 0 0 0 86970 43 0 0 25 0 1 0 482885497 69251072 15809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16907 15809 603 41 0 16866 0
vsize: 67628
[startup+880.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 17615 0 0 0 87969 44 0 0 25 0 1 0 482885497 71143424 16260 4294967295 134512640 134672761 3221224544 3221223648 134560128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17369 16260 603 41 0 17328 0
vsize: 69476
[startup+890.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 17884 0 0 0 88968 45 0 0 25 0 1 0 482885497 72220672 16529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17632 16529 603 41 0 17591 0
vsize: 70528
[startup+900.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 18545 0 0 0 89966 47 0 0 25 0 1 0 482885497 74919936 17190 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18291 17190 603 41 0 18250 0
vsize: 73164
[startup+910.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 19082 0 0 0 90965 48 0 0 25 0 1 0 482885497 77066240 17727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18815 17727 603 41 0 18774 0
vsize: 75260
[startup+920.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 19722 0 0 0 91963 50 0 0 25 0 1 0 482885497 79765504 18367 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19474 18367 603 41 0 19433 0
vsize: 77896
[startup+930.018 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 20189 0 0 0 92962 52 0 0 25 0 1 0 482885497 81653760 18834 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19935 18834 603 41 0 19894 0
vsize: 79740
[startup+940.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 20622 0 0 0 93961 52 0 0 25 0 1 0 482885497 83402752 19267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20362 19267 603 41 0 20321 0
vsize: 81448
[startup+950.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 21033 0 0 0 94960 54 0 0 25 0 1 0 482885497 85012480 19678 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20755 19678 603 41 0 20714 0
vsize: 83020
[startup+960.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 21381 0 0 0 95960 55 0 0 25 0 1 0 482885497 86515712 20026 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21122 20026 603 41 0 21081 0
vsize: 84488
[startup+970.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 21758 0 0 0 96959 55 0 0 25 0 1 0 482885497 88055808 20403 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21498 20403 603 41 0 21457 0
vsize: 85992
[startup+980.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 22124 0 0 0 97959 56 0 0 25 0 1 0 482885497 89538560 20769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21860 20769 603 41 0 21819 0
vsize: 87440
[startup+990.019 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 22357 0 0 0 98958 57 0 0 25 0 1 0 482885497 90488832 21002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22092 21002 603 41 0 22051 0
vsize: 88368
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 22622 0 0 0 99958 58 0 0 25 0 1 0 482885497 91619328 21267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22368 21267 603 41 0 22327 0
vsize: 89472
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 22897 0 0 0 100957 58 0 0 25 0 1 0 482885497 92704768 21542 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22633 21542 603 41 0 22592 0
vsize: 90532
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23075 0 0 0 101956 59 0 0 25 0 1 0 482885497 93511680 21720 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21720 603 41 0 22789 0
vsize: 91320
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23328 0 0 0 102956 60 0 0 25 0 1 0 482885497 94457856 21973 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23061 21973 603 41 0 23020 0
vsize: 92244
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23660 0 0 0 103954 61 0 0 25 0 1 0 482885497 95809536 22305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23391 22305 603 41 0 23350 0
vsize: 93564
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23884 0 0 0 104954 62 0 0 25 0 1 0 482885497 96755712 22529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23622 22529 603 41 0 23581 0
vsize: 94488
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 105954 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 106954 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 107954 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 108954 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 109955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 110955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 111955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 112955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 113955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 114955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 115956 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 116956 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 117956 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 118955 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.98 0.96 2/54 16470
Raw data (stat): 16470 (minisat+) R 16469 20937 20936 0 -1 0 23947 0 0 0 119956 62 0 0 25 0 1 0 482885497 96890880 22592 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23655 22592 603 41 0 23614 0
vsize: 94620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.98 0.96 1/54 16470
Raw data (stat): 16470 (minisat+) Z 16469 20937 20936 0 -1 12 23950 0 0 0 119956 67 0 0 25 0 1 0 482885497 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1199.57
CPU system time (s): 0.673897
CPU usage (%): 100.013
Max. virtual memory (Kb): 94620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####