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-ran17x17.opb
MD5SUM	4afffa77a031423497a8b9b377dd0292
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	689314
Optimality of the best value was proved	NO
Number of terms in the objective function	6069
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	1576985250
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	1576985250
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	6069
Total number of constraints	323
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	323
Minimum length of a constraint	21
Maximum length of a constraint	340
Trace number 14778

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 01:15:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19331 boxname=wulflinc28 idbench=1487 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4afffa77a031423497a8b9b377dd0292  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-ran17x17.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-ran17x17.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-ran17x17.opb
IDLAUNCH: 19331
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        295992 kB
Buffers:         34048 kB
Cached:         670676 kB
SwapCached:        164 kB
Active:         343620 kB
Inactive:       363512 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        295740 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6088 kB
Slab:            25828 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:35:32 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 19331 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 357 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 355]---> Adder-cost: 338   maxlim: 28143   bits: 15/15
c ---[ 353]---> Adder-cost: 310   maxlim: 15599   bits: 14/14
c ---[ 351]---> Adder-cost: 338   maxlim: 27887   bits: 15/15
c ---[ 349]---> Adder-cost: 338   maxlim: 28399   bits: 15/15
c ---[ 347]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 345]---> Adder-cost: 338   maxlim: 28527   bits: 15/15
c ---[ 343]---> Adder-cost: 338   maxlim: 28655   bits: 15/15
c ---[ 341]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 339]---> Adder-cost: 362   maxlim: 53871   bits: 16/16
c ---[ 337]---> Adder-cost: 360   maxlim: 47215   bits: 16/16
c ---[ 335]---> Adder-cost: 360   maxlim: 46959   bits: 16/16
c ---[ 333]---> Adder-cost: 338   maxlim: 27759   bits: 15/15
c ---[ 331]---> Adder-cost: 362   maxlim: 54255   bits: 16/16
c ---[ 329]---> Adder-cost: 360   maxlim: 46703   bits: 16/16
c ---[ 327]---> Adder-cost: 360   maxlim: 47727   bits: 16/16
c ---[ 325]---> Adder-cost: 310   maxlim: 15727   bits: 14/14
c ---[ 323]---> Adder-cost: 310   maxlim: 15855   bits: 14/14
c ---[ 321]---> Adder-cost: 358   maxlim: 45935   bits: 16/16
c ---[ 319]---> Adder-cost: 320   maxlim: 16623   bits: 15/15
c ---[ 317]---> Adder-cost: 342   maxlim: 30703   bits: 15/15
c ---[ 315]---> Adder-cost: 320   maxlim: 16879   bits: 15/15
c ---[ 313]---> Adder-cost: 342   maxlim: 29807   bits: 15/15
c ---[ 311]---> Adder-cost: 358   maxlim: 46063   bits: 16/16
c ---[ 309]---> Adder-cost: 342   maxlim: 30191   bits: 15/15
c ---[ 307]---> Adder-cost: 362   maxlim: 52079   bits: 16/16
c ---[ 305]---> Adder-cost: 358   maxlim: 45679   bits: 16/16
c ---[ 303]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 301]---> Adder-cost: 358   maxlim: 45551   bits: 16/16
c ---[ 299]---> Adder-cost: 358   maxlim: 44783   bits: 16/16
c ---[ 297]---> Adder-cost: 358   maxlim: 45167   bits: 16/16
c ---[ 295]---> Adder-cost: 362   maxlim: 51695   bits: 16/16
c ---[ 293]---> Adder-cost: 358   maxlim: 44271   bits: 16/16
c ---[ 291]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 289]---> Adder-cost: 358   maxlim: 44399   bits: 16/16
c ---[ 288]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   12
c ---[ 286]---> BDD-cost:   12
c ---[ 285]---> BDD-cost:   14
c ---[ 284]---> BDD-cost:   17
c ---[ 283]---> BDD-cost:   17
c ---[ 282]---> BDD-cost:   12
c ---[ 281]---> BDD-cost:   11
c ---[ 280]---> BDD-cost:   15
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   17
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   11
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   12
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   15
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   17
c ---[ 266]---> BDD-cost:   17
c ---[ 265]---> BDD-cost:   17
c ---[ 264]---> BDD-cost:   13
c ---[ 263]---> BDD-cost:   12
c ---[ 262]---> BDD-cost:   11
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:   17
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   17
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   11
c ---[ 255]---> BDD-cost:   17
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   13
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   14
c ---[ 207]---> BDD-cost:   12
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   14
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   14
c ---[ 201]---> BDD-cost:   14
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   14
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   14
c ---[ 190]---> BDD-cost:   14
c ---[ 189]---> BDD-cost:   12
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   14
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   14
c ---[ 179]---> BDD-cost:   12
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   14
c ---[ 170]---> BDD-cost:   17
c ---[ 169]---> BDD-cost:   12
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   17
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   15
c ---[ 153]---> BDD-cost:   12
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   15
c ---[ 147]---> BDD-cost:   15
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   15
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   15
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   12
c ---[ 131]---> BDD-cost:   12
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   12
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   12
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   15
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   12
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   12
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   12
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   15
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   17
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   85510   298438 |   28503       0        0     nan |  0.000 % |
c |       100 |   85496   298392 |   31353      98      307     3.1 | 20.432 % |
c |       250 |   85377   297979 |   34488     233      746     3.2 | 20.534 % |
c |       475 |   85240   297520 |   37937     443     1413     3.2 | 20.662 % |
c |       812 |   85079   296965 |   41731     760     2455     3.2 | 20.800 % |
c |      1318 |   84701   295689 |   45904    1216     3947     3.2 | 21.132 % |
c |      2077 |   84227   294073 |   50494    1916     6313     3.3 | 21.545 % |
c |      3216 |   83683   292199 |   55544    2980    10020     3.4 | 22.036 % |
c |      4924 |   83220   290614 |   61098    4637    16942     3.7 | 22.454 % |
c |      7486 |   82992   289820 |   67208    7167    28863     4.0 | 22.653 % |
c |     11330 |   82934   289628 |   73929   11004    58606     5.3 | 22.710 % |
c |     17097 |   82904   289530 |   81322   16766   450934    26.9 | 22.735 % |
c |     25747 |   82821   289259 |   89454   25403   769489    30.3 | 22.807 % |
c |     38721 |   82785   289133 |   98400   38372  1267693    33.0 | 22.837 % |
c |     58182 |   82785   289133 |  108240   57833  2249090    38.9 | 22.837 % |
c |     87375 |   82232   287246 |  119064   86949  2764292    31.8 | 23.363 % |
c |    131165 |   82198   287128 |  130970   18604  3561631   191.4 | 23.394 % |
c |    196851 |   80860   282668 |  144067   84081  4752368    56.5 | 24.666 % |
c |    295377 |   80824   282550 |  158474   52045  1166857    22.4 | 24.701 % |
c ==============================================================================
c [1mFound solution: 1764853[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11288   maxlim: 3702957   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    314452 |  159768   564520 |   53256   71120  1451951    20.4 | 24.701 % |
c |    314552 |  159768   564520 |   58581   22332   202641     9.1 | 15.694 % |
c |    314702 |  159768   564520 |   64439   22482   203358     9.0 | 15.694 % |
c |    314928 |  159768   564520 |   70883   22708   204407     9.0 | 15.694 % |
c |    315265 |  159768   564520 |   77972   23045   205927     8.9 | 15.694 % |
c |    315771 |  159768   564520 |   85769   23551   208346     8.8 | 15.694 % |
c |    316530 |  159768   564520 |   94346   24310   212236     8.7 | 15.694 % |
c |    317669 |  159768   564520 |  103780   25449   218139     8.6 | 15.694 % |
c |    319377 |  159768   564520 |  114158   27157   230827     8.5 | 15.694 % |
c |    321939 |  159768   564520 |  125574   29719   256436     8.6 | 15.694 % |
c |    325784 |  159768   564520 |  138132   33564   298630     8.9 | 15.694 % |
c |    331550 |  159759   564491 |  151945   39329   376057     9.6 | 15.700 % |
c |    340199 |  159759   564491 |  167140   47978   496371    10.3 | 15.700 % |
c |    353173 |  159750   564462 |  183854   60951   664271    10.9 | 15.707 % |
c |    372635 |  159741   564433 |  202239   80412   952185    11.8 | 15.713 % |
c |    401829 |  159695   564279 |  222463  109599  3622291    33.1 | 15.743 % |
c ==============================================================================
c [1mFound solution: 1656627[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3811183   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    413863 |  159673   564297 |   53224  121629  3796626    31.2 | 15.743 % |
c |    413963 |  159673   564297 |   58546   30539   333811    10.9 | 15.781 % |
c |    414114 |  159673   564297 |   64401   30690   334595    10.9 | 15.781 % |
c |    414339 |  159673   564297 |   70841   30915   335577    10.9 | 15.781 % |
c |    414676 |  159673   564297 |   77925   31252   337422    10.8 | 15.781 % |
c |    415182 |  159673   564297 |   85717   31758   340722    10.7 | 15.781 % |
c |    415941 |  159673   564297 |   94289   32517   345183    10.6 | 15.781 % |
c |    417080 |  159655   564237 |  103718   33654   353849    10.5 | 15.790 % |
c |    418788 |  159655   564237 |  114090   35362   371150    10.5 | 15.790 % |
c |    421350 |  159649   564217 |  125499   37923   397669    10.5 | 15.794 % |
c |    425194 |  159640   564188 |  138049   41766   442157    10.6 | 15.800 % |
c |    430962 |  159617   564109 |  151854   47530   633546    13.3 | 15.813 % |
c |    439611 |  159617   564109 |  167039   56179   774491    13.8 | 15.813 % |
c |    452585 |  159579   563988 |  183743   69142  1424018    20.6 | 15.836 % |
c |    472050 |  159579   563988 |  202118   88607  2775632    31.3 | 15.836 % |
c ==============================================================================
c [1mFound solution: 1635345[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3832465   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    478515 |  159587   564109 |   53195   95072  2943085    31.0 | 15.836 % |
c |    478616 |  159587   564109 |   58514   24939   848037    34.0 | 15.857 % |
c |    478766 |  159587   564109 |   64365   25089   848710    33.8 | 15.857 % |
c |    478992 |  159587   564109 |   70802   25315   849730    33.6 | 15.857 % |
c |    479329 |  159587   564109 |   77882   25652   851493    33.2 | 15.857 % |
c |    479835 |  159587   564109 |   85671   26158   853982    32.6 | 15.857 % |
c |    480594 |  159587   564109 |   94238   26917   857577    31.9 | 15.857 % |
c |    481733 |  159580   564086 |  103662   28053   863537    30.8 | 15.861 % |
c |    483441 |  159580   564086 |  114028   29761   873950    29.4 | 15.861 % |
c |    486004 |  159580   564086 |  125431   32324   898161    27.8 | 15.861 % |
c |    489848 |  159571   564057 |  137974   36167   939684    26.0 | 15.867 % |
c |    495616 |  159571   564057 |  151771   41935  1022715    24.4 | 15.867 % |
c |    504265 |  159571   564057 |  166948   50584  1242808    24.6 | 15.867 % |
c |    517240 |  159571   564057 |  183643   63559  1727962    27.2 | 15.867 % |
c |    536702 |  159571   564057 |  202007   83021  2874524    34.6 | 15.867 % |
c |    565894 |  159571   564057 |  222208  112213  3790490    33.8 | 15.867 % |
c |    609683 |  159571   564057 |  244429  156002  5468108    35.1 | 15.867 % |
c |    675367 |  159562   564026 |  268872  221684 19638533    88.6 | 15.870 % |
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 -X260_bit_7 -X260_bit_6 -X260_bit_5 -X260_bit_4 X260_bit_3 -X260_bit_2 -X260_bit_1 -X260_bit0 -X260_bit1 -X260_bit2 -X260_bit3 -X260_bit4 -X260_bit5 -X260_bit6 -X260_bit7 -X260_bit8 -X260_bit9 -X260_bit10 -X260_bit11 -X260_bit12 X261_bit_7 -X261_bit_6 -X261_bit_5 -X261_bit_4 X261_bit_3 -X261_bit_2 X261_bit_1 -X261_bit0 X261_bit1 -X261_bit2 -X261_bit3 -X261_bit4 -X261_bit5 -X261_bit6 -X261_bit7 -X261_bit8 -X261_bit9 -X261_bit10 -X261_bit11 -X261_bit12 -X262_bit_7 X262_bit_6 -X262_bit_5 X262_bit_4 X262_bit_3 -X262_bit_2 X262_bit_1 -X262_bit0 X262_bit1 X262_bit2 -X262_bit3 -X262_bit4 -X262_bit5 -X262_bit6 -X262_bit7 -X262_bit8 -X262_bit9 -X262_bit10 -X262_bit11 -X262_bit12 -X263_bit_7 -X263_bit_6 -X263_bit_5 -X263_bit_4 -X263_bit_3 -X263_bit_2 -X263_bit_1 -X263_bit0 -X263_bit1 -X263_bit2 -X263_bit3 -X263_bit4 -X263_bit5 -X263_bit6 -X263_bit7 -X263_bit8 -X263_bit9 -X263_bit10 -X263_bit11 -X263_bit12 -X264_bit_7 -X264_bit_6 -X264_bit_5 -X264_bit_4 -X264_bit_3 -X264_bit_2 -X264_bit_1 -X264_bit0 -X264_bit1 -X264_bit2 -X264_bit3 -X264_bit4 -X264_bit5 -X264_bit6 -X264_bit7 -X264_bit8 -X264_bit9 -X264_bit10 -X264_bit11 -X264_bit12 -X265_bit_7 X265_bit_6 -X265_bit_5 -X265_bit_4 -X265_bit_3 -X265_bit_2 X265_bit_1 -X265_bit0 -X265_bit1 -X265_bit2 -X265_bit3 -X265_bit4 -X265_bit5 -X265_bit6 -X265_bit7 -X265_bit8 -X265_bit9 -X265_bit10 -X265_bit11 -X265_bit12 -X266_bit_7 -X266_bit_6 -X266_bit_5 -X266_bit_4 -X266_bit_3 -X266_bit_2 X266_bit_1 -X266_bit0 -X266_bit1 -X266_bit2 -X266_bit3 -X266_bit4 -X266_bit5 -X266_bit6 -X266_bit7 -X266_bit8 -X266_bit9 -X266_bit10 -X266_bit11 -X266_bit12 X267_bit_7 X267_bit_6 -X267_bit_5 X267_bit_4 -X267_bit_3 -X267_bit_2 -X267_bit_1 X267_bit0 -X267_bit1 -X267_bit2 -X267_bit3 -X267_bit4 -X267_bit5 -X267_bit6 -X267_bit7 -X267_bit8 -X267_bit9 -X267_bit10 -X267_bit11 -X267_bit12 -X268_bit_7 -X268_bit_6 -X268_bit_5 -X268_bit_4 -X268_bit_3 -X268_bit_2 -X268_bit_1 -X268_bit0 -X268_bit1 X268_bit2 -X268_bit3 -X268_bit4 -X268_bit5 -X268_bit6 -X268_bit7 -X268_bit8 -X268_bit9 -X268_bit10 -X268_bit11 -X268_bit12 X269_bit_7 X269_bit_6 -X269_bit_5 -X269_bit_4 -X269_bit_3 -X269_bit_2 X269_bit_1 -X269_bit0 -X269_bit1 -X269_bit2 -X269_bit3 -X269_bit4 -X269_bit5 -X269_bit6 -X269_bit7 -X269_bit8 -X269_bit9 -X269_bit10 -X269_bit11 -X269_bit12 -X270_bit_7 -X270_bit_6 -X270_bit_5 -X270_bit_4 -X270_bit_3 X270_bit_2 X270_bit_1 -X270_bit0 X270_bit1 X270_bit2 -X270_bit3 -X270_bit4 -X270_bit5 -X270_bit6 -X270_bit7 -X270_bit8 -X270_bit9 -X270_bit10 -X270_bit11 -X270_bit12 X271_bit_7 X271_bit_6 X271_bit_5 -X271_bit_4 X271_bit_3 -X271_bit_2 X271_bit_1 -X271_bit0 X271_bit1 -X271_bit2 -X271_bit3 -X271_bit4 -X271_bit5 -X271_bit6 -X271_bit7 -X271_bit8 -X271_bit9 -X271_bit10 -X271_bit11 -X271_bit12 -X272_bit_7 -X272_bit_6 X272_bit_5 X272_bit_4 X272_bit_3 -X272_bit_2 -X272_bit_1 X272_bit0 X272_bit1 -X272_bit2 -X272_bit3 -X272_bit4 -X272_bit5 -X272_bit6 -X272_bit7 -X272_bit8 -X272_bit9 -X272_bit10 -X272_bit11 -X272_bit12 -X273_bit_7 -X273_bit_6 -X273_bit_5 -X273_bit_4 -X273_bit_3 -X273_bit_2 -X273_bit_1 -X273_bit0 -X273_bit1 -X273_bit2 -X273_bit3 -X273_bit4 -X273_bit5 -X273_bit6 -X273_bit7 -X273_bit8 -X273_bit9 -X273_bit10 -X273_bit11 -X273_bit12 -X274_bit_7 -X274_bit_6 X274_bit_5 -X274_bit_4 -X274_bit_3 -X274_bit_2 -X274_bit_1 -X274_bit0 -X274_bit1 -X274_bit2 -X274_bit3 -X274_bit4 -X274_bit5 -X274_bit6 -X274_bit7 -X274_bit8 -X274_bit9 -X274_bit10 -X274_bit11 -X274_bit12 -X275_bit_7 -X275_bit_6 -X275_bit_5 -X275_bit_4 -X275_bit_3 -X275_bit_2 -X275_bit_1 -X275_bit0 -X275_bit1 -X275_bit2 -X275_bit3 -X275_bit4 -X275_bit5 -X275_bit6 -X275_bit7 -X275_bit8 -X275_bit9 -X275_bit10 -X275_bit11 -X275_bit12 -X276_bit_7 X276_bit_6 -X276_bit_5 -X276_bit_4 -X276_bit_3 -X276_bit_2 -X276_bit_1 X276_bit0 -X276_bit1 -X276_bit2 -X276_bit3 -X276_bit4 -X276_bit5 -X276_bit6 -X276_bit7 -X276_bit8 -X276_bit9 -X276_bit10 -X276_bit11 -X276_bit12 -X277_bit_7 X277_bit_6 -X277_bit_5 -X277_bit_4 X277_bit_3 X277_bit_2 X277_bit_1 -X277_bit0 -X277_bit1 -X277_bit2 X277_bit3 -X277_bit4 -X277_bit5 -X277_bit6 -X277_bit7 -X277_bit8 -X277_bit9 -X277_bit10 -X277_bit11 -X277_bit12 -X278_bit_7 -X278_bit_6 -X278_bit_5 X278_bit_4 -X278_bit_3 -X278_bit_2 -X278_bit_1 -X278_bit0 -X278_bit1 -X278_bit2 X278_bit3 -X278_bit4 -X278_bit5 -X278_bit6 -X278_bit7 -X278_bit8 -X278_bit9 -X278_bit10 -X278_bit11 -X278_bit12 -X279_bit_7 -X279_bit_6 -X279_bit_5 X279_bit_4 -X279_bit_3 -X279_bit_2 -X279_bit_1 -X279_bit0 -X279_bit1 -X279_bit2 -X279_bit3 -X279_bit4 -X279_bit5 -X279_bit6 -X279_bit7 -X279_bit8 -X279_bit9 -X279_bit10 -X279_bit11 -X279_bit12 -X280_bit_7 -X280_bit_6 X280_bit_5 -X280_bit_4 -X280_bit_3 X280_bit_2 -X280_bit_1 -X280_bit0 -X280_bit1 -X280_bit2 -X280_bit3 -X280_bit4 -X280_bit5 -X280_bit6 -X280_bit7 -X280_bit8 -X280_bit9 -X280_bit10 -X280_bit11 -X280_bit12 -X281_bit_7 -X281_bit_6 -X281_bit_5 -X281_bit_4 -X281_bit_3 -X281_bit_2 X281_bit_1 X281_bit0 -X281_bit1 -X281_bit2 -X281_bit3 -X281_bit4 -X281_bit5 -X281_bit6 -X281_bit7 -X281_bit8 -X281_bit9 -X281_bit10 -X281_bit11 -X281_bit12 -X282_bit_7 -X282_bit_6 X282_bit_5 X282_bit_4 -X282_bit_3 -X282_bit_2 X282_bit_1 -X282_bit0 -X282_bit1 -X282_bit2 -X282_bit3 -X282_bit4 -X282_bit5 -X282_bit6 -X282_bit7 -X282_bit8 -X282_bit9 -X282_bit10 -X282_bit11 -X282_bit12 -X283_bit_7 X283_bit_6 -X283_bit_5 -X283_bit_4 -X283_bit_3 X283_bit_2 X283_bit_1 -X283_bit0 -X283_bit1 -X283_bit2 -X283_bit3 -X283_bit4 -X283_bit5 -X283_bit6 -X283_bit7 -X283_bit8 -X283_bit9 -X283_bit10 -X283_bit11 -X283_bit12 -X284_bit_7 X284_bit_6 -X284_bit_5 X284_bit_4 -X284_bit_3 X284_bit_2 -X284_bit_1 -X284_bit0 -X284_bit1 -X284_bit2 -X284_bit3 -X284_bit4 -X284_bit5 -X284_bit6 -X284_bit7 -X284_bit8 -X284_bit9 -X284_bit10 -X284_bit11 -X284_bit12 -X285_bit_7 -X285_bit_6 X285_bit_5 -X285_bit_4 -X285_bit_3 X285_bit_2 -X285_bit_1 -X285_bit0 -X285_bit1 X285_bit2 -X285_bit3 -X285_bit4 -X285_bit5 -X285_bit6 -X285_bit7 -X285_bit8 -X285_bit9 -X285_bit10 -X285_bit11 -X285_bit12 -X286_bit_7 -X286_bit_6 -X286_bit_5 -X286_bit_4 -X286_bit_3 -X286_bit_2 -X286_bit_1 -X286_bit0 -X286_bit1 -X286_bit2 -X286_bit3 -X286_bit4 -X286_bit5 -X286_bit6 -X286_bit7 -X286_bit8 -X286_bit9 -X286_bit10 -X286_bit11 -X286_bit12 -X287_bit_7 -X287_bit_6 X287_bit_5 X287_bit_4 -X287_bit_3 -X287_bit_2 -X287_bit_1 X287_bit0 -X287_bit1 X287_bit2 -X287_bit3 -X287_bit4 -X287_bit5 -X287_bit6 -X287_bit7 -X287_bit8 -X287_bit9 -X287_bit10 -X287_bit11 -X287_bit12 -X288_bit_7 -X288_bit_6 -X288_bit_5 -X288_bit_4 X288_bit_3 X288_bit_2 X288_bit_1 -X288_bit0 -X288_bit1 -X288_bit2 -X288_bit3 -X288_bit4 -X288_bit5 -X288_bit6 -X288_bit7 -X288_bit8 -X288_bit9 -X288_bit10 -X288_bit11 -X288_bit12 Y0_bit0 Y1_bit0 Y2_bit0 Y3_bit0 Y4_bit0 Y5_bit0 -Y6_bit0 Y7_bit0 -Y8_bit0 Y9_bit0 Y10_bit0 -Y11_bit0 -Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 Y17_bit0 Y18_bit0 -Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 -Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 Y41_bit0 -Y42_bit0 Y43_bit0 -Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 Y51_bit0 -Y52_bit0 -Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 Y57_bit0 -Y58_bit0 Y59_bit0 Y60_bit0 -Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 -Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 Y70_bit0 -Y71_bit0 Y72_bit0 Y73_bit0 Y74_bit0 Y75_bit0 -Y76_bit0 Y77_bit0 Y78_bit0 -Y79_bit0 Y80_bit0 Y81_bit0 Y82_bit0 -Y83_bit0 Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 -Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 -Y108_bit0 Y109_bit0 Y110_bit0 Y111_bit0 Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 -Y118_bit0 Y119_bit0 Y120_bit0 Y121_bit0 Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 Y128_bit0 Y129_bit0 Y130_bit0 Y131_bit0 Y132_bit0 Y133_bit0 Y134_bit0 -Y135_bit0 -Y136_bit0 -Y137_bit0 -Y138_bit0 -Y139_bit0 Y140_bit0 -Y141_bit0 Y142_bit0 Y143_bit0 -Y144_bit0 Y145_bit0 Y146_bit0 Y147_bit0 -Y148_bit0 Y149_bit0 Y150_bit0 Y151_bit0 Y152_bit0 Y153_bit0 -Y154_bit0 Y155_bit0 Y156_bit0 -Y157_bit0 Y158_bit0 Y159_bit0 -Y160_bit0 Y161_bit0 Y162_bit0 Y163_bit0 -Y164_bit0 -Y165_bit0 -Y166_bit0 Y167_bit0 -Y168_bit0 Y169_bit0 -Y170_bit0 Y171_bit0 -Y172_bit0 -Y173_bit0 -Y174_bit0 Y175_bit0 Y176_bit0 Y177_bit0 Y178_bit0 Y179_bit0 Y180_bit0 Y181_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.78 0.92 0.91 2/54 13650
Raw data (stat): 13650 (runsolver) R 13649 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541047620 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.0007 s]
Raw data (loadavg): 0.81 0.92 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 2221 0 0 0 993 6 0 0 25 0 1 0 541047620 11313152 2140 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2762 2140 603 41 0 2721 0
vsize: 11048
[startup+20.0013 s]
Raw data (loadavg): 0.84 0.92 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 2244 0 0 0 1992 6 0 0 25 0 1 0 541047620 11448320 2163 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2795 2163 603 41 0 2754 0
vsize: 11180
[startup+30.0016 s]
Raw data (loadavg): 0.86 0.92 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 2284 0 0 0 2992 7 0 0 25 0 1 0 541047620 11595776 2203 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2203 603 41 0 2790 0
vsize: 11324
[startup+40.0015 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 3216 0 0 0 3989 10 0 0 25 0 1 0 541047620 15376384 3135 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3754 3135 603 41 0 3713 0
vsize: 15016
[startup+50.0024 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 4967 0 0 0 4985 14 0 0 25 0 1 0 541047620 22515712 4886 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5497 4886 603 41 0 5456 0
vsize: 21988
[startup+60.0026 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 5316 0 0 0 5983 16 0 0 25 0 1 0 541047620 23998464 5235 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5859 5235 603 41 0 5818 0
vsize: 23436
[startup+70.0036 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 5459 0 0 0 6983 16 0 0 25 0 1 0 541047620 24801280 5378 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6055 5378 603 41 0 6014 0
vsize: 24220
[startup+80.0044 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 5711 0 0 0 7982 17 0 0 25 0 1 0 541047620 25743360 5630 4294967295 134512640 134672761 3221224544 3221223612 1075346629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6285 5630 603 41 0 6244 0
vsize: 25140
[startup+90.0046 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 5871 0 0 0 8982 18 0 0 25 0 1 0 541047620 26415104 5790 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6449 5790 603 41 0 6408 0
vsize: 25796
[startup+100.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 6085 0 0 0 9981 19 0 0 25 0 1 0 541047620 27226112 6004 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6004 603 41 0 6606 0
vsize: 26588
[startup+110.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 7579 0 0 0 10976 23 0 0 25 0 1 0 541047620 33415168 7498 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8158 7498 603 41 0 8117 0
vsize: 32632
[startup+120.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 9458 0 0 0 11971 29 0 0 25 0 1 0 541047620 40984576 9377 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10006 9377 603 41 0 9965 0
vsize: 40024
[startup+130.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 10967 0 0 0 12968 33 0 0 25 0 1 0 541047620 47194112 10886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11522 10886 603 41 0 11481 0
vsize: 46088
[startup+140.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12256 0 0 0 13964 36 0 0 25 0 1 0 541047620 52449280 12175 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12805 12176 603 41 0 12764 0
vsize: 51220
[startup+150.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 14963 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 15963 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+170.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 16963 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 17964 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 18964 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 19964 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 20964 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+220.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 21964 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 22965 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+240.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 23965 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+250.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 24965 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 25965 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+270.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 26965 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+280.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 27966 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+290.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12984 0 0 0 28966 38 0 0 25 0 1 0 541047620 55496704 12903 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12903 603 41 0 13508 0
vsize: 54196
[startup+300.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12985 0 0 0 29965 38 0 0 25 0 1 0 541047620 55496704 12904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12904 603 41 0 13508 0
vsize: 54196
[startup+310.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12985 0 0 0 30965 38 0 0 25 0 1 0 541047620 55496704 12904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12904 603 41 0 13508 0
vsize: 54196
[startup+320.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12985 0 0 0 31966 38 0 0 25 0 1 0 541047620 55496704 12904 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12904 603 41 0 13508 0
vsize: 54196
[startup+330.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12985 0 0 0 32966 38 0 0 25 0 1 0 541047620 55496704 12904 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12904 603 41 0 13508 0
vsize: 54196
[startup+340.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12985 0 0 0 33966 38 0 0 25 0 1 0 541047620 55496704 12904 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12904 603 41 0 13508 0
vsize: 54196
[startup+350.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12986 0 0 0 34966 38 0 0 25 0 1 0 541047620 55496704 12905 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13549 12905 603 41 0 13508 0
vsize: 54196
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 12995 0 0 0 35966 38 0 0 25 0 1 0 541047620 56020992 12914 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13677 12914 603 41 0 13636 0
vsize: 54708
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13005 0 0 0 36966 38 0 0 25 0 1 0 541047620 56020992 12924 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13677 12924 603 41 0 13636 0
vsize: 54708
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 37967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 38967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 39967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 40967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 41967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 42967 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 13010 0 0 0 43966 38 0 0 25 0 1 0 541047620 55988224 12929 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13669 12929 603 41 0 13628 0
vsize: 54676
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16914 0 0 0 44957 47 0 0 25 0 1 0 541047620 67944448 15637 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15637 603 41 0 16547 0
vsize: 66352
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16917 0 0 0 45957 47 0 0 25 0 1 0 541047620 67944448 15640 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15640 603 41 0 16547 0
vsize: 66352
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16922 0 0 0 46957 47 0 0 25 0 1 0 541047620 67944448 15645 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15645 603 41 0 16547 0
vsize: 66352
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16923 0 0 0 47957 47 0 0 25 0 1 0 541047620 67944448 15646 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15646 603 41 0 16547 0
vsize: 66352
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16923 0 0 0 48957 47 0 0 25 0 1 0 541047620 67944448 15646 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15646 603 41 0 16547 0
vsize: 66352
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16923 0 0 0 49958 47 0 0 25 0 1 0 541047620 67944448 15646 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15646 603 41 0 16547 0
vsize: 66352
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16924 0 0 0 50958 47 0 0 25 0 1 0 541047620 67944448 15647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15647 603 41 0 16547 0
vsize: 66352
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16924 0 0 0 51958 47 0 0 25 0 1 0 541047620 67944448 15647 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15647 603 41 0 16547 0
vsize: 66352
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16924 0 0 0 52958 47 0 0 25 0 1 0 541047620 67944448 15647 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15647 603 41 0 16547 0
vsize: 66352
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16924 0 0 0 53958 47 0 0 25 0 1 0 541047620 67944448 15647 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15647 603 41 0 16547 0
vsize: 66352
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 54958 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 55959 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 56959 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 57959 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 58959 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 59959 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 60960 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 61960 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16925 0 0 0 62960 47 0 0 25 0 1 0 541047620 67944448 15648 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15648 603 41 0 16547 0
vsize: 66352
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 63960 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223648 134554625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 64960 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223500 1075350666 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 65960 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 66961 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 67961 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 68961 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 69961 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 70961 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 71962 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16959 0 0 0 72962 48 0 0 25 0 1 0 541047620 67944448 15682 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15682 603 41 0 16547 0
vsize: 66352
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 73962 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 74962 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 75962 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 76962 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 77963 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+790.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 78963 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 79963 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 80963 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 81963 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 82964 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 83964 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 84964 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 85964 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 86964 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 87965 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 88965 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223760 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 89965 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 90965 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 91965 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 16961 0 0 0 92966 48 0 0 25 0 1 0 541047620 67944448 15684 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16588 15684 603 41 0 16547 0
vsize: 66352
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 17582 0 0 0 93964 49 0 0 25 0 1 0 541047620 70504448 16305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17213 16305 603 41 0 17172 0
vsize: 68852
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 17923 0 0 0 94963 50 0 0 25 0 1 0 541047620 71847936 16646 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17541 16646 603 41 0 17500 0
vsize: 70164
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 19069 0 0 0 95960 54 0 0 25 0 1 0 541047620 76570624 17792 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18694 17792 603 41 0 18653 0
vsize: 74776
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 20021 0 0 0 96959 55 0 0 25 0 1 0 541047620 80355328 18744 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19618 18744 603 41 0 19577 0
vsize: 78472
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 20904 0 0 0 97957 58 0 0 25 0 1 0 541047620 83984384 19627 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20504 19627 603 41 0 20463 0
vsize: 82016
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 21662 0 0 0 98955 59 0 0 25 0 1 0 541047620 87089152 20385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21262 20385 603 41 0 21221 0
vsize: 85048
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 22328 0 0 0 99954 61 0 0 25 0 1 0 541047620 89804800 21051 4294967295 134512640 134672761 3221224544 3221223648 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21925 21051 603 41 0 21884 0
vsize: 87700
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 22974 0 0 0 100952 62 0 0 25 0 1 0 541047620 92487680 21697 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22580 21697 603 41 0 22539 0
vsize: 90320
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 23612 0 0 0 101951 64 0 0 25 0 1 0 541047620 95047680 22335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23205 22335 603 41 0 23164 0
vsize: 92820
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 24211 0 0 0 102950 65 0 0 25 0 1 0 541047620 97472512 22934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23797 22934 603 41 0 23756 0
vsize: 95188
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 24885 0 0 0 103948 67 0 0 25 0 1 0 541047620 100311040 23608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24490 23608 603 41 0 24449 0
vsize: 97960
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 25629 0 0 0 104946 70 0 0 25 0 1 0 541047620 103407616 24352 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25246 24352 603 41 0 25205 0
vsize: 100984
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 26236 0 0 0 105945 71 0 0 25 0 1 0 541047620 105832448 24959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25838 24959 603 41 0 25797 0
vsize: 103352
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 26884 0 0 0 106943 73 0 0 25 0 1 0 541047620 108527616 25607 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26496 25607 603 41 0 26455 0
vsize: 105984
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 27613 0 0 0 107941 75 0 0 25 0 1 0 541047620 111501312 26336 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27222 26336 603 41 0 27181 0
vsize: 108888
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 28278 0 0 0 108939 77 0 0 25 0 1 0 541047620 114204672 27001 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27882 27001 603 41 0 27841 0
vsize: 111528
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 28817 0 0 0 109938 78 0 0 25 0 1 0 541047620 116359168 27540 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28408 27540 603 41 0 28367 0
vsize: 113632
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 29269 0 0 0 110937 79 0 0 25 0 1 0 541047620 118247424 27992 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28869 27992 603 41 0 28828 0
vsize: 115476
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 29766 0 0 0 111936 80 0 0 25 0 1 0 541047620 120266752 28489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29362 28489 603 41 0 29321 0
vsize: 117448
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 30351 0 0 0 112935 82 0 0 25 0 1 0 541047620 122556416 29074 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29921 29074 603 41 0 29880 0
vsize: 119684
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 30769 0 0 0 113934 83 0 0 25 0 1 0 541047620 124309504 29492 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30349 29492 603 41 0 30308 0
vsize: 121396
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 31267 0 0 0 114933 85 0 0 25 0 1 0 541047620 126332928 29990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30843 29990 603 41 0 30802 0
vsize: 123372
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 31832 0 0 0 115932 85 0 0 25 0 1 0 541047620 128634880 30555 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31405 30555 603 41 0 31364 0
vsize: 125620
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 32145 0 0 0 116931 86 0 0 25 0 1 0 541047620 129986560 30868 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31735 30868 603 41 0 31694 0
vsize: 126940
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 32357 0 0 0 117930 87 0 0 25 0 1 0 541047620 130793472 31080 4294967295 134512640 134672761 3221224544 3221223712 134564767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31932 31080 603 41 0 31891 0
vsize: 127728
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 32596 0 0 0 118930 88 0 0 25 0 1 0 541047620 131739648 31319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32163 31319 603 41 0 32122 0
vsize: 128652
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 13650
Raw data (stat): 13650 (minisat+) R 13649 10614 10613 0 -1 0 32984 0 0 0 119928 89 0 0 25 0 1 0 541047620 133349376 31707 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32556 31707 603 41 0 32515 0
vsize: 130224
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 13650
Raw data (stat): 13650 (minisat+) Z 13649 10614 10613 0 -1 12 32987 0 0 0 119929 95 0 0 25 0 1 0 541047620 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.26
CPU user time (s): 1199.3
CPU system time (s): 0.959854
CPU usage (%): 100.013
Max. virtual memory (Kb): 130224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####