PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran14x18.opb
MD5SUM	a7baaeaa26a0026c630e11c495604909
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1091178
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	1175.08
Number of variables	5292
Total number of constraints	284
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	21
Maximum length of a constraint	360
Trace number 17640

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        568304 kB
Buffers:         34332 kB
Cached:         410288 kB
SwapCached:        440 kB
Active:         152448 kB
Inactive:       294276 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        568052 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14024 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:23:08 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 19303 7 1200.19 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   78541   276437 |   23562       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13898          
c   -- var.elim.:  2000/13898          
c   -- var.elim.:  3000/13898          
c   -- var.elim.:  4000/13898          
c   -- var.elim.:  5000/13898          
c   -- var.elim.:  6000/13898          
c   -- var.elim.:  7000/13898          
c   -- var.elim.:  8000/13898          
c   -- var.elim.:  9000/13898          
c   -- var.elim.:  10000/13898          
c   -- var.elim.:  11000/13898          
c   -- var.elim.:  12000/13898          
c   -- var.elim.:  13000/13898          
c   -- var.elim.:  13898/13898          
c   -- var.elim.:  1000/2533          
c   -- var.elim.:  2000/2533          
c   -- var.elim.:  2533/2533          
c   -- subsuming                       
c   -- var.elim.:  1000/1426          
c   -- var.elim.:  1426/1426          
c   -- var.elim.:  1000/1257          
c   -- var.elim.:  1257/1257          
c   -- subsuming                       
c |         0 |   69220   237556 |      --       0       --      -- |     --   | -7181/-25656
c |         0 |   69220   237556 |   27688       0        0     nan |  0.000 % |
c |       100 |   69220   237556 |   30456     100      326     3.3 | 25.104 % |
c |       250 |   69210   237521 |   33497     249      815     3.3 | 25.110 % |
c |       475 |   69210   237521 |   36847     474     1538     3.2 | 25.110 % |
c |       812 |   69210   237521 |   40532     811     2645     3.3 | 25.110 % |
c |      1318 |   69210   237521 |   44585    1317     4307     3.3 | 25.110 % |
c |      2078 |   69210   237521 |   49043    2077     6897     3.3 | 25.110 % |
c |      3217 |   69200   237486 |   53940    3215    11152     3.5 | 25.116 % |
c |      4925 |   69200   237486 |   59334    4923    19913     4.0 | 25.116 % |
c |      7488 |   69200   237486 |   65267    7486    41286     5.5 | 25.116 % |
c |     11332 |   69190   237451 |   71784   11329   133895    11.8 | 25.122 % |
c |     17098 |   69190   237451 |   78962   17095   194978    11.4 | 25.122 % |
c |     25747 |   69190   237451 |   86859   25744   333948    13.0 | 25.122 % |
c |     38721 |   69190   237451 |   95545   38718   704787    18.2 | 25.122 % |
c |     58184 |   69190   237451 |  105099   58181  1440112    24.8 | 25.122 % |
c |     87377 |   69149   237309 |  115541   87371  3077870    35.2 | 25.152 % |
c |    131166 |   69087   237095 |  126981   27727   901156    32.5 | 25.200 % |
c |    196851 |   69046   236953 |  139596   93410  1981275    21.2 | 25.230 % |
c ==============================================================================
c (current CPU-time: 235.852 s)
c ==============================================================================
c [1mFound solution: 5490968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10447   maxlim: 3498657   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    213421 |  142025   497608 |   42607  109978  2414454    22.0 | 25.230 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13607          
c   -- var.elim.:  2000/13607          
c   -- var.elim.:  3000/13607          
c   -- var.elim.:  4000/13607          
c   -- var.elim.:  5000/13607          
c   -- var.elim.:  6000/13607          
c   -- var.elim.:  7000/13607          
c   -- var.elim.:  8000/13607          
c   -- var.elim.:  9000/13607          
c   -- var.elim.:  10000/13607          
c   -- var.elim.:  11000/13607          
c   -- var.elim.:  12000/13607          
c   -- var.elim.:  13000/13607          
c   -- var.elim.:  13607/13607          
c   -- var.elim.:  55/55          
c |    213421 |  141923   497140 |      --  109978       --      -- |     --   | -102/-458
c |    213421 |  141923   497140 |   56769  109968  2414395    22.0 | 25.230 % |
c |    213521 |  141923   497140 |   62446   27583   373994    13.6 | 15.557 % |
c |    213671 |  141923   497140 |   68690   27733   374592    13.5 | 15.557 % |
c |    213896 |  141923   497140 |   75559   27958   375633    13.4 | 15.557 % |
c |    214233 |  141923   497140 |   83115   28295   377151    13.3 | 15.557 % |
c |    214739 |  141923   497140 |   91427   28801   379636    13.2 | 15.557 % |
c |    215499 |  141923   497140 |  100570   29561   383779    13.0 | 15.557 % |
c |    216638 |  141923   497140 |  110627   30700   390280    12.7 | 15.557 % |
c |    218346 |  141923   497140 |  121689   32408   400908    12.4 | 15.557 % |
c |    220908 |  141923   497140 |  133858   34970   419023    12.0 | 15.557 % |
c |    224753 |  141923   497140 |  147244   38815   456621    11.8 | 15.557 % |
c |    230519 |  141923   497140 |  161969   44581   553688    12.4 | 15.557 % |
c |    239168 |  141892   497033 |  178127   53229   647659    12.2 | 15.572 % |
c |    252142 |  141892   497033 |  195939   66203   917362    13.9 | 15.572 % |
c |    271604 |  141819   496771 |  215422   85660  1199472    14.0 | 15.598 % |
c ==============================================================================
c (current CPU-time: 380.797 s)
c ==============================================================================
c [1mFound solution: 5112400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3877225   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    284600 |  141896   497159 |   42568   98656  1500337    15.2 | 15.598 % |
c   -- subsuming                       
c   -- var.elim.:  127/127          
c   -- var.elim.:  37/37          
c |    284600 |  141874   497059 |      --   98656       --      -- |     --   | -22/-90
c |    284600 |  141874   497059 |   56749   98651  1500322    15.2 | 15.598 % |
c |    284700 |  141874   497059 |   62424   25516   335847    13.2 | 15.626 % |
c |    284851 |  141874   497059 |   68667   25667   336571    13.1 | 15.626 % |
c |    285076 |  141874   497059 |   75533   25892   337538    13.0 | 15.626 % |
c |    285413 |  141874   497059 |   83087   26229   339079    12.9 | 15.626 % |
c |    285919 |  141874   497059 |   91395   26735   341649    12.8 | 15.626 % |
c |    286678 |  141874   497059 |  100535   27494   345441    12.6 | 15.627 % |
c |    287817 |  141874   497059 |  110588   28633   352023    12.3 | 15.626 % |
c |    289525 |  141874   497059 |  121647   30341   360783    11.9 | 15.626 % |
c |    292088 |  141874   497059 |  133812   32904   377051    11.5 | 15.626 % |
c |    295932 |  141874   497059 |  147193   36748   414903    11.3 | 15.626 % |
c |    301698 |  141874   497059 |  161913   42514   472830    11.1 | 15.626 % |
c |    310347 |  141863   497022 |  178090   51162   556532    10.9 | 15.630 % |
c |    323322 |  141853   496987 |  195886   64136   694319    10.8 | 15.634 % |
c |    342783 |  141831   496904 |  215441   83594  1147434    13.7 | 15.641 % |
c |    371976 |  141831   496904 |  236985  112787  4866122    43.1 | 15.641 % |
c ==============================================================================
c (current CPU-time: 544.348 s)
c ==============================================================================
c [1mFound solution: 3892852[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 5096773   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    377644 |  141850   497054 |   42554  118452  4932063    41.6 | 15.641 % |
c   -- subsuming                       
c   -- var.elim.:  102/102          
c   -- var.elim.:  28/28          
c |    377644 |  141839   496958 |      --  118452       --      -- |     --   | -11/-85
c |    377644 |  141839   496958 |   56735  118437  4931792    41.6 | 15.641 % |
c |    377744 |  141839   496958 |   62409   23874  1109037    46.5 | 15.692 % |
c |    377894 |  141839   496958 |   68650   24024  1109578    46.2 | 15.692 % |
c |    378119 |  141839   496958 |   75515   24249  1110433    45.8 | 15.692 % |
c |    378456 |  141839   496958 |   83066   24586  1111749    45.2 | 15.692 % |
c |    378962 |  141839   496958 |   91373   25092  1113814    44.4 | 15.692 % |
c |    379721 |  141839   496958 |  100510   25851  1117190    43.2 | 15.692 % |
c |    380860 |  141839   496958 |  110561   26990  1122590    41.6 | 15.692 % |
c |    382568 |  141839   496958 |  121617   28698  1131167    39.4 | 15.692 % |
c |    385130 |  141839   496958 |  133779   31260  1149316    36.8 | 15.692 % |
c |    388974 |  141839   496958 |  147157   35104  1179342    33.6 | 15.692 % |
c |    394740 |  141839   496958 |  161873   40870  1220053    29.9 | 15.692 % |
c |    403389 |  141839   496958 |  178060   49519  1290851    26.1 | 15.692 % |
c |    416363 |  141829   496923 |  195852   62491  1472783    23.6 | 15.696 % |
c |    435824 |  141829   496923 |  215438   81952  1734540    21.2 | 15.696 % |
c |    465016 |  141806   496838 |  236943  111141  2698388    24.3 | 15.703 % |
c |    508805 |  141794   496790 |  260615  154927  4292527    27.7 | 15.707 % |
c ==============================================================================
c (current CPU-time: 813.346 s)
c ==============================================================================
c [1mFound solution: 3768043[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5221582   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    524399 |  141823   497035 |   42546  170518  4697377    27.5 | 15.707 % |
c   -- subsuming                       
c   -- var.elim.:  83/83          
c   -- var.elim.:  28/28          
c |    524399 |  141806   496948 |      --  170518       --      -- |     --   | -17/-75
c |    524399 |  141806   496948 |   56722  169520  4644091    27.4 | 15.707 % |
c |    524499 |  141806   496948 |   62394   29558   416015    14.1 | 15.748 % |
c |    524650 |  141806   496948 |   68634   29709   416811    14.0 | 15.748 % |
c |    524875 |  141806   496948 |   75497   29934   417783    14.0 | 15.748 % |
c |    525213 |  141806   496948 |   83047   30272   419455    13.9 | 15.748 % |
c |    525719 |  141806   496948 |   91351   30778   422304    13.7 | 15.748 % |
c |    526478 |  141806   496948 |  100487   31537   427211    13.5 | 15.748 % |
c |    527617 |  141806   496948 |  110535   32676   435393    13.3 | 15.748 % |
c |    529325 |  141806   496948 |  121589   34384   445784    13.0 | 15.748 % |
c |    531887 |  141806   496948 |  133748   36946   466208    12.6 | 15.748 % |
c |    535731 |  141806   496948 |  147123   40790   499836    12.3 | 15.748 % |
c |    541497 |  141806   496948 |  161835   46556   567245    12.2 | 15.748 % |
c |    550146 |  141806   496948 |  178019   55205   651669    11.8 | 15.748 % |
c |    563120 |  141806   496948 |  195821   68179   855693    12.6 | 15.748 % |
c |    582581 |  141806   496948 |  215403   87640  1383653    15.8 | 15.748 % |
c |    611773 |  141806   496948 |  236943  116832  2479398    21.2 | 15.748 % |
c ==============================================================================
c (current CPU-time: 1013.34 s)
c ==============================================================================
c [1mFound solution: 3565403[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5424222   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    639228 |  141840   497209 |   42551  144287  3749098    26.0 | 15.748 % |
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  22/22          
c |    639228 |  141816   496970 |      --  144287       --      -- |     --   | -4/-8
c |    639228 |  141816   496970 |   56726  144287  3749098    26.0 | 15.748 % |
c |    639329 |  141816   496970 |   62399   28286   514674    18.2 | 15.780 % |
c |    639479 |  141816   496970 |   68638   28436   515326    18.1 | 15.780 % |
c |    639704 |  141816   496970 |   75502   28661   516321    18.0 | 15.780 % |
c |    640041 |  141816   496970 |   83053   28998   517956    17.9 | 15.780 % |
c |    640547 |  141816   496970 |   91358   29504   520573    17.6 | 15.780 % |
c |    641306 |  141816   496970 |  100494   30263   524512    17.3 | 15.780 % |
c |    642445 |  141816   496970 |  110543   31402   531356    16.9 | 15.780 % |
c |    644153 |  141816   496970 |  121598   33110   541383    16.4 | 15.780 % |
c |    646715 |  141816   496970 |  133757   35672   556526    15.6 | 15.780 % |
c |    650559 |  141816   496970 |  147133   39516   593847    15.0 | 15.780 % |
c |    656325 |  141816   496970 |  161847   45282   635201    14.0 | 15.780 % |
c |    664974 |  141816   496970 |  178031   53931   720410    13.4 | 15.780 % |
c |    677948 |  141816   496970 |  195834   66905   859083    12.8 | 15.780 % |
c |    697412 |  141816   496970 |  215418   86369  1417156    16.4 | 15.780 % |
c ==============================================================================
c (current CPU-time: 1153.15 s)
c ==============================================================================
c [1mFound solution: 2833164[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6156461   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    707819 |  141848   497203 |   42554   96776  1674371    17.3 | 15.780 % |
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  24/24          
c |    707819 |  141836   497145 |      --   96776       --      -- |     --   | -12/-46
c |    707819 |  141836   497145 |   56734   96776  1674371    17.3 | 15.780 % |
c |    707919 |  141836   497145 |   62407   24470   424927    17.4 | 15.818 % |
c |    708069 |  141836   497145 |   68648   24620   425573    17.3 | 15.818 % |
c |    708294 |  141836   497145 |   75513   24845   426669    17.2 | 15.818 % |
c |    708631 |  141836   497145 |   83064   25182   428733    17.0 | 15.818 % |
c |    709137 |  141836   497145 |   91371   25688   431662    16.8 | 15.818 % |
c |    709896 |  141836   497145 |  100508   26447   435775    16.5 | 15.818 % |
c |    711035 |  141836   497145 |  110559   27586   441532    16.0 | 15.818 % |
c |    712743 |  141836   497145 |  121615   29294   450995    15.4 | 15.818 % |
c |    715305 |  141836   497145 |  133776   31856   474171    14.9 | 15.818 % |
c |    719150 |  141836   497145 |  147154   35701   505634    14.2 | 15.818 % |
c |    724916 |  141836   497145 |  161869   41467   555234    13.4 | 15.818 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 X2_bit_6 -X2_bit_5 X2_bit_4 -X2_bit_3 X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 X4_bit_6 -X4_bit_5 -X4_bit_4 X4_bit_3 X4_bit_2 -X4_bit_1 X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 X6_bit_6 X6_bit_5 X6_bit_4 X6_bit_3 -X6_bit_2 X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 X7_bit_7 -X7_bit_6 X7_bit_5 -X7_bit_4 X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 X10_bit_6 X10_bit_5 -X10_bit_4 -X10_bit_3 X10_bit_2 X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 X11_bit_6 X11_bit_5 -X11_bit_4 -X11_bit_3 X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 X12_bit_4 X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 -X17_bit_6 X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 X19_bit_6 X19_bit_5 X19_bit_4 X19_bit_3 X19_bit_2 -X19_bit_1 X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 X20_bit_6 -X20_bit_5 X20_bit_4 -X20_bit_3 -X20_bit_2 X20_bit_1 X20_bit0 X20_bit1 X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 X28_bit_7 X28_bit_6 X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 X29_bit_6 X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 X29_bit_1 -X29_bit0 X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 -X31_bit_6 -X31_bit_5 X31_bit_4 -X31_bit_3 X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 X34_bit_6 -X34_bit_5 -X34_bit_4 X34_bit_3 -X34_bit_2 X34_bit_1 X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 X35_bit_2 X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 X37_bit_4 X37_bit_3 X37_bit_2 X37_bit_1 X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 X38_bit_3 -X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 X40_bit_1 X40_bit0 X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 X43_bit_3 -X43_bit_2 X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 X44_bit_3 -X44_bit_2 X44_bit_1 -X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 X45_bit_1 X45_bit0 X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 X46_bit0 X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 X55_bit_7 -X55_bit_6 X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 -X58_bit_6 X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 X58_bit_1 X58_bit0 X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 -X60_bit_6 X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 -X63_bit_6 X63_bit_5 X63_bit_4 -X63_bit_3 X63_bit_2 X63_bit_1 -X63_bit0 X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 X65_bit_5 X65_bit_4 -X65_bit_3 X65_bit_2 X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 -X78_bit_6 X78_bit_5 X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 -X80_bit_6 X80_bit_5 X80_bit_4 -X80_bit_3 X80_bit_2 -X80_bit_1 X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 X84_bit_3 X84_bit_2 X84_bit_1 X84_bit0 X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 X85_bit0 X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 X86_bit_3 -X86_bit_2 X86_bit_1 -X86_bit0 -X86_bit1 X86_bit2 X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 X88_bit_3 -X88_bit_2 X88_bit_1 -X88_bit0 X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 X89_bit_1 -X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 -X90_bit_6 X90_bit_5 -X90_bit_4 -X90_bit_3 X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 X96_bit_6 X96_bit_5 X96_bit_4 X96_bit_3 X96_bit_2 -X96_bit_1 X96_bit0 X96_bit1 X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 X97_bit_6 X97_bit_5 -X97_bit_4 X97_bit_3 -X97_bit_2 -X97_bit_1 X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 -X98_bit_6 -X98_bit_5 X98_bit_4 -X98_bit_3 X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 X100_bit_7 X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 X102_bit_7 X102_bit_6 -X102_bit_5 X102_bit_4 -X102_bit_3 X102_bit_2 X102_bit_1 X102_bit0 X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 X103_bit_7 X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 X103_bit_2 X103_bit_1 X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 -X105_bit_6 X105_bit_5 X105_bit_4 X105_bit_3 X105_bit_2 X105_bit_1 X105_bit0 X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 -X106_bit_6 X106_bit_5 X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 X108_bit_6 -X108_bit_5 X108_bit_4 X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 X111_bit_5 -X111_bit_4 X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 X112_bit_5 X112_bit_4 X112_bit_3 X112_bit_2 X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 X114_bit_6 X114_bit_5 X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 X115_bit_2 -X115_bit_1 X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 -X116_bit_6 X116_bit_5 X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 X117_bit_6 X117_bit_5 -X117_bit_4 X117_bit_3 X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 X122_bit_7 X122_bit_6 X122_bit_5 X122_bit_4 X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 X124_bit_7 -X124_bit_6 -X124_bit_5 X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 X124_bit0 X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 X125_bit_7 -X125_bit_6 -X125_bit_5 X125_bit_4 X125_bit_3 X125_bit_2 -X125_bit_1 X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 X126_bit_6 -X126_bit_5 X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 X127_bit_7 X127_bit_6 -X127_bit_5 X127_bit_4 -X127_bit_3 X127_bit_2 X127_bit_1 X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 X132_bit_6 X132_bit_5 X132_bit_4 X132_bit_3 -X132_bit_2 X132_bit_1 X132_bit0 X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 X136_bit_5 X136_bit_4 X136_bit_3 -X136_bit_2 X136_bit_1 X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 -X137_bit_6 X137_bit_5 X137_bit_4 X137_bit_3 X137_bit_2 -X137_bit_1 X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 X139_bit_7 X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 X140_bit_7 X140_bit_6 X140_bit_5 X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 X140_bit1 X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 X147_bit_5 X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 X148_bit_5 X148_bit_4 X148_bit_3 X148_bit_2 X148_bit_1 X148_bit0 X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 X152_bit_6 -X152_bit_5 X152_bit_4 -X152_bit_3 -X152_bit_2 X152_bit_1 -X152_bit0 X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 X157_bit_6 X157_bit_5 X157_bit_4 -X157_bit_3 X157_bit_2 -X157_bit_1 -X157_bit0 X157_bit1 -X157_bit2 X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 X162_bit_6 X162_bit_5 X162_bit_4 -X162_bit_3 -X162_bit_2 X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 X163_bit_6 -X163_bit_5 X163_bit_4 -X163_bit_3 X163_bit_2 X163_bit_1 X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 X166_bit_4 X166_bit_3 X166_bit_2 X166_bit_1 X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 X168_bit_7 X168_bit_6 X168_bit_5 X168_bit_4 X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 X168_bit1 X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 X169_bit_4 X169_bit_3 X169_bit_2 -X169_bit_1 -X169_bit0 X169_bit1 X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 X170_bit_7 X170_bit_6 X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 X170_bit0 X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 X173_bit_7 -X173_bit_6 X173_bit_5 -X173_bit_4 -X173_bit_3 X173_bit_2 -X173_bit_1 -X173_bit0 X173_bit1 X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 X175_bit0 X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 X176_bit_6 -X176_bit_5 X176_bit_4 -X176_bit_3 -X176_bit_2 X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 -X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 -X180_bit_6 X180_bit_5 X180_bit_4 -X180_bit_3 X180_bit_2 X180_bit_1 -X180_bit0 X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 X181_bit_7 -X181_bit_6 -X181_bit_5 X181_bit_4 -X181_bit_3 X181_bit_2 X181_bit_1 X181_bit0 X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 X183_bit_4 -X183_bit_3 -X183_bit_2 X183_bit_1 -X183_bit0 X183_bit1 X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 -X184_bit_6 -X184_bit_5 X184_bit_4 X184_bit_3 -X184_bit_2 X184_bit_1 X184_bit0 X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 X191_bit_5 X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 -X194_bit_5 X194_bit_4 -X194_bit_3 -X194_bit_2 X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 X197_bit_7 X197_bit_6 X197_bit_5 X197_bit_4 -X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 X204_bit_7 -X204_bit_6 -X204_bit_5 X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 -X208_bit_6 -X208_bit_5 -X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 X213_bit_6 -X213_bit_5 -X213_bit_4 X213_bit_3 X213_bit_2 X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 X216_bit_6 X216_bit_5 -X216_bit_4 X216_bit_3 X216_bit_2 X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 X218_bit_5 X218_bit_4 X218_bit_3 X218_bit_2 -X218_bit_1 X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 X219_bit_6 X219_bit_5 X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 -X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 X222_bit_7 -X222_bit_6 X222_bit_5 X222_bit_4 X222_bit_3 X222_bit_2 X222_bit_1 -X222_bit0 X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 X223_bit_7 -X223_bit_6 X223_bit_5 X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 X225_bit_5 X225_bit_4 X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 X226_bit_7 X226_bit_6 -X226_bit_5 X226_bit_4 -X226_bit_3 -X226_bit_2 X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 X227_bit_7 X227_bit_6 X227_bit_5 -X227_bit_4 -X227_bit_3 -X227_bit_2 X227_bit_1 -X227_bit0 -X227_bit1 X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 -X228_bit_5 X228_bit_4 -X228_bit_3 X228_bit_2 X228_bit_1 X228_bit0 X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 -X230_bit_6 -X230_bit_5 -X230_bit_4 -X230_bit_3 -X230_bit_2 -X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 X233_bit_5 X233_bit_4 X233_bit_3 -X233_bit_2 -X233_bit_1 X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 X234_bit_6 X234_bit_5 X234_bit_4 X234_bit_3 X234_bit_2 X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 X235_bit_6 X235_bit_5 X235_bit_4 X235_bit_3 X235_bit_2 X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 -X236_bit_5 X236_bit_4 X236_bit_3 X236_bit_2 X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 X237_bit_6 X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 X240_bit_7 X240_bit_6 X240_bit_5 X240_bit_4 X240_bit_3 X240_bit_2 X240_bit_1 -X240_bit0 -X240_bit1 X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 X241_bit_6 -X241_bit_5 X241_bit_4 X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 -X242_bit_5 X242_bit_4 -X242_bit_3 X242_bit_2 X242_bit_1 -X242_bit0 -X242_bit1 X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 -X244_bit_6 X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 X245_bit_6 X245_bit_5 X245_bit_4 -X245_bit_3 X245_bit_2 X245_bit_1 X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 X246_bit_2 X246_bit_1 X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 X247_bit_6 -X247_bit_5 X247_bit_4 -X247_bit_3 X247_bit_2 X247_bit_1 X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 X248_bit_5 X248_bit_4 X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 X250_bit_4 X250_bit_3 X250_bit_2 -X250_bit_1 X250_bit0 X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 X251_bit_5 X251_bit_4 -X251_bit_3 X251_bit_2 -X251_bit_1 #### 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.86 0.97 0.95 2/54 7283
Raw data (stat): 7283 (runsolver) R 7282 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486344073 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.0002 s]
Raw data (loadavg): 0.88 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 3662 0 0 0 988 10 0 0 25 0 1 0 486344073 16592896 3192 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4051 3192 603 41 0 4010 0
vsize: 16204
[startup+20.0001 s]
Raw data (loadavg): 0.90 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 3949 0 0 0 1987 10 0 0 25 0 1 0 486344073 17956864 3479 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3479 603 41 0 4343 0
vsize: 17536
[startup+30.0011 s]
Raw data (loadavg): 0.91 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 4267 0 0 0 2986 11 0 0 25 0 1 0 486344073 19165184 3797 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4679 3797 603 41 0 4638 0
vsize: 18716
[startup+40.0006 s]
Raw data (loadavg): 0.93 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 4783 0 0 0 3985 12 0 0 25 0 1 0 486344073 21299200 4313 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5200 4313 603 41 0 5159 0
vsize: 20800
[startup+50.0005 s]
Raw data (loadavg): 0.94 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 5100 0 0 0 4984 13 0 0 25 0 1 0 486344073 22634496 4630 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5526 4630 603 41 0 5485 0
vsize: 22104
[startup+60.0006 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 5902 0 0 0 5982 16 0 0 25 0 1 0 486344073 25825280 5432 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6305 5432 603 41 0 6264 0
vsize: 25220
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 6183 0 0 0 6982 16 0 0 25 0 1 0 486344073 27303936 5713 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6666 5713 603 41 0 6625 0
vsize: 26664
[startup+80.0019 s]
Raw data (loadavg): 0.96 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 7020 0 0 0 7980 18 0 0 25 0 1 0 486344073 30613504 6550 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6550 603 41 0 7433 0
vsize: 29896
[startup+90.0021 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 8004 0 0 0 8978 21 0 0 25 0 1 0 486344073 34738176 7534 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8481 7534 603 41 0 8440 0
vsize: 33924
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 8189 0 0 0 9978 21 0 0 25 0 1 0 486344073 35409920 7719 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7719 603 41 0 8604 0
vsize: 34580
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 8439 0 0 0 10977 22 0 0 25 0 1 0 486344073 36352000 7969 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8875 7969 603 41 0 8834 0
vsize: 35500
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9494 0 0 0 11975 24 0 0 25 0 1 0 486344073 40603648 9024 4294967295 134512640 134672761 3221224544 3221223584 134612663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9913 9024 603 41 0 9872 0
vsize: 39652
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 12974 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 13974 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 14974 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 15975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7283
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 16975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 17975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 18975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 19975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 20975 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 21976 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 9746 0 0 0 22976 25 0 0 25 0 1 0 486344073 41259008 9158 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9158 603 41 0 10032 0
vsize: 40292
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16795 0 0 0 23959 41 0 0 25 0 1 0 486344073 63860736 14489 4294967295 134512640 134672761 3221224544 3221223408 134645502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15591 14489 603 41 0 15550 0
vsize: 62364
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16795 0 0 0 24960 41 0 0 25 0 1 0 486344073 63336448 14381 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14381 603 41 0 15422 0
vsize: 61852
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16798 0 0 0 25961 41 0 0 25 0 1 0 486344073 63336448 14384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14384 603 41 0 15422 0
vsize: 61852
[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16801 0 0 0 26961 41 0 0 25 0 1 0 486344073 63336448 14387 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14387 603 41 0 15422 0
vsize: 61852
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16802 0 0 0 27961 42 0 0 25 0 1 0 486344073 63336448 14388 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14388 603 41 0 15422 0
vsize: 61852
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16802 0 0 0 28961 42 0 0 25 0 1 0 486344073 63336448 14388 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14388 603 41 0 15422 0
vsize: 61852
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16803 0 0 0 29961 42 0 0 25 0 1 0 486344073 63336448 14389 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14389 603 41 0 15422 0
vsize: 61852
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16803 0 0 0 30961 42 0 0 25 0 1 0 486344073 63336448 14389 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14389 603 41 0 15422 0
vsize: 61852
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16803 0 0 0 31962 42 0 0 25 0 1 0 486344073 63336448 14389 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14389 603 41 0 15422 0
vsize: 61852
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16803 0 0 0 32962 42 0 0 25 0 1 0 486344073 63336448 14389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14389 603 41 0 15422 0
vsize: 61852
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16803 0 0 0 33962 42 0 0 25 0 1 0 486344073 63336448 14389 4294967295 134512640 134672761 3221224544 3221223712 134564729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14389 603 41 0 15422 0
vsize: 61852
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16804 0 0 0 34962 42 0 0 25 0 1 0 486344073 63336448 14390 4294967295 134512640 134672761 3221224544 3221223680 134614560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14390 603 41 0 15422 0
vsize: 61852
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16804 0 0 0 35962 42 0 0 25 0 1 0 486344073 63336448 14390 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14390 603 41 0 15422 0
vsize: 61852
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16805 0 0 0 36962 42 0 0 25 0 1 0 486344073 63336448 14391 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14391 603 41 0 15422 0
vsize: 61852
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 16805 0 0 0 37963 42 0 0 25 0 1 0 486344073 63336448 14391 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15463 14391 603 41 0 15422 0
vsize: 61852
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 38959 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 39959 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 40959 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+420.026 s]
Raw data (loadavg): 1.07 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 41959 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+430.027 s]
Raw data (loadavg): 1.06 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 42960 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+440.027 s]
Raw data (loadavg): 1.05 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 43960 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+450.027 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 44960 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+460.027 s]
Raw data (loadavg): 1.04 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 45960 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+470.027 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 46960 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+480.027 s]
Raw data (loadavg): 1.03 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 47961 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+490.027 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 48961 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223744 134610743 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+500.027 s]
Raw data (loadavg): 1.02 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 17993 0 0 0 49961 45 0 0 25 0 1 0 486344073 63582208 14482 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14482 603 41 0 15482 0
vsize: 62092
[startup+510.027 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 18008 0 0 0 50961 45 0 0 25 0 1 0 486344073 63713280 14497 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15555 14497 603 41 0 15514 0
vsize: 62220
[startup+520.026 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 19457 0 0 0 51957 49 0 0 25 0 1 0 486344073 69582848 15946 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16988 15946 603 41 0 16947 0
vsize: 67952
[startup+530.026 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 20582 0 0 0 52954 52 0 0 25 0 1 0 486344073 74207232 17071 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18117 17071 603 41 0 18076 0
vsize: 72468
[startup+540.026 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 20950 0 0 0 53953 53 0 0 25 0 1 0 486344073 75800576 17439 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18506 17439 603 41 0 18465 0
vsize: 74024
[startup+550.027 s]
Raw data (loadavg): 1.01 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 54950 56 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+560.027 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 55950 56 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+570.028 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 56949 56 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+580.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 57949 57 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+590.029 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 58948 57 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+600.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 59948 58 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+610.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 60948 58 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+620.03 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 61947 58 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+630.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 62947 59 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+640.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 63946 59 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+650.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 64946 60 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+660.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 65946 60 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+670.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 66946 60 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+680.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 67945 61 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+690.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 68945 61 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+700.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 69945 61 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+710.033 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 70945 62 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+720.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 71945 62 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+730.034 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22342 0 0 0 72945 62 0 0 25 0 1 0 486344073 76419072 17618 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17618 603 41 0 18616 0
vsize: 74628
[startup+740.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22346 0 0 0 73945 62 0 0 25 0 1 0 486344073 76419072 17622 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18657 17622 603 41 0 18616 0
vsize: 74628
[startup+750.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22353 0 0 0 74944 63 0 0 25 0 1 0 486344073 76943360 17629 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 17629 603 41 0 18744 0
vsize: 75140
[startup+760.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22360 0 0 0 75944 63 0 0 25 0 1 0 486344073 76943360 17636 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 17636 603 41 0 18744 0
vsize: 75140
[startup+770.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22366 0 0 0 76944 63 0 0 25 0 1 0 486344073 76943360 17642 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 17642 603 41 0 18744 0
vsize: 75140
[startup+780.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22372 0 0 0 77944 64 0 0 25 0 1 0 486344073 76943360 17648 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 17648 603 41 0 18744 0
vsize: 75140
[startup+790.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22377 0 0 0 78944 64 0 0 25 0 1 0 486344073 76943360 17653 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18785 17653 603 41 0 18744 0
vsize: 75140
[startup+800.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22452 0 0 0 79943 64 0 0 25 0 1 0 486344073 77344768 17728 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18883 17728 603 41 0 18842 0
vsize: 75532
[startup+810.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 22694 0 0 0 80941 66 0 0 25 0 1 0 486344073 78290944 17970 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19114 17970 603 41 0 19073 0
vsize: 76456
[startup+820.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 81938 70 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+830.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 82937 71 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 83937 71 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223696 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+850.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 84937 71 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+860.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 85937 72 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+870.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 86937 72 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+880.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 87937 72 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+890.041 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 88937 72 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+900.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 89937 73 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+910.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 90936 73 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+920.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 91936 73 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+930.043 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 92936 74 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+940.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 93936 74 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+950.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 94935 74 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+960.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 95935 75 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+970.044 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 96935 75 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+980.045 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 97935 75 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+990.045 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 98935 76 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 99935 76 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 24061 0 0 0 100935 76 0 0 25 0 1 0 486344073 80027648 18325 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19538 18325 603 41 0 19497 0
vsize: 78152
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 101932 79 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 102932 79 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 103932 79 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 104932 80 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 105931 80 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 106931 80 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 107931 81 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 108931 81 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 109931 81 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 110930 82 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 111930 82 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 112930 82 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 113930 82 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223584 134612701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 25043 0 0 0 114930 83 0 0 25 0 1 0 486344073 79147008 18114 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18114 603 41 0 19282 0
vsize: 77292
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 26113 0 0 0 115928 86 0 0 25 0 1 0 486344073 79147008 18121 4294967295 134512640 134672761 3221224544 3221223696 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18121 603 41 0 19282 0
vsize: 77292
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 26113 0 0 0 116927 86 0 0 25 0 1 0 486344073 79147008 18121 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18121 603 41 0 19282 0
vsize: 77292
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 26113 0 0 0 117927 86 0 0 25 0 1 0 486344073 79147008 18121 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18121 603 41 0 19282 0
vsize: 77292
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 26113 0 0 0 118927 87 0 0 25 0 1 0 486344073 79147008 18121 4294967295 134512640 134672761 3221224544 3221223536 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18121 603 41 0 19282 0
vsize: 77292
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/54 7285
Raw data (stat): 7283 (minisat+) R 7282 29151 29150 0 -1 0 26113 0 0 0 119927 87 0 0 25 0 1 0 486344073 79147008 18121 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19323 18121 603 41 0 19282 0
vsize: 77292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.95 1/54 7285
Raw data (stat): 7283 (minisat+) Z 7282 29151 29150 0 -1 12 26114 0 0 0 119928 91 0 0 25 0 1 0 486344073 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.11
CPU time (s): 1200.19
CPU user time (s): 1199.28
CPU system time (s): 0.911861
CPU usage (%): 100.007
Max. virtual memory (Kb): 78152
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####