PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 11:02:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19302 boxname=wulflinc26 idbench=1485 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a7baaeaa26a0026c630e11c495604909  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran14x18.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran14x18.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-ran14x18.opb
IDLAUNCH: 19302
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        554516 kB
Buffers:         25416 kB
Cached:         424540 kB
SwapCached:         68 kB
Active:          54856 kB
Inactive:       398024 kB
HighTotal:      131008 kB
HighFree:         7448 kB
LowTotal:       903652 kB
LowFree:        547068 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            21824 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:22:57 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19302 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 386   maxlim: 47470   bits: 16/16
c ---[ 312]---> Adder-cost: 386   maxlim: 47726   bits: 16/16
c ---[ 310]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 308]---> Adder-cost: 388   maxlim: 58222   bits: 16/16
c ---[ 306]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 304]---> Adder-cost: 386   maxlim: 46830   bits: 16/16
c ---[ 302]---> Adder-cost: 386   maxlim: 47086   bits: 16/16
c ---[ 300]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 298]---> Adder-cost: 386   maxlim: 46702   bits: 16/16
c ---[ 296]---> Adder-cost: 386   maxlim: 46958   bits: 16/16
c ---[ 294]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 292]---> Adder-cost: 386   maxlim: 48110   bits: 16/16
c ---[ 290]---> Adder-cost: 386   maxlim: 47982   bits: 16/16
c ---[ 288]---> Adder-cost: 388   maxlim: 57582   bits: 16/16
c ---[ 286]---> Adder-cost: 260   maxlim: 13554   bits: 14/14
c ---[ 284]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 282]---> Adder-cost: 260   maxlim: 13426   bits: 14/14
c ---[ 280]---> Adder-cost: 310   maxlim: 50930   bits: 16/16
c ---[ 278]---> Adder-cost: 286   maxlim: 26866   bits: 15/15
c ---[ 276]---> Adder-cost: 310   maxlim: 50418   bits: 16/16
c ---[ 274]---> Adder-cost: 312   maxlim: 57202   bits: 16/16
c ---[ 272]---> Adder-cost: 312   maxlim: 55666   bits: 16/16
c ---[ 270]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 268]---> Adder-cost: 286   maxlim: 27634   bits: 15/15
c ---[ 266]---> Adder-cost: 310   maxlim: 50546   bits: 16/16
c ---[ 264]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 262]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 260]---> Adder-cost: 260   maxlim: 13810   bits: 14/14
c ---[ 258]---> Adder-cost: 312   maxlim: 56946   bits: 16/16
c ---[ 256]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 254]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 252]---> Adder-cost: 286   maxlim: 27506   bits: 15/15
c ---[ 251]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 249]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 247]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 246]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 245]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 244]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 243]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 242]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 240]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 237]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 236]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 235]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 234]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 232]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 231]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 227]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 226]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 225]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 224]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 223]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 221]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 218]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 217]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 216]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 215]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 214]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 212]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 211]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 210]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 209]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 205]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 204]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 203]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 202]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 200]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 199]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 198]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 197]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 196]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 195]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 194]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 193]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 192]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 188]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 187]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 186]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 185]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 184]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 183]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 181]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 180]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 179]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 177]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 175]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 173]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 172]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 170]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 169]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 168]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 167]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 165]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 164]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 163]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 162]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 161]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 159]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 157]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 156]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 153]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 152]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 150]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 149]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 147]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 145]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 144]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 143]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 141]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 138]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 137]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 136]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 134]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 132]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 131]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 130]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 127]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 124]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 123]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 122]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 119]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 118]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 115]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 114]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 113]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 112]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 110]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 107]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 106]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 105]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 103]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 102]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 100]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  98]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  97]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  95]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  93]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  92]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  91]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  89]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  87]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  85]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  83]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  82]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  80]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  77]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  76]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  75]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  71]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  70]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  69]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  66]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  62]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  61]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  54]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  52]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  45]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  41]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  30]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  26]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  25]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  20]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  19]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  14]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  13]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   82180   302580 |   27393       0        0     nan |  0.000 % |
c |       100 |   82180   302580 |   30132     100      283     2.8 | 28.708 % |
c |       250 |   82106   302336 |   33145     241      920     3.8 | 28.770 % |
c |       475 |   82106   302336 |   36460     466     1618     3.5 | 28.770 % |
c |       812 |   82081   302247 |   40106     799     3610     4.5 | 28.789 % |
c |      1318 |   81997   301967 |   44116    1296     5797     4.5 | 28.866 % |
c |      2077 |   81709   300987 |   48528    1989    10026     5.0 | 29.119 % |
c |      3216 |   81518   300336 |   53381    3104    16760     5.4 | 29.282 % |
c |      4924 |   81133   299035 |   58719    4756    26464     5.6 | 29.616 % |
c |      7486 |   80785   297859 |   64591    7266    40479     5.6 | 29.917 % |
c |     11330 |   80168   295764 |   71050   11028    59246     5.4 | 30.453 % |
c |     17096 |   79369   293077 |   78155   16705    88732     5.3 | 31.170 % |
c |     25745 |   78871   291393 |   85970   25284   136569     5.4 | 31.595 % |
c |     38719 |   78552   290320 |   94568   38207   218999     5.7 | 31.872 % |
c |     58180 |   78155   288983 |  104024   57608   371564     6.4 | 32.212 % |
c |     87372 |   78012   288508 |  114427   86782   694180     8.0 | 32.345 % |
c |    131161 |   77906   288156 |  125870   38388   451905    11.8 | 32.432 % |
c |    196845 |   77872   288044 |  138457  104065  1355765    13.0 | 32.460 % |
c |    295371 |   77804   287808 |  152302   85402  1863736    21.8 | 32.522 % |
c ==============================================================================
c [1mFound solution: 5430552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10447   maxlim: 3559073   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    318897 |  150774   548448 |   50258  108922  2224150    20.4 | 32.522 % |
c |    318998 |  150774   548448 |   55283   28670   268864     9.4 | 21.745 % |
c |    319148 |  150774   548448 |   60812   28820   269610     9.4 | 21.745 % |
c |    319373 |  150774   548448 |   66893   29045   270724     9.3 | 21.745 % |
c |    319710 |  150774   548448 |   73582   29382   272337     9.3 | 21.745 % |
c |    320216 |  150774   548448 |   80941   29888   274763     9.2 | 21.745 % |
c |    320975 |  150767   548425 |   89035   30646   278695     9.1 | 21.748 % |
c |    322114 |  150767   548425 |   97938   31785   284810     9.0 | 21.748 % |
c |    323822 |  150767   548425 |  107732   33493   295820     8.8 | 21.748 % |
c |    326384 |  150767   548425 |  118505   36055   312399     8.7 | 21.748 % |
c |    330228 |  150767   548425 |  130356   39899   347499     8.7 | 21.748 % |
c |    335995 |  150767   548425 |  143391   45666   394882     8.6 | 21.748 % |
c |    344644 |  150758   548396 |  157731   54314   473169     8.7 | 21.754 % |
c |    357618 |  150751   548373 |  173504   67287   628505     9.3 | 21.757 % |
c ==============================================================================
c [1mFound solution: 5171926[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3817699   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    365955 |  150765   548495 |   50255   75624   755191    10.0 | 21.757 % |
c |    366055 |  150765   548495 |   55280   28686   220819     7.7 | 21.774 % |
c |    366205 |  150765   548495 |   60808   28836   221568     7.7 | 21.774 % |
c |    366430 |  150765   548495 |   66889   29061   222794     7.7 | 21.774 % |
c |    366767 |  150765   548495 |   73578   29398   224466     7.6 | 21.774 % |
c |    367276 |  150756   548466 |   80936   29906   226871     7.6 | 21.780 % |
c |    368035 |  150756   548466 |   89029   30665   230791     7.5 | 21.780 % |
c |    369174 |  150756   548466 |   97932   31804   237390     7.5 | 21.780 % |
c |    370882 |  150756   548466 |  107726   33512   248022     7.4 | 21.780 % |
c |    373444 |  150756   548466 |  118498   36074   265536     7.4 | 21.780 % |
c |    377289 |  150756   548466 |  130348   39919   298961     7.5 | 21.780 % |
c |    383056 |  150756   548466 |  143383   45686   412907     9.0 | 21.780 % |
c |    391705 |  150756   548466 |  157721   54335   511508     9.4 | 21.780 % |
c |    404679 |  150747   548437 |  173493   67307   747839    11.1 | 21.787 % |
c ==============================================================================
c [1mFound solution: 4781239[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4208386   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    411548 |  150782   548652 |   50260   74176   839161    11.3 | 21.787 % |
c |    411649 |  150782   548652 |   55286   28612   252292     8.8 | 21.804 % |
c |    411799 |  150782   548652 |   60814   28762   253020     8.8 | 21.804 % |
c |    412024 |  150782   548652 |   66896   28987   254151     8.8 | 21.804 % |
c |    412361 |  150782   548652 |   73585   29324   256319     8.7 | 21.804 % |
c |    412867 |  150782   548652 |   80944   29830   260520     8.7 | 21.804 % |
c |    413626 |  150782   548652 |   89038   30589   265361     8.7 | 21.804 % |
c |    414765 |  150782   548652 |   97942   31728   274805     8.7 | 21.804 % |
c |    416473 |  150782   548652 |  107736   33436   287025     8.6 | 21.804 % |
c |    419035 |  150782   548652 |  118510   35998   312430     8.7 | 21.804 % |
c |    422879 |  150782   548652 |  130361   39842   349960     8.8 | 21.804 % |
c |    428645 |  150782   548652 |  143397   45608   415023     9.1 | 21.804 % |
c |    437294 |  150782   548652 |  157737   54257   561302    10.3 | 21.804 % |
c |    450269 |  150775   548629 |  173511   67230   765709    11.4 | 21.807 % |
c |    469730 |  150740   548510 |  190862   86686  1099560    12.7 | 21.826 % |
c ==============================================================================
c [1mFound solution: 4721575[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4268050   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    479544 |  150747   548610 |   50249   96499  1263914    13.1 | 21.826 % |
c |    479644 |  150747   548610 |   55273   29673   242759     8.2 | 21.843 % |
c |    479794 |  150747   548610 |   60801   29823   243492     8.2 | 21.843 % |
c |    480019 |  150731   548558 |   66881   30044   244526     8.1 | 21.853 % |
c |    480356 |  150731   548558 |   73569   30381   246625     8.1 | 21.853 % |
c |    480863 |  150731   548558 |   80926   30888   249089     8.1 | 21.853 % |
c |    481622 |  150731   548558 |   89019   31647   253254     8.0 | 21.853 % |
c |    482761 |  150731   548558 |   97921   32786   259456     7.9 | 21.853 % |
c |    484469 |  150731   548558 |  107713   34494   269718     7.8 | 21.853 % |
c |    487032 |  150731   548558 |  118484   37057   286385     7.7 | 21.853 % |
c |    490876 |  150731   548558 |  130332   40901   315724     7.7 | 21.853 % |
c |    496642 |  150731   548558 |  143366   46667   383202     8.2 | 21.853 % |
c |    505291 |  150731   548558 |  157702   55316   470941     8.5 | 21.853 % |
c |    518265 |  150731   548558 |  173473   68290   653280     9.6 | 21.853 % |
c |    537727 |  150731   548558 |  190820   87752  1138933    13.0 | 21.853 % |
c ==============================================================================
c [1mFound solution: 4469888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4519737   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    557649 |  150743   548743 |   50247  107670  1521131    14.1 | 21.853 % |
c |    557749 |  150743   548743 |   55271   31975   302852     9.5 | 21.883 % |
c |    557899 |  150743   548743 |   60798   32125   303608     9.5 | 21.883 % |
c |    558124 |  150743   548743 |   66878   32350   304819     9.4 | 21.883 % |
c |    558462 |  150743   548743 |   73566   32688   307264     9.4 | 21.883 % |
c |    558969 |  150743   548743 |   80923   33195   310685     9.4 | 21.883 % |
c |    559728 |  150743   548743 |   89015   33954   316371     9.3 | 21.883 % |
c |    560867 |  150743   548743 |   97917   35093   323657     9.2 | 21.883 % |
c |    562575 |  150743   548743 |  107708   36801   337148     9.2 | 21.883 % |
c |    565138 |  150743   548743 |  118479   39364   359135     9.1 | 21.883 % |
c |    568982 |  150743   548743 |  130327   43208   394168     9.1 | 21.883 % |
c |    574748 |  150743   548743 |  143360   48974   448475     9.2 | 21.883 % |
c |    583397 |  150743   548743 |  157696   57623   529174     9.2 | 21.883 % |
c |    596372 |  150743   548743 |  173466   70598   920305    13.0 | 21.883 % |
c ==============================================================================
c [1mFound solution: 4196273[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4793352   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    610726 |  150751   548835 |   50250   84952  1112694    13.1 | 21.883 % |
c |    610826 |  150751   548835 |   55275   30639   232178     7.6 | 21.897 % |
c |    610977 |  150751   548835 |   60802   30790   232878     7.6 | 21.897 % |
c |    611202 |  150751   548835 |   66882   31015   234050     7.5 | 21.897 % |
c |    611539 |  150751   548835 |   73571   31352   235712     7.5 | 21.897 % |
c |    612045 |  150751   548835 |   80928   31858   238374     7.5 | 21.897 % |
c |    612804 |  150751   548835 |   89020   32617   242385     7.4 | 21.897 % |
c |    613943 |  150751   548835 |   97923   33756   248881     7.4 | 21.897 % |
c |    615651 |  150751   548835 |  107715   35464   259457     7.3 | 21.897 % |
c |    618213 |  150751   548835 |  118486   38026   276582     7.3 | 21.897 % |
c |    622057 |  150751   548835 |  130335   41870   309055     7.4 | 21.897 % |
c |    627825 |  150751   548835 |  143369   47638   443097     9.3 | 21.897 % |
c |    636474 |  150742   548804 |  157706   56284   609880    10.8 | 21.900 % |
c |    649448 |  150733   548773 |  173476   69252   757385    10.9 | 21.903 % |
c |    668910 |  150733   548773 |  190824   88714  1687621    19.0 | 21.903 % |
c |    698102 |  150733   548773 |  209906  117906  2723285    23.1 | 21.903 % |
c ==============================================================================
c [1mFound solution: 3730741[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5258884   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    726091 |  150749   548929 |   50249  145895  3754494    25.7 | 21.903 % |
c |    726191 |  150749   548929 |   55273   29507   540688    18.3 | 21.922 % |
c |    726341 |  150749   548929 |   60801   29657   541337    18.3 | 21.922 % |
c |    726566 |  150749   548929 |   66881   29882   542310    18.1 | 21.922 % |
c |    726903 |  150749   548929 |   73569   30219   543781    18.0 | 21.922 % |
c |    727409 |  150749   548929 |   80926   30725   545907    17.8 | 21.922 % |
c |    728168 |  150749   548929 |   89019   31484   549121    17.4 | 21.922 % |
c |    729307 |  150749   548929 |   97921   32623   554948    17.0 | 21.922 % |
c |    731015 |  150749   548929 |  107713   34331   564507    16.4 | 21.922 % |
c |    733577 |  150749   548929 |  118484   36893   581226    15.8 | 21.922 % |
c |    737421 |  150749   548929 |  130332   40737   606901    14.9 | 21.922 % |
c |    743187 |  150749   548929 |  143366   46503   652418    14.0 | 21.922 % |
c |    751837 |  150749   548929 |  157702   55153   750747    13.6 | 21.922 % |
c |    764811 |  150749   548929 |  173473   68127   874057    12.8 | 21.922 % |
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 -Y0_bit0 -Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 -Y11_bit0 -Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 -Y17_bit0 -Y18_bit0 Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 -Y23_bit0 Y24_bit0 -Y25_bit0 -Y26_bit0 -Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 Y43_bit0 -Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 -Y53_bit0 -Y54_bit0 -Y55_bit0 Y56_bit0 -Y57_bit0 -Y58_bit0 Y59_bit0 -Y60_bit0 Y61_bit0 Y62_bit0 Y63_bit0 -Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 -Y69_bit0 Y70_bit0 Y71_bit0 -Y72_bit0 Y73_bit0 Y74_bit0 Y75_bit0 -Y76_bit0 Y77_bit0 Y78_bit0 -Y79_bit0 Y80_bit0 -Y81_bit0 Y82_bit0 Y83_bit0 -Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 Y88_bit0 -Y89_bit0 -Y90_bit0 Y91_bit0 Y92_bit0 -Y93_bit0 Y94_bit0 Y95_bit0 -Y96_bit0 Y97_bit0 Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 -Y104_bit0 -Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 Y110_bit0 Y111_bit0 Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 Y118_bit0 Y119_bit0 Y120_bit0 Y121_bit0 Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 Y128_bit0 Y129_bit0 Y130_bit0 -Y131_bit0 Y132_bit0 -Y133_bit0 Y134_bit0 Y135_bit0 Y136_bit0 -Y137_bit0 Y138_bit0 Y139_bit0 Y140_bit0 Y141_bit0 Y142_bit0 -Y143_bit0 -Y144_bit0 Y145_bit0 -Y146_bit0 Y147_bit0 Y148_bit0 Y149_bit0 Y150_bit0 Y151_bit0 Y152_bit0 -Y153_bit0 Y154_bit0 Y155_bit0 Y156_bit0 Y157_bit0 Y158_bit0 Y159_bit0 Y160_bit0 Y161_bit0 Y162_bit0 Y163_bit0 Y164_bit0 Y165_bit0 -Y166_bit0 -Y167_bit0 Y168_bit0 -Y169_bit0 Y170_bit0 -Y171_bit0 -Y172_bit0 Y173_bit0 Y174_bit0 -Y175_bit0 -Y176_bit0 -Y177_bit0 Y178_bit0 -Y179_bit0 Y180_bit0 -Y181_bit0 Y182_bit0 Y183_bit0 Y184_bit0 -Y185_bit0 Y186_bit0 -Y187_bit0 Y188_bit0 Y189_bit0 -Y190_bit0 Y191_bit0 -Y192_bit0 -Y193_bit0 -Y194_bit0 -Y195_bit0 -Y196_bit0 Y197_bit0 Y198_bit0 Y199_bit0 Y200_bit0 Y201_bit0 Y202_bit0 -Y203_bit0 -Y204_bit0 Y205_bit0 Y206_bit0 Y207_bit0 Y208_bit0 Y209_bit0 Y210_bit0 Y211_bit0 -Y212_bit0 Y213_bit0 -Y214_bit0 Y215_bit0 Y216_bit0 -Y217_bit0 Y218_bit0 Y219_bit0 Y220_bit0 -Y221_bit0 Y222_bit0 Y223_bit0 Y224_bit0 Y225_bit0 Y226_bit0 Y227_bit0 Y228_bit0 Y229#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.93 2/54 30924
Raw data (stat): 30924 (runsolver) R 30923 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544572837 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2451 0 0 0 993 5 0 0 25 0 1 0 544572837 12697600 2376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3100 2376 603 41 0 3059 0
vsize: 12400
[startup+20.0019 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2531 0 0 0 1993 6 0 0 25 0 1 0 544572837 12963840 2456 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3165 2456 603 41 0 3124 0
vsize: 12660
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2593 0 0 0 2993 6 0 0 25 0 1 0 544572837 13344768 2518 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3258 2518 603 41 0 3217 0
vsize: 13032
[startup+40.0029 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2663 0 0 0 3992 7 0 0 25 0 1 0 544572837 13615104 2588 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3324 2588 603 41 0 3283 0
vsize: 13296
[startup+50.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2733 0 0 0 4991 8 0 0 25 0 1 0 544572837 13885440 2658 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3390 2658 603 41 0 3349 0
vsize: 13560
[startup+60.0047 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2815 0 0 0 5991 8 0 0 25 0 1 0 544572837 14147584 2740 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 2740 603 41 0 3413 0
vsize: 13816
[startup+70.0049 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 2907 0 0 0 6991 9 0 0 25 0 1 0 544572837 14680064 2832 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3584 2832 603 41 0 3543 0
vsize: 14336
[startup+80.0051 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3021 0 0 0 7990 9 0 0 25 0 1 0 544572837 15085568 2946 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 2946 603 41 0 3642 0
vsize: 14732
[startup+90.0057 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3132 0 0 0 8989 10 0 0 25 0 1 0 544572837 15491072 3057 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3782 3057 603 41 0 3741 0
vsize: 15128
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3263 0 0 0 9988 11 0 0 25 0 1 0 544572837 16023552 3188 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3912 3188 603 41 0 3871 0
vsize: 15648
[startup+110.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3386 0 0 0 10988 12 0 0 25 0 1 0 544572837 16560128 3311 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4043 3311 603 41 0 4002 0
vsize: 16172
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3560 0 0 0 11987 13 0 0 25 0 1 0 544572837 17494016 3485 4294967295 134512640 134672761 3221224544 3221223712 134564651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4271 3485 603 41 0 4230 0
vsize: 17084
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3741 0 0 0 12986 14 0 0 25 0 1 0 544572837 18169856 3666 4294967295 134512640 134672761 3221224544 3221223708 134564608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4436 3666 603 41 0 4395 0
vsize: 17744
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 3900 0 0 0 13985 15 0 0 25 0 1 0 544572837 18841600 3825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4600 3825 603 41 0 4559 0
vsize: 18400
[startup+150.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 4066 0 0 0 14984 16 0 0 25 0 1 0 544572837 19378176 3991 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4731 3991 603 41 0 4690 0
vsize: 18924
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30924
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 4242 0 0 0 15983 17 0 0 25 0 1 0 544572837 20189184 4167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4929 4167 603 41 0 4888 0
vsize: 19716
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 4517 0 0 0 16982 19 0 0 25 0 1 0 544572837 21262336 4442 4294967295 134512640 134672761 3221224544 3221223728 134557980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5191 4442 603 41 0 5150 0
vsize: 20764
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 4909 0 0 0 17980 20 0 0 25 0 1 0 544572837 22740992 4834 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 4834 603 41 0 5511 0
vsize: 22208
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 18980 21 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 19980 21 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 20979 21 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 21979 22 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 22979 22 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 23979 23 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 24979 23 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 25979 23 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 26979 24 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5006 0 0 0 27979 24 0 0 25 0 1 0 544572837 23142400 4931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5650 4931 603 41 0 5609 0
vsize: 22600
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5134 0 0 0 28978 25 0 0 25 0 1 0 544572837 23683072 5059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5782 5059 603 41 0 5741 0
vsize: 23128
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5424 0 0 0 29977 26 0 0 25 0 1 0 544572837 24899584 5349 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6079 5349 603 41 0 6038 0
vsize: 24316
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5630 0 0 0 30976 27 0 0 25 0 1 0 544572837 25706496 5555 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6276 5555 603 41 0 6235 0
vsize: 25104
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 5955 0 0 0 31975 28 0 0 25 0 1 0 544572837 27574272 5880 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6732 5880 603 41 0 6691 0
vsize: 26928
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6319 0 0 0 32973 30 0 0 25 0 1 0 544572837 28913664 6244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7059 6244 603 41 0 7018 0
vsize: 28236
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 33974 30 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 34973 31 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 35973 31 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 36973 31 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 37973 31 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 38973 32 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 39973 32 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+410.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 40973 32 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 6374 0 0 0 41973 32 0 0 25 0 1 0 544572837 29184000 6299 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7125 6299 603 41 0 7084 0
vsize: 28500
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7474 0 0 0 42970 35 0 0 25 0 1 0 544572837 32894976 7316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7316 603 41 0 7990 0
vsize: 32124
[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7478 0 0 0 43970 35 0 0 25 0 1 0 544572837 32894976 7320 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7320 603 41 0 7990 0
vsize: 32124
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7479 0 0 0 44969 36 0 0 25 0 1 0 544572837 32894976 7321 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7321 603 41 0 7990 0
vsize: 32124
[startup+460.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7480 0 0 0 45969 36 0 0 25 0 1 0 544572837 32894976 7322 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7322 603 41 0 7990 0
vsize: 32124
[startup+470.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7482 0 0 0 46969 37 0 0 25 0 1 0 544572837 32894976 7324 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7324 603 41 0 7990 0
vsize: 32124
[startup+480.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7482 0 0 0 47969 37 0 0 25 0 1 0 544572837 32894976 7324 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7324 603 41 0 7990 0
vsize: 32124
[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7482 0 0 0 48969 37 0 0 25 0 1 0 544572837 32894976 7324 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8031 7324 603 41 0 7990 0
vsize: 32124
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7482 0 0 0 49969 37 0 0 25 0 1 0 544572837 32894976 7324 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8031 7324 603 41 0 7990 0
vsize: 32124
[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7482 0 0 0 50969 37 0 0 25 0 1 0 544572837 32894976 7324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8031 7324 603 41 0 7990 0
vsize: 32124
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 51969 37 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 52969 37 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 53969 37 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 54969 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 55969 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 56969 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 57969 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 58970 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+600.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7522 0 0 0 59970 38 0 0 25 0 1 0 544572837 33189888 7364 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7364 603 41 0 8062 0
vsize: 32412
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 60970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+620.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 61970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 62970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 63970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 64970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 65970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 66970 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 67971 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+690.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 68971 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 69971 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 70971 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+720.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7524 0 0 0 71971 39 0 0 25 0 1 0 544572837 33189888 7366 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7366 603 41 0 8062 0
vsize: 32412
[startup+730.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 72971 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223692 1074733089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+740.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 73971 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 74972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223808 134562218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+760.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 75972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 76972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 77972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 78972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 79972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 80972 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223728 134559463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 81973 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 82973 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 83973 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7525 0 0 0 84973 39 0 0 25 0 1 0 544572837 33189888 7367 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7367 603 41 0 8062 0
vsize: 32412
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 85973 39 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 86973 39 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+880.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 87973 39 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+890.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 88974 39 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 89974 40 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 90973 40 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 91973 40 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 92973 40 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223744 134557892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7527 0 0 0 93973 40 0 0 25 0 1 0 544572837 33189888 7369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7369 603 41 0 8062 0
vsize: 32412
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 94973 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 95973 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+970.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 96974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 97974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223696 134565134 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+990.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 98974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 99974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 100974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 101974 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 102975 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 103975 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7528 0 0 0 104975 40 0 0 25 0 1 0 544572837 33189888 7370 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7370 603 41 0 8062 0
vsize: 32412
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 7735 0 0 0 105975 40 0 0 25 0 1 0 544572837 33992704 7577 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8299 7577 603 41 0 8258 0
vsize: 33196
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 8239 0 0 0 106973 42 0 0 25 0 1 0 544572837 36020224 8081 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8794 8081 603 41 0 8753 0
vsize: 35176
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 8547 0 0 0 107973 43 0 0 25 0 1 0 544572837 37363712 8389 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9122 8389 603 41 0 9081 0
vsize: 36488
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 8790 0 0 0 108972 43 0 0 25 0 1 0 544572837 38293504 8632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9349 8632 603 41 0 9308 0
vsize: 37396
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9447 0 0 0 109971 45 0 0 25 0 1 0 544572837 40988672 9289 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10007 9289 603 41 0 9966 0
vsize: 40028
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 110970 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 111971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 112971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 113971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 114971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223668 134566073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 115971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 116971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 117971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 118971 46 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 30926
Raw data (stat): 30924 (minisat+) R 30923 22612 22611 0 -1 0 9822 0 0 0 119971 47 0 0 25 0 1 0 544572837 42385408 9634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10348 9634 603 41 0 10307 0
vsize: 41392
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 30926
Raw data (stat): 30924 (minisat+) Z 30923 22612 22611 0 -1 12 9825 0 0 0 119972 49 0 0 25 0 1 0 544572837 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.07
CPU time (s): 1200.21
CPU user time (s): 1199.72
CPU system time (s): 0.490925
CPU usage (%): 100.012
Max. virtual memory (Kb): 41392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####