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/milp/normalized-mps-v2-13-7-ran14x18_1.opb
MD5SUM	27cc6bcebfcedf07c5cf3ac138a419c6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	913429
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1421968313
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	1421968313
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	5292
Total number of constraints	536
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	252
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	1
Maximum length of a constraint	360
Trace number 14004

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-20 22:36:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19812 boxname=wulflinc8 idbench=1524 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  27cc6bcebfcedf07c5cf3ac138a419c6  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran14x18_1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran14x18_1.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-ran14x18_1.opb
IDLAUNCH: 19812
/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:        678144 kB
Buffers:         33684 kB
Cached:         299788 kB
SwapCached:          0 kB
Active:         100068 kB
Inactive:       236232 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        677892 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14588 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 22:56:30 (client local time) WITH STATUS 10 IN 1200.06 SECONDS
stats: 19812 7 1200.06 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 386   maxlim: 47470   bits: 16/16
c ---[ 312]---> Adder-cost: 386   maxlim: 47726   bits: 16/16
c ---[ 310]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 308]---> Adder-cost: 388   maxlim: 58222   bits: 16/16
c ---[ 306]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 304]---> Adder-cost: 386   maxlim: 46830   bits: 16/16
c ---[ 302]---> Adder-cost: 386   maxlim: 47086   bits: 16/16
c ---[ 300]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 298]---> Adder-cost: 386   maxlim: 46702   bits: 16/16
c ---[ 296]---> Adder-cost: 386   maxlim: 46958   bits: 16/16
c ---[ 294]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 292]---> Adder-cost: 386   maxlim: 48110   bits: 16/16
c ---[ 290]---> Adder-cost: 386   maxlim: 47982   bits: 16/16
c ---[ 288]---> Adder-cost: 388   maxlim: 57582   bits: 16/16
c ---[ 286]---> Adder-cost: 260   maxlim: 13554   bits: 14/14
c ---[ 284]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 282]---> Adder-cost: 260   maxlim: 13426   bits: 14/14
c ---[ 280]---> Adder-cost: 310   maxlim: 50930   bits: 16/16
c ---[ 278]---> Adder-cost: 286   maxlim: 26866   bits: 15/15
c ---[ 276]---> Adder-cost: 310   maxlim: 50418   bits: 16/16
c ---[ 274]---> Adder-cost: 312   maxlim: 57202   bits: 16/16
c ---[ 272]---> Adder-cost: 312   maxlim: 55666   bits: 16/16
c ---[ 270]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 268]---> Adder-cost: 286   maxlim: 27634   bits: 15/15
c ---[ 266]---> Adder-cost: 310   maxlim: 50546   bits: 16/16
c ---[ 264]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 262]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 260]---> Adder-cost: 260   maxlim: 13810   bits: 14/14
c ---[ 258]---> Adder-cost: 312   maxlim: 56946   bits: 16/16
c ---[ 256]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 254]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 252]---> Adder-cost: 286   maxlim: 27506   bits: 15/15
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:   14
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   12
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:   16
c ---[ 237]---> BDD-cost:   14
c ---[ 236]---> BDD-cost:   14
c ---[ 235]---> BDD-cost:   14
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   14
c ---[ 232]---> BDD-cost:   14
c ---[ 231]---> BDD-cost:   14
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   14
c ---[ 227]---> BDD-cost:   14
c ---[ 226]---> BDD-cost:   14
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   14
c ---[ 223]---> BDD-cost:   14
c ---[ 222]---> BDD-cost:   14
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   12
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   15
c ---[ 216]---> BDD-cost:   17
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   13
c ---[ 207]---> BDD-cost:   14
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   17
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   12
c ---[ 199]---> BDD-cost:   15
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   17
c ---[ 193]---> BDD-cost:   17
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   15
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   17
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:   15
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:   19
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   12
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   15
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   16
c ---[ 167]---> BDD-cost:   14
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   19
c ---[ 164]---> BDD-cost:   18
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   12
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   12
c ---[ 159]---> BDD-cost:   15
c ---[ 158]---> BDD-cost:   17
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   15
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:   16
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   13
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   16
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   12
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   17
c ---[ 138]---> BDD-cost:   17
c ---[ 137]---> BDD-cost:   17
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   11
c ---[ 133]---> BDD-cost:   19
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   15
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   16
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   19
c ---[ 122]---> BDD-cost:   15
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   12
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:   17
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   17
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   11
c ---[ 113]---> BDD-cost:   16
c ---[ 112]---> BDD-cost:   15
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   16
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   16
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   16
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   15
c ---[  98]---> BDD-cost:   17
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   17
c ---[  93]---> BDD-cost:   16
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   16
c ---[  85]---> BDD-cost:   16
c ---[  84]---> BDD-cost:   16
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   16
c ---[  76]---> BDD-cost:   15
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   17
c ---[  71]---> BDD-cost:   15
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   15
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   11
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   16
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:   14
c ---[  52]---> BDD-cost:   14
c ---[  51]---> BDD-cost:   15
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   12
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   17
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   14
c ---[  40]---> BDD-cost:   14
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   14
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   15
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   15
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   16
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   17
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   15
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78212   272154 |   26070       0        0     nan |  0.000 % |
c |       101 |   77980   271366 |   28677      75      247     3.3 | 19.497 % |
c |       251 |   77966   271320 |   31544     222      730     3.3 | 19.509 % |
c |       476 |   77802   270768 |   34699     428     1401     3.3 | 19.677 % |
c |       813 |   77582   270030 |   38169     743     2484     3.3 | 19.913 % |
c |      1319 |   77178   268668 |   41985    1194     4041     3.4 | 20.313 % |
c |      2078 |   76765   267271 |   46184    1905     6449     3.4 | 20.734 % |
c |      3217 |   76203   265363 |   50803    2978    10331     3.5 | 21.296 % |
c |      4925 |   75989   264631 |   55883    4665    16822     3.6 | 21.499 % |
c |      7487 |   75957   264525 |   61471    7224    69128     9.6 | 21.533 % |
c |     11332 |   75846   264150 |   67618   11056    94033     8.5 | 21.651 % |
c |     17099 |   75782   263934 |   74380   16812   147906     8.8 | 21.701 % |
c |     25750 |   75718   263724 |   81818   25452   232315     9.1 | 21.763 % |
c |     38725 |   75639   263451 |   90000   38417   598948    15.6 | 21.842 % |
c |     58187 |   75381   262577 |   99000   57845   873365    15.1 | 22.117 % |
c |     87379 |   75117   261669 |  108900   87005  1636322    18.8 | 22.398 % |
c |    131169 |   74583   259847 |  119790   43275  1674772    38.7 | 22.961 % |
c |    196855 |   74402   259254 |  131770  108933  4481434    41.1 | 23.157 % |
c |    295381 |   74270   258826 |  144947   96470  2733398    28.3 | 23.304 % |
c ==============================================================================
c [1mFound solution: 5217606[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10447   maxlim: 3772019   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    429682 |  147188   519326 |   49062   90910  3286500    36.2 | 23.304 % |
c |    429782 |  147188   519326 |   53968   25097   229727     9.2 | 14.807 % |
c |    429933 |  147188   519326 |   59365   25248   230459     9.1 | 14.807 % |
c |    430158 |  147188   519326 |   65301   25473   231650     9.1 | 14.807 % |
c |    430495 |  147188   519326 |   71831   25810   233683     9.1 | 14.807 % |
c |    431001 |  147188   519326 |   79014   26316   237083     9.0 | 14.807 % |
c |    431761 |  147188   519326 |   86916   27076   256810     9.5 | 14.807 % |
c |    432900 |  147188   519326 |   95607   28215   278833     9.9 | 14.807 % |
c |    434608 |  147188   519326 |  105168   29923   291138     9.7 | 14.807 % |
c |    437170 |  147188   519326 |  115685   32485   329248    10.1 | 14.807 % |
c |    441014 |  147188   519326 |  127254   36329   368567    10.1 | 14.807 % |
c |    446780 |  147181   519303 |  139979   42094   432100    10.3 | 14.810 % |
c |    455429 |  147181   519303 |  153977   50743   527928    10.4 | 14.810 % |
c |    468404 |  147164   519242 |  169375   63716   681798    10.7 | 14.817 % |
c |    487865 |  147132   519134 |  186312   83173  1078753    13.0 | 14.839 % |
c ==============================================================================
c [1mFound solution: 5201169[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3788456   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    512343 |  147005   518808 |   49001  107628  2794905    26.0 | 14.839 % |
c |    512443 |  147005   518808 |   53901   23822  1170752    49.1 | 14.963 % |
c |    512593 |  147005   518808 |   59291   23972  1171433    48.9 | 14.963 % |
c |    512818 |  147005   518808 |   65220   24197  1172459    48.5 | 14.963 % |
c |    513155 |  147005   518808 |   71742   24534  1174324    47.9 | 14.963 % |
c |    513661 |  147005   518808 |   78916   25040  1176857    47.0 | 14.963 % |
c |    514420 |  147005   518808 |   86808   25799  1180383    45.8 | 14.963 % |
c |    515559 |  147005   518808 |   95489   26938  1188853    44.1 | 14.963 % |
c |    517267 |  147005   518808 |  105037   28646  1200445    41.9 | 14.963 % |
c |    519829 |  147005   518808 |  115541   31208  1223047    39.2 | 14.963 % |
c |    523673 |  147005   518808 |  127095   35052  1260654    36.0 | 14.963 % |
c |    529439 |  147005   518808 |  139805   40818  1312691    32.2 | 14.963 % |
c |    538088 |  146996   518777 |  153786   49466  1424544    28.8 | 14.966 % |
c |    551062 |  146965   518676 |  169164   62436  1564476    25.1 | 14.987 % |
c |    570523 |  146865   518350 |  186081   81883  1990718    24.3 | 15.055 % |
c ==============================================================================
c [1mFound solution: 5012876[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3976749   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    577536 |  146863   518446 |   48954   88893  2078540    23.4 | 15.055 % |
c |    577636 |  146863   518446 |   53849   25471   300979    11.8 | 15.097 % |
c |    577786 |  146863   518446 |   59234   25621   301723    11.8 | 15.097 % |
c |    578011 |  146863   518446 |   65157   25846   302914    11.7 | 15.097 % |
c |    578348 |  146863   518446 |   71673   26183   304637    11.6 | 15.097 % |
c |    578855 |  146854   518417 |   78840   26688   307403    11.5 | 15.104 % |
c |    579614 |  146854   518417 |   86724   27447   311891    11.4 | 15.104 % |
c |    580753 |  146854   518417 |   95397   28586   318224    11.1 | 15.104 % |
c |    582461 |  146854   518417 |  104937   30294   328995    10.9 | 15.104 % |
c |    585024 |  146845   518388 |  115430   32856   353896    10.8 | 15.111 % |
c |    588868 |  146845   518388 |  126974   36700   388236    10.6 | 15.111 % |
c |    594634 |  146845   518388 |  139671   42466   484011    11.4 | 15.111 % |
c |    603283 |  146845   518388 |  153638   51115   573441    11.2 | 15.111 % |
c |    616257 |  146836   518357 |  169002   64086  1241601    19.4 | 15.115 % |
c |    635718 |  146832   518347 |  185902   83546  4573727    54.7 | 15.119 % |
c ==============================================================================
c [1mFound solution: 4658593[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4331032   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    653961 |  146824   518406 |   48941  101779  4827670    47.4 | 15.119 % |
c |    654062 |  146824   518406 |   53835   28807   205395     7.1 | 15.155 % |
c |    654212 |  146824   518406 |   59218   28957   206719     7.1 | 15.155 % |
c |    654437 |  146824   518406 |   65140   29182   207902     7.1 | 15.155 % |
c |    654774 |  146824   518406 |   71654   29519   210053     7.1 | 15.155 % |
c |    655280 |  146824   518406 |   78819   30025   213481     7.1 | 15.155 % |
c |    656039 |  146824   518406 |   86701   30784   219393     7.1 | 15.155 % |
c |    657178 |  146824   518406 |   95372   31923   227645     7.1 | 15.155 % |
c |    658886 |  146824   518406 |  104909   33631   246749     7.3 | 15.155 % |
c |    661448 |  146824   518406 |  115400   36193   264674     7.3 | 15.155 % |
c |    665292 |  146824   518406 |  126940   40037   337472     8.4 | 15.155 % |
c |    671058 |  146824   518406 |  139634   45803   386642     8.4 | 15.155 % |
c |    679707 |  146824   518406 |  153597   54452   509087     9.3 | 15.155 % |
c |    692681 |  146817   518383 |  168957   67425   724991    10.8 | 15.159 % |
c |    712142 |  146799   518323 |  185853   86881  2847030    32.8 | 15.169 % |
c |    741334 |  146799   518323 |  204438  116073  4279361    36.9 | 15.169 % |
c ==============================================================================
c [1mFound solution: 3133796[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5855829   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    745102 |  146822   518508 |   48940  119841  4461556    37.2 | 15.169 % |
c |    745202 |  146822   518508 |   53834   22806   800824    35.1 | 15.201 % |
c |    745353 |  146822   518508 |   59217   22957   801498    34.9 | 15.201 % |
c |    745578 |  146822   518508 |   65139   23182   802280    34.6 | 15.201 % |
c |    745915 |  146822   518508 |   71653   23519   803617    34.2 | 15.201 % |
c |    746421 |  146822   518508 |   78818   24025   806012    33.5 | 15.201 % |
c |    747182 |  146822   518508 |   86700   24786   810361    32.7 | 15.201 % |
c |    748321 |  146822   518508 |   95370   25925   817005    31.5 | 15.201 % |
c |    750029 |  146822   518508 |  104907   27633   829441    30.0 | 15.201 % |
c |    752591 |  146822   518508 |  115397   30195   856276    28.4 | 15.201 % |
c |    756435 |  146822   518508 |  126937   34039   900733    26.5 | 15.201 % |
c |    762202 |  146818   518498 |  139631   39805   988498    24.8 | 15.204 % |
c |    770851 |  146795   518419 |  153594   48450  1155641    23.9 | 15.218 % |
c |    783827 |  146795   518419 |  168954   61426  1497398    24.4 | 15.218 % |
c |    803288 |  146795   518419 |  185849   80887  2082922    25.8 | 15.218 % |
c |    832481 |  146795   518419 |  204434  110080  2631630    23.9 | 15.218 % |
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 -Y0_bit0 -Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 -Y9_bit0 -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 -Y10_bit0 -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 Y11_bit0 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 Y12_bit0 -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 Y13_bit0 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 Y14_bit0 Y15_bit0 -Y16_bit0 -Y17_bit0 Y18_bit0 Y19_bit0 -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 Y20_bit0 -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 Y21_bit0 -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 Y22_bit0 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 Y23_bit0 -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 Y24_bit0 -Y25_bit0 Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 -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 Y30_bit0 -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 -Y31_bit0 -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 Y32_bit0 -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 Y33_bit0 -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 Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 -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 -Y40_bit0 -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 Y41_bit0 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 Y42_bit0 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 Y43_bit0 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 Y44_bit0 Y45_bit0 Y46_bit0 -Y47_bit0 -Y48_bit0 Y49_bit0 -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 Y50_bit0 -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 -Y51_bit0 -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 -Y52_bit0 -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 -Y53_bit0 -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 Y54_bit0 -Y55_bit0 Y56_bit0 -Y57_bit0 -Y58_bit0 Y59_bit0 -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 -Y60_bit0 -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 Y61_bit0 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 Y62_bit0 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 -Y63_bit0 -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 Y64_bit0 Y65_bit0 Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 -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 Y70_bit0 -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 -Y71_bit0 -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 -Y72_bit0 -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 -Y73_bit0 -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 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 -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 -Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 -Y106_bit0 Y107_bit0 -Y108_bit0 Y109_bit0 Y110_bit0 -Y111_bit0 Y112_bit0 Y113_bit0 -Y114_bit0 -Y115_bit0 Y116_bit0 Y117_bit0 -Y118_bit0 Y119_bit0 -Y120_bit0 Y121_bit0 Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 -Y126_bit0 Y127_bit0 -Y128_bit0 -Y129_bit0 Y130_bit0 Y131_bit0 Y132_bit0 -Y133_bit0 Y134_bit0 Y135_bit0 Y136_bit0 Y137_bit0 -Y138_bit0 Y139_bit0 Y140_bit0 -Y141_bit0 Y142_bit0 -Y143_bit0 Y144_bit0 Y145_bit0 -Y146_bit0 Y147_bit0 Y148_bit0 Y149_bit0 -Y150_bit0 -Y151_bit0 Y152_bit0 Y153_bit0 -Y154_bit0 Y155_bit0 Y156_bit0 Y157_bit0 Y158_bit0 Y159_bit0 Y160_bit0 -Y161_bit0 -Y162_bit0 -Y163_bit0 -Y164_bit0 -Y165_bit0 -Y166_bit0 Y167_bit0 Y168_bit0 Y169_bit0 -Y170_bit0 Y171_bit0 Y172_bit0 -Y173_bit0 Y174_bit0 Y175_bit0 -Y176_bit0 Y177_bit0 -Y178_bit0 -Y179_bit0 -Y180_bit0 -Y181_bit0 -Y182_bit0 -Y183_bit0 Y184_bit0 -Y185_bit0 -Y186_bit0 Y187_bit0 Y188_bit0 -Y189_bit0 -Y190_bit0 Y191_bit0 -Y192_bit0 -Y193_bit0 Y194_bit0 Y195_bit0 -Y196_bit0 Y197_bit0 -Y198_bit0 -Y199_bit0 -Y200_bit0 Y201_bit0 Y202_bit0 -Y203_bit0 -Y204_bit0 Y205_bit0 -Y206_bit0 Y207_bit0 Y208_bit0 Y209_bit0 Y210_bit0 Y211_bit0 Y212_bit0 -Y213_bit0 Y214_bit0 -Y215_bit0 -Y216_bit0 -Y217_bit0 -Y218_bit0 -Y219_bit0 Y220_bit0 Y221_bit0 Y222_bit0 Y223_bit0 -Y224_bit0 Y225_bit0 Y22#### 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.75 0.94 0.91 2/54 17396
Raw data (stat): 17396 (runsolver) R 17395 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 468302204 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.79 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 2034 0 0 0 993 5 0 0 25 0 1 0 468302204 10833920 2001 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2645 2001 603 41 0 2604 0
vsize: 10580
[startup+20.0021 s]
Raw data (loadavg): 0.82 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 2190 0 0 0 1993 6 0 0 25 0 1 0 468302204 11567104 2157 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2824 2157 603 41 0 2783 0
vsize: 11296
[startup+30.0061 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 2358 0 0 0 2992 7 0 0 25 0 1 0 468302204 12275712 2325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2997 2325 603 41 0 2956 0
vsize: 11988
[startup+40.0066 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 2574 0 0 0 3991 8 0 0 25 0 1 0 468302204 13086720 2541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3195 2541 603 41 0 3154 0
vsize: 12780
[startup+50.0075 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 3131 0 0 0 4990 9 0 0 25 0 1 0 468302204 15511552 3098 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3787 3098 603 41 0 3746 0
vsize: 15148
[startup+60.0082 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 3358 0 0 0 5989 10 0 0 25 0 1 0 468302204 16322560 3325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3325 603 41 0 3944 0
vsize: 15940
[startup+70.009 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 3593 0 0 0 6987 11 0 0 25 0 1 0 468302204 17268736 3560 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4216 3560 603 41 0 4175 0
vsize: 16864
[startup+80.0098 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 3964 0 0 0 7986 13 0 0 25 0 1 0 468302204 19005440 3931 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4640 3931 603 41 0 4599 0
vsize: 18560
[startup+90.0106 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 4144 0 0 0 8985 14 0 0 25 0 1 0 468302204 19816448 4111 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4838 4111 603 41 0 4797 0
vsize: 19352
[startup+100.011 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 4612 0 0 0 9983 15 0 0 25 0 1 0 468302204 21569536 4579 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5266 4579 603 41 0 5225 0
vsize: 21064
[startup+110.012 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 4812 0 0 0 10983 15 0 0 25 0 1 0 468302204 22376448 4779 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5463 4779 603 41 0 5422 0
vsize: 21852
[startup+120.013 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 5203 0 0 0 11981 17 0 0 25 0 1 0 468302204 23994368 5170 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5858 5170 603 41 0 5817 0
vsize: 23432
[startup+130.013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 5381 0 0 0 12981 18 0 0 25 0 1 0 468302204 24670208 5348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6023 5348 603 41 0 5982 0
vsize: 24092
[startup+140.013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 5468 0 0 0 13980 18 0 0 25 0 1 0 468302204 25075712 5435 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6122 5435 603 41 0 6081 0
vsize: 24488
[startup+150.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 5468 0 0 0 14980 18 0 0 25 0 1 0 468302204 25075712 5435 4294967295 134512640 134672761 3221224544 3221223680 134566155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6122 5435 603 41 0 6081 0
vsize: 24488
[startup+160.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 5468 0 0 0 15980 18 0 0 25 0 1 0 468302204 25075712 5435 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6122 5435 603 41 0 6081 0
vsize: 24488
[startup+170.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 6531 0 0 0 16977 21 0 0 25 0 1 0 468302204 29392896 6498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7176 6498 603 41 0 7135 0
vsize: 28704
[startup+180.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 7000 0 0 0 17975 23 0 0 25 0 1 0 468302204 31272960 6967 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7635 6967 603 41 0 7594 0
vsize: 30540
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 7293 0 0 0 18974 24 0 0 25 0 1 0 468302204 32485376 7260 4294967295 134512640 134672761 3221224544 3221223544 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7931 7260 603 41 0 7890 0
vsize: 31724
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 7473 0 0 0 19974 24 0 0 25 0 1 0 468302204 33292288 7440 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8128 7440 603 41 0 8087 0
vsize: 32512
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 7643 0 0 0 20974 25 0 0 25 0 1 0 468302204 33968128 7610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8293 7610 603 41 0 8252 0
vsize: 33172
[startup+220.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 7990 0 0 0 21974 26 0 0 25 0 1 0 468302204 35303424 7957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8619 7957 603 41 0 8578 0
vsize: 34476
[startup+230.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 8297 0 0 0 22973 27 0 0 25 0 1 0 468302204 36651008 8264 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8948 8264 603 41 0 8907 0
vsize: 35792
[startup+240.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 8746 0 0 0 23972 28 0 0 25 0 1 0 468302204 38395904 8713 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9374 8713 603 41 0 9333 0
vsize: 37496
[startup+250.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9159 0 0 0 24971 29 0 0 25 0 1 0 468302204 40538112 9126 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9897 9126 603 41 0 9856 0
vsize: 39588
[startup+260.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 25971 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+270.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 26971 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 27972 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 28972 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 29972 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223792 134562289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 30972 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 31972 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 32973 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 33973 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9224 0 0 0 34973 29 0 0 25 0 1 0 468302204 40808448 9191 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9963 9191 603 41 0 9922 0
vsize: 39852
[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 9873 0 0 0 35972 31 0 0 25 0 1 0 468302204 43511808 9840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10623 9840 603 41 0 10582 0
vsize: 42492
[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 11254 0 0 0 36969 34 0 0 25 0 1 0 468302204 49168384 11221 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12004 11221 603 41 0 11963 0
vsize: 48016
[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12459 0 0 0 37966 37 0 0 25 0 1 0 468302204 54169600 12426 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13225 12427 603 41 0 13184 0
vsize: 52900
[startup+390.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 38967 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+400.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 39968 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+410.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 40968 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+420.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 41968 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+430.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 42968 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+440.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 43969 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+450.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 44969 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+460.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 12985 0 0 0 45969 38 0 0 25 0 1 0 468302204 56324096 12952 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13751 12952 603 41 0 13710 0
vsize: 55004
[startup+470.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17195 0 0 0 46959 48 0 0 25 0 1 0 468302204 68546560 15828 4294967295 134512640 134672761 3221224544 3221223844 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16735 15828 603 41 0 16694 0
vsize: 66940
[startup+480.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17199 0 0 0 47958 48 0 0 25 0 1 0 468302204 68546560 15832 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15832 603 41 0 16694 0
vsize: 66940
[startup+490.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17202 0 0 0 48958 48 0 0 25 0 1 0 468302204 68546560 15835 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15835 603 41 0 16694 0
vsize: 66940
[startup+500.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17203 0 0 0 49958 49 0 0 25 0 1 0 468302204 68546560 15836 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15836 603 41 0 16694 0
vsize: 66940
[startup+510.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17203 0 0 0 50958 49 0 0 25 0 1 0 468302204 68546560 15836 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15836 603 41 0 16694 0
vsize: 66940
[startup+520.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17204 0 0 0 51957 49 0 0 25 0 1 0 468302204 68546560 15837 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15837 603 41 0 16694 0
vsize: 66940
[startup+530.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17204 0 0 0 52957 49 0 0 25 0 1 0 468302204 68546560 15837 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15837 603 41 0 16694 0
vsize: 66940
[startup+540.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17204 0 0 0 53957 50 0 0 25 0 1 0 468302204 68546560 15837 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15837 603 41 0 16694 0
vsize: 66940
[startup+550.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 54956 50 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134564708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+560.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 55956 51 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+570.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 56956 51 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+580.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 57956 51 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+590.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 58956 51 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+600.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 59955 52 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+610.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17205 0 0 0 60955 52 0 0 25 0 1 0 468302204 68546560 15838 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15838 603 41 0 16694 0
vsize: 66940
[startup+620.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 61954 52 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+630.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 62954 53 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+640.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 63954 53 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+650.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 64954 53 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+660.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 65953 53 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+670.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 66953 53 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+680.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 67953 54 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+690.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 68952 54 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+700.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 69952 54 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+710.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 70952 55 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+720.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 71951 55 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+730.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 72951 55 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+740.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17241 0 0 0 73950 55 0 0 25 0 1 0 468302204 68546560 15874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15874 603 41 0 16694 0
vsize: 66940
[startup+750.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 74950 56 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+760.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 75950 56 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+770.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 76949 57 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+780.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 77949 57 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+790.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 78949 57 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+800.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 79948 58 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+810.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 80938 58 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+820.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 81937 58 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+830.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 82937 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+840.096 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 83937 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+850.097 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 84937 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+860.098 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 85936 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+870.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 86936 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+880.099 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 87936 59 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+890.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17243 0 0 0 88936 60 0 0 25 0 1 0 468302204 68546560 15876 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16735 15876 603 41 0 16694 0
vsize: 66940
[startup+900.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 89935 60 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+910.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 90934 61 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+920.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 91934 61 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+930.102 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 92934 61 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+940.103 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 93933 62 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+950.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 94933 62 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+960.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 95933 62 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+970.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 96933 62 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+980.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 97932 62 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+990.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 98932 63 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 99932 63 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 100931 63 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 101931 63 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 102931 63 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17336 0 0 0 103930 64 0 0 25 0 1 0 468302204 68620288 15898 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15898 603 41 0 16712 0
vsize: 67012
[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 104930 64 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 105930 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 106930 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 107930 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 108931 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1100.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 109933 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1110.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 110933 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1120.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 111933 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 112934 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 113935 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 114935 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1160.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 115935 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1170.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 116936 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1180.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17381 0 0 0 117936 65 0 0 25 0 1 0 468302204 68620288 15901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15901 603 41 0 16712 0
vsize: 67012
[startup+1190.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17382 0 0 0 118937 65 0 0 25 0 1 0 468302204 68620288 15902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15902 603 41 0 16712 0
vsize: 67012
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17396
Raw data (stat): 17396 (minisat+) R 17395 26667 26666 0 -1 0 17382 0 0 0 119937 65 0 0 25 0 1 0 468302204 68620288 15902 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16753 15902 603 41 0 16712 0
vsize: 67012
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 17396
Raw data (stat): 17396 (minisat+) Z 17395 26667 26666 0 -1 12 17385 0 0 0 119938 68 0 0 25 0 1 0 468302204 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.21
CPU time (s): 1200.06
CPU user time (s): 1199.38
CPU system time (s): 0.682896
CPU usage (%): 99.9876
Max. virtual memory (Kb): 67012
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####