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-ran8x32.opb
MD5SUM	ff0017de67077abd1f68238274b64e50
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1695644
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
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	1517603678
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	1517603678
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.03
Number of variables	5376
Total number of constraints	296
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	296
Minimum length of a constraint	21
Maximum length of a constraint	640
Trace number 13825

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-20 21:55:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19370 boxname=wulflinc7 idbench=1490 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ff0017de67077abd1f68238274b64e50  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb
IDLAUNCH: 19370
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        590860 kB
Buffers:         35524 kB
Cached:         384916 kB
SwapCached:          4 kB
Active:          94260 kB
Inactive:       328956 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        590580 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14936 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:15:05 (client local time) WITH STATUS 10 IN 1200.93 SECONDS
stats: 19370 7 1200.93 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> Adder-cost: 646   maxlim: 45920   bits: 16/16
c ---[ 332]---> Adder-cost: 670   maxlim: 69856   bits: 17/17
c ---[ 330]---> Adder-cost: 670   maxlim: 67552   bits: 17/17
c ---[ 328]---> Adder-cost: 670   maxlim: 71392   bits: 17/17
c ---[ 326]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 324]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 322]---> Adder-cost: 670   maxlim: 70368   bits: 17/17
c ---[ 320]---> Adder-cost: 670   maxlim: 64608   bits: 17/16
c ---[ 318]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   15
c ---[ 253]---> BDD-cost:   12
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   14
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   12
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:   12
c ---[ 227]---> BDD-cost:   12
c ---[ 226]---> BDD-cost:   18
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   15
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   10
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   14
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   12
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   15
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   10
c ---[ 193]---> BDD-cost:   12
c ---[ 192]---> BDD-cost:   12
c ---[ 191]---> BDD-cost:   18
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   16
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   10
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   16
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   12
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   12
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   10
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   10
c ---[ 114]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   15
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   16
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   12
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   19
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   15
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  145887   390357 |   48629       0        0     nan |  0.000 % |
c |       100 |  145884   390351 |   53491      99      845     8.5 |  9.250 % |
c |       251 |  145782   390120 |   58841     245     1481     6.0 |  9.318 % |
c |       476 |  145691   389912 |   64725     465     2324     5.0 |  9.375 % |
c |       813 |  145642   389747 |   71197     798     3747     4.7 |  9.394 % |
c |      1320 |  145500   389416 |   78317    1286     5742     4.5 |  9.483 % |
c |      2079 |  145359   389099 |   86149    2039     8728     4.3 |  9.572 % |
c |      3219 |  144766   387752 |   94764    3138    13009     4.1 |  9.953 % |
c |      4928 |  143795   385413 |  104240    4765    19176     4.0 | 10.563 % |
c |      7490 |  143074   383747 |  114664    7276    29160     4.0 | 11.010 % |
c |     11334 |  142105   381519 |  126131   11042    50360     4.6 | 11.657 % |
c |     17100 |  140363   377490 |  138744   16672    81263     4.9 | 12.830 % |
c |     25749 |  138138   372183 |  152618   25082   127699     5.1 | 14.267 % |
c |     38724 |  135904   366890 |  167880   37808   307540     8.1 | 15.733 % |
c ==============================================================================
c [1mFound solution: 5358199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10869   maxlim: 3548135   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50073 |  210986   636096 |   70328   49046   460772     9.4 | 15.733 % |
c |     50173 |  210978   636070 |   77360   49145   461217     9.4 | 13.280 % |
c |     50323 |  210909   635912 |   85096   49284   461983     9.4 | 13.320 % |
c |     50548 |  210909   635912 |   93606   49509   463562     9.4 | 13.320 % |
c |     50886 |  210909   635912 |  102967   49847   465520     9.3 | 13.320 % |
c |     51392 |  210882   635851 |  113263   50352   478798     9.5 | 13.334 % |
c |     52151 |  210870   635824 |  124590   51110   494866     9.7 | 13.341 % |
c |     53294 |  210836   635747 |  137049   52252   521026    10.0 | 13.360 % |
c |     55002 |  210728   635482 |  150754   53940   536514     9.9 | 13.415 % |
c |     57564 |  210641   635272 |  165829   56491   599797    10.6 | 13.458 % |
c ==============================================================================
c [1mFound solution: 5249864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3656470   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57694 |  210674   635514 |   70224   56621   604680    10.7 | 13.458 % |
c |     57794 |  210660   635481 |   77246   56718   605093    10.7 | 13.482 % |
c |     57944 |  210660   635481 |   84971   56868   605728    10.7 | 13.482 % |
c |     58169 |  210644   635429 |   93468   57089   606946    10.6 | 13.487 % |
c |     58506 |  210644   635429 |  102814   57426   609732    10.6 | 13.487 % |
c |     59012 |  210644   635429 |  113096   57932   616133    10.6 | 13.487 % |
c |     59771 |  210628   635392 |  124406   58688   624520    10.6 | 13.494 % |
c |     60910 |  210628   635392 |  136846   59827   669992    11.2 | 13.494 % |
c |     62618 |  210318   634674 |  150531   61505   687344    11.2 | 13.671 % |
c |     65181 |  210121   634216 |  165584   64049   733109    11.4 | 13.787 % |
c |     69025 |  209905   633682 |  182142   67849   771790    11.4 | 13.897 % |
c |     74792 |  209617   633002 |  200357   73587  1020238    13.9 | 14.059 % |
c |     83442 |  209576   632902 |  220392   82235  1393616    16.9 | 14.083 % |
c |     96416 |  209576   632902 |  242432   95209  2053461    21.6 | 14.083 % |
c |    115877 |  209494   632705 |  266675  114657  3085469    26.9 | 14.129 % |
c |    145069 |  209167   631924 |  293343  143796  6007262    41.8 | 14.300 % |
c ==============================================================================
c [1mFound solution: 4722835[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4183499   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    160685 |  209066   631816 |   69688  159395  6734074    42.2 | 14.300 % |
c |    160785 |  209037   631749 |   76656   24675   715721    29.0 | 14.416 % |
c |    160935 |  209030   631733 |   84322   24824   716343    28.9 | 14.421 % |
c |    161160 |  208987   631635 |   92754   25046   717238    28.6 | 14.445 % |
c |    161497 |  208943   631534 |  102030   25377   718701    28.3 | 14.471 % |
c |    162003 |  208897   631429 |  112233   25876   721330    27.9 | 14.497 % |
c |    162762 |  208845   631305 |  123456   26630   726354    27.3 | 14.528 % |
c |    163901 |  208754   631096 |  135802   27764   734475    26.5 | 14.581 % |
c |    165609 |  208649   630850 |  149382   29456   747963    25.4 | 14.643 % |
c |    168171 |  208603   630742 |  164320   32015   771017    24.1 | 14.671 % |
c |    172015 |  208500   630500 |  180752   35848   810342    22.6 | 14.726 % |
c |    177781 |  208313   630064 |  198827   41598   896836    21.6 | 14.841 % |
c |    186431 |  208117   629607 |  218710   50207   986922    19.7 | 14.949 % |
c |    199405 |  207814   628895 |  240581   63137  1151810    18.2 | 15.123 % |
c |    218869 |  207572   628332 |  264640   82554  1952634    23.7 | 15.254 % |
c |    248061 |  207493   628151 |  291104  111731  4870843    43.6 | 15.294 % |
c |    291850 |  207465   628085 |  320214  155515  8206156    52.8 | 15.309 % |
c ==============================================================================
c [1mFound solution: 4623619[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4282715   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    297822 |  207476   628240 |   69158  161485  8452286    52.3 | 15.309 % |
c |    297923 |  207476   628240 |   76073   30469  1719675    56.4 | 15.328 % |
c |    298074 |  207454   628191 |   83681   30619  1720593    56.2 | 15.340 % |
c |    298299 |  207433   628142 |   92049   30843  1722018    55.8 | 15.354 % |
c |    298636 |  207433   628142 |  101254   31180  1723760    55.3 | 15.354 % |
c |    299142 |  207423   628119 |  111379   31684  1726630    54.5 | 15.359 % |
c |    299901 |  207423   628119 |  122517   32443  1738283    53.6 | 15.359 % |
c |    301040 |  207399   628063 |  134769   33575  1744808    52.0 | 15.375 % |
c |    302748 |  207399   628063 |  148246   35283  1754317    49.7 | 15.375 % |
c |    305310 |  207348   627944 |  163070   37839  1771036    46.8 | 15.404 % |
c |    309156 |  207283   627790 |  179378   41674  1967914    47.2 | 15.445 % |
c |    314922 |  207283   627790 |  197315   47440  2293238    48.3 | 15.445 % |
c |    323571 |  207213   627629 |  217047   56081  2390063    42.6 | 15.486 % |
c |    336545 |  207172   627524 |  238752   69045  2753152    39.9 | 15.505 % |
c |    356006 |  207162   627501 |  262627   88505  5273285    59.6 | 15.510 % |
c ==============================================================================
c [1mFound solution: 3465746[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5440588   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    378358 |  207173   627631 |   69057  110856  7808378    70.4 | 15.510 % |
c |    378458 |  207168   627618 |   75962   29760  1624204    54.6 | 15.528 % |
c |    378608 |  207168   627618 |   83558   29910  1624879    54.3 | 15.528 % |
c |    378833 |  207163   627607 |   91914   30134  1625882    54.0 | 15.532 % |
c |    379170 |  207163   627607 |  101106   30471  1627884    53.4 | 15.532 % |
c |    379676 |  207156   627590 |  111216   30976  1630564    52.6 | 15.537 % |
c |    380436 |  207146   627567 |  122338   31735  1635154    51.5 | 15.544 % |
c |    381575 |  207146   627567 |  134572   32874  1641344    49.9 | 15.544 % |
c |    383283 |  207142   627558 |  148029   34581  1655978    47.9 | 15.547 % |
c |    385845 |  207142   627558 |  162832   37143  1682417    45.3 | 15.547 % |
c |    389690 |  207079   627414 |  179116   40977  1706761    41.7 | 15.583 % |
c |    395456 |  207046   627339 |  197027   46736  1751028    37.5 | 15.604 % |
c |    404106 |  207023   627285 |  216730   55384  2023139    36.5 | 15.616 % |
c |    417080 |  206909   626641 |  238403   68345  2605074    38.1 | 15.657 % |
c |    436542 |  206865   626518 |  262243   87799  6313276    71.9 | 15.671 % |
c |    465734 |  206837   626452 |  288468  116990  7512014    64.2 | 15.688 % |
c |    509525 |  206837   626452 |  317315  160781 10496493    65.3 | 15.688 % |
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 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 Y12#### 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.82 0.95 0.91 2/54 24485
Raw data (stat): 24485 (runsolver) R 24484 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481623504 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.85 0.95 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4465 0 0 0 988 10 0 0 25 0 1 0 481623504 20701184 4280 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5054 4280 603 41 0 5013 0
vsize: 20216
[startup+20.0015 s]
Raw data (loadavg): 0.87 0.95 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4513 0 0 0 1988 10 0 0 25 0 1 0 481623504 20836352 4328 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4328 603 41 0 5046 0
vsize: 20348
[startup+30.0021 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4551 0 0 0 2987 10 0 0 25 0 1 0 481623504 20971520 4366 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4366 603 41 0 5079 0
vsize: 20480
[startup+40.001 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4600 0 0 0 3987 10 0 0 25 0 1 0 481623504 21331968 4415 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5208 4415 603 41 0 5167 0
vsize: 20832
[startup+50.0019 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4641 0 0 0 4988 10 0 0 25 0 1 0 481623504 21467136 4456 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5241 4456 603 41 0 5200 0
vsize: 20964
[startup+60.0016 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4674 0 0 0 5988 11 0 0 25 0 1 0 481623504 21602304 4489 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5274 4489 603 41 0 5233 0
vsize: 21096
[startup+70.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4711 0 0 0 6987 11 0 0 25 0 1 0 481623504 21737472 4526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5307 4526 603 41 0 5266 0
vsize: 21228
[startup+80.003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4744 0 0 0 7986 11 0 0 25 0 1 0 481623504 21737472 4559 4294967295 134512640 134672761 3221224544 3221223712 134564676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5307 4559 603 41 0 5266 0
vsize: 21228
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4810 0 0 0 8986 11 0 0 25 0 1 0 481623504 22134784 4625 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5404 4625 603 41 0 5363 0
vsize: 21616
[startup+100.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 4963 0 0 0 9986 12 0 0 25 0 1 0 481623504 22810624 4778 4294967295 134512640 134672761 3221224544 3221223712 134553607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 4778 603 41 0 5528 0
vsize: 22276
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 5035 0 0 0 10985 12 0 0 25 0 1 0 481623504 23076864 4850 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5634 4850 603 41 0 5593 0
vsize: 22536
[startup+120.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 5165 0 0 0 11984 13 0 0 25 0 1 0 481623504 23613440 4980 4294967295 134512640 134672761 3221224544 3221223712 134564767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5765 4980 603 41 0 5724 0
vsize: 23060
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 11460 0 0 0 12971 26 0 0 25 0 1 0 481623504 45309952 10073 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11062 10073 603 41 0 11021 0
vsize: 44248
[startup+140.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 11630 0 0 0 13971 27 0 0 25 0 1 0 481623504 45850624 10243 4294967295 134512640 134672761 3221224544 3221223712 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11194 10243 603 41 0 11153 0
vsize: 44776
[startup+150.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 11710 0 0 0 14971 27 0 0 25 0 1 0 481623504 46252032 10323 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11292 10323 603 41 0 11251 0
vsize: 45168
[startup+160.032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12063 0 0 0 15973 28 0 0 25 0 1 0 481623504 47443968 10615 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11583 10615 603 41 0 11542 0
vsize: 46332
[startup+170.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12067 0 0 0 16973 28 0 0 25 0 1 0 481623504 47443968 10619 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11583 10619 603 41 0 11542 0
vsize: 46332
[startup+180.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12148 0 0 0 17973 28 0 0 25 0 1 0 481623504 47714304 10700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11649 10700 603 41 0 11608 0
vsize: 46596
[startup+190.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12203 0 0 0 18974 28 0 0 25 0 1 0 481623504 48246784 10755 4294967295 134512640 134672761 3221224544 3221223692 1074754724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11779 10755 603 41 0 11738 0
vsize: 47116
[startup+200.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12301 0 0 0 19974 28 0 0 25 0 1 0 481623504 48644096 10853 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11876 10853 603 41 0 11835 0
vsize: 47504
[startup+210.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 12940 0 0 0 20972 30 0 0 25 0 1 0 481623504 51191808 11492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12498 11492 603 41 0 12457 0
vsize: 49992
[startup+220.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 13404 0 0 0 21971 31 0 0 25 0 1 0 481623504 53067776 11956 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12956 11956 603 41 0 12915 0
vsize: 51824
[startup+230.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 13784 0 0 0 22970 33 0 0 25 0 1 0 481623504 54554624 12336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13319 12336 603 41 0 13278 0
vsize: 53276
[startup+240.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 13993 0 0 0 23969 33 0 0 25 0 1 0 481623504 55365632 12545 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13517 12545 603 41 0 13476 0
vsize: 54068
[startup+250.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 14628 0 0 0 24968 36 0 0 25 0 1 0 481623504 57925632 13180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14142 13180 603 41 0 14101 0
vsize: 56568
[startup+260.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 14952 0 0 0 25968 37 0 0 25 0 1 0 481623504 59273216 13504 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14471 13504 603 41 0 14430 0
vsize: 57884
[startup+270.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 15189 0 0 0 26966 38 0 0 25 0 1 0 481623504 60219392 13741 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13741 603 41 0 14661 0
vsize: 58808
[startup+280.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 15395 0 0 0 27965 39 0 0 25 0 1 0 481623504 61030400 13947 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14900 13947 603 41 0 14859 0
vsize: 59600
[startup+290.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 15691 0 0 0 28964 40 0 0 25 0 1 0 481623504 62242816 14243 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15196 14243 603 41 0 15155 0
vsize: 60784
[startup+300.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24485
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 15792 0 0 0 29964 40 0 0 25 0 1 0 481623504 63168512 14344 4294967295 134512640 134672761 3221224544 3221223680 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15422 14344 603 41 0 15381 0
vsize: 61688
[startup+310.072 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 24520
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 16140 0 0 0 30963 41 0 0 25 0 1 0 481623504 64655360 14692 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15785 14692 603 41 0 15744 0
vsize: 63140
[startup+320.073 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 17033 0 0 0 31961 44 0 0 25 0 1 0 481623504 68272128 15585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16668 15585 603 41 0 16627 0
vsize: 66672
[startup+330.112 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 17857 0 0 0 32962 46 0 0 25 0 1 0 481623504 71643136 16409 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17491 16409 603 41 0 17450 0
vsize: 69964
[startup+340.111 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 18269 0 0 0 33962 47 0 0 25 0 1 0 481623504 73261056 16821 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17886 16821 603 41 0 17845 0
vsize: 71544
[startup+350.112 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 18587 0 0 0 34960 49 0 0 25 0 1 0 481623504 74604544 17139 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18214 17139 603 41 0 18173 0
vsize: 72856
[startup+360.125 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19054 0 0 0 35960 51 0 0 25 0 1 0 481623504 76484608 17606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18673 17606 603 41 0 18632 0
vsize: 74692
[startup+370.125 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 24538
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 36959 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+380.135 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 37960 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+390.135 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 38960 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+400.135 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 39961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+410.134 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 40961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+420.134 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 41961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+430.135 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 42961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+440.134 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 43961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+450.134 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 44961 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+460.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 45962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+470.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 46962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+480.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 47962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+490.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 48962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+500.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 49962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+510.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 50962 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+520.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 51963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+530.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 52963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+540.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 53963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+550.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 54963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+560.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 55963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+570.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 56963 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+580.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 57964 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+590.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 58964 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+600.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 59964 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+610.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24540
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 60964 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+620.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19325 0 0 0 61964 51 0 0 25 0 1 0 481623504 77135872 17795 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18832 17795 603 41 0 18791 0
vsize: 75328
[startup+630.136 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19526 0 0 0 62964 52 0 0 25 0 1 0 481623504 78077952 17996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19062 17996 603 41 0 19021 0
vsize: 76248
[startup+640.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 19681 0 0 0 63964 52 0 0 25 0 1 0 481623504 78614528 18151 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19193 18151 603 41 0 19152 0
vsize: 76772
[startup+650.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 20251 0 0 0 64962 54 0 0 25 0 1 0 481623504 81039360 18721 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19785 18721 603 41 0 19744 0
vsize: 79140
[startup+660.135 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 20923 0 0 0 65960 56 0 0 25 0 1 0 481623504 83738624 19393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20444 19393 603 41 0 20403 0
vsize: 81776
[startup+670.152 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21294 0 0 0 66960 58 0 0 25 0 1 0 481623504 85217280 19764 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20805 19764 603 41 0 20764 0
vsize: 83220
[startup+680.171 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21598 0 0 0 67962 58 0 0 25 0 1 0 481623504 86425600 20063 4294967295 134512640 134672761 3221224544 3220961536 134594069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21100 20063 603 41 0 21059 0
vsize: 84400
[startup+690.55 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 69000 58 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+700.551 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 69998 58 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+710.578 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 71001 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+720.621 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 72005 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+730.622 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 73005 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+740.621 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 74006 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+750.622 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 75006 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+760.726 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 76016 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+770.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 77017 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+780.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 78017 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+790.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 79017 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+800.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 80017 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+810.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 81018 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+820.731 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 82018 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+830.732 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 83018 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+840.733 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 84018 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+850.734 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 85019 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+860.734 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 86019 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+870.734 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21665 0 0 0 87019 59 0 0 25 0 1 0 481623504 86478848 20073 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20073 603 41 0 21072 0
vsize: 84452
[startup+880.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 88019 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+890.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 89019 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+900.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 90019 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+910.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 91019 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+920.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 92020 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+930.736 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 93020 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+940.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 94020 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+950.735 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 95020 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+960.741 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 96021 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+970.742 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 97021 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+980.741 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 98021 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+990.741 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 99021 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1000.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 100022 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1010.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 101022 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1020.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 102022 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1030.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 103022 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1040.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 104022 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1050.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 105023 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1060.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21668 0 0 0 106023 59 0 0 25 0 1 0 481623504 86478848 20076 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20076 603 41 0 21072 0
vsize: 84452
[startup+1070.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 21670 0 0 0 107023 59 0 0 25 0 1 0 481623504 86478848 20078 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21113 20078 603 41 0 21072 0
vsize: 84452
[startup+1080.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 22388 0 0 0 108021 61 0 0 25 0 1 0 481623504 89444352 20796 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21837 20796 603 41 0 21796 0
vsize: 87348
[startup+1090.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 22899 0 0 0 109019 63 0 0 25 0 1 0 481623504 91602944 21307 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22364 21307 603 41 0 22323 0
vsize: 89456
[startup+1100.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 23358 0 0 0 110018 65 0 0 25 0 1 0 481623504 93511680 21766 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21766 603 41 0 22789 0
vsize: 91320
[startup+1110.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 23757 0 0 0 111017 66 0 0 25 0 1 0 481623504 95150080 22165 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23230 22165 603 41 0 23189 0
vsize: 92920
[startup+1120.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 24140 0 0 0 112015 68 0 0 25 0 1 0 481623504 96874496 22548 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23651 22548 603 41 0 23610 0
vsize: 94604
[startup+1130.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 24368 0 0 0 113014 69 0 0 25 0 1 0 481623504 97812480 22776 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23880 22776 603 41 0 23839 0
vsize: 95520
[startup+1140.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 24694 0 0 0 114013 70 0 0 25 0 1 0 481623504 99024896 23102 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24176 23102 603 41 0 24135 0
vsize: 96704
[startup+1150.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 25013 0 0 0 115013 71 0 0 25 0 1 0 481623504 100368384 23421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24504 23421 603 41 0 24463 0
vsize: 98016
[startup+1160.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 25510 0 0 0 116011 72 0 0 25 0 1 0 481623504 102387712 23918 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24997 23918 603 41 0 24956 0
vsize: 99988
[startup+1170.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 26032 0 0 0 117010 74 0 0 25 0 1 0 481623504 104550400 24440 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25525 24440 603 41 0 25484 0
vsize: 102100
[startup+1180.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 26489 0 0 0 118009 75 0 0 25 0 1 0 481623504 106430464 24897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25984 24897 603 41 0 25943 0
vsize: 103936
[startup+1190.74 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 26766 0 0 0 119008 76 0 0 25 0 1 0 481623504 107507712 25174 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26247 25174 603 41 0 26206 0
vsize: 104988
[startup+1200.75 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 24542
Raw data (stat): 24485 (minisat+) R 24484 22932 22931 0 -1 0 27025 0 0 0 120008 77 0 0 25 0 1 0 481623504 108580864 25433 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26509 25433 603 41 0 26468 0
vsize: 106036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.82 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 24542
Raw data (stat): 24485 (minisat+) Z 24484 22932 22931 0 -1 12 27028 0 0 0 120010 82 0 0 25 0 1 0 481623504 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.82
CPU time (s): 1200.93
CPU user time (s): 1200.1
CPU system time (s): 0.824874
CPU usage (%): 100.009
Max. virtual memory (Kb): 106036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####