PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-ran14x18_1.opb
MD5SUM	27cc6bcebfcedf07c5cf3ac138a419c6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	913429
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1421968313
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1421968313
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	5292
Total number of constraints	536
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	252
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	1
Maximum length of a constraint	360
Trace number 14007

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        685736 kB
Buffers:         33396 kB
Cached:         283980 kB
SwapCached:        388 kB
Active:          61560 kB
Inactive:       258264 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        685484 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6220 kB
Slab:            23308 kB
Committed_AS:    63780 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:56:43 (client local time) WITH STATUS 10 IN 1200.39 SECONDS
stats: 19810 7 1200.39 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 |       101 |   69220   237556 |   30456     101      328     3.2 | 25.104 % |
c |       251 |   69220   237556 |   33502     251      790     3.1 | 25.104 % |
c |       476 |   69220   237556 |   36852     476     1547     3.2 | 25.104 % |
c |       813 |   69220   237556 |   40538     813     2683     3.3 | 25.104 % |
c |      1319 |   69220   237556 |   44591    1319     4389     3.3 | 25.104 % |
c |      2078 |   69220   237556 |   49050    2078     6974     3.4 | 25.104 % |
c |      3217 |   69210   237521 |   53948    3216    11495     3.6 | 25.110 % |
c |      4926 |   69200   237486 |   59334    4924    19483     4.0 | 25.116 % |
c |      7488 |   69190   237451 |   65258    7484    35182     4.7 | 25.122 % |
c |     11332 |   69180   237416 |   71774   11327    60551     5.3 | 25.128 % |
c |     17098 |   69180   237416 |   78951   17093    95032     5.6 | 25.128 % |
c |     25750 |   69180   237416 |   86846   25745   175082     6.8 | 25.128 % |
c |     38724 |   69180   237416 |   95531   38719   485511    12.5 | 25.128 % |
c |     58185 |   69149   237309 |  105037   58179   785614    13.5 | 25.152 % |
c |     87377 |   69149   237309 |  115541   87371  7790808    89.2 | 25.152 % |
c |    131169 |   69118   237202 |  127038   21004  4511361   214.8 | 25.176 % |
c |    196853 |   69027   236885 |  139557   86685  6375488    73.5 | 25.248 % |
c |    295379 |   69016   236848 |  153489   64056  1629471    25.4 | 25.254 % |
c ==============================================================================
c (current CPU-time: 447.043 s)
c ==============================================================================
c [1mFound solution: 5407220[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10447   maxlim: 3582405   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    347696 |  141988   497501 |   42596  116370  4043802    34.7 | 25.254 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13617          
c   -- var.elim.:  2000/13617          
c   -- var.elim.:  3000/13617          
c   -- var.elim.:  4000/13617          
c   -- var.elim.:  5000/13617          
c   -- var.elim.:  6000/13617          
c   -- var.elim.:  7000/13617          
c   -- var.elim.:  8000/13617          
c   -- var.elim.:  9000/13617          
c   -- var.elim.:  10000/13617          
c   -- var.elim.:  11000/13617          
c   -- var.elim.:  12000/13617          
c   -- var.elim.:  13000/13617          
c   -- var.elim.:  13617/13617          
c   -- var.elim.:  56/56          
c |    347696 |  141878   496937 |      --  116370       --      -- |     --   | -110/-552
c |    347696 |  141878   496937 |   56751  116350  4043725    34.8 | 25.254 % |
c |    347796 |  141878   496937 |   62426   28415   386565    13.6 | 15.583 % |
c |    347946 |  141878   496937 |   68668   28565   387335    13.6 | 15.583 % |
c |    348171 |  141878   496937 |   75535   28790   388463    13.5 | 15.583 % |
c |    348508 |  141878   496937 |   83089   29127   390438    13.4 | 15.583 % |
c |    349014 |  141878   496937 |   91398   29633   393674    13.3 | 15.583 % |
c |    349773 |  141878   496937 |  100538   30392   398387    13.1 | 15.583 % |
c |    350912 |  141878   496937 |  110592   31531   405262    12.9 | 15.583 % |
c |    352620 |  141878   496937 |  121651   33239   416567    12.5 | 15.583 % |
c |    355182 |  141878   496937 |  133816   35801   478579    13.4 | 15.583 % |
c |    359026 |  141878   496937 |  147197   39645   511625    12.9 | 15.583 % |
c |    364793 |  141878   496937 |  161917   45412   574753    12.7 | 15.583 % |
c |    373442 |  141878   496937 |  178109   54061   675073    12.5 | 15.583 % |
c |    386416 |  141867   496900 |  195905   67034   842565    12.6 | 15.587 % |
c ==============================================================================
c (current CPU-time: 558.874 s)
c ==============================================================================
c [1mFound solution: 5366323[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3623302   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    400383 |  141940   497258 |   42581   81001  1014207    12.5 | 15.587 % |
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  26/26          
c |    400383 |  141932   497263 |      --   81001       --      -- |     --   | -8/13
c |    400383 |  141932   497263 |   56772   81001  1014207    12.5 | 15.587 % |
c |    400483 |  141932   497263 |   62450   25963   201483     7.8 | 15.605 % |
c |    400633 |  141932   497263 |   68695   26113   202095     7.7 | 15.605 % |
c |    400858 |  141932   497263 |   75564   26338   203054     7.7 | 15.605 % |
c |    401195 |  141932   497263 |   83121   26675   204652     7.7 | 15.605 % |
c |    401702 |  141932   497263 |   91433   27182   207110     7.6 | 15.605 % |
c |    402461 |  141932   497263 |  100576   27941   211288     7.6 | 15.605 % |
c |    403600 |  141932   497263 |  110634   29080   217772     7.5 | 15.605 % |
c |    405308 |  141932   497263 |  121697   30788   227246     7.4 | 15.605 % |
c |    407870 |  141932   497263 |  133867   33350   244077     7.3 | 15.605 % |
c |    411714 |  141932   497263 |  147254   37194   279272     7.5 | 15.605 % |
c |    417480 |  141932   497263 |  161979   42960   340204     7.9 | 15.605 % |
c |    426129 |  141922   497228 |  178164   51608   433114     8.4 | 15.608 % |
c |    439104 |  141912   497193 |  195967   64581   608416     9.4 | 15.612 % |
c ==============================================================================
c (current CPU-time: 645.374 s)
c ==============================================================================
c [1mFound solution: 5210372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3779253   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    439317 |  141952   497459 |   42585   64794   611551     9.4 | 15.612 % |
c   -- subsuming                       
c   -- var.elim.:  63/63          
c   -- var.elim.:  25/25          
c |    439317 |  141930   497231 |      --   64794       --      -- |     --   | -11/-40
c |    439317 |  141930   497231 |   56772   64793   611549     9.4 | 15.612 % |
c |    439417 |  141930   497231 |   62449   25542   216584     8.5 | 15.648 % |
c |    439567 |  141930   497231 |   68694   25692   217170     8.5 | 15.648 % |
c |    439792 |  141930   497231 |   75563   25917   218137     8.4 | 15.648 % |
c |    440129 |  141930   497231 |   83119   26254   220538     8.4 | 15.648 % |
c |    440635 |  141918   497183 |   91424   26758   223433     8.4 | 15.652 % |
c |    441394 |  141918   497183 |  100566   27517   227528     8.3 | 15.652 % |
c |    442533 |  141918   497183 |  110623   28656   234190     8.2 | 15.652 % |
c |    444242 |  141918   497183 |  121685   30365   256622     8.5 | 15.652 % |
c |    446804 |  141886   497074 |  133823   32926   272633     8.3 | 15.666 % |
c |    450648 |  141886   497074 |  147206   36770   329681     9.0 | 15.666 % |
c |    456414 |  141886   497074 |  161926   42536   386084     9.1 | 15.666 % |
c |    465063 |  141855   496967 |  178080   51184   474192     9.3 | 15.681 % |
c |    478037 |  141855   496967 |  195888   64158   621246     9.7 | 15.681 % |
c ==============================================================================
c (current CPU-time: 763.193 s)
c ==============================================================================
c [1mFound solution: 3500527[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 5489098   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    491880 |  141911   497277 |   42573   78001   786324    10.1 | 15.681 % |
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  34/34          
c |    491880 |  141898   497183 |      --   78001       --      -- |     --   | -13/-82
c |    491880 |  141898   497183 |   56759   77993   786262    10.1 | 15.681 % |
c |    491980 |  141898   497183 |   62435   26393   197038     7.5 | 15.718 % |
c |    492130 |  141898   497183 |   68678   26543   197680     7.4 | 15.718 % |
c |    492355 |  141898   497183 |   75546   26768   198652     7.4 | 15.718 % |
c |    492692 |  141898   497183 |   83101   27105   200585     7.4 | 15.718 % |
c |    493198 |  141898   497183 |   91411   27611   203022     7.4 | 15.718 % |
c |    493957 |  141898   497183 |  100552   28370   207004     7.3 | 15.718 % |
c |    495096 |  141898   497183 |  110607   29509   213523     7.2 | 15.718 % |
c |    496804 |  141898   497183 |  121668   31217   232118     7.4 | 15.718 % |
c |    499367 |  141898   497183 |  133835   33780   249662     7.4 | 15.718 % |
c |    503211 |  141898   497183 |  147218   37624   279686     7.4 | 15.718 % |
c |    508977 |  141898   497183 |  161940   43390   338243     7.8 | 15.718 % |
c |    517627 |  141898   497183 |  178134   52040   448658     8.6 | 15.718 % |
c |    530601 |  141898   497183 |  195948   65014   649489    10.0 | 15.718 % |
c |    550062 |  141860   497038 |  215485   84467  1181545    14.0 | 15.730 % |
c |    579254 |  141831   496920 |  236985  113655  3848390    33.9 | 15.737 % |
c |    623043 |  141831   496920 |  260683  157444  8112956    51.5 | 15.737 % |
c |    688729 |  141820   496883 |  286729  223128 10525197    47.2 | 15.741 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v X0_bit_7 X0_bit_6 -X0_bit_5 X0_bit_4 X0_bit_3 -X0_bit_2 X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 -X2_bit_6 -X2_bit_5 X2_bit_4 X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 X4_bit_6 -X4_bit_5 X4_bit_4 -X4_bit_3 X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 X6_bit_5 X6_bit_4 X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 X8_bit_6 X8_bit_5 X8_bit_4 X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 Y5_bit0 Y6_bit0 -Y7_bit0 Y8_bit0 -Y9_bit0 X10_bit_7 -X10_bit_6 -X10_bit_5 X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 -X11_bit_6 X11_bit_5 X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 X12_bit_5 -X12_bit_4 X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 X13_bit_6 -X13_bit_5 -X13_bit_4 X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 X14_bit_7 X14_bit_6 X14_bit_5 -X14_bit_4 X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 X15_bit_6 -X15_bit_5 X15_bit_4 X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 X16_bit_7 X16_bit_6 -X16_bit_5 -X16_bit_4 X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 X17_bit_6 -X17_bit_5 X17_bit_4 X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 X20_bit_3 -X20_bit_2 X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 X23_bit_6 -X23_bit_5 X23_bit_4 X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 X24_bit_5 X24_bit_4 X24_bit_3 -X24_bit_2 -X24_bit_1 X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 X26_bit_5 -X26_bit_4 X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 X29_bit_3 X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 X30_bit_6 X30_bit_5 X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 -X33_bit_5 X33_bit_4 -X33_bit_3 -X33_bit_2 X33_bit_1 X33_bit0 X33_bit1 X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 X35_bit_6 -X35_bit_5 X35_bit_4 X35_bit_3 -X35_bit_2 X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 X36_bit_6 -X36_bit_5 X36_bit_4 X36_bit_3 -X36_bit_2 X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 -X38_bit_6 -X38_bit_5 X38_bit_4 -X38_bit_3 -X38_bit_2 X38_bit_1 X38_bit0 X38_bit1 X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 X39_bit_6 X39_bit_5 -X39_bit_4 -X39_bit_3 X39_bit_2 X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 X41_bit_6 -X41_bit_5 X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 -X44_bit_5 X44_bit_4 -X44_bit_3 X44_bit_2 X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 -X45_bit_6 -X45_bit_5 X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 -X48_bit_5 X48_bit_4 -X48_bit_3 -X48_bit_2 X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 -X49_bit_5 -X49_bit_4 X49_bit_3 X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 X50_bit_6 X50_bit_5 -X50_bit_4 -X50_bit_3 X50_bit_2 -X50_bit_1 -X50_bit0 X50_bit1 -X50_bit2 X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 X52_bit_6 X52_bit_5 -X52_bit_4 X52_bit_3 -X52_bit_2 X52_bit_1 -X52_bit0 X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 X58_bit_6 -X58_bit_5 X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 X59_bit_6 -X59_bit_5 X59_bit_4 -X59_bit_3 -X59_bit_2 X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 X65_bit_2 X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 -X66_bit_5 X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 X68_bit_6 -X68_bit_5 X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 X72_bit_6 X72_bit_5 -X72_bit_4 -X72_bit_3 X72_bit_2 X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 -X74_bit_6 -X74_bit_5 X74_bit_4 -X74_bit_3 -X74_bit_2 X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 X75_bit_6 X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 -X76_bit_6 X76_bit_5 X76_bit_4 -X76_bit_3 X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 X77_bit_5 X77_bit_4 -X77_bit_3 X77_bit_2 X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 X79_bit_6 X79_bit_5 X79_bit_4 -X79_bit_3 -X79_bit_2 X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 X80_bit_6 X80_bit_5 X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 X87_bit_6 X87_bit_5 X87_bit_4 -X87_bit_3 X87_bit_2 X87_bit_1 -X87_bit0 X87_bit1 X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 X89_bit_1 -X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 X90_bit_6 -X90_bit_5 -X90_bit_4 X90_bit_3 -X90_bit_2 X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 X95_bit_6 X95_bit_5 -X95_bit_4 X95_bit_3 X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 X96_bit_4 X96_bit_3 X96_bit_2 -X96_bit_1 X96_bit0 X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 X97_bit_3 -X97_bit_2 X97_bit_1 X97_bit0 X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 X98_bit_6 -X98_bit_5 X98_bit_4 X98_bit_3 -X98_bit_2 X98_bit_1 X98_bit0 X98_bit1 -X98_bit2 X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 X102_bit_4 X102_bit_3 X102_bit_2 -X102_bit_1 -X102_bit0 X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 X107_bit_6 -X107_bit_5 X107_bit_4 X107_bit_3 X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 X108_bit_6 X108_bit_5 X108_bit_4 -X108_bit_3 -X108_bit_2 X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 X109_bit_7 X109_bit_6 -X109_bit_5 X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 -X110_bit_6 X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 X111_bit_5 X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 X114_bit_7 X114_bit_6 X114_bit_5 X114_bit_4 -X114_bit_3 X114_bit_2 X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 X115_bit_6 X115_bit_5 X115_bit_4 -X115_bit_3 X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 X117_bit_6 -X117_bit_5 X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 X120_bit_6 X120_bit_5 X120_bit_4 X120_bit_3 -X120_bit_2 -X120_bit_1 X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 X121_bit_5 -X121_bit_4 X121_bit_3 -X121_bit_2 -X121_bit_1 X121_bit0 X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 X123_bit_5 -X123_bit_4 X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 X124_bit_7 X124_bit_6 X124_bit_5 X124_bit_4 X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 X126_bit_6 X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 X127_bit_7 X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 X130_bit_6 X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 X131_bit_6 -X131_bit_5 X131_bit_4 -X131_bit_3 X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 X132_bit_6 -X132_bit_5 -X132_bit_4 X132_bit_3 X132_bit_2 -X132_bit_1 X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 X135_bit_7 X135_bit_6 -X135_bit_5 X135_bit_4 X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 Y10_bit0 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 Y11_bit0 X137_bit_7 -X137_bit_6 X137_bit_5 X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 Y12_bit0 X138_bit_7 X138_bit_6 -X138_bit_5 X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 Y13_bit0 X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 Y19_bit0 X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 X141_bit_7 -X141_bit_6 -X141_bit_5 X141_bit_4 X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 X142_bit_7 X142_bit_6 -X142_bit_5 X142_bit_4 X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 X143_bit_7 -X143_bit_6 -X143_bit_5 X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 Y20_bit0 X146_bit_7 -X146_bit_6 X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 X146_bit0 X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -Y21_bit0 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -Y22_bit0 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 Y23_bit0 X149_bit_7 X149_bit_6 -X149_bit_5 X149_bit_4 X149_bit_3 X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 Y24_bit0 -Y25_bit0 Y26_bit0 -Y27_bit0 -Y28_bit0 Y29_bit0 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 X152_bit_7 -X152_bit_6 -X152_bit_5 X152_bit_4 -X152_bit_3 -X152_bit_2 X152_bit_1 X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 X155_bit_7 X155_bit_6 -X155_bit_5 X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 Y30_bit0 X156_bit_7 X156_bit_6 -X156_bit_5 X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -Y31_bit0 -X157_bit_7 -X157_bit_6 X157_bit_5 X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -Y32_bit0 X158_bit_7 -X158_bit_6 X158_bit_5 -X158_bit_4 X158_bit_3 -X158_bit_2 X158_bit_1 -X158_bit0 X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 Y33_bit0 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -Y34_bit0 Y35_bit0 Y36_bit0 -Y37_bit0 Y38_bit0 Y39_bit0 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -Y40_bit0 -X166_bit_7 -X166_bit_6 -X166_bit_5 X166_bit_4 X166_bit_3 -X166_bit_2 X166_bit_1 -X166_bit0 -X166_bit1 X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 Y41_bit0 -X167_bit_7 -X167_bit_6 X167_bit_5 -X167_bit_4 X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -Y42_bit0 -X168_bit_7 X168_bit_6 X168_bit_5 X168_bit_4 -X168_bit_3 X168_bit_2 X168_bit_1 X168_bit0 -X168_bit1 -X168_bit2 X168_bit3 X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -Y43_bit0 -X169_bit_7 X169_bit_6 -X169_bit_5 X169_bit_4 X169_bit_3 -X169_bit_2 -X169_bit_1 X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 Y44_bit0 Y45_bit0 -Y46_bit0 -Y47_bit0 Y48_bit0 Y49_bit0 -X170_bit_7 X170_bit_6 X170_bit_5 X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 X171_bit_7 -X171_bit_6 X171_bit_5 -X171_bit_4 -X171_bit_3 X171_bit_2 -X171_bit_1 -X171_bit0 X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 Y50_bit0 X176_bit_7 -X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -Y51_bit0 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 Y52_bit0 -X178_bit_7 X178_bit_6 -X178_bit_5 X178_bit_4 -X178_bit_3 X178_bit_2 X178_bit_1 X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -Y53_bit0 X179_bit_7 X179_bit_6 -X179_bit_5 X179_bit_4 -X179_bit_3 X179_bit_2 -X179_bit_1 X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 Y58_bit0 Y59_bit0 X180_bit_7 -X180_bit_6 X180_bit_5 -X180_bit_4 X180_bit_3 -X180_bit_2 X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 X181_bit_7 X181_bit_6 X181_bit_5 -X181_bit_4 X181_bit_3 X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 X183_bit_1 -X183_bit0 -X183_bit1 X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 X184_bit_6 -X184_bit_5 X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -Y60_bit0 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 Y61_bit0 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 Y62_bit0 -X188_bit_7 X188_bit_6 X188_bit_5 X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 Y63_bit0 -X189_bit_7 X189_bit_6 X189_bit_5 X189_bit_4 -X189_bit_3 -X189_bit_2 X189_bit_1 -X189_bit0 X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 -Y69_bit0 -X190_bit_7 -X190_bit_6 -X190_bit_5 X190_bit_4 -X190_bit_3 -X190_bit_2 X190_bit_1 X190_bit0 -X190_bit1 X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 X191_bit_3 -X191_bit_2 X191_bit_1 X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 X192_bit_6 X192_bit_5 X192_bit_4 -X192_bit_3 X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 X194_bit_7 -X194_bit_6 -X194_bit_5 X194_bit_4 -X194_bit_3 X194_bit_2 X194_bit_1 X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 Y70_bit0 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -Y71_bit0 -X197_bit_7 -X197_bit_6 X197_bit_5 X197_bit_4 X197_bit_3 X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 Y72_bit0 -X198_bit_7 -X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 Y73_bit0 -X199_bit_7 X199_bit_6 X199_bit_5 -X199_bit_4 X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 -Y78_bit0 Y79_bit0 Y80_bit0 -Y81_bit0 Y82_bit0 Y83_bit0 Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 -Y88_bit0 Y89_bit0 Y90_bit0 -Y91_bit0 Y92_bit0 -Y93_bit0 -Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 -Y99_bit0 -X200_bit_7 -X200_bit_6 X200_bit_5 -X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 X205_bit_3 -X205_bit_2 -X205_bit_1 X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 X207_bit_6 X207_bit_5 X207_bit_4 X207_bit_3 X207_bit_2 X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 X208_bit_6 X208_bit_5 X208_bit_4 X208_bit_3 X208_bit_2 X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 X209_bit_6 X209_bit_5 -X209_bit_4 X209_bit_3 -X209_bit_2 X209_bit_1 X209_bit0 X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 X210_bit_6 -X210_bit_5 -X210_bit_4 X210_bit_3 X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 X211_bit_3 -X211_bit_2 X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 X212_bit_3 -X212_bit_2 X212_bit_1 X212_bit0 X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 X213_bit1 X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 X214_bit_3 X214_bit_2 X214_bit_1 X214_bit0 -X214_bit1 X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 X215_bit_6 X215_bit_5 X215_bit_4 -X215_bit_3 X215_bit_2 -X215_bit_1 X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 X218_bit_3 X218_bit_2 -X218_bit_1 X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 X220_bit_5 X220_bit_4 X220_bit_3 X220_bit_2 X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 X221_bit_6 X221_bit_5 -X221_bit_4 X221_bit_3 X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 X223_bit_1 -X223_bit0 X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 X224_bit_5 -X224_bit_4 X224_bit_3 X224_bit_2 -X224_bit_1 X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 X225_bit_7 -X225_bit_6 X225_bit_5 X225_bit_4 X225_bit_3 X225_bit_2 -X225_bit_1 -X225_bit0 X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 X226_bit_7 X226_bit_6 X226_bit_5 X226_bit_4 -X226_bit_3 X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 X227_bit_5 -X227_bit_4 -X227_bit_3 -X227_bit_2 -X227_bit_1 X227_bit0 X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 X228_bit_6 X228_bit_5 -X228_bit_4 X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 -X229_bit_6 X229_bit_5 X229_bit_4 -X229_bit_3 X229_bit_2 X229_bit_1 -X229_bit0 -X229_bit1 X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 -X230_bit_5 X230_bit_4 X230_bit_3 X230_bit_2 X230_bit_1 X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 -X233_bit_5 X233_bit_4 X233_bit_3 X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 X234_bit_6 X234_bit_5 -X234_bit_4 -X234_bit_3 X234_bit_2 -X234_bit_1 X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 -X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 X236_bit_7 X236_bit_6 -X236_bit_5 X236_bit_4 X236_bit_3 X236_bit_2 X236_bit_1 X236_bit0 X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 X237_bit_1 X237_bit0 -X237_bit1 X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 X238_bit_6 -X238_bit_5 X238_bit_4 X238_bit_3 X238_bit_2 X238_bit_1 -X238_bit0 X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 X239_bit_7 X239_bit_6 X239_bit_5 -X239_bit_4 X239_bit_3 X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 X241_bit_1 X241_bit0 X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 X242_bit_6 X242_bit_5 -X242_bit_4 X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 X245_bit_6 X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 X245_bit_1 X245_bit0 X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 X247_bit_7 -X247_bit_6 X247_bit_5 X247_bit_4 -X247_bit_3 -X247_bit_2 X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 X248_bit_7 -X248_bit_6 X248_bit_5 X248_bit_4 X248_bit_3 X248_bit_2 X248_bit_1 X248_bit0 X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249#### 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.76 0.91 0.89 2/55 11209
Raw data (stat): 11209 (runsolver) R 11208 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540081144 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.79 0.91 0.89 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 3662 0 0 0 991 8 0 0 25 0 1 0 540081144 16592896 3192 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.0007 s]
Raw data (loadavg): 0.82 0.91 0.89 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 3764 0 0 0 1990 8 0 0 25 0 1 0 540081144 17129472 3294 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4182 3294 603 41 0 4141 0
vsize: 16728
[startup+30.0021 s]
Raw data (loadavg): 0.85 0.92 0.89 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 3885 0 0 0 2990 9 0 0 25 0 1 0 540081144 17670144 3415 4294967295 134512640 134672761 3221224544 3221223668 134566120 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4314 3415 603 41 0 4273 0
vsize: 17256
[startup+40.0026 s]
Raw data (loadavg): 0.87 0.92 0.89 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 4092 0 0 0 3989 10 0 0 25 0 1 0 540081144 18481152 3622 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 3622 603 41 0 4471 0
vsize: 18048
[startup+50.0039 s]
Raw data (loadavg): 0.89 0.92 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 4463 0 0 0 4988 11 0 0 25 0 1 0 540081144 20074496 3993 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4901 3993 603 41 0 4860 0
vsize: 19604
[startup+60.0048 s]
Raw data (loadavg): 0.91 0.92 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 4812 0 0 0 5987 13 0 0 25 0 1 0 540081144 21397504 4342 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5224 4342 603 41 0 5183 0
vsize: 20896
[startup+70.0053 s]
Raw data (loadavg): 0.92 0.92 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 5089 0 0 0 6986 14 0 0 25 0 1 0 540081144 22601728 4619 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5518 4619 603 41 0 5477 0
vsize: 22072
[startup+80.0066 s]
Raw data (loadavg): 0.93 0.93 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 5810 0 0 0 7984 16 0 0 25 0 1 0 540081144 25522176 5340 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6231 5340 603 41 0 6190 0
vsize: 24924
[startup+90.0075 s]
Raw data (loadavg): 0.94 0.93 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 7715 0 0 0 8979 21 0 0 25 0 1 0 540081144 33476608 7245 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8173 7245 603 41 0 8132 0
vsize: 32692
[startup+100.008 s]
Raw data (loadavg): 0.95 0.93 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 9244 0 0 0 9974 26 0 0 25 0 1 0 540081144 39792640 8774 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9715 8774 603 41 0 9674 0
vsize: 38860
[startup+110.009 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 10548 0 0 0 10972 28 0 0 25 0 1 0 540081144 45064192 10078 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11002 10078 603 41 0 10961 0
vsize: 44008
[startup+120.01 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 11749 0 0 0 11969 31 0 0 25 0 1 0 540081144 49946624 11279 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12194 11279 603 41 0 12153 0
vsize: 48776
[startup+130.011 s]
Raw data (loadavg): 0.97 0.94 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 12551 0 0 0 12967 34 0 0 25 0 1 0 540081144 53256192 12081 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13002 12081 603 41 0 12961 0
vsize: 52008
[startup+140.015 s]
Raw data (loadavg): 0.97 0.94 0.90 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 12806 0 0 0 13966 35 0 0 25 0 1 0 540081144 54341632 12336 4294967295 134512640 134672761 3221224544 3221223728 134615491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13267 12336 603 41 0 13226 0
vsize: 53068
[startup+150.021 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 13091 0 0 0 14966 35 0 0 25 0 1 0 540081144 55525376 12621 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13556 12621 603 41 0 13515 0
vsize: 54224
[startup+160.022 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 13802 0 0 0 15964 37 0 0 25 0 1 0 540081144 58318848 13332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14238 13332 603 41 0 14197 0
vsize: 56952
[startup+170.022 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 15332 0 0 0 16961 41 0 0 25 0 1 0 540081144 64524288 14862 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15753 14862 603 41 0 15712 0
vsize: 63012
[startup+180.023 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 16694 0 0 0 17957 45 0 0 25 0 1 0 540081144 70094848 16224 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17113 16224 603 41 0 17072 0
vsize: 68452
[startup+190.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17675 0 0 0 18954 48 0 0 25 0 1 0 540081144 73539584 17048 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17048 603 41 0 17913 0
vsize: 71816
[startup+200.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 19954 48 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+210.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 20954 49 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+220.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 21954 49 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+230.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 22954 49 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+240.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11209
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 23954 50 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+250.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 24953 51 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+260.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 25953 51 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+270.03 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 26952 51 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+280.031 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 27952 51 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+290.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 28952 52 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+300.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 29952 52 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+310.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 30952 52 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+320.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17676 0 0 0 31952 53 0 0 25 0 1 0 540081144 73539584 17049 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17954 17049 603 41 0 17913 0
vsize: 71816
[startup+330.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17684 0 0 0 32951 53 0 0 25 0 1 0 540081144 74063872 17057 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17057 603 41 0 18041 0
vsize: 72328
[startup+340.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17691 0 0 0 33951 54 0 0 25 0 1 0 540081144 74063872 17064 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17064 603 41 0 18041 0
vsize: 72328
[startup+350.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 34950 54 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+360.036 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 35951 54 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+370.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 36951 54 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+380.053 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 37951 55 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+390.157 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 38961 56 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+400.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 39961 56 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+410.159 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 40960 57 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+420.158 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 41960 57 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+430.16 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 42960 57 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+440.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 17850 0 0 0 43960 58 0 0 25 0 1 0 540081144 74063872 17079 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18082 17079 603 41 0 18041 0
vsize: 72328
[startup+450.161 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22288 0 0 0 44949 68 0 0 25 0 1 0 540081144 87064576 20111 4294967295 134512640 134672761 3221224544 3221223088 134621328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20111 603 41 0 21215 0
vsize: 85024
[startup+460.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22430 0 0 0 45949 69 0 0 25 0 1 0 540081144 87064576 20114 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20114 603 41 0 21215 0
vsize: 85024
[startup+470.162 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22434 0 0 0 46949 69 0 0 25 0 1 0 540081144 87064576 20118 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20118 603 41 0 21215 0
vsize: 85024
[startup+480.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22434 0 0 0 47949 69 0 0 25 0 1 0 540081144 87064576 20118 4294967295 134512640 134672761 3221224544 3221223792 134618067 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20118 603 41 0 21215 0
vsize: 85024
[startup+490.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22434 0 0 0 48949 69 0 0 25 0 1 0 540081144 87064576 20118 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20118 603 41 0 21215 0
vsize: 85024
[startup+500.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22434 0 0 0 49950 69 0 0 25 0 1 0 540081144 87064576 20118 4294967295 134512640 134672761 3221224544 3221223696 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20118 603 41 0 21215 0
vsize: 85024
[startup+510.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22436 0 0 0 50950 69 0 0 25 0 1 0 540081144 87064576 20120 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20120 603 41 0 21215 0
vsize: 85024
[startup+520.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22436 0 0 0 51950 69 0 0 25 0 1 0 540081144 87064576 20120 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20120 603 41 0 21215 0
vsize: 85024
[startup+530.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22436 0 0 0 52950 69 0 0 25 0 1 0 540081144 87064576 20120 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20120 603 41 0 21215 0
vsize: 85024
[startup+540.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11211
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22437 0 0 0 53950 69 0 0 25 0 1 0 540081144 87064576 20121 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20121 603 41 0 21215 0
vsize: 85024
[startup+550.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22437 0 0 0 54951 69 0 0 25 0 1 0 540081144 87064576 20121 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20121 603 41 0 21215 0
vsize: 85024
[startup+560.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 22770 0 0 0 55950 70 0 0 25 0 1 0 540081144 87064576 20122 4294967295 134512640 134672761 3221224544 3221222016 134522440 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21256 20122 603 41 0 21215 0
vsize: 85024
[startup+570.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 56949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+580.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 57949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+590.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 58949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+600.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 59949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+610.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 60949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+620.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 61949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+630.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 62949 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+640.171 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23079 0 0 0 63950 71 0 0 25 0 1 0 540081144 87064576 20153 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20153 603 41 0 21215 0
vsize: 85024
[startup+650.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 64948 72 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+660.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 65947 72 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+670.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 66946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+680.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 67946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+690.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 68946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+700.175 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 69946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+710.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 70946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+720.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 71946 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+730.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 72947 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+740.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 73947 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+750.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 74947 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+760.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 23691 0 0 0 75947 73 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+770.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 76944 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+780.179 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 77945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+790.179 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 78945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+800.179 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 79945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+810.18 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 80945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+820.18 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 81945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+830.181 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 82945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+840.182 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11213
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 83945 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+850.182 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 84946 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223712 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+860.183 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 85946 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+870.183 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 86946 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+880.184 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 87946 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+890.184 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 88946 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+900.184 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 89947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223584 134603512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+910.184 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 90947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+920.184 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 91947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+930.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 92947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+940.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 93947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+950.185 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 94947 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+960.186 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 95948 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+970.186 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 96948 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+980.187 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24301 0 0 0 97948 75 0 0 25 0 1 0 540081144 87064576 20155 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21256 20155 603 41 0 21215 0
vsize: 85024
[startup+990.186 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 24955 0 0 0 98947 77 0 0 25 0 1 0 540081144 89808896 20809 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21926 20809 603 41 0 21885 0
vsize: 87704
[startup+1000.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 25359 0 0 0 99945 78 0 0 25 0 1 0 540081144 91496448 21213 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 21213 603 41 0 22297 0
vsize: 89352
[startup+1010.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 25717 0 0 0 100945 79 0 0 25 0 1 0 540081144 92946432 21571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22692 21571 603 41 0 22651 0
vsize: 90768
[startup+1020.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 26039 0 0 0 101944 80 0 0 25 0 1 0 540081144 94134272 21893 4294967295 134512640 134672761 3221224544 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22982 21893 603 41 0 22941 0
vsize: 91928
[startup+1030.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 26298 0 0 0 102944 81 0 0 25 0 1 0 540081144 95191040 22152 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23240 22152 603 41 0 23199 0
vsize: 92960
[startup+1040.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 26443 0 0 0 103943 81 0 0 25 0 1 0 540081144 95862784 22297 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23404 22297 603 41 0 23363 0
vsize: 93616
[startup+1050.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 26606 0 0 0 104943 81 0 0 25 0 1 0 540081144 96395264 22460 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23534 22460 603 41 0 23493 0
vsize: 94136
[startup+1060.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 27233 0 0 0 105942 83 0 0 25 0 1 0 540081144 99045376 23087 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24181 23087 603 41 0 24140 0
vsize: 96724
[startup+1070.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 27641 0 0 0 106941 84 0 0 25 0 1 0 540081144 100659200 23495 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24575 23495 603 41 0 24534 0
vsize: 98300
[startup+1080.19 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 27930 0 0 0 107941 84 0 0 25 0 1 0 540081144 101724160 23784 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24835 23784 603 41 0 24794 0
vsize: 99340
[startup+1090.2 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 28300 0 0 0 108941 85 0 0 25 0 1 0 540081144 103329792 24154 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25227 24154 603 41 0 25186 0
vsize: 100908
[startup+1100.2 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 28463 0 0 0 109941 86 0 0 25 0 1 0 540081144 103866368 24317 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25358 24317 603 41 0 25317 0
vsize: 101432
[startup+1110.2 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 28767 0 0 0 110940 87 0 0 25 0 1 0 540081144 105070592 24621 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25652 24621 603 41 0 25611 0
vsize: 102608
[startup+1120.2 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 29065 0 0 0 111939 88 0 0 25 0 1 0 540081144 106393600 24919 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 24919 603 41 0 25934 0
vsize: 103900
[startup+1130.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 29621 0 0 0 112939 89 0 0 25 0 1 0 540081144 108646400 25475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26525 25475 603 41 0 26484 0
vsize: 106100
[startup+1140.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11215
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 30076 0 0 0 113938 91 0 0 25 0 1 0 540081144 110383104 25930 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26949 25930 603 41 0 26908 0
vsize: 107796
[startup+1150.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 30517 0 0 0 114937 92 0 0 25 0 1 0 540081144 112234496 26371 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27401 26371 603 41 0 27360 0
vsize: 109604
[startup+1160.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 30942 0 0 0 115937 94 0 0 25 0 1 0 540081144 113963008 26796 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27823 26796 603 41 0 27782 0
vsize: 111292
[startup+1170.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 31377 0 0 0 116936 94 0 0 25 0 1 0 540081144 115687424 27231 4294967295 134512640 134672761 3221224544 3221223728 134615508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28244 27231 603 41 0 28203 0
vsize: 112976
[startup+1180.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 31722 0 0 0 117935 95 0 0 25 0 1 0 540081144 117215232 27576 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28617 27576 603 41 0 28576 0
vsize: 114468
[startup+1190.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 32061 0 0 0 118935 96 0 0 25 0 1 0 540081144 118525952 27915 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28937 27915 603 41 0 28896 0
vsize: 115748
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 11217
Raw data (stat): 11209 (minisat+) R 11208 20024 20023 0 -1 0 32371 0 0 0 119934 97 0 0 25 0 1 0 540081144 119853056 28225 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29261 28225 603 41 0 29220 0
vsize: 117044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 11217
Raw data (stat): 11209 (minisat+) Z 11208 20024 20023 0 -1 12 32372 0 0 0 119935 103 0 0 24 0 1 0 540081144 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.31
CPU time (s): 1200.39
CPU user time (s): 1199.35
CPU system time (s): 1.03284
CPU usage (%): 100.006
Max. virtual memory (Kb): 117044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####