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-ran4x64.opb
MD5SUM	6a6f7751d9c11fcafeb386712eac2f08
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3097606
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1473474440
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	1473474440
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	433.74
Number of variables	5376
Total number of constraints	324
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	324
Minimum length of a constraint	21
Maximum length of a constraint	1280
Trace number 17618

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        268616 kB
Buffers:         21864 kB
Cached:         720900 kB
SwapCached:          0 kB
Active:          42544 kB
Inactive:       703004 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        268364 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14788 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:15:07 (client local time) WITH STATUS 10 IN 1200.26 SECONDS
stats: 19344 7 1200.26 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 392 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 390]---> Adder-cost: 1332   maxlim: 117952   bits: 18/17
c ---[ 388]---> Adder-cost: 1332   maxlim: 118336   bits: 18/17
c ---[ 386]---> Adder-cost: 1332   maxlim: 115520   bits: 18/17
c ---[ 384]---> Adder-cost: 1332   maxlim: 91584   bits: 18/17
c ---[ 382]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 380]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 378]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  279     Base: 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  479     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  359     Base: 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   12
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   11
c ---[ 252]---> BDD-cost:   12
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:   12
c ---[ 249]---> BDD-cost:   11
c ---[ 248]---> BDD-cost:   12
c ---[ 247]---> BDD-cost:   10
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   15
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:   19
c ---[ 241]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   10
c ---[ 239]---> BDD-cost:   15
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   15
c ---[ 233]---> BDD-cost:   19
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   17
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   12
c ---[ 219]---> BDD-cost:   12
c ---[ 218]---> BDD-cost:   16
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   10
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   10
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   19
c ---[ 209]---> BDD-cost:   14
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   12
c ---[ 206]---> BDD-cost:   14
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   17
c ---[ 203]---> BDD-cost:   11
c ---[ 202]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   14
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:   12
c ---[ 193]---> BDD-cost:   11
c ---[ 192]---> BDD-cost:   15
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   10
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:   12
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   12
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:   12
c ---[ 177]---> BDD-cost:   10
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   11
c ---[ 173]---> BDD-cost:   15
c ---[ 172]---> BDD-cost:   16
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   10
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   19
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   11
c ---[ 156]---> BDD-cost:   11
c ---[ 155]---> BDD-cost:   17
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   12
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   16
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   14
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   10
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   10
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   14
c ---[ 134]---> BDD-cost:   12
c ---[ 133]---> BDD-cost:   17
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:   15
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:   14
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   11
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   12
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   12
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:   17
c ---[ 108]---> BDD-cost:   12
c ---[ 107]---> BDD-cost:   11
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   16
c ---[ 100]---> BDD-cost:   17
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   13
c ---[  95]---> BDD-cost:   13
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   13
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   19
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   12
c ---[  86]---> BDD-cost:   13
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   11
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   13
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   17
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   12
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:   12
c ---[  66]---> BDD-cost:   11
c ---[  65]---> BDD-cost:   14
c ---[  64]---> BDD-cost:   12
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   11
c ---[  60]---> BDD-cost:   15
c ---[  59]---> BDD-cost:   16
c ---[  58]---> BDD-cost:   17
c ---[  57]---> BDD-cost:   10
c ---[  56]---> BDD-cost:   15
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   19
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   12
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   10
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:   11
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   12
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   12
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   11
c ---[  11]---> BDD-cost:   12
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   11
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   12
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   99610   282182 |   33203       0        0     nan |  0.000 % |
c |       100 |   99553   282041 |   36523      96      470     4.9 | 14.174 % |
c |       251 |   99473   281854 |   40175     238      951     4.0 | 14.249 % |
c |       476 |   99473   281854 |   44193     463     1672     3.6 | 14.249 % |
c |       813 |   99396   281641 |   48612     788     2673     3.4 | 14.305 % |
c |      1319 |   99255   281321 |   53473    1283     4214     3.3 | 14.443 % |
c |      2078 |   99163   281075 |   58821    2033     6634     3.3 | 14.518 % |
c |      3217 |   98981   280669 |   64703    3149    11408     3.6 | 14.693 % |
c |      4925 |   98779   280208 |   71173    4832    18185     3.8 | 14.881 % |
c |      7487 |   98585   279763 |   78290    7372    31193     4.2 | 15.066 % |
c |     11333 |   98333   279192 |   86120   11192    62728     5.6 | 15.316 % |
c |     17099 |   98079   278609 |   94732   16925   159071     9.4 | 15.557 % |
c |     25748 |   97995   278424 |  104205   25560  1154919    45.2 | 15.641 % |
c |     38722 |   97782   277954 |  114625   38507  1520449    39.5 | 15.857 % |
c |     58184 |   97691   277732 |  126088   57956  2353426    40.6 | 15.936 % |
c |     87380 |   97508   277291 |  138697   87127  3386549    38.9 | 16.108 % |
c ==============================================================================
c [1mFound solution: 5207410[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10520   maxlim: 3172374   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91901 |  171085   540137 |   57028   91645  3587583    39.1 | 16.108 % |
c |     92001 |  171085   540137 |   62730   19860   590017    29.7 | 12.149 % |
c |     92151 |  171085   540137 |   69003   20010   590751    29.5 | 12.149 % |
c |     92376 |  171085   540137 |   75904   20235   591860    29.2 | 12.149 % |
c |     92713 |  171085   540137 |   83494   20572   593861    28.9 | 12.149 % |
c |     93219 |  171085   540137 |   91844   21078   600479    28.5 | 12.149 % |
c |     93979 |  171085   540137 |  101028   21838   605498    27.7 | 12.149 % |
c |     95119 |  171052   540061 |  111131   22975   616686    26.8 | 12.173 % |
c |     96827 |  171046   540047 |  122244   24682   635763    25.8 | 12.177 % |
c |     99389 |  171046   540047 |  134469   27244   687710    25.2 | 12.177 % |
c |    103234 |  171027   540004 |  147915   31086   736435    23.7 | 12.191 % |
c |    109001 |  170974   539884 |  162707   36848   838577    22.8 | 12.229 % |
c |    117651 |  170871   539651 |  178978   45485   959866    21.1 | 12.304 % |
c |    130625 |  170871   539651 |  196876   58459  1340446    22.9 | 12.304 % |
c |    150087 |  170784   539452 |  216563   77912  2390261    30.7 | 12.368 % |
c |    179280 |  170702   539257 |  238220  107095  4551414    42.5 | 12.424 % |
c |    223071 |  170623   539049 |  262042  150875  6302234    41.8 | 12.474 % |
c |    288756 |  170520   538814 |  288246  216548 11971382    55.3 | 12.551 % |
c |    387282 |  170500   538768 |  317070  315070 29210504    92.7 | 12.566 % |
c |    535073 |  170420   538584 |  348778  149508  9617794    64.3 | 12.622 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v X0_bit_7 -X0_bit_6 X0_bit_5 X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 X1_bit_4 X1_bit_3 -X1_bit_2 -X1_bit_1 X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 -X2_bit_6 X2_bit_5 X2_bit_4 X2_bit_3 -X2_bit_2 -X2_bit_1 X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 -X3_bit_6 X3_bit_5 X3_bit_4 X3_bit_3 X3_bit_2 -X3_bit_1 -X3_bit0 X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 -X4_bit_6 X4_bit_5 X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 -X5_bit_6 X5_bit_5 X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 X5_bit1 -X5_bit2 X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 X6_bit_3 X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 X7_bit_6 -X7_bit_5 X7_bit_4 -X7_bit_3 X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 X8_bit_5 X8_bit_4 X8_bit_3 X8_bit_2 X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 -X9_bit_6 -X9_bit_5 X9_bit_4 X9_bit_3 X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 X11_bit_6 X11_bit_5 X11_bit_4 X11_bit_3 X11_bit_2 X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 -X12_bit_5 X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 X15_bit_6 X15_bit_5 -X15_bit_4 X15_bit_3 X15_bit_2 X15_bit_1 X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 X16_bit_7 X16_bit_6 X16_bit_5 -X16_bit_4 X16_bit_3 -X16_bit_2 X16_bit_1 X16_bit0 -X16_bit1 X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 X17_bit_6 -X17_bit_5 X17_bit_4 -X17_bit_3 X17_bit_2 -X17_bit_1 X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 -X18_bit_6 -X18_bit_5 X18_bit_4 -X18_bit_3 X18_bit_2 -X18_bit_1 X18_bit0 X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 -X19_bit_5 X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 X20_bit_5 -X20_bit_4 X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 X22_bit_3 X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 X23_bit_6 X23_bit_5 X23_bit_4 X23_bit_3 -X23_bit_2 X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 X23_bit3 X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 -X24_bit_5 -X24_bit_4 X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 X25_bit_5 -X25_bit_4 X25_bit_3 X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 -X27_bit_6 X27_bit_5 X27_bit_4 X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 X32_bit_7 -X32_bit_6 X32_bit_5 -X32_bit_4 -X32_bit_3 X32_bit_2 -X32_bit_1 -X32_bit0 X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 X34_bit_6 -X34_bit_5 X34_bit_4 X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 X38_bit_3 X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 X39_bit_6 -X39_bit_5 -X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 X41_bit_6 -X41_bit_5 -X41_bit_4 X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 X42_bit_6 -X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 X43_bit_6 X43_bit_5 X43_bit_4 X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 X46_bit_7 X46_bit_6 -X46_bit_5 X46_bit_4 X46_bit_3 X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 -X50_bit_6 X50_bit_5 X50_bit_4 X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 X51_bit_6 X51_bit_5 X51_bit_4 X51_bit_3 X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 X52_bit_6 X52_bit_5 X52_bit_4 X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 X53_bit_6 -X53_bit_5 X53_bit_4 X53_bit_3 X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 X54_bit_6 X54_bit_5 -X54_bit_4 -X54_bit_3 X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 X55_bit_6 X55_bit_5 X55_bit_4 X55_bit_3 X55_bit_2 X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 X56_bit_6 X56_bit_5 X56_bit_4 X56_bit_3 X56_bit_2 X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 X57_bit_6 X57_bit_5 X57_bit_4 X57_bit_3 X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 X58_bit_6 -X58_bit_5 X58_bit_4 X58_bit_3 X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 X60_bit_6 X60_bit_5 X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 X62_bit_4 -X62_bit_3 X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 X65_bit_6 -X65_bit_5 -X65_bit_4 X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 -X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 -X67_bit_5 X67_bit_4 X67_bit_3 X67_bit_2 -X67_bit_1 X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 X68_bit_6 -X68_bit_5 X68_bit_4 -X68_bit_3 X68_bit_2 X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 -X69_bit_6 X69_bit_5 X69_bit_4 -X69_bit_3 -X69_bit_2 X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 X71_bit_6 -X71_bit_5 X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 X72_bit_6 -X72_bit_5 X72_bit_4 -X72_bit_3 X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 X73_bit_5 -X73_bit_4 X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 X75_bit_5 -X75_bit_4 -X75_bit_3 X75_bit_2 X75_bit_1 X75_bit0 -X75_bit1 X75_bit2 X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 -X78_bit_6 -X78_bit_5 X78_bit_4 -X78_bit_3 X78_bit_2 -X78_bit_1 X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 X79_bit_2 X79_bit_1 X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 -X80_bit_6 -X80_bit_5 X80_bit_4 X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 X82_bit_3 X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 X83_bit_5 -X83_bit_4 -X83_bit_3 X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 -X84_bit_6 X84_bit_5 -X84_bit_4 X84_bit_3 -X84_bit_2 X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 X86_bit_6 X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 X86_bit_1 X86_bit0 X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 X87_bit_7 X87_bit_6 X87_bit_5 X87_bit_4 X87_bit_3 -X87_bit_2 X87_bit_1 -X87_bit0 -X87_bit1 X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 X89_bit_5 X89_bit_4 -X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 X96_bit_2 X96_bit_1 X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 X98_bit_6 X98_bit_5 X98_bit_4 X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 X101_bit_6 X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 X102_bit_7 X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 -X106_bit_6 -X106_bit_5 X106_bit_4 X106_bit_3 X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 X107_bit_6 X107_bit_5 -X107_bit_4 -X107_bit_3 X107_bit_2 -X107_bit_1 X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 X108_bit_5 -X108_bit_4 X108_bit_3 X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 X109_bit_3 -X109_bit_2 X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 -X110_bit_6 -X110_bit_5 X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 X110_bit0 X110_bit1 -X110_bit2 X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 -X116_bit_5 X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 X117_bit_6 X117_bit_5 X117_bit_4 -X117_bit_3 X117_bit_2 -X117_bit_1 X117_bit0 X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 -X119_bit_6 X119_bit_5 -X119_bit_4 -X119_bit_3 X119_bit_2 -X119_bit_1 -X119_bit0 X119_bit1 X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 X120_bit_5 -X120_bit_4 -X120_bit_3 X120_bit_2 X120_bit_1 -X120_bit0 -X120_bit1 X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 X121_bit_7 X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 X122_bit_6 -X122_bit_5 X122_bit_4 -X122_bit_3 -X122_bit_2 X122_bit_1 -X122_bit0 X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 X124_bit_5 X124_bit_4 X124_bit_3 X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 X125_bit_7 -X125_bit_6 X125_bit_5 X125_bit_4 X125_bit_3 X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 -X126_bit_6 X126_bit_5 X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 X128_bit_6 -X128_bit_5 X128_bit_4 X128_bit_3 -X128_bit_2 X128_bit_1 X128_bit0 X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 X129_bit_5 X129_bit_4 X129_bit_3 X129_bit_2 -X129_bit_1 X129_bit0 X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 X130_bit_4 X130_bit_3 X130_bit_2 -X130_bit_1 X130_bit0 X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 X131_bit_6 X131_bit_5 X131_bit_4 X131_bit_3 X131_bit_2 -X131_bit_1 X131_bit0 X131_bit1 -X131_bit2 X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 X132_bit_6 -X132_bit_5 X132_bit_4 X132_bit_3 X132_bit_2 X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 X133_bit_6 -X133_bit_5 X133_bit_4 X133_bit_3 -X133_bit_2 -X133_bit_1 X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 X134_bit_7 -X134_bit_6 -X134_bit_5 X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 X135_bit_6 X135_bit_5 X135_bit_4 -X135_bit_3 X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 X136_bit_7 X136_bit_6 -X136_bit_5 X136_bit_4 X136_bit_3 X136_bit_2 -X136_bit_1 X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 X137_bit_6 X137_bit_5 X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 X139_bit_7 X139_bit_6 -X139_bit_5 X139_bit_4 X139_bit_3 -X139_bit_2 X139_bit_1 X139_bit0 -X139_bit1 -X139_bit2 X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 X140_bit_6 X140_bit_5 X140_bit_4 X140_bit_3 X140_bit_2 X140_bit_1 X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 X142_bit_4 -X142_bit_3 X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 X143_bit_7 X143_bit_6 -X143_bit_5 X143_bit_4 X143_bit_3 X143_bit_2 X143_bit_1 X143_bit0 X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 X144_bit_3 -X144_bit_2 -X144_bit_1 X144_bit0 X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 X145_bit_6 X145_bit_5 X145_bit_4 -X145_bit_3 X145_bit_2 X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 X147_bit_7 -X147_bit_6 -X147_bit_5 X147_bit_4 X147_bit_3 X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 X148_bit_6 X148_bit_5 X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 X149_bit_3 -X149_bit_2 X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 X150_bit_6 X150_bit_5 X150_bit_4 X150_bit_3 X150_bit_2 X150_bit_1 X150_bit0 X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 X151_bit_7 X151_bit_6 -X151_bit_5 X151_bit_4 X151_bit_3 X151_bit_2 X151_bit_1 X151_bit0 X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 X153_bit_7 -X153_bit_6 X153_bit_5 X153_bit_4 X153_bit_3 X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 X155_bit_6 X155_bit_5 X155_bit_4 X155_bit_3 -X155_bit_2 X155_bit_1 -X155_bit0 X155_bit1 X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 X156_bit_3 -X156_bit_2 X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 X157_bit_1 -X157_bit0 X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 X160_bit_7 -X160_bit_6 X160_bit_5 X160_bit_4 X160_bit_3 X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 -X162_bit_6 -X162_bit_5 X162_bit_4 -X162_bit_3 X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 X165_bit_7 X165_bit_6 X165_bit_5 X165_bit_4 -X165_bit_3 X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 X166_bit_7 X166_bit_6 -X166_bit_5 X166_bit_4 -X166_bit_3 X166_bit_2 X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 X167_bit_7 X167_bit_6 -X167_bit_5 -X167_bit_4 X167_bit_3 X167_bit_2 X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 X169_bit_7 X169_bit_6 -X169_bit_5 -X169_bit_4 X169_bit_3 X169_bit_2 X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 X170_bit_7 -X170_bit_6 X170_bit_5 X170_bit_4 -X170_bit_3 X170_bit_2 -X170_bit_1 X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 X171_bit_7 X171_bit_6 X171_bit_5 X171_bit_4 -X171_bit_3 X171_bit_2 -X171_bit_1 X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 X172_bit_7 -X172_bit_6 X172_bit_5 X172_bit_4 -X172_bit_3 X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 X173_bit_7 -X173_bit_6 X173_bit_5 X173_bit_4 -X173_bit_3 X173_bit_2 -X173_bit_1 X173_bit0 -X173_bit1 X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 X174_bit_7 -X174_bit_6 X174_bit_5 X174_bit_4 -X174_bit_3 X174_bit_2 -X174_bit_1 X174_bit0 -X174_bit1 X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 X176_bit_5 -X176_bit_4 -X176_bit_3 X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 X179_bit_7 X179_bit_6 X179_bit_5 X179_bit_4 X179_bit_3 -X179_bit_2 X179_bit_1 X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 -X180_bit_6 X180_bit_5 X180_bit_4 X180_bit_3 X180_bit_2 -X180_bit_1 X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 X181_bit_5 X181_bit_4 X181_bit_3 X181_bit_2 -X181_bit_1 X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 X182_bit_7 -X182_bit_6 X182_bit_5 X182_bit_4 X182_bit_3 X182_bit_2 -X182_bit_1 X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 X183_bit_7 X183_bit_6 X183_bit_5 X183_bit_4 X183_bit_3 X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 X184_bit_6 X184_bit_5 X184_bit_4 X184_bit_3 X184_bit_2 X184_bit_1 X184_bit0 -X184_bit1 X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 X185_bit_7 X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 X185_bit_2 -X185_bit_1 -X185_bit0 X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 X186_bit_6 X186_bit_5 X186_bit_4 X186_bit_3 X186_bit_2 -X186_bit_1 X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 X188_bit_7 -X188_bit_6 -X188_bit_5 X188_bit_4 X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 X189_bit_6 X189_bit_5 -X189_bit_4 X189_bit_3 -X189_bit_2 -X189_bit_1 X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 X190_bit_7 X190_bit_6 X190_bit_5 -X190_bit_4 X190_bit_3 X190_bit_2 -X190_bit_1 X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 X191_bit_5 -X191_bit_4 X191_bit_3 X191_bit_2 -X191_bit_1 -X191_bit0 X191_bit1 X191_bit2 X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 X193_bit_6 -X193_bit_5 X193_bit_4 X193_bit_3 -X193_bit_2 -X193_bit_1 X193_bit0 X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 X194_bit_3 -X194_bit_2 -X194_bit_1 X194_bit0 X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 X195_bit_5 X195_bit_4 -X195_bit_3 -X195_bit_2 X195_bit_1 -X195_bit0 -X195_bit1 X195_bit2 X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 X196_bit_7 X196_bit_6 X196_bit_5 X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 X196_bit2 X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 X197_bit_5 X197_bit_4 -X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 X197_bit2 X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 X198_bit_6 X198_bit_5 X198_bit_4 X198_bit_3 X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 X199_bit_6 X199_bit_5 X199_bit_4 X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 X200_bit_6 X200_bit_5 X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 X201_bit_5 -X201_bit_4 -X201_bit_3 X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 X203_bit_7 X203_bit_6 X203_bit_5 X203_bit_4 X203_bit_3 X203_bit_2 -X203_bit_1 -X203_bit0 X203_bit1 X203_bit2 X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 X204_bit_7 X204_bit_6 X204_bit_5 -X204_bit_4 X204_bit_3 X204_bit_2 -X204_bit_1 X204_bit0 X204_bit1 X204_bit2 X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 X206_bit_6 X206_bit_5 X206_bit_4 -X206_bit_3 X206_bit_2 -X206_bit_1 X206_bit0 X206_bit1 X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 -X207_bit_6 X207_bit_5 X207_bit_4 -X207_bit_3 X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 X208_bit_6 X208_bit_5 X208_bit_4 X208_bit_3 X208_bit_2 X208_bit_1 X208_bit0 X208_bit1 -X208_bit2 X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 X209_bit_7 X209_bit_6 X209_bit_5 -X209_bit_4 X209_bit_3 -X209_bit_2 X209_bit_1 X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 X210_bit_6 X210_bit_5 -X210_bit_4 -X210_bit_3 X210_bit_2 -X210_bit_1 X210_bit0 X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 X211_bit_6 -X211_bit_5 X211_bit_4 X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 X212_bit_6 X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 -X214_bit_6 X214_bit_5 X214_bit_4 X214_bit_3 X214_bit_2 X214_bit_1 X214_bit0 X214_bit1 X214_bit2 X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 X215_bit_7 X215_bit_6 X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 X215_bit_1 -X215_bit0 X215_bit1 -X215_bit2 X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 -X216_bit_6 X216_bit_5 -X216_bit_4 -X216_bit_3 X216_bit_2 X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 -X217_bit_6 X217_bit_5 X217_bit_4 X217_bit_3 -X217_bit_2 X217_bit_1 -X217_bit0 X217_bit1 X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 X219_bit_5 X219_bit_4 X219_bit_3 X219_bit_2 -X219_bit_1 X219_bit0 X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 X220_bit_3 X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 -X221_bit_5 -X221_bit_4 X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 X221_bit1 -X221_bit2 X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 X224_bit_6 X224_bit_5 X224_bit_4 X224_bit_3 X224_bit_2 -X224_bit_1 -X224_bit0 X224_bit1 X224_bit2 X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 X226_bit_6 X226_bit_5 X226_bit_4 X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 -X227_bit_4 -X227_bit_3 -X227_bit_2 -X227_bit_1 -X227_bit0 -X227_bit1 X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 X230_bit_6 X230_bit_5 X230_bit_4 X230_bit_3 -X230_bit_2 -X230_bit_1 -X230_bit0 -X230_bit1 X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 X231_bit_7 X231_bit_6 -X231_bit_5 X231_bit_4 -X231_bit_3 X231_bit_2 X231_bit_1 -X231_bit0 X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 X232_bit1 X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 X233_bit_6 -X233_bit_5 X233_bit_4 X233_bit_3 X233_bit_2 X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 X234_bit_7 X234_bit_6 X234_bit_5 X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 X234_bit0 -X234_bit1 X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 -X235_bit_6 X235_bit_5 X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 -X236_bit_5 X236_bit_4 X236_bit_3 -X236_bit_2 -X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 X238_bit_7 X238_bit_6 X238_bit_5 X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 X238_bit1 X238_bit2 X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 X241_bit2 X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 X243_bit_6 -X243_bit_5 -X243_bit_4 X243_bit_3 -X243_bit_2 X243_bit_1 X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 X244_bit_6 -X244_bit_5 X244_bit_4 X244_bit_3 -X244_bit_2 -X244_bit_1 X244_bit0 -X244_bit1 X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 X245_bit_6 -X245_bit_5 X245_bit_4 X245_bit_3 -X245_bit_2 X245_bit_1 X245_bit0 -X245_bit1 X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 X246_bit_7 -X246_bit_6 X246_bit_5 X246_bit_4 X246_bit_3 -X246_bit_2 -X246_bit_1 X246_bit0 X246_bit1 -X246_bit2 X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 X247_bit_6 X247_bit_5 X247_bit_4 X247_bit_3 -X247_bit_2 -X247_bit_1 X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 X248_bit_7 X248_bit_6 X248_bit_5 X248_bit_4 X248_bit_3 -X248_bit_2 -X248_bit_1 X248_bit0 X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 X249_bit_5 X249_bit_4 X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 X250_bit_6 X250_bit_5 X250_bit_4 X250_bit_3 X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 -X251_bit_4 -X251_bit_3 -X251_bit_2 -X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 -X252_bit_6 X252_bit_5 X252_bit_4 X252_bit_3 -X252_bit_2 -X252_bit_1 X252_bit0 X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 -X253_bit_6 -X253_bit_5 X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 X253_bit0 X253_bit1 -X253_bit2 X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 -X254_bit_6 X254_bit_5 X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 -X255_bit_6 -X255_bit_5 X255_bit_4 -X255_bit_3 X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_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_#### 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.79 0.92 0.89 2/54 7673
Raw data (stat): 7673 (runsolver) R 7672 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486295008 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 3040 0 0 0 993 5 0 0 25 0 1 0 486295008 14163968 2953 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3458 2953 603 41 0 3417 0
vsize: 13832
[startup+20.0018 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 3080 0 0 0 1992 5 0 0 25 0 1 0 486295008 14327808 2993 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3498 2993 603 41 0 3457 0
vsize: 13992
[startup+30.0022 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 3148 0 0 0 2991 6 0 0 25 0 1 0 486295008 14598144 3061 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3564 3061 603 41 0 3523 0
vsize: 14256
[startup+40.0023 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 3306 0 0 0 3990 7 0 0 25 0 1 0 486295008 15400960 3219 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3760 3219 603 41 0 3719 0
vsize: 15040
[startup+50.0031 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 4030 0 0 0 4987 10 0 0 25 0 1 0 486295008 18219008 3943 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4448 3943 603 41 0 4407 0
vsize: 17792
[startup+60.0026 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 4468 0 0 0 5986 11 0 0 25 0 1 0 486295008 20103168 4381 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4908 4381 603 41 0 4867 0
vsize: 19632
[startup+70.0038 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 4928 0 0 0 6985 12 0 0 25 0 1 0 486295008 21987328 4841 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4841 603 41 0 5327 0
vsize: 21472
[startup+80.0047 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 5477 0 0 0 7984 14 0 0 25 0 1 0 486295008 24276992 5390 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5927 5390 603 41 0 5886 0
vsize: 23708
[startup+90.0043 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 5984 0 0 0 8982 15 0 0 25 0 1 0 486295008 26300416 5897 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6421 5897 603 41 0 6380 0
vsize: 25684
[startup+100.004 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 6323 0 0 0 9982 16 0 0 25 0 1 0 486295008 27906048 6236 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6236 603 41 0 6772 0
vsize: 27252
[startup+110.005 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 6736 0 0 0 10980 18 0 0 25 0 1 0 486295008 29523968 6649 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7208 6649 603 41 0 7167 0
vsize: 28832
[startup+120.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 7155 0 0 0 11979 19 0 0 25 0 1 0 486295008 31281152 7068 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7637 7068 603 41 0 7596 0
vsize: 30548
[startup+130.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 8145 0 0 0 12976 23 0 0 25 0 1 0 486295008 34557952 7927 4294967295 134512640 134672761 3221224544 3221222784 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8437 7927 603 41 0 8396 0
vsize: 33748
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 13961 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134564668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 14961 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+160.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 15961 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+170.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 16962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 17962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+190.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 18962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 19962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+210.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 20962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+220.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14038 0 0 0 21962 37 0 0 25 0 1 0 486295008 56946688 12666 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13903 12666 603 41 0 13862 0
vsize: 55612
[startup+230.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14164 0 0 0 22962 38 0 0 25 0 1 0 486295008 57348096 12792 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14001 12792 603 41 0 13960 0
vsize: 56004
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 14761 0 0 0 23961 39 0 0 25 0 1 0 486295008 59772928 13389 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14593 13389 603 41 0 14552 0
vsize: 58372
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 15383 0 0 0 24960 40 0 0 25 0 1 0 486295008 62316544 14011 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15214 14011 603 41 0 15173 0
vsize: 60856
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 15860 0 0 0 25958 42 0 0 25 0 1 0 486295008 64208896 14488 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15676 14488 603 41 0 15635 0
vsize: 62704
[startup+270.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 16403 0 0 0 26957 44 0 0 25 0 1 0 486295008 66494464 15031 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16234 15031 603 41 0 16193 0
vsize: 64936
[startup+280.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 16831 0 0 0 27956 45 0 0 25 0 1 0 486295008 68108288 15459 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16628 15459 603 41 0 16587 0
vsize: 66512
[startup+290.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7673
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 17080 0 0 0 28954 46 0 0 25 0 1 0 486295008 69705728 15708 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17018 15708 603 41 0 16977 0
vsize: 68072
[startup+300.014 s]
Raw data (loadavg): 0.99 0.96 0.91 4/57 7696
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 17326 0 0 0 29954 47 0 0 25 0 1 0 486295008 70647808 15954 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17248 15954 603 41 0 17207 0
vsize: 68992
[startup+310.014 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 17643 0 0 0 30953 48 0 0 25 0 1 0 486295008 71995392 16271 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17577 16271 603 41 0 17536 0
vsize: 70308
[startup+320.014 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 17878 0 0 0 31953 48 0 0 25 0 1 0 486295008 72937472 16506 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17807 16506 603 41 0 17766 0
vsize: 71228
[startup+330.014 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 18062 0 0 0 32953 48 0 0 25 0 1 0 486295008 73609216 16690 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17971 16690 603 41 0 17930 0
vsize: 71884
[startup+340.014 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 18381 0 0 0 33952 50 0 0 25 0 1 0 486295008 74952704 17009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18299 17009 603 41 0 18258 0
vsize: 73196
[startup+350.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 19071 0 0 0 34950 52 0 0 25 0 1 0 486295008 77774848 17699 4294967295 134512640 134672761 3221224544 3221223648 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18988 17699 603 41 0 18947 0
vsize: 75952
[startup+360.015 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 19813 0 0 0 35948 54 0 0 25 0 1 0 486295008 80740352 18441 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19712 18441 603 41 0 19671 0
vsize: 78848
[startup+370.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 7726
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 20346 0 0 0 36947 56 0 0 25 0 1 0 486295008 82890752 18974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20237 18974 603 41 0 20196 0
vsize: 80948
[startup+380.015 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 20776 0 0 0 37946 57 0 0 25 0 1 0 486295008 84639744 19404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20664 19404 603 41 0 20623 0
vsize: 82656
[startup+390.014 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 21168 0 0 0 38944 58 0 0 25 0 1 0 486295008 86265856 19796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21061 19796 603 41 0 21020 0
vsize: 84244
[startup+400.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 21560 0 0 0 39943 59 0 0 25 0 1 0 486295008 87879680 20188 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21455 20188 603 41 0 21414 0
vsize: 85820
[startup+410.015 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 21935 0 0 0 40941 62 0 0 25 0 1 0 486295008 89358336 20563 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21816 20563 603 41 0 21775 0
vsize: 87264
[startup+420.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 22272 0 0 0 41941 62 0 0 25 0 1 0 486295008 90710016 20900 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22146 20900 603 41 0 22105 0
vsize: 88584
[startup+430.016 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 22931 0 0 0 42939 64 0 0 25 0 1 0 486295008 93523968 21559 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22833 21559 603 41 0 22792 0
vsize: 91332
[startup+440.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 23416 0 0 0 43937 66 0 0 25 0 1 0 486295008 95412224 22044 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23294 22044 603 41 0 23253 0
vsize: 93176
[startup+450.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 23872 0 0 0 44935 67 0 0 25 0 1 0 486295008 97304576 22500 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23756 22500 603 41 0 23715 0
vsize: 95024
[startup+460.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 23996 0 0 0 45935 68 0 0 25 0 1 0 486295008 97849344 22624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23889 22624 603 41 0 23848 0
vsize: 95556
[startup+470.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 24298 0 0 0 46934 69 0 0 25 0 1 0 486295008 99061760 22926 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24185 22926 603 41 0 24144 0
vsize: 96740
[startup+480.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 24739 0 0 0 47932 70 0 0 25 0 1 0 486295008 100810752 23367 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24612 23367 603 41 0 24571 0
vsize: 98448
[startup+490.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 25113 0 0 0 48931 72 0 0 25 0 1 0 486295008 102293504 23741 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24974 23741 603 41 0 24933 0
vsize: 99896
[startup+500.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 25514 0 0 0 49930 73 0 0 25 0 1 0 486295008 103907328 24142 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25368 24142 603 41 0 25327 0
vsize: 101472
[startup+510.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 25921 0 0 0 50929 74 0 0 25 0 1 0 486295008 105660416 24549 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25796 24549 603 41 0 25755 0
vsize: 103184
[startup+520.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 26485 0 0 0 51928 75 0 0 25 0 1 0 486295008 107819008 25113 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26323 25113 603 41 0 26282 0
vsize: 105292
[startup+530.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 27209 0 0 0 52926 78 0 0 25 0 1 0 486295008 110780416 25837 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27046 25837 603 41 0 27005 0
vsize: 108184
[startup+540.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 28038 0 0 0 53924 80 0 0 25 0 1 0 486295008 115191808 26666 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28123 26666 603 41 0 28082 0
vsize: 112492
[startup+550.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 28872 0 0 0 54922 82 0 0 25 0 1 0 486295008 118685696 27500 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28976 27500 603 41 0 28935 0
vsize: 115904
[startup+560.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 29674 0 0 0 55919 85 0 0 25 0 1 0 486295008 121901056 28302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29761 28302 603 41 0 29720 0
vsize: 119044
[startup+570.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 30397 0 0 0 56918 86 0 0 25 0 1 0 486295008 124858368 29025 4294967295 134512640 134672761 3221224544 3221223728 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30483 29025 603 41 0 30442 0
vsize: 121932
[startup+580.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 31050 0 0 0 57917 87 0 0 25 0 1 0 486295008 127549440 29678 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31140 29678 603 41 0 31099 0
vsize: 124560
[startup+590.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 31724 0 0 0 58915 89 0 0 25 0 1 0 486295008 130240512 30352 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31797 30352 603 41 0 31756 0
vsize: 127188
[startup+600.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 32355 0 0 0 59914 91 0 0 25 0 1 0 486295008 132808704 30983 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32424 30983 603 41 0 32383 0
vsize: 129696
[startup+610.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 32945 0 0 0 60912 93 0 0 25 0 1 0 486295008 135233536 31573 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33016 31573 603 41 0 32975 0
vsize: 132064
[startup+620.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 33517 0 0 0 61911 95 0 0 25 0 1 0 486295008 137662464 32145 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33609 32145 603 41 0 33568 0
vsize: 134436
[startup+630.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 34074 0 0 0 62910 96 0 0 25 0 1 0 486295008 139825152 32702 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34137 32702 603 41 0 34096 0
vsize: 136548
[startup+640.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 34643 0 0 0 63908 97 0 0 25 0 1 0 486295008 142254080 33271 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34730 33271 603 41 0 34689 0
vsize: 138920
[startup+650.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 35245 0 0 0 64907 99 0 0 25 0 1 0 486295008 144666624 33873 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35319 33873 603 41 0 35278 0
vsize: 141276
[startup+660.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 35801 0 0 0 65905 101 0 0 25 0 1 0 486295008 146956288 34429 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35878 34429 603 41 0 35837 0
vsize: 143512
[startup+670.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7728
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 36367 0 0 0 66904 103 0 0 25 0 1 0 486295008 149254144 34995 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36439 34995 603 41 0 36398 0
vsize: 145756
[startup+680.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 36885 0 0 0 67902 104 0 0 25 0 1 0 486295008 151416832 35513 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36967 35513 603 41 0 36926 0
vsize: 147868
[startup+690.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 37391 0 0 0 68901 105 0 0 25 0 1 0 486295008 153436160 36019 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37460 36019 603 41 0 37419 0
vsize: 149840
[startup+700.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 37887 0 0 0 69900 106 0 0 25 0 1 0 486295008 155459584 36515 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37954 36515 603 41 0 37913 0
vsize: 151816
[startup+710.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 38346 0 0 0 70899 108 0 0 25 0 1 0 486295008 157339648 36974 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38413 36974 603 41 0 38372 0
vsize: 153652
[startup+720.028 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 38894 0 0 0 71897 110 0 0 25 0 1 0 486295008 159625216 37522 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38971 37522 603 41 0 38930 0
vsize: 155884
[startup+730.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 39352 0 0 0 72897 112 0 0 25 0 1 0 486295008 161505280 37980 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39430 37980 603 41 0 39389 0
vsize: 157720
[startup+740.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 39800 0 0 0 73896 113 0 0 25 0 1 0 486295008 163246080 38428 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39855 38428 603 41 0 39814 0
vsize: 159420
[startup+750.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 40236 0 0 0 74895 114 0 0 25 0 1 0 486295008 164995072 38864 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40282 38864 603 41 0 40241 0
vsize: 161128
[startup+760.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 40693 0 0 0 75893 116 0 0 25 0 1 0 486295008 166883328 39321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40743 39321 603 41 0 40702 0
vsize: 162972
[startup+770.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 41134 0 0 0 76893 117 0 0 25 0 1 0 486295008 168771584 39762 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41204 39762 603 41 0 41163 0
vsize: 164816
[startup+780.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 41562 0 0 0 77892 118 0 0 25 0 1 0 486295008 170524672 40190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41632 40190 603 41 0 41591 0
vsize: 166528
[startup+790.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 41966 0 0 0 78891 119 0 0 25 0 1 0 486295008 172146688 40594 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42028 40594 603 41 0 41987 0
vsize: 168112
[startup+800.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 42342 0 0 0 79890 120 0 0 25 0 1 0 486295008 173629440 40970 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42390 40970 603 41 0 42349 0
vsize: 169560
[startup+810.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 42710 0 0 0 80889 121 0 0 25 0 1 0 486295008 175120384 41338 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42754 41338 603 41 0 42713 0
vsize: 171016
[startup+820.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 42955 0 0 0 81888 122 0 0 25 0 1 0 486295008 176214016 41583 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43021 41583 603 41 0 42980 0
vsize: 172084
[startup+830.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 82887 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223672 134556405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+840.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 83887 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+850.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 84887 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+860.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 85888 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+870.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 86888 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+880.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 87888 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+890.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 88888 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+900.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 89888 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+910.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 90889 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223648 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+920.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 91889 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+930.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43235 0 0 0 92889 123 0 0 25 0 1 0 486295008 177295360 41863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41863 603 41 0 43244 0
vsize: 173140
[startup+940.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43236 0 0 0 93889 123 0 0 25 0 1 0 486295008 177295360 41864 4294967295 134512640 134672761 3221224544 3221223668 134565980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41864 603 41 0 43244 0
vsize: 173140
[startup+950.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 94889 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+960.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 95890 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+970.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 96890 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+980.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 97890 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+990.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 98890 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 99890 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 100891 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43237 0 0 0 101891 123 0 0 25 0 1 0 486295008 177295360 41865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41865 603 41 0 43244 0
vsize: 173140
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 102891 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 103891 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 104891 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 105892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 106892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 107892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223808 134562281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 108892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 109892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 110892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 111893 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 112892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 113892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43238 0 0 0 114892 123 0 0 25 0 1 0 486295008 177295360 41866 4294967295 134512640 134672761 3221224544 3221223668 134565986 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41866 603 41 0 43244 0
vsize: 173140
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43239 0 0 0 115893 123 0 0 25 0 1 0 486295008 177295360 41867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41867 603 41 0 43244 0
vsize: 173140
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43239 0 0 0 116893 123 0 0 25 0 1 0 486295008 177295360 41867 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41867 603 41 0 43244 0
vsize: 173140
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43239 0 0 0 117893 123 0 0 25 0 1 0 486295008 177295360 41867 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41867 603 41 0 43244 0
vsize: 173140
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43239 0 0 0 118893 123 0 0 25 0 1 0 486295008 177295360 41867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41867 603 41 0 43244 0
vsize: 173140
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7730
Raw data (stat): 7673 (minisat+) R 7672 5897 5896 0 -1 0 43239 0 0 0 119893 123 0 0 25 0 1 0 486295008 177295360 41867 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43285 41867 603 41 0 43244 0
vsize: 173140
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 7730
Raw data (stat): 7673 (minisat+) Z 7672 5897 5896 0 -1 12 43242 0 0 0 119894 131 0 0 25 0 1 0 486295008 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.26
CPU user time (s): 1198.95
CPU system time (s): 1.3148
CPU usage (%): 100.009
Max. virtual memory (Kb): 173140
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####