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 17599

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        629048 kB
Buffers:          8236 kB
Cached:         375160 kB
SwapCached:        328 kB
Active:          50744 kB
Inactive:       335176 kB
HighTotal:      131008 kB
HighFree:         1288 kB
LowTotal:       903652 kB
LowFree:        627760 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            14048 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:11:13 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19362 7 1200.24 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 |  144205   384224 |   48068       0        0     nan |  0.000 % |
c |       101 |  143894   383508 |   52874      66      318     4.8 |  9.453 % |
c |       251 |  143657   382969 |   58162     208      800     3.8 |  9.606 % |
c |       478 |  143324   382155 |   63978     412     1563     3.8 |  9.813 % |
c |       815 |  143107   381659 |   70376     741     2835     3.8 |  9.960 % |
c |      1321 |  142938   381226 |   77413    1229     4788     3.9 | 10.059 % |
c |      2080 |  142897   381119 |   85155    1984     7876     4.0 | 10.082 % |
c |      3219 |  142439   380071 |   93670    3082    12180     4.0 | 10.373 % |
c |      4927 |  142113   379324 |  103038    4765    18996     4.0 | 10.574 % |
c |      7489 |  141435   377773 |  113341    7272    29201     4.0 | 11.019 % |
c |     11334 |  140163   374836 |  124676   11037    46404     4.2 | 11.873 % |
c |     17100 |  137982   369803 |  137143   16603    71000     4.3 | 13.307 % |
c |     25749 |  135304   363521 |  150857   24976   111133     4.4 | 15.072 % |
c |     38723 |  133208   358577 |  165943   37669   207430     5.5 | 16.472 % |
c |     58184 |  132451   356706 |  182538   57043   681358    11.9 | 16.959 % |
c |     87376 |  131994   355630 |  200791   86176  1622302    18.8 | 17.275 % |
c ==============================================================================
c [1mFound solution: 5846672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10869   maxlim: 3059662   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88349 |  208000   627194 |   69333   87149  1680166    19.3 | 17.275 % |
c |     88449 |  208000   627194 |   76266   26294   560330    21.3 | 14.065 % |
c |     88599 |  207944   627064 |   83892   26433   560917    21.2 | 14.093 % |
c |     88826 |  207870   626885 |   92282   26650   561827    21.1 | 14.129 % |
c |     89163 |  207835   626796 |  101510   26982   563525    20.9 | 14.148 % |
c |     89670 |  207740   626571 |  111661   27478   567066    20.6 | 14.198 % |
c |     90429 |  207707   626489 |  122827   28233   575230    20.4 | 14.213 % |
c |     91572 |  207707   626489 |  135110   29376   617611    21.0 | 14.213 % |
c |     93280 |  207572   626169 |  148621   31076   628301    20.2 | 14.294 % |
c |     95842 |  207384   625733 |  163483   33617   654476    19.5 | 14.401 % |
c |     99686 |  207323   625596 |  179831   37454   694987    18.6 | 14.432 % |
c |    105452 |  207166   625231 |  197815   43205   764996    17.7 | 14.520 % |
c |    114101 |  206875   624555 |  217596   51815   935660    18.1 | 14.675 % |
c ==============================================================================
c [1mFound solution: 5547096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3359238   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    126409 |  206349   623308 |   68783   64028  1187221    18.5 | 14.675 % |
c |    126509 |  206349   623308 |   75661   64128  1188071    18.5 | 14.962 % |
c |    126659 |  206349   623308 |   83227   64278  1189378    18.5 | 14.962 % |
c |    126884 |  206349   623308 |   91550   64503  1190920    18.5 | 14.962 % |
c |    127221 |  206299   623176 |  100705   64831  1194747    18.4 | 14.989 % |
c |    127727 |  206278   623127 |  110775   65336  1199949    18.4 | 15.003 % |
c |    128487 |  206093   622615 |  121853   66070  1207898    18.3 | 15.086 % |
c |    129626 |  206082   622588 |  134038   67207  1222047    18.2 | 15.093 % |
c |    131334 |  206038   622476 |  147442   68908  1251349    18.2 | 15.111 % |
c ==============================================================================
c [1mFound solution: 5466716[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3439618   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131675 |  205994   622471 |   68664   69242  1255958    18.1 | 15.111 % |
c |    131775 |  205975   622425 |   75530   69340  1256530    18.1 | 15.166 % |
c |    131925 |  205913   622281 |   83083   69482  1257520    18.1 | 15.204 % |
c |    132150 |  205905   622263 |   91391   69706  1259309    18.1 | 15.209 % |
c |    132488 |  205905   622263 |  100530   70044  1263601    18.0 | 15.209 % |
c |    132995 |  205872   622186 |  110584   70546  1268344    18.0 | 15.228 % |
c ==============================================================================
c [1mFound solution: 5466530[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3439804   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133464 |  205884   622331 |   68628   71015  1276422    18.0 | 15.228 % |
c |    133564 |  205869   622295 |   75490   71114  1276861    18.0 | 15.245 % |
c |    133714 |  205850   622252 |   83039   71262  1277529    17.9 | 15.258 % |
c |    133939 |  205835   622199 |   91343   71485  1278707    17.9 | 15.259 % |
c |    134276 |  205835   622199 |  100478   71822  1282132    17.9 | 15.259 % |
c |    134783 |  205822   622167 |  110526   72328  1287623    17.8 | 15.266 % |
c |    135543 |  205822   622167 |  121578   73088  1305319    17.9 | 15.266 % |
c |    136683 |  205800   622116 |  133736   74225  1320219    17.8 | 15.280 % |
c |    138391 |  205793   622093 |  147110   75931  1402758    18.5 | 15.282 % |
c |    140953 |  205784   622062 |  161821   78491  1488559    19.0 | 15.283 % |
c |    144798 |  205774   622033 |  178003   82333  1617844    19.7 | 15.287 % |
c |    150564 |  205758   621996 |  195803   88097  1774299    20.1 | 15.297 % |
c |    159213 |  205758   621996 |  215384   96746  3310225    34.2 | 15.297 % |
c ==============================================================================
c [1mFound solution: 3443634[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 5462700   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    165707 |  205778   622194 |   68592  103235  3574828    34.6 | 15.297 % |
c |    165807 |  205778   622194 |   75451   27962  1484814    53.1 | 15.317 % |
c |    165957 |  205778   622194 |   82996   28112  1485521    52.8 | 15.317 % |
c |    166182 |  205778   622194 |   91295   28337  1487056    52.5 | 15.317 % |
c |    166519 |  205778   622194 |  100425   28674  1488655    51.9 | 15.317 % |
c |    167025 |  205778   622194 |  110468   29180  1491649    51.1 | 15.317 % |
c |    167784 |  205766   622166 |  121514   29938  1496002    50.0 | 15.326 % |
c |    168923 |  205743   622113 |  133666   31074  1503179    48.4 | 15.336 % |
c |    170631 |  205717   622051 |  147033   32778  1519334    46.4 | 15.350 % |
c |    173193 |  205662   621923 |  161736   35334  1547784    43.8 | 15.383 % |
c |    177037 |  205618   621821 |  177909   39172  1572725    40.1 | 15.409 % |
c |    182804 |  205600   621780 |  195700   44937  1623079    36.1 | 15.421 % |
c |    191453 |  205569   621697 |  215271   53572  1865645    34.8 | 15.433 % |
c |    204428 |  205549   621649 |  236798   66543  2191016    32.9 | 15.445 % |
c |    223889 |  205478   621474 |  260478   85994  2764498    32.1 | 15.483 % |
c |    253081 |  205472   621460 |  286525  115184  4574051    39.7 | 15.488 % |
c ==============================================================================
c [1mFound solution: 3430223[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5476111   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    271352 |  205471   621537 |   68490  133453  5946536    44.6 | 15.488 % |
c |    271452 |  205471   621537 |   75339   30935  1195186    38.6 | 15.503 % |
c |    271602 |  205471   621537 |   82872   31085  1195936    38.5 | 15.503 % |
c |    271827 |  205471   621537 |   91160   31310  1197550    38.2 | 15.503 % |
c |    272164 |  205462   621514 |  100276   31645  1199370    37.9 | 15.508 % |
c |    272670 |  205462   621514 |  110303   32151  1201983    37.4 | 15.508 % |
c |    273429 |  205458   621505 |  121334   32909  1208893    36.7 | 15.511 % |
c |    274568 |  205417   621400 |  133467   34037  1214441    35.7 | 15.535 % |
c |    276276 |  205411   621386 |  146814   35744  1224246    34.3 | 15.539 % |
c |    278838 |  205371   621294 |  161495   38301  1241197    32.4 | 15.558 % |
c |    282682 |  205345   621234 |  177645   42142  1266242    30.0 | 15.573 % |
c |    288448 |  205255   621019 |  195409   47898  1386965    29.0 | 15.621 % |
c |    297099 |  205240   620983 |  214950   56547  1799221    31.8 | 15.628 % |
c |    310073 |  205208   620910 |  236446   69515  2294825    33.0 | 15.647 % |
c |    329535 |  205133   620733 |  260090   88968  2969796    33.4 | 15.687 % |
c |    358727 |  205113   620687 |  286099  118157  4869169    41.2 | 15.699 % |
c ==============================================================================
c [1mFound solution: 3237337[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5668997   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    381206 |  205124   620787 |   68374  140636  7009734    49.8 | 15.699 % |
c |    381306 |  205124   620787 |   75211   31656  1685810    53.3 | 15.706 % |
c |    381456 |  205124   620787 |   82732   31806  1686416    53.0 | 15.706 % |
c |    381682 |  205119   620775 |   91005   32031  1687321    52.7 | 15.709 % |
c |    382019 |  205119   620775 |  100106   32368  1688865    52.2 | 15.709 % |
c |    382525 |  205113   620761 |  110117   32873  1691688    51.5 | 15.713 % |
c |    383285 |  205108   620749 |  121128   33632  1696132    50.4 | 15.716 % |
c |    384425 |  205037   620584 |  133241   34763  1703888    49.0 | 15.758 % |
c |    386133 |  205017   620537 |  146565   36467  1718466    47.1 | 15.768 % |
c |    388695 |  205017   620537 |  161222   39029  1740018    44.6 | 15.768 % |
c |    392539 |  204978   620449 |  177344   42868  1772129    41.3 | 15.794 % |
c |    398305 |  204951   620386 |  195079   48629  1832259    37.7 | 15.813 % |
c |    406954 |  204922   620319 |  214586   57274  3240991    56.6 | 15.828 % |
c |    419929 |  204900   620267 |  236045   70246  3706617    52.8 | 15.842 % |
c |    439392 |  204894   620253 |  259650   89708  4551142    50.7 | 15.847 % |
c |    468585 |  204876   620213 |  285615  118896  5757279    48.4 | 15.859 % |
c |    512376 |  204828   620102 |  314176  162681  8221999    50.5 | 15.887 % |
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_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.96 0.97 2/54 21676
Raw data (stat): 21676 (runsolver) R 21675 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486276370 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0056 s]
Raw data (loadavg): 0.94 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4487 0 0 0 987 11 0 0 25 0 1 0 486276370 20742144 4302 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5064 4302 603 41 0 5023 0
vsize: 20256
[startup+20.0054 s]
Raw data (loadavg): 0.95 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4541 0 0 0 1986 11 0 0 25 0 1 0 486276370 21028864 4356 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5134 4356 603 41 0 5093 0
vsize: 20536
[startup+30.0062 s]
Raw data (loadavg): 0.95 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4572 0 0 0 2986 12 0 0 25 0 1 0 486276370 21159936 4387 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5166 4387 603 41 0 5125 0
vsize: 20664
[startup+40.0059 s]
Raw data (loadavg): 0.96 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4608 0 0 0 3985 13 0 0 25 0 1 0 486276370 21385216 4423 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5221 4423 603 41 0 5180 0
vsize: 20884
[startup+50.0057 s]
Raw data (loadavg): 0.97 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4637 0 0 0 4985 13 0 0 25 0 1 0 486276370 21385216 4452 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5221 4452 603 41 0 5180 0
vsize: 20884
[startup+60.0054 s]
Raw data (loadavg): 0.97 0.96 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4671 0 0 0 5984 14 0 0 25 0 1 0 486276370 21520384 4486 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5254 4486 603 41 0 5213 0
vsize: 21016
[startup+70.0067 s]
Raw data (loadavg): 0.97 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4703 0 0 0 6984 14 0 0 25 0 1 0 486276370 21655552 4518 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5287 4518 603 41 0 5246 0
vsize: 21148
[startup+80.008 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4751 0 0 0 7984 15 0 0 25 0 1 0 486276370 21790720 4566 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5320 4566 603 41 0 5279 0
vsize: 21280
[startup+90.0076 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4808 0 0 0 8983 15 0 0 25 0 1 0 486276370 22188032 4623 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5417 4623 603 41 0 5376 0
vsize: 21668
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4847 0 0 0 9983 15 0 0 25 0 1 0 486276370 22323200 4662 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5450 4662 603 41 0 5409 0
vsize: 21800
[startup+110.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 4902 0 0 0 10983 16 0 0 25 0 1 0 486276370 22593536 4717 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 4717 603 41 0 5475 0
vsize: 22064
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 5128 0 0 0 11983 16 0 0 25 0 1 0 486276370 23535616 4943 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5746 4943 603 41 0 5705 0
vsize: 22984
[startup+130.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 5314 0 0 0 12982 17 0 0 25 0 1 0 486276370 24207360 5129 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5910 5129 603 41 0 5869 0
vsize: 23640
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 5540 0 0 0 13981 18 0 0 25 0 1 0 486276370 25149440 5355 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6140 5355 603 41 0 6099 0
vsize: 24560
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 5681 0 0 0 14980 19 0 0 25 0 1 0 486276370 25686016 5496 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6271 5496 603 41 0 6230 0
vsize: 25084
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 5903 0 0 0 15980 20 0 0 25 0 1 0 486276370 26886144 5718 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6564 5718 603 41 0 6523 0
vsize: 26256
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 6233 0 0 0 16979 21 0 0 25 0 1 0 486276370 28094464 6048 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6859 6048 603 41 0 6818 0
vsize: 27436
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 6590 0 0 0 17978 22 0 0 25 0 1 0 486276370 29581312 6405 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7222 6405 603 41 0 7181 0
vsize: 28888
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13044 0 0 0 18964 36 0 0 25 0 1 0 486276370 52015104 11656 4294967295 134512640 134672761 3221224624 3221223776 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11656 603 41 0 12658 0
vsize: 50796
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13044 0 0 0 19964 36 0 0 25 0 1 0 486276370 52015104 11656 4294967295 134512640 134672761 3221224624 3221223824 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11656 603 41 0 12658 0
vsize: 50796
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13044 0 0 0 20964 36 0 0 25 0 1 0 486276370 52015104 11656 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11656 603 41 0 12658 0
vsize: 50796
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13047 0 0 0 21964 36 0 0 25 0 1 0 486276370 52015104 11659 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11659 603 41 0 12658 0
vsize: 50796
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13047 0 0 0 22964 36 0 0 25 0 1 0 486276370 52015104 11659 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11659 603 41 0 12658 0
vsize: 50796
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13047 0 0 0 23964 36 0 0 25 0 1 0 486276370 52015104 11659 4294967295 134512640 134672761 3221224624 3221223776 1074743855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11659 603 41 0 12658 0
vsize: 50796
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13047 0 0 0 24965 36 0 0 25 0 1 0 486276370 52015104 11659 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11659 603 41 0 12658 0
vsize: 50796
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13049 0 0 0 25965 36 0 0 25 0 1 0 486276370 52015104 11661 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11661 603 41 0 12658 0
vsize: 50796
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13053 0 0 0 26965 36 0 0 25 0 1 0 486276370 52015104 11665 4294967295 134512640 134672761 3221224624 3221223792 134564752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11665 603 41 0 12658 0
vsize: 50796
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13053 0 0 0 27965 36 0 0 25 0 1 0 486276370 52015104 11665 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11665 603 41 0 12658 0
vsize: 50796
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13053 0 0 0 28965 36 0 0 25 0 1 0 486276370 52015104 11665 4294967295 134512640 134672761 3221224624 3221223840 134557662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12699 11665 603 41 0 12658 0
vsize: 50796
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13201 0 0 0 29965 36 0 0 25 0 1 0 486276370 52285440 11740 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12765 11740 603 41 0 12724 0
vsize: 51060
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13201 0 0 0 30965 37 0 0 25 0 1 0 486276370 52285440 11740 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12765 11740 603 41 0 12724 0
vsize: 51060
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13269 0 0 0 31965 37 0 0 25 0 1 0 486276370 52445184 11766 4294967295 134512640 134672761 3221224624 3221221280 134544524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12804 11766 603 41 0 12763 0
vsize: 51216
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13350 0 0 0 32964 37 0 0 25 0 1 0 486276370 52285440 11743 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12765 11743 603 41 0 12724 0
vsize: 51060
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13350 0 0 0 33964 37 0 0 25 0 1 0 486276370 52285440 11743 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12765 11743 603 41 0 12724 0
vsize: 51060
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13509 0 0 0 34964 38 0 0 25 0 1 0 486276370 52957184 11902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12929 11902 603 41 0 12888 0
vsize: 51716
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 13743 0 0 0 35964 38 0 0 25 0 1 0 486276370 53895168 12136 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13158 12136 603 41 0 13117 0
vsize: 52632
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 14321 0 0 0 36963 39 0 0 25 0 1 0 486276370 56315904 12714 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13749 12714 603 41 0 13708 0
vsize: 54996
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15239 0 0 0 37961 41 0 0 25 0 1 0 486276370 60076032 13632 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14667 13632 603 41 0 14626 0
vsize: 58668
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15584 0 0 0 38960 42 0 0 25 0 1 0 486276370 61427712 13977 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14997 13977 603 41 0 14956 0
vsize: 59988
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 39959 43 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 40960 43 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 41960 43 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 42959 43 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 43959 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223748 134566040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 44959 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 45959 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 46959 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 47960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 48960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 49960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 50960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 51960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223760 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.97 2/54 21676
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 52960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+540.009 s]
Raw data (loadavg): 1.07 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 53960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+550.01 s]
Raw data (loadavg): 1.06 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 15919 0 0 0 54960 44 0 0 25 0 1 0 486276370 62558208 14259 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14259 603 41 0 15232 0
vsize: 61092
[startup+560.01 s]
Raw data (loadavg): 1.05 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 16060 0 0 0 55960 45 0 0 25 0 1 0 486276370 63234048 14400 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15438 14400 603 41 0 15397 0
vsize: 61752
[startup+570.01 s]
Raw data (loadavg): 1.04 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 16753 0 0 0 56958 47 0 0 25 0 1 0 486276370 65937408 15093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16098 15093 603 41 0 16057 0
vsize: 64392
[startup+580.01 s]
Raw data (loadavg): 1.04 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 17123 0 0 0 57956 49 0 0 25 0 1 0 486276370 67424256 15463 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16461 15463 603 41 0 16420 0
vsize: 65844
[startup+590.01 s]
Raw data (loadavg): 1.03 0.99 0.97 2/54 21729
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 17516 0 0 0 58955 50 0 0 25 0 1 0 486276370 69046272 15856 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16857 15856 603 41 0 16816 0
vsize: 67428
[startup+600.01 s]
Raw data (loadavg): 1.03 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18014 0 0 0 59953 52 0 0 25 0 1 0 486276370 71065600 16354 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17350 16354 603 41 0 17309 0
vsize: 69400
[startup+610.01 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18486 0 0 0 60952 53 0 0 25 0 1 0 486276370 73482240 16826 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17940 16826 603 41 0 17899 0
vsize: 71760
[startup+620.011 s]
Raw data (loadavg): 1.02 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 61952 54 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+630.011 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 62952 54 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+640.011 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 63952 55 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+650.011 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 64951 55 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+660.011 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 65951 55 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+670.012 s]
Raw data (loadavg): 1.01 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 66951 55 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+680.012 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 67951 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+690.013 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 68951 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+700.013 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 69951 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+710.014 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 70951 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+720.013 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 71951 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+730.014 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 72952 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+740.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 73952 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+750.014 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 74952 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+760.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 75952 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+770.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 76952 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+780.015 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 77953 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+790.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18864 0 0 0 78953 56 0 0 25 0 1 0 486276370 74395648 17052 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17052 603 41 0 18122 0
vsize: 72652
[startup+800.016 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18865 0 0 0 79953 56 0 0 25 0 1 0 486276370 74395648 17053 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17053 603 41 0 18122 0
vsize: 72652
[startup+810.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 18865 0 0 0 80953 56 0 0 25 0 1 0 486276370 74395648 17053 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18163 17053 603 41 0 18122 0
vsize: 72652
[startup+820.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 19627 0 0 0 81951 59 0 0 25 0 1 0 486276370 77631488 17815 4294967295 134512640 134672761 3221224624 3221223728 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18953 17815 603 41 0 18912 0
vsize: 75812
[startup+830.018 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20004 0 0 0 82950 60 0 0 25 0 1 0 486276370 79118336 18192 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19316 18192 603 41 0 19275 0
vsize: 77264
[startup+840.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20248 0 0 0 83949 61 0 0 25 0 1 0 486276370 80060416 18436 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19546 18436 603 41 0 19505 0
vsize: 78184
[startup+850.017 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 84949 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+860.018 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21731
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 85949 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+870.018 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 86949 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+880.019 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 87949 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+890.02 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 88950 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+900.02 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 89950 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+910.021 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 90950 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+920.021 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 91950 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+930.022 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 92950 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+940.023 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 93951 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+950.026 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20450 0 0 0 94951 61 0 0 25 0 1 0 486276370 80613376 18572 4294967295 134512640 134672761 3221224624 3221223728 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18572 603 41 0 19640 0
vsize: 78724
[startup+960.026 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 95951 61 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+970.026 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 96951 61 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+980.027 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 97952 61 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+990.027 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 98952 61 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 99952 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 100952 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 101952 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 102953 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 103953 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 104953 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20451 0 0 0 105953 62 0 0 25 0 1 0 486276370 80613376 18573 4294967295 134512640 134672761 3221224624 3221223776 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18573 603 41 0 19640 0
vsize: 78724
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20452 0 0 0 106953 62 0 0 25 0 1 0 486276370 80613376 18574 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 18574 603 41 0 19640 0
vsize: 78724
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 20564 0 0 0 107954 62 0 0 25 0 1 0 486276370 81154048 18686 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19813 18686 603 41 0 19772 0
vsize: 79252
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 21006 0 0 0 108953 63 0 0 25 0 1 0 486276370 82903040 19128 4294967295 134512640 134672761 3221224624 3221223808 134559618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20240 19128 603 41 0 20199 0
vsize: 80960
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 21466 0 0 0 109951 64 0 0 25 0 1 0 486276370 84791296 19588 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20701 19588 603 41 0 20660 0
vsize: 82804
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 21894 0 0 0 110951 65 0 0 25 0 1 0 486276370 86532096 20016 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21126 20016 603 41 0 21085 0
vsize: 84504
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 22142 0 0 0 111950 66 0 0 25 0 1 0 486276370 87478272 20264 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21357 20264 603 41 0 21316 0
vsize: 85428
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 22622 0 0 0 112949 67 0 0 25 0 1 0 486276370 89358336 20744 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21816 20744 603 41 0 21775 0
vsize: 87264
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 23142 0 0 0 113948 68 0 0 25 0 1 0 486276370 91516928 21264 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22343 21264 603 41 0 22302 0
vsize: 89372
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 23819 0 0 0 114946 71 0 0 25 0 1 0 486276370 94339072 21941 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23032 21941 603 41 0 22991 0
vsize: 92128
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 24368 0 0 0 115945 71 0 0 25 0 1 0 486276370 96493568 22490 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23558 22490 603 41 0 23517 0
vsize: 94232
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 25135 0 0 0 116944 73 0 0 25 0 1 0 486276370 99594240 23257 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24315 23257 603 41 0 24274 0
vsize: 97260
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 25710 0 0 0 117943 74 0 0 25 0 1 0 486276370 102019072 23832 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24907 23832 603 41 0 24866 0
vsize: 99628
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 26183 0 0 0 118943 75 0 0 25 0 1 0 486276370 103907328 24305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25368 24305 603 41 0 25327 0
vsize: 101472
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.97 2/54 21733
Raw data (stat): 21676 (minisat+) R 21675 24215 24214 0 -1 0 26534 0 0 0 119941 76 0 0 25 0 1 0 486276370 105390080 24656 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25730 24656 603 41 0 25689 0
vsize: 102920
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.97 1/54 21733
Raw data (stat): 21676 (minisat+) Z 21675 24215 24214 0 -1 12 26537 0 0 0 119942 81 0 0 25 0 1 0 486276370 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.24
CPU user time (s): 1199.43
CPU system time (s): 0.816875
CPU usage (%): 100.012
Max. virtual memory (Kb): 102920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####