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-ran10x26.opb
MD5SUM	f8a5d8e99e0f063cb10208b1e5f7bf38
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1277437
Optimality of the best value was proved	NO
Number of terms in the objective function	5460
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	1567797422
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	1567797422
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	5460
Total number of constraints	296
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	296
Minimum length of a constraint	21
Maximum length of a constraint	520
Trace number 17668

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        744372 kB
Buffers:          2764 kB
Cached:         263836 kB
SwapCached:        844 kB
Active:          44408 kB
Inactive:       224276 kB
HighTotal:      131008 kB
HighFree:         3808 kB
LowTotal:       903652 kB
LowFree:        740564 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15984 kB
Committed_AS:    63780 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:33:09 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19253 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 332 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 330]---> Adder-cost: 538   maxlim: 57062   bits: 16/16
c ---[ 328]---> Adder-cost: 536   maxlim: 52326   bits: 16/16
c ---[ 326]---> Adder-cost: 536   maxlim: 52582   bits: 16/16
c ---[ 324]---> Adder-cost: 536   maxlim: 53094   bits: 16/16
c ---[ 322]---> Adder-cost: 536   maxlim: 53606   bits: 16/16
c ---[ 320]---> Adder-cost: 538   maxlim: 58982   bits: 16/16
c ---[ 318]---> Adder-cost: 522   maxlim: 38502   bits: 16/16
c ---[ 316]---> Adder-cost: 538   maxlim: 57574   bits: 16/16
c ---[ 314]---> Adder-cost: 536   maxlim: 53990   bits: 16/16
c ---[ 312]---> Adder-cost: 538   maxlim: 56806   bits: 16/16
c ---[ 310]---> Adder-cost: 216   maxlim: 36214   bits: 16/16
c ---[ 308]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Adder-cost: 216   maxlim: 35190   bits: 16/16
c ---[ 304]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Adder-cost: 216   maxlim: 35446   bits: 16/16
c ---[ 296]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Adder-cost: 216   maxlim: 35062   bits: 16/16
c ---[ 288]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 280]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Adder-cost: 216   maxlim: 36470   bits: 16/16
c ---[ 266]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   12
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   17
c ---[ 255]---> BDD-cost:   11
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   11
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   14
c ---[ 249]---> BDD-cost:   14
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   12
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   17
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   10
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   12
c ---[ 233]---> BDD-cost:   12
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   12
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   12
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   12
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   12
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   17
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   19
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   10
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   12
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   12
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   13
c ---[ 184]---> BDD-cost:   15
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   10
c ---[ 177]---> BDD-cost:   12
c ---[ 176]---> BDD-cost:   12
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   15
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   12
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   17
c ---[ 165]---> BDD-cost:   12
c ---[ 164]---> BDD-cost:   14
c ---[ 163]---> BDD-cost:   14
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   17
c ---[ 154]---> BDD-cost:   18
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   12
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   12
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   16
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   10
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   12
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   12
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   17
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   17
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   12
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   12
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  153624   418346 |   51208       0        0     nan |  0.000 % |
c |       101 |  153621   418340 |   56328     100      955     9.6 |  8.520 % |
c |       251 |  153496   418059 |   61961     241     1573     6.5 |  8.593 % |
c |       476 |  153223   417363 |   68157     436     2560     5.9 |  8.737 % |
c |       815 |  153172   417212 |   74973     771     4010     5.2 |  8.760 % |
c |      1321 |  153087   417006 |   82470    1269     6557     5.2 |  8.810 % |
c |      2082 |  152492   415591 |   90718    2016     9890     4.9 |  9.178 % |
c |      3221 |  151816   414010 |   99789    3113    14950     4.8 |  9.590 % |
c |      4929 |  151004   412122 |  109768    4787    22754     4.8 | 10.105 % |
c |      7491 |  150096   409953 |  120745    7314    35680     4.9 | 10.679 % |
c |     11337 |  149332   408128 |  132820   11098    53954     4.9 | 11.170 % |
c |     17103 |  147218   403186 |  146102   16753    82124     4.9 | 12.513 % |
c |     25752 |  142035   391161 |  160712   24952   127058     5.1 | 15.871 % |
c |     38726 |  139353   384695 |  176783   37702   242671     6.4 | 17.671 % |
c |     58187 |  138537   382646 |  194462   56985   574801    10.1 | 18.179 % |
c |     87380 |  137177   379095 |  213908   86001  1041932    12.1 | 18.964 % |
c ==============================================================================
c [1mFound solution: 4953344[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11067   maxlim: 3757998   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115299 |  214182   654637 |   71394  113822  2294918    20.2 | 18.964 % |
c |    115399 |  214182   654637 |   78533   31638   335810    10.6 | 15.624 % |
c |    115549 |  214182   654637 |   86386   31788   336541    10.6 | 15.624 % |
c |    115774 |  214168   654605 |   95025   32010   337646    10.5 | 15.633 % |
c |    116111 |  213959   654123 |  104527   32334   339327    10.5 | 15.744 % |
c |    116617 |  213895   653974 |  114980   32838   341942    10.4 | 15.780 % |
c |    117376 |  213844   653839 |  126478   33591   346017    10.3 | 15.810 % |
c |    118515 |  213844   653839 |  139126   34730   358094    10.3 | 15.810 % |
c |    120223 |  213782   653695 |  153039   36429   377717    10.4 | 15.842 % |
c |    122785 |  213752   653600 |  168343   38984   400980    10.3 | 15.853 % |
c |    126630 |  213752   653600 |  185177   42829   503726    11.8 | 15.853 % |
c |    132396 |  213734   653542 |  203695   48593   576094    11.9 | 15.859 % |
c |    141045 |  213386   652718 |  224064   57208   860406    15.0 | 16.050 % |
c |    154019 |  212922   651579 |  246471   70120  1036808    14.8 | 16.282 % |
c |    173481 |  212681   650914 |  271118   89543  2341353    26.1 | 16.392 % |
c ==============================================================================
c [1mFound solution: 4872745[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3838597   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    178632 |  212471   650506 |   70823   94680  2429816    25.7 | 16.392 % |
c |    178732 |  212471   650506 |   77905   29475  1269279    43.1 | 16.522 % |
c |    178882 |  212471   650506 |   85695   29625  1270206    42.9 | 16.522 % |
c |    179107 |  212471   650506 |   94265   29850  1271364    42.6 | 16.522 % |
c |    179444 |  212389   650320 |  103691   30175  1273316    42.2 | 16.564 % |
c |    179950 |  212297   650110 |  114061   30674  1276202    41.6 | 16.613 % |
c |    180710 |  212297   650110 |  125467   31434  1280187    40.7 | 16.613 % |
c |    181849 |  211980   649372 |  138013   32554  1291090    39.7 | 16.793 % |
c |    183557 |  211929   649254 |  151815   34254  1306977    38.2 | 16.821 % |
c |    186119 |  211860   649090 |  166996   36802  1323136    36.0 | 16.859 % |
c |    189963 |  211649   648595 |  183696   40622  1359819    33.5 | 16.975 % |
c |    195729 |  211643   648581 |  202066   46386  1529285    33.0 | 16.979 % |
c |    204378 |  211540   648338 |  222272   55026  1627557    29.6 | 17.045 % |
c |    217353 |  211377   647951 |  244500   67981  1892419    27.8 | 17.124 % |
c |    236819 |  211342   647853 |  268950   87441  4179896    47.8 | 17.139 % |
c ==============================================================================
c [1mFound solution: 4871776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3839566   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    246889 |  211338   647922 |   70446   97506  5187723    53.2 | 17.139 % |
c |    246989 |  211338   647922 |   77490   29751  1577981    53.0 | 17.156 % |
c |    247139 |  211338   647922 |   85239   29901  1578765    52.8 | 17.156 % |
c |    247364 |  211338   647922 |   93763   30126  1580259    52.5 | 17.156 % |
c |    247702 |  211338   647922 |  103139   30464  1582264    51.9 | 17.156 % |
c |    248208 |  211331   647899 |  113453   30968  1584851    51.2 | 17.158 % |
c |    248967 |  211327   647890 |  124799   31726  1588600    50.1 | 17.160 % |
c |    250106 |  211313   647858 |  137279   32864  1594863    48.5 | 17.168 % |
c |    251815 |  211284   647792 |  151007   34569  1604133    46.4 | 17.185 % |
c |    254377 |  211258   647733 |  166107   37122  1620062    43.6 | 17.198 % |
c |    258221 |  211092   647345 |  182718   40928  1645968    40.2 | 17.283 % |
c |    263988 |  211092   647345 |  200990   46695  1702981    36.5 | 17.283 % |
c |    272637 |  211009   647149 |  221089   55332  1815337    32.8 | 17.329 % |
c |    285611 |  210934   646973 |  243198   68288  2180241    31.9 | 17.368 % |
c |    305072 |  210836   646690 |  267518   87737  4113018    46.9 | 17.405 % |
c ==============================================================================
c [1mFound solution: 4773083[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3938259   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    321974 |  210827   646743 |   70275  104631  5043356    48.2 | 17.405 % |
c |    322074 |  210827   646743 |   77302   29752   785182    26.4 | 17.431 % |
c |    322224 |  210827   646743 |   85032   29902   785909    26.3 | 17.431 % |
c |    322449 |  210827   646743 |   93536   30127   786933    26.1 | 17.431 % |
c |    322786 |  210827   646743 |  102889   30464   788512    25.9 | 17.431 % |
c |    323292 |  210802   646683 |  113178   30969   791363    25.6 | 17.446 % |
c |    324051 |  210802   646683 |  124496   31728   795633    25.1 | 17.446 % |
c |    325190 |  210749   646559 |  136946   32858   803457    24.5 | 17.477 % |
c |    326898 |  210697   646438 |  150640   34562   825411    23.9 | 17.507 % |
c |    329460 |  210642   646308 |  165704   37109   846399    22.8 | 17.541 % |
c |    333304 |  210614   646243 |  182275   40950   871047    21.3 | 17.556 % |
c |    339070 |  210581   646167 |  200502   46711   944173    20.2 | 17.575 % |
c |    347719 |  210571   646144 |  220553   55357  1038758    18.8 | 17.582 % |
c |    360693 |  210479   645922 |  242608   68312  1375203    20.1 | 17.632 % |
c |    380154 |  210436   645821 |  266869   87767  4038650    46.0 | 17.659 % |
c ==============================================================================
c [1mFound solution: 3814092[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4897250   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    387378 |  210461   646031 |   70153   94990  4332290    45.6 | 17.659 % |
c |    387479 |  210438   645977 |   77168   29906  1908530    63.8 | 17.689 % |
c |    387629 |  210407   645905 |   84885   30043  1909228    63.5 | 17.705 % |
c |    387855 |  210395   645877 |   93373   30267  1910357    63.1 | 17.711 % |
c |    388192 |  210361   645799 |  102711   30597  1912312    62.5 | 17.730 % |
c |    388698 |  210361   645799 |  112982   31103  1915305    61.6 | 17.730 % |
c |    389457 |  210303   645664 |  124280   31854  1919086    60.2 | 17.760 % |
c |    390596 |  210303   645664 |  136708   32993  1925107    58.3 | 17.760 % |
c |    392304 |  210297   645650 |  150379   34698  1946055    56.1 | 17.764 % |
c |    394866 |  210231   645501 |  165417   37246  1962774    52.7 | 17.794 % |
c |    398710 |  210220   645474 |  181958   41088  1986082    48.3 | 17.801 % |
c |    404476 |  210178   645378 |  200154   46845  2123094    45.3 | 17.823 % |
c |    413125 |  210140   645290 |  220170   55487  2302289    41.5 | 17.843 % |
c |    426100 |  210067   645117 |  242187   68450  2472448    36.1 | 17.885 % |
c |    445561 |  209987   644905 |  266405   87893  5651418    64.3 | 17.923 % |
c |    474753 |  209968   644854 |  293046  117081  7105055    60.7 | 17.931 % |
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 -X252_bit_7 -X252_bit_6 -X252_bit_5 -X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 X253_bit_6 X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 X253_bit_1 X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 X254_bit_6 X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 -X255_bit_6 -X255_bit_5 -X255_bit_4 -X255_bit_3 -X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -X256_bit_7 -X256_bit_6 -X256_bit_5 -X256_bit_4 -X256_bit_3 -X256_bit_2 -X256_bit_1 -X256_bit0 -X256_bit1 -X256_bit2 -X256_bit3 -X256_bit4 -X256_bit5 -X256_bit6 -X256_bit7 -X256_bit8 -X256_bit9 -X256_bit10 -X256_bit11 -X256_bit12 -X257_bit_7 -X257_bit_6 -X257_bit_5 -X257_bit_4 -X257_bit_3 -X257_bit_2 -X257_bit_1 -X257_bit0 -X257_bit1 -X257_bit2 -X257_bit3 -X257_bit4 -X257_bit5 -X257_bit6 -X257_bit7 -X257_bit8 -X257_bit9 -X257_bit10 -X257_bit11 -X257_bit12 X258_bit_7 X258_bit_6 X258_bit_5 X258_bit_4 X258_bit_3 X258_bit_2 -X258_bit_1 -X258_bit0 -X258_bit1 -X258_bit2 -X258_bit3 -X258_bit4 -X258_bit5 -X258_bit6 -X258_bit7 -X258_bit8 -X258_bit9 -X258_bit10 -X258_bit11 -X258_bit12 -X259_bit_7 X259_bit_6 -X259_bit_5 X259_bit_4 -X259_bit_3 X259_bit_2 -X259_bit_1 -X259_bit0 -X259_bit1 -X259_bit2 -X259_bit3 -X259_bit4 -X259_bit5 -X259_bit6 -X259_bit7 -X259_bit8 -X259_bit9 -X259_bit10 -X259_bit11 -X259_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 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.92 2/55 28372
Raw data (stat): 28372 (runsolver) R 28371 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544620365 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.92 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4529 0 0 0 986 12 0 0 25 0 1 0 544620365 20930560 4356 4294967295 134512640 134672761 3221224544 3221223716 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5110 4356 603 41 0 5069 0
vsize: 20440
[startup+20.0016 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4592 0 0 0 1986 12 0 0 25 0 1 0 544620365 21200896 4419 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4419 603 41 0 5135 0
vsize: 20704
[startup+30.0022 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4633 0 0 0 2985 13 0 0 25 0 1 0 544620365 21336064 4460 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5209 4460 603 41 0 5168 0
vsize: 20836
[startup+40.0025 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4666 0 0 0 3985 13 0 0 25 0 1 0 544620365 21549056 4493 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5261 4493 603 41 0 5220 0
vsize: 21044
[startup+50.0034 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4694 0 0 0 4984 14 0 0 25 0 1 0 544620365 21684224 4521 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5294 4521 603 41 0 5253 0
vsize: 21176
[startup+60.0039 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4724 0 0 0 5984 14 0 0 25 0 1 0 544620365 21684224 4551 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5294 4551 603 41 0 5253 0
vsize: 21176
[startup+70.0053 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4774 0 0 0 6984 15 0 0 25 0 1 0 544620365 21954560 4601 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5360 4601 603 41 0 5319 0
vsize: 21440
[startup+80.0061 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4813 0 0 0 7984 15 0 0 25 0 1 0 544620365 22089728 4640 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5393 4640 603 41 0 5352 0
vsize: 21572
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4881 0 0 0 8983 16 0 0 25 0 1 0 544620365 22487040 4708 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5490 4708 603 41 0 5449 0
vsize: 21960
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 4973 0 0 0 9983 16 0 0 25 0 1 0 544620365 22892544 4800 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5589 4800 603 41 0 5548 0
vsize: 22356
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5049 0 0 0 10983 17 0 0 25 0 1 0 544620365 23162880 4876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5655 4876 603 41 0 5614 0
vsize: 22620
[startup+120.009 s]
Raw data (loadavg): 1.06 0.99 0.93 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5357 0 0 0 11982 18 0 0 25 0 1 0 544620365 24367104 5184 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5949 5184 603 41 0 5908 0
vsize: 23796
[startup+130.01 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5421 0 0 0 12981 19 0 0 25 0 1 0 544620365 24637440 5248 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6015 5248 603 41 0 5974 0
vsize: 24060
[startup+140.009 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5470 0 0 0 13981 19 0 0 25 0 1 0 544620365 24772608 5297 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6048 5297 603 41 0 6007 0
vsize: 24192
[startup+150.01 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 28372
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5572 0 0 0 14981 19 0 0 25 0 1 0 544620365 25174016 5399 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6146 5399 603 41 0 6105 0
vsize: 24584
[startup+160.01 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5654 0 0 0 15981 19 0 0 25 0 1 0 544620365 25579520 5481 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5481 603 41 0 6204 0
vsize: 24980
[startup+170.011 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5763 0 0 0 16981 19 0 0 25 0 1 0 544620365 26247168 5590 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6408 5590 603 41 0 6367 0
vsize: 25632
[startup+180.011 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5888 0 0 0 17981 20 0 0 25 0 1 0 544620365 26648576 5715 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6506 5715 603 41 0 6465 0
vsize: 26024
[startup+190.011 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 5996 0 0 0 18981 20 0 0 25 0 1 0 544620365 27185152 5823 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6637 5823 603 41 0 6596 0
vsize: 26548
[startup+200.012 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 6161 0 0 0 19981 20 0 0 25 0 1 0 544620365 27725824 5988 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6769 5988 603 41 0 6728 0
vsize: 27076
[startup+210.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 6928 0 0 0 20979 22 0 0 25 0 1 0 544620365 30957568 6755 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7558 6755 603 41 0 7517 0
vsize: 30232
[startup+220.013 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 7382 0 0 0 21978 23 0 0 25 0 1 0 544620365 32710656 7209 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7986 7209 603 41 0 7945 0
vsize: 31944
[startup+230.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 7523 0 0 0 22978 24 0 0 25 0 1 0 544620365 33247232 7350 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8117 7350 603 41 0 8076 0
vsize: 32468
[startup+240.012 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 7704 0 0 0 23977 25 0 0 25 0 1 0 544620365 34058240 7531 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8315 7531 603 41 0 8274 0
vsize: 33260
[startup+250.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14083 0 0 0 24963 39 0 0 25 0 1 0 544620365 55877632 12708 4294967295 134512640 134672761 3221224544 3221223484 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12708 603 41 0 13601 0
vsize: 54568
[startup+260.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14088 0 0 0 25963 39 0 0 25 0 1 0 544620365 55877632 12713 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12713 603 41 0 13601 0
vsize: 54568
[startup+270.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14092 0 0 0 26964 39 0 0 25 0 1 0 544620365 55877632 12717 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12717 603 41 0 13601 0
vsize: 54568
[startup+280.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14092 0 0 0 27964 39 0 0 25 0 1 0 544620365 55877632 12717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12717 603 41 0 13601 0
vsize: 54568
[startup+290.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14092 0 0 0 28964 39 0 0 25 0 1 0 544620365 55877632 12717 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12717 603 41 0 13601 0
vsize: 54568
[startup+300.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14092 0 0 0 29964 39 0 0 25 0 1 0 544620365 55877632 12717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12717 603 41 0 13601 0
vsize: 54568
[startup+310.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14093 0 0 0 30964 39 0 0 25 0 1 0 544620365 55877632 12718 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12718 603 41 0 13601 0
vsize: 54568
[startup+320.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14093 0 0 0 31964 39 0 0 25 0 1 0 544620365 55877632 12718 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12718 603 41 0 13601 0
vsize: 54568
[startup+330.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14093 0 0 0 32965 39 0 0 25 0 1 0 544620365 55877632 12718 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12718 603 41 0 13601 0
vsize: 54568
[startup+340.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14094 0 0 0 33965 39 0 0 25 0 1 0 544620365 55877632 12719 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12719 603 41 0 13601 0
vsize: 54568
[startup+350.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14094 0 0 0 34965 39 0 0 25 0 1 0 544620365 55877632 12719 4294967295 134512640 134672761 3221224544 3221223680 134560720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12719 603 41 0 13601 0
vsize: 54568
[startup+360.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14094 0 0 0 35965 39 0 0 25 0 1 0 544620365 55877632 12719 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12719 603 41 0 13601 0
vsize: 54568
[startup+370.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14094 0 0 0 36965 39 0 0 25 0 1 0 544620365 55877632 12719 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12719 603 41 0 13601 0
vsize: 54568
[startup+380.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14094 0 0 0 37965 39 0 0 25 0 1 0 544620365 55877632 12719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13642 12719 603 41 0 13601 0
vsize: 54568
[startup+390.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14359 0 0 0 38964 40 0 0 25 0 1 0 544620365 56958976 12984 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13906 12984 603 41 0 13865 0
vsize: 55624
[startup+400.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14415 0 0 0 39965 40 0 0 25 0 1 0 544620365 57229312 13040 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13972 13040 603 41 0 13931 0
vsize: 55888
[startup+410.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 40964 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+420.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 41964 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+430.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 42964 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+440.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 43964 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+450.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28374
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 44964 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+460.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 45965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+470.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 46965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+480.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 47965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+490.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 48965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+500.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 49965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+510.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 50965 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+520.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 14788 0 0 0 51966 41 0 0 25 0 1 0 544620365 58433536 13342 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13342 603 41 0 14225 0
vsize: 57064
[startup+530.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 15328 0 0 0 52965 43 0 0 25 0 1 0 544620365 60592128 13882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14793 13882 603 41 0 14752 0
vsize: 59172
[startup+540.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 16309 0 0 0 53962 45 0 0 25 0 1 0 544620365 64630784 14863 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15779 14863 603 41 0 15738 0
vsize: 63116
[startup+550.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 16566 0 0 0 54962 45 0 0 25 0 1 0 544620365 65708032 15120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16042 15120 603 41 0 16001 0
vsize: 64168
[startup+560.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17205 0 0 0 55961 47 0 0 25 0 1 0 544620365 68255744 15759 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16664 15759 603 41 0 16623 0
vsize: 66656
[startup+570.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 56959 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+580.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 57960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+590.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 58960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+600.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 59960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+610.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 60960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+620.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 61960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+630.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 62960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+640.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 63961 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+650.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 64961 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+660.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 65960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+670.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 66960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+680.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 67960 49 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+690.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 68961 50 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+700.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 69961 50 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+710.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 70961 50 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+720.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 71961 50 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+730.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 17770 0 0 0 72961 50 0 0 25 0 1 0 544620365 70045696 16198 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17101 16198 603 41 0 17060 0
vsize: 68404
[startup+740.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 73960 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223808 134562166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+750.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28376
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 74960 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+760.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 75960 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+770.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 76961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+780.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 77961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+790.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 78961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223680 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+800.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 79961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+810.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 80961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223680 134560632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+820.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 81961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+830.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 82961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+840.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 83961 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+850.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 84962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 85962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+870.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 86962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+880.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 87962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+890.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 88962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+900.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 89962 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+910.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18024 0 0 0 90963 51 0 0 25 0 1 0 544620365 70889472 16385 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16385 603 41 0 17266 0
vsize: 69228
[startup+920.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 91963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223760 134561982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+930.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 92963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+940.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 93963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+950.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 94963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+960.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 95963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+970.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 96963 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+980.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 97964 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+990.034 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 98964 51 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 99964 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 100964 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 101964 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 102964 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223728 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 103964 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28378
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 104965 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18028 0 0 0 105965 52 0 0 25 0 1 0 544620365 70889472 16389 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17307 16389 603 41 0 17266 0
vsize: 69228
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18537 0 0 0 106963 54 0 0 25 0 1 0 544620365 72908800 16898 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17800 16898 603 41 0 17759 0
vsize: 71200
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18616 0 0 0 107963 54 0 0 25 0 1 0 544620365 73310208 16977 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17898 16977 603 41 0 17857 0
vsize: 71592
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18706 0 0 0 108963 54 0 0 25 0 1 0 544620365 73715712 17067 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17997 17067 603 41 0 17956 0
vsize: 71988
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18800 0 0 0 109962 55 0 0 25 0 1 0 544620365 73986048 17161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18063 17161 603 41 0 18022 0
vsize: 72252
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 18917 0 0 0 110962 55 0 0 25 0 1 0 544620365 74522624 17278 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18194 17278 603 41 0 18153 0
vsize: 72776
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 19356 0 0 0 111961 56 0 0 25 0 1 0 544620365 76386304 17717 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18649 17717 603 41 0 18608 0
vsize: 74596
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 19642 0 0 0 112961 57 0 0 25 0 1 0 544620365 77459456 18003 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18911 18003 603 41 0 18870 0
vsize: 75644
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 20250 0 0 0 113960 58 0 0 25 0 1 0 544620365 80015360 18611 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19535 18611 603 41 0 19494 0
vsize: 78140
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 20804 0 0 0 114959 60 0 0 25 0 1 0 544620365 82165760 19165 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20060 19165 603 41 0 20019 0
vsize: 80240
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 21580 0 0 0 115957 62 0 0 25 0 1 0 544620365 85917696 19941 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20976 19941 603 41 0 20935 0
vsize: 83904
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 22176 0 0 0 116955 64 0 0 25 0 1 0 544620365 88338432 20537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21567 20537 603 41 0 21526 0
vsize: 86268
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 22651 0 0 0 117953 65 0 0 25 0 1 0 544620365 90255360 21012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22035 21012 603 41 0 21994 0
vsize: 88140
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 23160 0 0 0 118952 67 0 0 25 0 1 0 544620365 92413952 21521 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22562 21521 603 41 0 22521 0
vsize: 90248
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 28380
Raw data (stat): 28372 (minisat+) R 28371 20024 20023 0 -1 0 23626 0 0 0 119950 69 0 0 25 0 1 0 544620365 94351360 21987 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23035 21987 603 41 0 22994 0
vsize: 92140
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.93 1/55 28380
Raw data (stat): 28372 (minisat+) Z 28371 20024 20023 0 -1 12 23629 0 0 0 119951 73 0 0 25 0 1 0 544620365 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.25
CPU user time (s): 1199.52
CPU system time (s): 0.735888
CPU usage (%): 100.013
Max. virtual memory (Kb): 92140
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####