PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran16x16.opb
MD5SUM	9ccd6fd38eec7ec6eedca3a615a280ba
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1042560
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1526874453
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	1526874453
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	5376
Total number of constraints	288
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	288
Minimum length of a constraint	21
Maximum length of a constraint	320
Trace number 17633

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 11:02:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19316 boxname=wulflinc31 idbench=1486 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9ccd6fd38eec7ec6eedca3a615a280ba  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-ran16x16.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-ran16x16.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-ran16x16.opb
IDLAUNCH: 19316
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        631240 kB
Buffers:         33484 kB
Cached:         342152 kB
SwapCached:        540 kB
Active:         124680 kB
Inactive:       252948 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        630988 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20220 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:22:08 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 19316 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 320 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 318]---> Adder-cost: 332   maxlim: 41712   bits: 16/16
c ---[ 316]---> Adder-cost: 332   maxlim: 41456   bits: 16/16
c ---[ 314]---> Adder-cost: 332   maxlim: 42096   bits: 16/16
c ---[ 312]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 310]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 308]---> Adder-cost: 316   maxlim: 24432   bits: 15/15
c ---[ 306]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 304]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 302]---> Adder-cost: 316   maxlim: 24816   bits: 15/15
c ---[ 300]---> Adder-cost: 268   maxlim: 7280   bits: 13/13
c ---[ 298]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 296]---> Adder-cost: 336   maxlim: 49904   bits: 16/16
c ---[ 294]---> Adder-cost: 316   maxlim: 24944   bits: 15/15
c ---[ 292]---> Adder-cost: 332   maxlim: 42352   bits: 16/16
c ---[ 290]---> Adder-cost: 316   maxlim: 24176   bits: 15/15
c ---[ 288]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 286]---> Adder-cost: 328   maxlim: 27760   bits: 15/15
c ---[ 284]---> Adder-cost: 344   maxlim: 44528   bits: 16/16
c ---[ 282]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 280]---> Adder-cost: 350   maxlim: 52208   bits: 16/16
c ---[ 278]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 276]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 274]---> Adder-cost: 344   maxlim: 43760   bits: 16/16
c ---[ 272]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 270]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 268]---> Adder-cost: 350   maxlim: 53616   bits: 16/16
c ---[ 266]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 264]---> Adder-cost: 344   maxlim: 44784   bits: 16/16
c ---[ 262]---> Adder-cost: 350   maxlim: 54640   bits: 16/16
c ---[ 260]---> Adder-cost: 328   maxlim: 28144   bits: 15/15
c ---[ 258]---> Adder-cost: 328   maxlim: 28016   bits: 15/15
c ---[ 256]---> Adder-cost: 344   maxlim: 45552   bits: 16/16
c ---[ 255]---> BDD-cost:   15
c ---[ 254]---> BDD-cost:   16
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   12
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:   15
c ---[ 244]---> BDD-cost:   15
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   15
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   15
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   10
c ---[ 236]---> BDD-cost:   17
c ---[ 235]---> BDD-cost:   10
c ---[ 234]---> BDD-cost:   17
c ---[ 233]---> BDD-cost:   17
c ---[ 232]---> BDD-cost:   12
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:   17
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:   10
c ---[ 218]---> BDD-cost:   15
c ---[ 217]---> BDD-cost:   10
c ---[ 216]---> BDD-cost:   15
c ---[ 215]---> BDD-cost:   15
c ---[ 214]---> BDD-cost:   12
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:   15
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:   15
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   10
c ---[ 201]---> BDD-cost:   16
c ---[ 200]---> BDD-cost:   10
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   16
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:   16
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   15
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   10
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   17
c ---[ 179]---> BDD-cost:   12
c ---[ 178]---> BDD-cost:   15
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   14
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   17
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   10
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   17
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   16
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   12
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:   12
c ---[ 147]---> BDD-cost:   10
c ---[ 146]---> BDD-cost:   12
c ---[ 145]---> BDD-cost:   12
c ---[ 144]---> BDD-cost:   12
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:   12
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   12
c ---[ 137]---> BDD-cost:   12
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   12
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   10
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   18
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   12
c ---[ 108]---> BDD-cost:   18
c ---[ 107]---> BDD-cost:   12
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:   16
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   12
c ---[  91]---> BDD-cost:   12
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   12
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   14
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   14
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   10
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   10
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   10
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   75012   263756 |   22503       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13184          
c   -- var.elim.:  2000/13184          
c   -- var.elim.:  3000/13184          
c   -- var.elim.:  4000/13184          
c   -- var.elim.:  5000/13184          
c   -- var.elim.:  6000/13184          
c   -- var.elim.:  7000/13184          
c   -- var.elim.:  8000/13184          
c   -- var.elim.:  9000/13184          
c   -- var.elim.:  10000/13184          
c   -- var.elim.:  11000/13184          
c   -- var.elim.:  12000/13184          
c   -- var.elim.:  13000/13184          
c   -- var.elim.:  13184/13184          
c   -- var.elim.:  1000/2755          
c   -- var.elim.:  2000/2755          
c   -- var.elim.:  2755/2755          
c   -- subsuming                       
c   -- var.elim.:  972/972          
c   -- var.elim.:  993/993          
c   -- subsuming                       
c |         0 |   66292   227850 |      --       0       --      -- |     --   | -6632/-23365
c |         0 |   66292   227850 |   26516       0        0     nan |  0.000 % |
c |       100 |   66292   227850 |   29168     100      328     3.3 | 26.505 % |
c |       250 |   66292   227850 |   32085     250      786     3.1 | 26.505 % |
c |       475 |   66282   227815 |   35288     474     1637     3.5 | 26.511 % |
c |       812 |   66282   227815 |   38817     811     2703     3.3 | 26.511 % |
c |      1318 |   66282   227815 |   42699    1317     4310     3.3 | 26.511 % |
c |      2077 |   66282   227815 |   46969    2076     6851     3.3 | 26.511 % |
c |      3217 |   66272   227780 |   51658    3214    10972     3.4 | 26.517 % |
c |      4926 |   66272   227780 |   56823    4923    20261     4.1 | 26.517 % |
c |      7488 |   66261   227743 |   62495    7483    33134     4.4 | 26.524 % |
c |     11332 |   66250   227706 |   68734   11326    69275     6.1 | 26.530 % |
c |     17098 |   66239   227669 |   75595   17090   140904     8.2 | 26.536 % |
c |     25747 |   66218   227597 |   83128   25735   222875     8.7 | 26.548 % |
c |     38721 |   66187   227490 |   91398   38705   387758    10.0 | 26.567 % |
c |     58182 |   66156   227383 |  100490   58165  1097610    18.9 | 26.591 % |
c ==============================================================================
c (current CPU-time: 97.4232 s)
c ==============================================================================
c [1mFound solution: 5402352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10697   maxlim: 3342437   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     83675 |  140809   494018 |   42242   83654  1711652    20.5 | 26.591 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13751          
c   -- var.elim.:  2000/13751          
c   -- var.elim.:  3000/13751          
c   -- var.elim.:  4000/13751          
c   -- var.elim.:  5000/13751          
c   -- var.elim.:  6000/13751          
c   -- var.elim.:  7000/13751          
c   -- var.elim.:  8000/13751          
c   -- var.elim.:  9000/13751          
c   -- var.elim.:  10000/13751          
c   -- var.elim.:  11000/13751          
c   -- var.elim.:  12000/13751          
c   -- var.elim.:  13000/13751          
c   -- var.elim.:  13751/13751          
c   -- var.elim.:  57/57          
c |     83675 |  140736   493661 |      --   83654       --      -- |     --   | -73/-349
c |     83675 |  140736   493661 |   56294   83637  1711545    20.5 | 26.591 % |
c |     83775 |  140736   493661 |   61923   24505   281088    11.5 | 16.105 % |
c |     83925 |  140736   493661 |   68116   24655   281863    11.4 | 16.105 % |
c |     84150 |  140736   493661 |   74927   24880   283114    11.4 | 16.105 % |
c |     84487 |  140736   493661 |   82420   25217   284927    11.3 | 16.105 % |
c |     84993 |  140736   493661 |   90662   25723   298145    11.6 | 16.105 % |
c |     85752 |  140736   493661 |   99728   26482   303139    11.4 | 16.105 % |
c |     86892 |  140736   493661 |  109701   27622   311331    11.3 | 16.105 % |
c |     88600 |  140736   493661 |  120672   29330   323712    11.0 | 16.105 % |
c |     91162 |  140736   493661 |  132739   31892   346191    10.9 | 16.105 % |
c |     95006 |  140736   493661 |  146013   35736   384610    10.8 | 16.105 % |
c |    100773 |  140736   493661 |  160614   41503   453509    10.9 | 16.105 % |
c |    109422 |  140725   493624 |  176662   50151   630670    12.6 | 16.108 % |
c ==============================================================================
c (current CPU-time: 160.34 s)
c ==============================================================================
c [1mFound solution: 5203549[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3541240   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    113452 |  140767   493888 |   42230   54179   692346    12.8 | 16.108 % |
c   -- subsuming                       
c   -- var.elim.:  80/80          
c   -- var.elim.:  36/36          
c |    113452 |  140752   493847 |      --   54179       --      -- |     --   | -15/-32
c |    113452 |  140752   493847 |   56300   54175   692329    12.8 | 16.108 % |
c |    113552 |  140752   493847 |   61930   54275   692783    12.8 | 16.142 % |
c |    113703 |  140741   493810 |   68118   54425   693701    12.7 | 16.146 % |
c |    113928 |  140730   493773 |   74924   54649   695615    12.7 | 16.150 % |
c |    114265 |  140730   493773 |   82417   54986   698455    12.7 | 16.150 % |
c |    114771 |  140730   493773 |   90658   55492   703281    12.7 | 16.150 % |
c |    115530 |  140730   493773 |   99724   56251   711690    12.7 | 16.150 % |
c |    116669 |  140730   493773 |  109697   57390   725048    12.6 | 16.150 % |
c |    118377 |  140730   493773 |  120666   59098   744267    12.6 | 16.150 % |
c ==============================================================================
c (current CPU-time: 175.501 s)
c ==============================================================================
c [1mFound solution: 5040961[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3703828   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    119763 |  140758   493945 |   42227   60484   762618    12.6 | 16.150 % |
c   -- subsuming                       
c   -- var.elim.:  56/56          
c   -- var.elim.:  22/22          
c |    119763 |  140737   493767 |      --   60484       --      -- |     --   | -6/14
c |    119763 |  140737   493767 |   56294   60484   762618    12.6 | 16.150 % |
c |    119863 |  140737   493767 |   61924   60584   763358    12.6 | 16.167 % |
c |    120013 |  140737   493767 |   68116   60734   764574    12.6 | 16.167 % |
c |    120239 |  140737   493767 |   74928   60960   766301    12.6 | 16.167 % |
c |    120577 |  140737   493767 |   82421   61298   775000    12.6 | 16.167 % |
c |    121083 |  140737   493767 |   90663   61804   780373    12.6 | 16.167 % |
c |    121843 |  140737   493767 |   99729   62564   802863    12.8 | 16.167 % |
c |    122983 |  140713   493684 |  109683   63702   811651    12.7 | 16.174 % |
c |    124691 |  140693   493614 |  120635   65406   831305    12.7 | 16.182 % |
c |    127254 |  140682   493577 |  132688   67967   871216    12.8 | 16.186 % |
c |    131099 |  140682   493577 |  145957   71812  1464955    20.4 | 16.186 % |
c |    136865 |  140672   493542 |  160541   77577  1529505    19.7 | 16.189 % |
c |    145517 |  140658   493483 |  176578   86227  1671173    19.4 | 16.193 % |
c |    158492 |  140619   493330 |  194181   99192  2074447    20.9 | 16.204 % |
c ==============================================================================
c (current CPU-time: 249.674 s)
c ==============================================================================
c [1mFound solution: 4745548[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3999241   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    161277 |  140640   493473 |   42191  101977  2133528    20.9 | 16.204 % |
c   -- subsuming                       
c   -- var.elim.:  104/104          
c   -- var.elim.:  38/38          
c |    161277 |  140637   493404 |      --  101977       --      -- |     --   | -3/-63
c |    161277 |  140637   493404 |   56254  101944  2133163    20.9 | 16.204 % |
c |    161377 |  140637   493404 |   61880   27616   417453    15.1 | 16.225 % |
c |    161527 |  140637   493404 |   68068   27766   418189    15.1 | 16.225 % |
c |    161752 |  140637   493404 |   74875   27991   419329    15.0 | 16.225 % |
c |    162089 |  140637   493404 |   82362   28328   420926    14.9 | 16.225 % |
c |    162595 |  140637   493404 |   90598   28834   425186    14.7 | 16.225 % |
c |    163354 |  140637   493404 |   99658   29593   431890    14.6 | 16.225 % |
c |    164494 |  140637   493404 |  109624   30733   438669    14.3 | 16.225 % |
c |    166203 |  140637   493404 |  120587   32442   453295    14.0 | 16.225 % |
c |    168765 |  140637   493404 |  132645   35004   480096    13.7 | 16.225 % |
c |    172609 |  140637   493404 |  145910   38848   584965    15.1 | 16.225 % |
c |    178375 |  140637   493404 |  160501   44614   650737    14.6 | 16.225 % |
c |    187024 |  140637   493404 |  176551   53263   764355    14.4 | 16.225 % |
c |    199998 |  140637   493404 |  194206   66237  1740066    26.3 | 16.225 % |
c |    219460 |  140637   493404 |  213627   85699  3389932    39.6 | 16.225 % |
c ==============================================================================
c (current CPU-time: 356.724 s)
c ==============================================================================
c [1mFound solution: 4742819[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4001970   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    224104 |  140637   493486 |   42191   90340  3437085    38.0 | 16.225 % |
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  25/25          
c |    224104 |  140610   493254 |      --   90340       --      -- |     --   | -27/-226
c |    224104 |  140610   493254 |   56244   90156  3418355    37.9 | 16.225 % |
c |    224204 |  140610   493254 |   61868   21920  1241602    56.6 | 16.249 % |
c |    224354 |  140610   493254 |   68055   22070  1242161    56.3 | 16.249 % |
c |    224579 |  140610   493254 |   74860   22295  1243061    55.8 | 16.249 % |
c |    224916 |  140610   493254 |   82346   22632  1244641    55.0 | 16.249 % |
c |    225422 |  140610   493254 |   90581   23138  1246870    53.9 | 16.249 % |
c |    226181 |  140610   493254 |   99639   23897  1250380    52.3 | 16.249 % |
c |    227321 |  140610   493254 |  109603   25037  1257552    50.2 | 16.249 % |
c |    229030 |  140610   493254 |  120564   26746  1269985    47.5 | 16.249 % |
c |    231592 |  140610   493254 |  132620   29308  1287846    43.9 | 16.249 % |
c |    235438 |  140610   493254 |  145882   33154  1327998    40.1 | 16.249 % |
c |    241205 |  140610   493254 |  160470   38921  1381349    35.5 | 16.249 % |
c |    249854 |  140610   493254 |  176517   47570  1743749    36.7 | 16.249 % |
c |    262828 |  140610   493254 |  194169   60544  1946887    32.2 | 16.249 % |
c |    282289 |  140571   493101 |  213527   79999  3801271    47.5 | 16.260 % |
c ==============================================================================
c (current CPU-time: 491.898 s)
c ==============================================================================
c [1mFound solution: 3968693[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4776096   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    294724 |  140613   493301 |   42183   92431  3996930    43.2 | 16.260 % |
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  31/31          
c |    294724 |  140603   493246 |      --   92431       --      -- |     --   | -10/-47
c |    294724 |  140603   493246 |   56241   92429  3996926    43.2 | 16.260 % |
c |    294824 |  140603   493246 |   61865   26326   269513    10.2 | 16.287 % |
c |    294974 |  140603   493246 |   68051   26476   270159    10.2 | 16.287 % |
c |    295199 |  140603   493246 |   74857   26701   271308    10.2 | 16.287 % |
c |    295536 |  140603   493246 |   82342   27038   273006    10.1 | 16.287 % |
c |    296043 |  140603   493246 |   90577   27545   275610    10.0 | 16.287 % |
c |    296802 |  140603   493246 |   99634   28304   280307     9.9 | 16.287 % |
c |    297941 |  140603   493246 |  109598   29443   299863    10.2 | 16.287 % |
c |    299649 |  140603   493246 |  120558   31151   314903    10.1 | 16.287 % |
c |    302211 |  140603   493246 |  132613   33713   339584    10.1 | 16.287 % |
c |    306055 |  140603   493246 |  145875   37557   377145    10.0 | 16.287 % |
c |    311821 |  140603   493246 |  160462   43323   437236    10.1 | 16.287 % |
c |    320470 |  140603   493246 |  176508   51972   576229    11.1 | 16.287 % |
c |    333446 |  140603   493246 |  194159   64948  1263704    19.5 | 16.287 % |
c |    352909 |  140586   493176 |  213550   84409  1704581    20.2 | 16.290 % |
c |    382101 |  140586   493176 |  234905  113601  2860816    25.2 | 16.290 % |
c |    425892 |  140586   493176 |  258395  157392  4745524    30.2 | 16.290 % |
c |    491576 |  140575   493139 |  284212  223074  8728136    39.1 | 16.294 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v X0_bit_7 -X0_bit_6 -X0_bit_5 X0_bit_4 -X0_bit_3 -X0_bit_2 X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 X1_bit_2 X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 X2_bit_6 -X2_bit_5 X2_bit_4 -X2_bit_3 X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 -X3_bit_6 -X3_bit_5 X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 X6_bit1 X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 X8_bit_2 -X8_bit_1 -X8_bit0 X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 X9_bit_6 -X9_bit_5 X9_bit_4 X9_bit_3 X9_bit_2 X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 X11_bit_6 -X11_bit_5 X11_bit_4 X11_bit_3 X11_bit_2 -X11_bit_1 X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 X12_bit_6 -X12_bit_5 X12_bit_4 X12_bit_3 X12_bit_2 X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 X14_bit_4 X14_bit_3 -X14_bit_2 X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 X15_bit_5 -X15_bit_4 X15_bit_3 X15_bit_2 X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 X17_bit_2 X17_bit_1 X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 X19_bit_5 X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 X21_bit_5 X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 X23_bit_4 X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 -X24_bit_6 -X24_bit_5 X24_bit_4 X24_bit_3 X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 -X25_bit_6 X25_bit_5 X25_bit_4 X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 X26_bit_5 X26_bit_4 X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 X27_bit_5 X27_bit_4 X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 X29_bit_6 X29_bit_5 X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 X30_bit_5 -X30_bit_4 X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 X31_bit_6 -X31_bit_5 X31_bit_4 X31_bit_3 -X31_bit_2 X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 X34_bit_4 -X34_bit_3 X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 X35_bit_6 X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 X38_bit_3 X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 -X41_bit_6 X41_bit_5 -X41_bit_4 -X41_bit_3 X41_bit_2 X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 -X42_bit_6 X42_bit_5 X42_bit_4 X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 X43_bit_6 X43_bit_5 X43_bit_4 -X43_bit_3 X43_bit_2 -X43_bit_1 X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 X44_bit_5 X44_bit_4 -X44_bit_3 X44_bit_2 X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 X45_bit_6 X45_bit_5 X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 X47_bit_5 X47_bit_4 -X47_bit_3 X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 X48_bit_2 X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 X49_bit_7 X49_bit_6 -X49_bit_5 X49_bit_4 -X49_bit_3 X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 -X52_bit_5 X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 X53_bit_6 X53_bit_5 X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 X54_bit_5 X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 X55_bit_6 X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 X56_bit_6 -X56_bit_5 X56_bit_4 -X56_bit_3 X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 X57_bit_7 -X57_bit_6 X57_bit_5 -X57_bit_4 -X57_bit_3 X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 X59_bit_5 -X59_bit_4 X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 X60_bit_6 -X60_bit_5 -X60_bit_4 X60_bit_3 X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 X61_bit_6 -X61_bit_5 -X61_bit_4 X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 X64_bit_6 X64_bit_5 X64_bit_4 -X64_bit_3 X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 X65_bit_6 -X65_bit_5 X65_bit_4 -X65_bit_3 X65_bit_2 -X65_bit_1 X65_bit0 -X65_bit1 X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 X67_bit_6 X67_bit_5 X67_bit_4 X67_bit_3 -X67_bit_2 -X67_bit_1 X67_bit0 -X67_bit1 X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 X69_bit_6 X69_bit_5 X69_bit_4 X69_bit_3 -X69_bit_2 -X69_bit_1 X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 X72_bit_6 X72_bit_5 -X72_bit_4 X72_bit_3 X72_bit_2 X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 X74_bit_6 X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 X76_bit_6 X76_bit_5 -X76_bit_4 X76_bit_3 -X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 X77_bit_5 -X77_bit_4 X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 X79_bit_5 X79_bit_4 X79_bit_3 X79_bit_2 X79_bit_1 X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 X80_bit_3 -X80_bit_2 X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 X83_bit_5 X83_bit_4 X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 X83_bit2 X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 X87_bit_4 -X87_bit_3 X87_bit_2 X87_bit_1 X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 X88_bit_2 X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 X89_bit_5 -X89_bit_4 -X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 X90_bit_6 X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 X91_bit_3 -X91_bit_2 -X91_bit_1 X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 X92_bit_2 X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 -X94_bit_6 X94_bit_5 X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 X94_bit0 X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 -X95_bit_6 X95_bit_5 X95_bit_4 X95_bit_3 X95_bit_2 X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 -X96_bit_6 -X96_bit_5 X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bit_6 X99_bit_5 X99_bit_4 X99_bit_3 X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 X101_bit_6 X101_bit_5 X101_bit_4 X101_bit_3 X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 X104_bit_7 X104_bit_6 -X104_bit_5 -X104_bit_4 X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 X106_bit_6 -X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 X107_bit_6 X107_bit_5 -X107_bit_4 X107_bit_3 X107_bit_2 -X107_bit_1 X107_bit0 -X107_bit1 X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 X108_bit_6 X108_bit_5 X108_bit_4 -X108_bit_3 X108_bit_2 X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 -X111_bit_5 X111_bit_4 X111_bit_3 X111_bit_2 X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 X112_bit_5 X112_bit_4 -X112_bit_3 X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 X115_bit_6 -X115_bit_5 X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 X115_bit0 -X115_bit1 X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 X117_bit_6 X117_bit_5 -X117_bit_4 X117_bit_3 X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 -X118_bit_6 -X118_bit_5 X118_bit_4 X118_bit_3 -X118_bit_2 X118_bit_1 X118_bit0 -X118_bit1 X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 X119_bit_6 -X119_bit_5 X119_bit_4 X119_bit_3 -X119_bit_2 X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 X122_bit_7 X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 X123_bit_6 X123_bit_5 -X123_bit_4 X123_bit_3 X123_bit_2 X123_bit_1 X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 X125_bit_7 X125_bit_6 X125_bit_5 X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 X127_bit_7 -X127_bit_6 X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 X128_bit_7 -X128_bit_6 X128_bit_5 -X128_bit_4 -X128_bit_3 X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 X129_bit_3 -X129_bit_2 X129_bit_1 X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 X131_bit_3 X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 X135_bit_6 X135_bit_5 X135_bit_4 X135_bit_3 -X135_bit_2 X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 X136_bit_6 -X136_bit_5 -X136_bit_4 X136_bit_3 -X136_bit_2 X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 -X137_bit_6 -X137_bit_5 X137_bit_4 -X137_bit_3 X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 X139_bit_6 X139_bit_5 X139_bit_4 -X139_bit_3 -X139_bit_2 X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 X140_bit_6 X140_bit_5 X140_bit_4 -X140_bit_3 X140_bit_2 X140_bit_1 -X140_bit0 -X140_bit1 X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 X141_bit_7 X141_bit_6 X141_bit_5 X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 X143_bit_7 X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 X143_bit_2 X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 X145_bit_3 X145_bit_2 -X145_bit_1 -X145_bit0 X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 X146_bit_3 X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 X150_bit_6 X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 X150_bit0 -X150_bit1 X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 X155_bit_3 X155_bit_2 -X155_bit_1 X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 X157_bit_7 X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 X159_bit_6 -X159_bit_5 -X159_bit_4 X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 X160_bit_5 X160_bit_4 X160_bit_3 X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 X161_bit_7 X161_bit_6 X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 X162_bit_6 -X162_bit_5 X162_bit_4 X162_bit_3 X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 X164_bit_7 X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 X165_bit_7 -X165_bit_6 X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 X167_bit_6 -X167_bit_5 X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 X168_bit_7 X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 X170_bit_7 -X170_bit_6 X170_bit_5 X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 X174_bit1 X174_bit2 X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 X175_bit_6 X175_bit_5 X175_bit_4 X175_bit_3 X175_bit_2 X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 X176_bit_7 X176_bit_6 X176_bit_5 -X176_bit_4 -X176_bit_3 X176_bit_2 -X176_bit_1 -X176_bit0 X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 X177_bit_6 X177_bit_5 -X177_bit_4 -X177_bit_3 X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 X179_bit_7 -X179_bit_6 X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 X181_bit_7 X181_bit_6 X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 X191_bit_2 X191_bit_1 X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 X194_bit_5 -X194_bit_4 X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 X197_bit_5 -X197_bit_4 X197_bit_3 X197_bit_2 X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 X198_bit_1 -X198_bit0 X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 X199_bit_6 -X199_bit_5 X199_bit_4 -X199_bit_3 -X199_bit_2 X199_bit_1 X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 -X200_bit_6 X200_bit_5 -X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 -X207_bit_6 X207_bit_5 -X207_bit_4 X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 X208_bit_5 X208_bit_4 X208_bit_3 X208_bit_2 X208_bit_1 -X208_bit0 X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 X209_bit_6 -X209_bit_5 X209_bit_4 -X209_bit_3 -X209_bit_2 X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 X211_bit_4 -X211_bit_3 X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 X214_bit_4 -X214_bit_3 X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 X216_bit_6 -X216_bit_5 -X216_bit_4 X216_bit_3 X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 X217_bit_6 X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 X217_bit_1 -X217_bit0 -X217_bit1 X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 X220_bit_4 -X220_bit_3 -X220_bit_2 X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 -X221_bit_6 -X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 X222_bit_1 -X222_bit0 X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 X223_bit_5 X223_bit_4 X223_bit_3 -X223_bit_2 X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 X224_bit_5 -X224_bit_4 -X224_bit_3 X224_bit_2 X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 X226_bit_7 X226_bit_6 X226_bit_5 -X226_bit_4 X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 X227_bit_4 -X227_bit_3 X227_bit_2 -X227_bit_1 -X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 -X228_bit_5 -X228_bit_4 X228_bit_3 X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 -X229_bit_6 X229_bit_5 -X229_bit_4 X229_bit_3 X229_bit_2 X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 X230_bit_6 -X230_bit_5 -X230_bit_4 X230_bit_3 -X230_bit_2 X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 X231_bit_6 -X231_bit_5 X231_bit_4 -X231_bit_3 -X231_bit_2 X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 X232_bit_7 X232_bit_6 -X232_bit_5 -X232_bit_4 X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 X233_bit_6 X233_bit_5 -X233_bit_4 -X233_bit_3 -X233_bit_2 X233_bit_1 -X233_bit0 -X233_bit1 X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 X234_bit_7 X234_bit_6 -X234_bit_5 -X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 -X235_bit_4 X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 X236_bit_5 X236_bit_4 -X236_bit_3 X236_bit_2 X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 X238_bit_1 -X238_bit0 -X238_bit1 X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 X240_bit_2 X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 X241_bit_3 X241_bit_2 X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 X243_bit_7 -X243_bit_6 -X243_bit_5 X243_bit_4 X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 X244_bit_6 X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 X245_bit_6 X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 X247_bit_5 X247_bit_4 X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 X250_bit_7 -X250_bit_6 X250_bit_5 -X250_bit_4 -X250_bit_3 X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 -X251_bit_4 X251_bit_3 -X251_bit_2 -X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 X252_bit_6 X252_bit_5 X252_bit_4 X252_bit_3 X252_bit_2 X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 -X253_bit_6 X253_bit_5 X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 X254_bit_6 -X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 -X255_bit_6 X255#### 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.92 0.98 0.99 2/54 25545
Raw data (stat): 25545 (runsolver) R 25544 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544548886 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 3480 0 0 0 991 8 0 0 25 0 1 0 544548886 16572416 3072 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4046 3072 603 41 0 4005 0
vsize: 16184
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 3694 0 0 0 1990 8 0 0 25 0 1 0 544548886 17391616 3286 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4246 3286 603 41 0 4205 0
vsize: 16984
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 3889 0 0 0 2989 9 0 0 25 0 1 0 544548886 18243584 3481 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4454 3481 603 41 0 4413 0
vsize: 17816
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 4041 0 0 0 3989 9 0 0 25 0 1 0 544548886 18784256 3633 4294967295 134512640 134672761 3221224544 3221223696 134565149 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4586 3633 603 41 0 4545 0
vsize: 18344
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 4251 0 0 0 4988 10 0 0 25 0 1 0 544548886 19718144 3843 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 3843 603 41 0 4773 0
vsize: 19256
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 4914 0 0 0 5986 12 0 0 25 0 1 0 544548886 22515712 4506 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5497 4506 603 41 0 5456 0
vsize: 21988
[startup+70.002 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 5317 0 0 0 6984 14 0 0 25 0 1 0 544548886 23994368 4909 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5858 4909 603 41 0 5817 0
vsize: 23432
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 5755 0 0 0 7983 15 0 0 25 0 1 0 544548886 26128384 5347 4294967295 134512640 134672761 3221224544 3221223680 134614753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6379 5347 603 41 0 6338 0
vsize: 25516
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 6175 0 0 0 8982 16 0 0 25 0 1 0 544548886 27721728 5767 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6768 5767 603 41 0 6727 0
vsize: 27072
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14075 0 0 0 9964 34 0 0 25 0 1 0 544548886 54923264 12199 4294967295 134512640 134672761 3221224544 3221223088 134621359 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13409 12199 603 41 0 13368 0
vsize: 53636
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 10963 35 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 11963 35 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 12963 35 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 13963 35 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 14963 35 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 14399 0 0 0 15963 36 0 0 25 0 1 0 544548886 55296000 12302 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13500 12302 603 41 0 13459 0
vsize: 54000
[startup+170.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 15491 0 0 0 16960 39 0 0 25 0 1 0 544548886 56352768 12537 4294967295 134512640 134672761 3221224544 3221223744 134610630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12537 603 41 0 13717 0
vsize: 55032
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16477 0 0 0 17956 41 0 0 25 0 1 0 544548886 55762944 12393 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13614 12393 603 41 0 13573 0
vsize: 54456
[startup+190.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25545
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16477 0 0 0 18957 41 0 0 25 0 1 0 544548886 55762944 12393 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13614 12393 603 41 0 13573 0
vsize: 54456
[startup+200.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16477 0 0 0 19957 41 0 0 25 0 1 0 544548886 55762944 12393 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13614 12393 603 41 0 13573 0
vsize: 54456
[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16554 0 0 0 20955 42 0 0 25 0 1 0 544548886 56164352 12470 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13712 12470 603 41 0 13671 0
vsize: 54848
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16696 0 0 0 21954 43 0 0 25 0 1 0 544548886 56700928 12612 4294967295 134512640 134672761 3221224544 3221223584 134613001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13843 12612 603 41 0 13802 0
vsize: 55372
[startup+230.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 16953 0 0 0 22953 44 0 0 25 0 1 0 544548886 57765888 12869 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14103 12869 603 41 0 14062 0
vsize: 56412
[startup+240.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 17075 0 0 0 23953 44 0 0 25 0 1 0 544548886 58167296 12991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14201 12991 603 41 0 14160 0
vsize: 56804
[startup+250.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 17385 0 0 0 24952 45 0 0 25 0 1 0 544548886 59498496 13301 4294967295 134512640 134672761 3221224544 3221223712 134614524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14526 13301 603 41 0 14485 0
vsize: 58104
[startup+260.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 25948 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+270.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 26947 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+280.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 27947 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+290.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 28947 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+300.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 29948 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+310.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 30949 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+320.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 31950 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+330.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18715 0 0 0 32950 50 0 0 25 0 1 0 544548886 60080128 13419 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14668 13419 603 41 0 14627 0
vsize: 58672
[startup+340.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 18746 0 0 0 33950 50 0 0 25 0 1 0 544548886 60211200 13450 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14700 13450 603 41 0 14659 0
vsize: 58800
[startup+350.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 19950 0 0 0 34946 54 0 0 25 0 1 0 544548886 65224704 14654 4294967295 134512640 134672761 3221224544 3221223680 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15924 14654 603 41 0 15883 0
vsize: 63696
[startup+360.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 35942 58 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+370.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 36941 58 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+380.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 37941 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+390.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 38941 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+400.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 39941 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+410.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 40941 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+420.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 41942 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+430.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 42942 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+440.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 43942 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+450.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 44942 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+460.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21301 0 0 0 45942 59 0 0 25 0 1 0 544548886 65736704 14807 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16049 14807 603 41 0 16008 0
vsize: 64196
[startup+470.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21624 0 0 0 46942 60 0 0 25 0 1 0 544548886 67059712 15130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16372 15130 603 41 0 16331 0
vsize: 65488
[startup+480.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21699 0 0 0 47942 60 0 0 25 0 1 0 544548886 67465216 15205 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16471 15205 603 41 0 16430 0
vsize: 65884
[startup+490.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 21871 0 0 0 48942 60 0 0 25 0 1 0 544548886 68124672 15377 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16632 15377 603 41 0 16591 0
vsize: 66528
[startup+500.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 49939 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+510.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 50938 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+520.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 51938 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+530.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 52938 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+540.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 53939 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+550.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 54939 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+560.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 55939 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223480 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+570.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 56939 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+580.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 57940 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+590.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 58940 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+600.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 59940 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+610.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 60941 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+620.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23007 0 0 0 61941 63 0 0 25 0 1 0 544548886 69296128 15677 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15677 603 41 0 16877 0
vsize: 67672
[startup+630.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23015 0 0 0 62941 64 0 0 25 0 1 0 544548886 69296128 15685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15685 603 41 0 16877 0
vsize: 67672
[startup+640.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23021 0 0 0 63942 64 0 0 25 0 1 0 544548886 69296128 15691 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15691 603 41 0 16877 0
vsize: 67672
[startup+650.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23025 0 0 0 64943 64 0 0 25 0 1 0 544548886 69296128 15695 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15695 603 41 0 16877 0
vsize: 67672
[startup+660.079 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23029 0 0 0 65943 64 0 0 25 0 1 0 544548886 69296128 15699 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15699 603 41 0 16877 0
vsize: 67672
[startup+670.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23034 0 0 0 66943 64 0 0 25 0 1 0 544548886 69296128 15704 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 15704 603 41 0 16877 0
vsize: 67672
[startup+680.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23039 0 0 0 67943 64 0 0 25 0 1 0 544548886 69820416 15709 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17046 15709 603 41 0 17005 0
vsize: 68184
[startup+690.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23057 0 0 0 68943 64 0 0 25 0 1 0 544548886 69955584 15727 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17079 15727 603 41 0 17038 0
vsize: 68316
[startup+700.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23237 0 0 0 69943 64 0 0 25 0 1 0 544548886 70627328 15907 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17243 15907 603 41 0 17202 0
vsize: 68972
[startup+710.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 23770 0 0 0 70942 65 0 0 25 0 1 0 544548886 72761344 16440 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17764 16440 603 41 0 17723 0
vsize: 71056
[startup+720.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 24125 0 0 0 71941 66 0 0 25 0 1 0 544548886 74215424 16795 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18119 16795 603 41 0 18078 0
vsize: 72476
[startup+730.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 24468 0 0 0 72940 67 0 0 25 0 1 0 544548886 75681792 17138 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18477 17138 603 41 0 18436 0
vsize: 73908
[startup+740.082 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 25350 0 0 0 73938 70 0 0 25 0 1 0 544548886 79249408 18020 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19348 18020 603 41 0 19307 0
vsize: 77392
[startup+750.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 26090 0 0 0 74936 72 0 0 25 0 1 0 544548886 82161664 18760 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20059 18760 603 41 0 20018 0
vsize: 80236
[startup+760.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 26344 0 0 0 75935 73 0 0 25 0 1 0 544548886 83238912 19014 4294967295 134512640 134672761 3221224544 3221223680 134614699 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20322 19014 603 41 0 20281 0
vsize: 81288
[startup+770.083 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 26623 0 0 0 76935 74 0 0 25 0 1 0 544548886 84307968 19293 4294967295 134512640 134672761 3221224544 3221223536 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20583 19293 603 41 0 20542 0
vsize: 82332
[startup+780.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 27028 0 0 0 77933 75 0 0 25 0 1 0 544548886 86044672 19698 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21007 19698 603 41 0 20966 0
vsize: 84028
[startup+790.084 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 27484 0 0 0 78932 77 0 0 25 0 1 0 544548886 87891968 20154 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21458 20154 603 41 0 21417 0
vsize: 85832
[startup+800.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 27846 0 0 0 79931 78 0 0 25 0 1 0 544548886 89247744 20516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21789 20516 603 41 0 21748 0
vsize: 87156
[startup+810.085 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 28114 0 0 0 80930 80 0 0 25 0 1 0 544548886 90451968 20784 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22083 20784 603 41 0 22042 0
vsize: 88332
[startup+820.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 28628 0 0 0 81928 81 0 0 25 0 1 0 544548886 92450816 21298 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22571 21298 603 41 0 22530 0
vsize: 90284
[startup+830.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 28878 0 0 0 82928 82 0 0 25 0 1 0 544548886 93511680 21548 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22830 21548 603 41 0 22789 0
vsize: 91320
[startup+840.086 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 29095 0 0 0 83927 82 0 0 25 0 1 0 544548886 94322688 21765 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23028 21765 603 41 0 22987 0
vsize: 92112
[startup+850.087 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 29361 0 0 0 84927 83 0 0 25 0 1 0 544548886 95383552 22031 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23287 22031 603 41 0 23246 0
vsize: 93148
[startup+860.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 29526 0 0 0 85927 84 0 0 25 0 1 0 544548886 96047104 22196 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23449 22196 603 41 0 23408 0
vsize: 93796
[startup+870.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 29774 0 0 0 86926 85 0 0 25 0 1 0 544548886 97103872 22444 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23707 22444 603 41 0 23666 0
vsize: 94828
[startup+880.088 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 30055 0 0 0 87925 86 0 0 25 0 1 0 544548886 98336768 22725 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24008 22725 603 41 0 23967 0
vsize: 96032
[startup+890.089 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 30185 0 0 0 88924 87 0 0 25 0 1 0 544548886 98746368 22855 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24108 22855 603 41 0 24067 0
vsize: 96432
[startup+900.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 30435 0 0 0 89923 88 0 0 25 0 1 0 544548886 99819520 23105 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24370 23105 603 41 0 24329 0
vsize: 97480
[startup+910.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 30766 0 0 0 90922 89 0 0 25 0 1 0 544548886 101138432 23436 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24692 23436 603 41 0 24651 0
vsize: 98768
[startup+920.09 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 31119 0 0 0 91921 90 0 0 25 0 1 0 544548886 102608896 23789 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25051 23789 603 41 0 25010 0
vsize: 100204
[startup+930.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 31416 0 0 0 92920 91 0 0 25 0 1 0 544548886 103821312 24086 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25347 24086 603 41 0 25306 0
vsize: 101388
[startup+940.091 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 31726 0 0 0 93919 92 0 0 25 0 1 0 544548886 105046016 24396 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25646 24396 603 41 0 25605 0
vsize: 102584
[startup+950.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 31989 0 0 0 94919 93 0 0 25 0 1 0 544548886 107163648 24659 4294967295 134512640 134672761 3221224544 3221223584 134614225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26163 24659 603 41 0 26122 0
vsize: 104652
[startup+960.092 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 32276 0 0 0 95919 94 0 0 25 0 1 0 544548886 108367872 24946 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26457 24946 603 41 0 26416 0
vsize: 105828
[startup+970.093 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 32550 0 0 0 96919 94 0 0 25 0 1 0 544548886 109441024 25220 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26719 25220 603 41 0 26678 0
vsize: 106876
[startup+980.094 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 32799 0 0 0 97918 95 0 0 25 0 1 0 544548886 110522368 25469 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26983 25469 603 41 0 26942 0
vsize: 107932
[startup+990.094 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 33022 0 0 0 98918 95 0 0 25 0 1 0 544548886 111321088 25692 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27178 25692 603 41 0 27137 0
vsize: 108712
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 33294 0 0 0 99917 96 0 0 25 0 1 0 544548886 112504832 25964 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27467 25964 603 41 0 27426 0
vsize: 109868
[startup+1010.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 33528 0 0 0 100917 97 0 0 25 0 1 0 544548886 113561600 26198 4294967295 134512640 134672761 3221224544 3221223540 1075346562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27725 26198 603 41 0 27684 0
vsize: 110900
[startup+1020.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 33771 0 0 0 101916 98 0 0 25 0 1 0 544548886 114487296 26441 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27951 26441 603 41 0 27910 0
vsize: 111804
[startup+1030.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 34030 0 0 0 102916 98 0 0 25 0 1 0 544548886 115548160 26700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28210 26700 603 41 0 28169 0
vsize: 112840
[startup+1040.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 34257 0 0 0 103915 99 0 0 25 0 1 0 544548886 116473856 26927 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28436 26927 603 41 0 28395 0
vsize: 113744
[startup+1050.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 34509 0 0 0 104915 100 0 0 25 0 1 0 544548886 117530624 27179 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28694 27179 603 41 0 28653 0
vsize: 114776
[startup+1060.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 34767 0 0 0 105914 100 0 0 25 0 1 0 544548886 118599680 27437 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28955 27437 603 41 0 28914 0
vsize: 115820
[startup+1070.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 35013 0 0 0 106913 102 0 0 25 0 1 0 544548886 119517184 27683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29179 27683 603 41 0 29138 0
vsize: 116716
[startup+1080.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 35269 0 0 0 107912 103 0 0 25 0 1 0 544548886 120578048 27939 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29438 27939 603 41 0 29397 0
vsize: 117752
[startup+1090.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 35487 0 0 0 108912 103 0 0 25 0 1 0 544548886 121520128 28157 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29668 28157 603 41 0 29627 0
vsize: 118672
[startup+1100.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 35729 0 0 0 109911 104 0 0 25 0 1 0 544548886 122490880 28399 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29905 28399 603 41 0 29864 0
vsize: 119620
[startup+1110.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 35971 0 0 0 110911 105 0 0 25 0 1 0 544548886 123576320 28641 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30170 28641 603 41 0 30129 0
vsize: 120680
[startup+1120.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 36187 0 0 0 111910 105 0 0 25 0 1 0 544548886 124395520 28857 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30370 28857 603 41 0 30329 0
vsize: 121480
[startup+1130.1 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 36404 0 0 0 112910 106 0 0 25 0 1 0 544548886 125370368 29074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30608 29074 603 41 0 30567 0
vsize: 122432
[startup+1140.1 s]
Raw data (loadavg): 1.07 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 36629 0 0 0 113909 107 0 0 25 0 1 0 544548886 126304256 29299 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30836 29299 603 41 0 30795 0
vsize: 123344
[startup+1150.1 s]
Raw data (loadavg): 1.06 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 36834 0 0 0 114909 107 0 0 25 0 1 0 544548886 127098880 29504 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31030 29504 603 41 0 30989 0
vsize: 124120
[startup+1160.1 s]
Raw data (loadavg): 1.05 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 37037 0 0 0 115909 108 0 0 25 0 1 0 544548886 127918080 29707 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31230 29707 603 41 0 31189 0
vsize: 124920
[startup+1170.1 s]
Raw data (loadavg): 1.04 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 37556 0 0 0 116908 109 0 0 25 0 1 0 544548886 130801664 30226 4294967295 134512640 134672761 3221224544 3221223600 134644229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31934 30226 603 41 0 31893 0
vsize: 127736
[startup+1180.1 s]
Raw data (loadavg): 1.04 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 37746 0 0 0 117907 110 0 0 25 0 1 0 544548886 130277376 30113 4294967295 134512640 134672761 3221224544 3221223480 1075350787 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31806 30113 603 41 0 31765 0
vsize: 127224
[startup+1190.1 s]
Raw data (loadavg): 1.03 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 37746 0 0 0 118907 110 0 0 25 0 1 0 544548886 130277376 30113 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31806 30113 603 41 0 31765 0
vsize: 127224
[startup+1200.1 s]
Raw data (loadavg): 1.03 1.00 1.00 2/54 25547
Raw data (stat): 25545 (minisat+) R 25544 23176 23175 0 -1 0 37746 0 0 0 119908 110 0 0 25 0 1 0 544548886 130277376 30113 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31806 30113 603 41 0 31765 0
vsize: 127224
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.03 1.00 1.00 1/54 25547
Raw data (stat): 25545 (minisat+) Z 25544 23176 23175 0 -1 12 37747 0 0 0 119908 116 0 0 25 0 1 0 544548886 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.18
CPU time (s): 1200.25
CPU user time (s): 1199.09
CPU system time (s): 1.16082
CPU usage (%): 100.006
Max. virtual memory (Kb): 127736
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####