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 17623

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 10:57:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19336 boxname=wulflinc3 idbench=1488 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6a6f7751d9c11fcafeb386712eac2f08  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran4x64.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-ran4x64.opb
IDLAUNCH: 19336
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        306872 kB
Buffers:         34792 kB
Cached:         669768 kB
SwapCached:         56 kB
Active:         166292 kB
Inactive:       541140 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        306620 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              64 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            14760 kB
Committed_AS:    71664 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:17:50 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19336 7 1200.3 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 |   98034   276354 |   32678       0        0     nan |  0.000 % |
c |       100 |   97988   276250 |   35945      94      282     3.0 | 14.168 % |
c |       250 |   97957   276176 |   39540     240      741     3.1 | 14.196 % |
c |       475 |   97945   276150 |   43494     463     1397     3.0 | 14.208 % |
c |       812 |   97893   276006 |   47843     793     2406     3.0 | 14.249 % |
c |      1318 |   97773   275734 |   52628    1286     3943     3.1 | 14.365 % |
c |      2077 |   97624   275371 |   57891    2029     6233     3.1 | 14.496 % |
c |      3216 |   97348   274739 |   63680    3137    10122     3.2 | 14.756 % |
c |      4924 |   97152   274269 |   70048    4823    17855     3.7 | 14.931 % |
c |      7486 |   96815   273435 |   77053    7333    34649     4.7 | 15.222 % |
c |     11330 |   96663   273090 |   84758   11158    78997     7.1 | 15.369 % |
c |     17096 |   96583   272912 |   93234   16916   234262    13.8 | 15.451 % |
c |     25747 |   96409   272495 |  102557   25542   452504    17.7 | 15.610 % |
c |     38721 |   95946   271457 |  112813   38472   788366    20.5 | 16.067 % |
c ==============================================================================
c [1mFound solution: 5714495[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10520   maxlim: 2665289   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57714 |  169433   534035 |   56477   57453  1687223    29.4 | 16.067 % |
c |     57814 |  169433   534035 |   62124   57553  1688134    29.3 | 12.156 % |
c |     57964 |  169415   533993 |   68337   57702  1689117    29.3 | 12.170 % |
c |     58189 |  169415   533993 |   75170   57927  1691115    29.2 | 12.170 % |
c |     58526 |  169415   533993 |   82687   58264  1693714    29.1 | 12.170 % |
c |     59032 |  169415   533993 |   90956   58770  1698254    28.9 | 12.170 % |
c |     59791 |  169415   533993 |  100052   59529  1707616    28.7 | 12.170 % |
c |     60930 |  169375   533902 |  110057   60665  1721178    28.4 | 12.201 % |
c |     62639 |  169375   533902 |  121063   62374  1746745    28.0 | 12.201 % |
c |     65201 |  169375   533902 |  133169   64936  1787518    27.5 | 12.201 % |
c |     69047 |  169357   533860 |  146486   68780  1834500    26.7 | 12.213 % |
c |     74813 |  169321   533782 |  161135   74543  1917770    25.7 | 12.241 % |
c |     83464 |  169309   533756 |  177249   83193  2436978    29.3 | 12.250 % |
c |     96438 |  169273   533678 |  194973   96161  2970606    30.9 | 12.278 % |
c ==============================================================================
c [1mFound solution: 5575105[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2804679   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111008 |  169247   533745 |   56415  110724  3832850    34.6 | 12.278 % |
c |    111108 |  169247   533745 |   62056   19323   782149    40.5 | 12.334 % |
c |    111258 |  169232   533711 |   68262   19472   782709    40.2 | 12.346 % |
c |    111483 |  169193   533621 |   75088   19693   783921    39.8 | 12.376 % |
c |    111820 |  169185   533604 |   82597   20027   785910    39.2 | 12.383 % |
c |    112326 |  169167   533562 |   90856   20532   788586    38.4 | 12.395 % |
c |    113085 |  169167   533562 |   99942   21291   794400    37.3 | 12.395 % |
c |    114224 |  169167   533562 |  109936   22430   824346    36.8 | 12.395 % |
c |    115934 |  169131   533480 |  120930   24138   854651    35.4 | 12.423 % |
c |    118496 |  169099   533407 |  133023   26697   927782    34.8 | 12.447 % |
c |    122340 |  169078   533359 |  146325   30540   992304    32.5 | 12.463 % |
c |    128106 |  168979   533132 |  160958   36295  1068377    29.4 | 12.539 % |
c |    136755 |  168961   533090 |  177054   44943  1558963    34.7 | 12.553 % |
c |    149729 |  168901   532956 |  194759   57911  1805632    31.2 | 12.600 % |
c |    169190 |  168889   532930 |  214235   77370  5438575    70.3 | 12.609 % |
c |    198383 |  168824   532783 |  235659  106556  7169408    67.3 | 12.659 % |
c |    242172 |  168767   532649 |  259225  150335  8698435    57.9 | 12.699 % |
c ==============================================================================
c [1mFound solution: 5248200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3131584   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    266152 |  168784   532795 |   56261  174314  9698842    55.6 | 12.699 % |
c |    266252 |  168784   532795 |   61887   19110   630793    33.0 | 12.719 % |
c |    266402 |  168784   532795 |   68075   19260   631996    32.8 | 12.719 % |
c |    266627 |  168784   532795 |   74883   19485   634087    32.5 | 12.719 % |
c |    266964 |  168784   532795 |   82371   19822   636531    32.1 | 12.719 % |
c |    267470 |  168746   532709 |   90608   20322   673002    33.1 | 12.747 % |
c |    268230 |  168746   532709 |   99669   21082   678420    32.2 | 12.747 % |
c |    269369 |  168742   532700 |  109636   22219   684766    30.8 | 12.749 % |
c |    271077 |  168742   532700 |  120600   23927   695064    29.0 | 12.749 % |
c |    273640 |  168729   532670 |  132660   26488   743404    28.1 | 12.759 % |
c |    277484 |  168681   532561 |  145926   30327   773877    25.5 | 12.796 % |
c |    283250 |  168670   532536 |  160519   36090   999639    27.7 | 12.803 % |
c |    291899 |  168610   532400 |  176571   44729  1246640    27.9 | 12.846 % |
c |    304873 |  168598   532374 |  194228   57702  1921293    33.3 | 12.855 % |
c |    324334 |  168552   532271 |  213651   77158  2548581    33.0 | 12.886 % |
c |    353528 |  168522   532203 |  235016  106349  4092464    38.5 | 12.909 % |
c |    397317 |  168522   532203 |  258517  150138  9427883    62.8 | 12.909 % |
c |    463001 |  168486   532120 |  284369  215818 15896902    73.7 | 12.938 % |
c ==============================================================================
c [1mFound solution: 5026432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3353352   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    528003 |  168481   532209 |   56160  280814 25690474    91.5 | 12.938 % |
c |    528103 |  168481   532209 |   61776   28172  1663901    59.1 | 12.971 % |
c |    528256 |  168481   532209 |   67953   28325  1666532    58.8 | 12.971 % |
c |    528481 |  168481   532209 |   74748   28550  1667970    58.4 | 12.971 % |
c |    528818 |  168477   532200 |   82223   28886  1669919    57.8 | 12.973 % |
c |    529324 |  168477   532200 |   90446   29392  1677413    57.1 | 12.973 % |
c |    530083 |  168462   532166 |   99490   30150  1710417    56.7 | 12.983 % |
c |    531222 |  168456   532152 |  109439   31288  1720961    55.0 | 12.987 % |
c |    532930 |  168456   532152 |  120383   32996  1734638    52.6 | 12.987 % |
c |    535492 |  168435   532104 |  132422   35557  1773090    49.9 | 13.004 % |
c |    539338 |  168429   532090 |  145664   39402  1934385    49.1 | 13.009 % |
c |    545105 |  168429   532090 |  160231   45169  1996888    44.2 | 13.009 % |
c |    553754 |  168429   532090 |  176254   53818  2788069    51.8 | 13.009 % |
c |    566728 |  168429   532090 |  193879   66792  3721378    55.7 | 13.009 % |
c ==============================================================================
c [1mFound solution: 4307707[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4072077   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    578416 |  168443   532228 |   56147   78480  4302799    54.8 | 13.009 % |
c |    578516 |  168443   532228 |   61761   18312   634881    34.7 | 13.026 % |
c |    578666 |  168443   532228 |   67937   18462   635450    34.4 | 13.026 % |
c |    578891 |  168443   532228 |   74731   18687   636740    34.1 | 13.026 % |
c |    579229 |  168443   532228 |   82204   19025   638583    33.6 | 13.026 % |
c |    579735 |  168443   532228 |   90425   19531   641502    32.8 | 13.026 % |
c |    580494 |  168443   532228 |   99467   20290   645314    31.8 | 13.026 % |
c |    581634 |  168443   532228 |  109414   21430   652543    30.4 | 13.026 % |
c |    583342 |  168443   532228 |  120356   23138   673042    29.1 | 13.026 % |
c |    585904 |  168443   532228 |  132391   25700   693970    27.0 | 13.026 % |
c |    589750 |  168443   532228 |  145630   29546   778192    26.3 | 13.026 % |
c |    595518 |  168407   532146 |  160193   35311   885682    25.1 | 13.054 % |
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 Y1#### 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.91 0.95 0.90 2/54 11401
Raw data (stat): 11401 (runsolver) R 11400 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486311292 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 3049 0 0 0 991 7 0 0 25 0 1 0 486311292 14188544 2962 4294967295 134512640 134672761 3221224624 3221223776 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3464 2962 603 41 0 3423 0
vsize: 13856
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 3097 0 0 0 1991 7 0 0 25 0 1 0 486311292 14458880 3010 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3530 3010 603 41 0 3489 0
vsize: 14120
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 3316 0 0 0 2990 8 0 0 25 0 1 0 486311292 15302656 3229 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3736 3229 603 41 0 3695 0
vsize: 14944
[startup+40.0026 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 3524 0 0 0 3989 9 0 0 25 0 1 0 486311292 16273408 3437 4294967295 134512640 134672761 3221224624 3221223564 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3973 3437 603 41 0 3932 0
vsize: 15892
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 3896 0 0 0 4987 11 0 0 25 0 1 0 486311292 17756160 3809 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4335 3809 603 41 0 4294 0
vsize: 17340
[startup+60.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 4123 0 0 0 5987 11 0 0 25 0 1 0 486311292 18690048 4036 4294967295 134512640 134672761 3221224624 3221223788 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4563 4036 603 41 0 4522 0
vsize: 18252
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 4534 0 0 0 6986 12 0 0 25 0 1 0 486311292 20430848 4447 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4447 603 41 0 4947 0
vsize: 19952
[startup+80.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 5233 0 0 0 7984 14 0 0 25 0 1 0 486311292 23265280 5146 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5680 5146 603 41 0 5639 0
vsize: 22720
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 11878 0 0 0 8969 29 0 0 25 0 1 0 486311292 48058368 10507 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11733 10507 603 41 0 11692 0
vsize: 46932
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 12053 0 0 0 9969 30 0 0 25 0 1 0 486311292 48734208 10682 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11898 10682 603 41 0 11857 0
vsize: 47592
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 12273 0 0 0 10968 31 0 0 25 0 1 0 486311292 49807360 10902 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12160 10902 603 41 0 12119 0
vsize: 48640
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 12745 0 0 0 11967 32 0 0 25 0 1 0 486311292 51683328 11374 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12618 11374 603 41 0 12577 0
vsize: 50472
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11401
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 13054 0 0 0 12966 33 0 0 25 0 1 0 486311292 53030912 11683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12947 11683 603 41 0 12906 0
vsize: 51788
[startup+140.007 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 13652 0 0 0 13964 35 0 0 25 0 1 0 486311292 55308288 12281 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13503 12281 603 41 0 13462 0
vsize: 54012
[startup+150.008 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14405 0 0 0 14963 37 0 0 25 0 1 0 486311292 58417152 13034 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14262 13034 603 41 0 14221 0
vsize: 57048
[startup+160.009 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14569 0 0 0 15962 38 0 0 25 0 1 0 486311292 59092992 13198 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14427 13198 603 41 0 14386 0
vsize: 57708
[startup+170.009 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 16961 39 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+180.009 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 17961 39 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+190.01 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 18961 40 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223824 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+200.01 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 11454
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 19961 40 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+210.011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 20961 41 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223864 134541793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+220.011 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 21961 41 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+230.013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 22961 41 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+240.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 23960 41 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+250.013 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 24960 42 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223696 1074719016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+260.014 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 25960 42 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+270.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 14884 0 0 0 26960 42 0 0 25 0 1 0 486311292 60178432 13465 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14692 13465 603 41 0 14651 0
vsize: 58768
[startup+280.014 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 15199 0 0 0 27959 43 0 0 25 0 1 0 486311292 61382656 13780 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14986 13780 603 41 0 14945 0
vsize: 59944
[startup+290.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 16247 0 0 0 28957 46 0 0 25 0 1 0 486311292 65691648 14828 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16038 14828 603 41 0 15997 0
vsize: 64152
[startup+300.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 16528 0 0 0 29956 47 0 0 25 0 1 0 486311292 66908160 15109 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16335 15109 603 41 0 16294 0
vsize: 65340
[startup+310.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 16843 0 0 0 30955 48 0 0 25 0 1 0 486311292 68116480 15424 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16630 15424 603 41 0 16589 0
vsize: 66520
[startup+320.016 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 17501 0 0 0 31952 51 0 0 25 0 1 0 486311292 70799360 16082 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17285 16082 603 41 0 17244 0
vsize: 69140
[startup+330.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 18053 0 0 0 32951 53 0 0 25 0 1 0 486311292 73089024 16634 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17844 16634 603 41 0 17803 0
vsize: 71376
[startup+340.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 18471 0 0 0 33949 55 0 0 25 0 1 0 486311292 74850304 17052 4294967295 134512640 134672761 3221224624 3221223760 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18274 17052 603 41 0 18233 0
vsize: 73096
[startup+350.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 18665 0 0 0 34947 56 0 0 25 0 1 0 486311292 75661312 17246 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18472 17246 603 41 0 18431 0
vsize: 73888
[startup+360.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 18784 0 0 0 35947 57 0 0 25 0 1 0 486311292 76058624 17365 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18569 17365 603 41 0 18528 0
vsize: 74276
[startup+370.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 19279 0 0 0 36945 59 0 0 25 0 1 0 486311292 78069760 17860 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19060 17860 603 41 0 19019 0
vsize: 76240
[startup+380.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 19676 0 0 0 37944 60 0 0 25 0 1 0 486311292 80203776 18257 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19581 18257 603 41 0 19540 0
vsize: 78324
[startup+390.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 19845 0 0 0 38944 61 0 0 25 0 1 0 486311292 80879616 18426 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19746 18426 603 41 0 19705 0
vsize: 78984
[startup+400.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 20048 0 0 0 39943 62 0 0 25 0 1 0 486311292 81686528 18629 4294967295 134512640 134672761 3221224624 3221223776 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19943 18629 603 41 0 19902 0
vsize: 79772
[startup+410.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 20137 0 0 0 40943 62 0 0 25 0 1 0 486311292 82092032 18718 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20042 18718 603 41 0 20001 0
vsize: 80168
[startup+420.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 20572 0 0 0 41941 64 0 0 25 0 1 0 486311292 83849216 19153 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20471 19153 603 41 0 20430 0
vsize: 81884
[startup+430.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21051 0 0 0 42940 65 0 0 25 0 1 0 486311292 85733376 19632 4294967295 134512640 134672761 3221224624 3221223564 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20931 19632 603 41 0 20890 0
vsize: 83724
[startup+440.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11456
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21479 0 0 0 43940 66 0 0 25 0 1 0 486311292 87486464 20060 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21359 20060 603 41 0 21318 0
vsize: 85436
[startup+450.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 44938 68 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+460.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 45938 68 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223776 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+470.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 46938 68 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+480.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 47938 69 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+490.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 48938 69 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+500.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 49937 70 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223880 134562565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+510.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 50937 70 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+520.029 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 51937 70 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+530.03 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 52937 71 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+540.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 53937 71 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+550.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 54937 71 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+560.031 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 55937 71 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+570.032 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 56936 72 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+580.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 57936 72 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+590.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 58936 72 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+600.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 59936 72 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+610.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 60936 73 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+620.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 61935 73 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+630.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 62936 73 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+640.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 63936 73 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+650.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 64936 74 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+660.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 65935 74 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+670.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 66935 74 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+680.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21836 0 0 0 67935 74 0 0 25 0 1 0 486311292 88600576 20350 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21631 20350 603 41 0 21590 0
vsize: 86524
[startup+690.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 21999 0 0 0 68935 75 0 0 25 0 1 0 486311292 89276416 20513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21796 20513 603 41 0 21755 0
vsize: 87184
[startup+700.039 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 22369 0 0 0 69934 76 0 0 25 0 1 0 486311292 90759168 20883 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22158 20883 603 41 0 22117 0
vsize: 88632
[startup+710.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 22435 0 0 0 70934 77 0 0 25 0 1 0 486311292 91164672 20949 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22257 20949 603 41 0 22216 0
vsize: 89028
[startup+720.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 22976 0 0 0 71932 79 0 0 25 0 1 0 486311292 93306880 21490 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22780 21490 603 41 0 22739 0
vsize: 91120
[startup+730.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 23636 0 0 0 72930 81 0 0 25 0 1 0 486311292 95993856 22150 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23436 22150 603 41 0 23395 0
vsize: 93744
[startup+740.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 24177 0 0 0 73928 83 0 0 25 0 1 0 486311292 98283520 22691 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23995 22691 603 41 0 23954 0
vsize: 95980
[startup+750.042 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 24681 0 0 0 74927 85 0 0 25 0 1 0 486311292 100323328 23195 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24493 23195 603 41 0 24452 0
vsize: 97972
[startup+760.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 25171 0 0 0 75926 86 0 0 25 0 1 0 486311292 102334464 23685 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24984 23685 603 41 0 24943 0
vsize: 99936
[startup+770.043 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 25622 0 0 0 76925 87 0 0 25 0 1 0 486311292 104087552 24136 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25412 24136 603 41 0 25371 0
vsize: 101648
[startup+780.044 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 26105 0 0 0 77923 89 0 0 25 0 1 0 486311292 106110976 24619 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25906 24619 603 41 0 25865 0
vsize: 103624
[startup+790.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 26555 0 0 0 78922 90 0 0 25 0 1 0 486311292 107855872 25069 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26332 25069 603 41 0 26291 0
vsize: 105328
[startup+800.045 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 26995 0 0 0 79921 91 0 0 25 0 1 0 486311292 109740032 25509 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26792 25509 603 41 0 26751 0
vsize: 107168
[startup+810.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 27427 0 0 0 80920 92 0 0 25 0 1 0 486311292 111501312 25941 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27222 25941 603 41 0 27181 0
vsize: 108888
[startup+820.046 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 27840 0 0 0 81919 94 0 0 25 0 1 0 486311292 113119232 26354 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27617 26354 603 41 0 27576 0
vsize: 110468
[startup+830.047 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 28173 0 0 0 82918 95 0 0 25 0 1 0 486311292 114483200 26687 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27950 26687 603 41 0 27909 0
vsize: 111800
[startup+840.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 28491 0 0 0 83917 96 0 0 25 0 1 0 486311292 115863552 27005 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28287 27005 603 41 0 28246 0
vsize: 113148
[startup+850.048 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 28896 0 0 0 84916 97 0 0 25 0 1 0 486311292 117477376 27410 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28681 27410 603 41 0 28640 0
vsize: 114724
[startup+860.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 29278 0 0 0 85916 98 0 0 25 0 1 0 486311292 118956032 27792 4294967295 134512640 134672761 3221224624 3221223760 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29042 27792 603 41 0 29001 0
vsize: 116168
[startup+870.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 29832 0 0 0 86914 100 0 0 25 0 1 0 486311292 121245696 28346 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29601 28346 603 41 0 29560 0
vsize: 118404
[startup+880.049 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 30169 0 0 0 87913 101 0 0 25 0 1 0 486311292 122589184 28683 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29929 28683 603 41 0 29888 0
vsize: 119716
[startup+890.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 30851 0 0 0 88911 103 0 0 25 0 1 0 486311292 125427712 29365 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30622 29365 603 41 0 30581 0
vsize: 122488
[startup+900.051 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 31689 0 0 0 89910 105 0 0 25 0 1 0 486311292 128790528 30203 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31443 30203 603 41 0 31402 0
vsize: 125772
[startup+910.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 32617 0 0 0 90907 108 0 0 25 0 1 0 486311292 132554752 31131 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32362 31131 603 41 0 32321 0
vsize: 129448
[startup+920.052 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 33376 0 0 0 91906 109 0 0 25 0 1 0 486311292 135659520 31890 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33120 31890 603 41 0 33079 0
vsize: 132480
[startup+930.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 33959 0 0 0 92904 111 0 0 25 0 1 0 486311292 138084352 32473 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33712 32473 603 41 0 33671 0
vsize: 134848
[startup+940.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 34494 0 0 0 93903 112 0 0 25 0 1 0 486311292 140247040 33008 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34240 33008 603 41 0 34199 0
vsize: 136960
[startup+950.053 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 35029 0 0 0 94902 114 0 0 25 0 1 0 486311292 142532608 33543 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34798 33543 603 41 0 34757 0
vsize: 139192
[startup+960.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 35572 0 0 0 95900 116 0 0 25 0 1 0 486311292 144691200 34086 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35325 34086 603 41 0 35284 0
vsize: 141300
[startup+970.055 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 36098 0 0 0 96899 117 0 0 25 0 1 0 486311292 146837504 34612 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35849 34612 603 41 0 35808 0
vsize: 143396
[startup+980.056 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 36604 0 0 0 97898 119 0 0 25 0 1 0 486311292 149905408 35118 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36598 35118 603 41 0 36557 0
vsize: 146392
[startup+990.057 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 37140 0 0 0 98896 120 0 0 25 0 1 0 486311292 152195072 35654 4294967295 134512640 134672761 3221224624 3221223792 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37157 35654 603 41 0 37116 0
vsize: 148628
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 37641 0 0 0 99895 122 0 0 25 0 1 0 486311292 154222592 36155 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37652 36155 603 41 0 37611 0
vsize: 150608
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 38175 0 0 0 100893 124 0 0 25 0 1 0 486311292 156385280 36689 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38180 36689 603 41 0 38139 0
vsize: 152720
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 38594 0 0 0 101892 126 0 0 25 0 1 0 486311292 158138368 37108 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38608 37108 603 41 0 38567 0
vsize: 154432
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 38818 0 0 0 102891 126 0 0 25 0 1 0 486311292 158953472 37332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38807 37332 603 41 0 38766 0
vsize: 155228
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 38980 0 0 0 103891 127 0 0 25 0 1 0 486311292 159633408 37494 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38973 37494 603 41 0 38932 0
vsize: 155892
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39313 0 0 0 104890 128 0 0 25 0 1 0 486311292 160980992 37827 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39302 37827 603 41 0 39261 0
vsize: 157208
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 105889 129 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 106889 129 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 107889 129 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 108889 129 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223792 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 109889 129 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 110889 130 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 111889 130 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 112889 130 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 113889 131 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39529 0 0 0 114889 131 0 0 25 0 1 0 486311292 161243136 37910 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37910 603 41 0 39325 0
vsize: 157464
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39530 0 0 0 115889 131 0 0 25 0 1 0 486311292 161243136 37911 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37911 603 41 0 39325 0
vsize: 157464
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39530 0 0 0 116889 131 0 0 25 0 1 0 486311292 161243136 37911 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37911 603 41 0 39325 0
vsize: 157464
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39530 0 0 0 117889 131 0 0 25 0 1 0 486311292 161243136 37911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37911 603 41 0 39325 0
vsize: 157464
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39530 0 0 0 118889 132 0 0 25 0 1 0 486311292 161243136 37911 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37911 603 41 0 39325 0
vsize: 157464
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 11458
Raw data (stat): 11401 (minisat+) R 11400 10720 10719 0 -1 0 39530 0 0 0 119888 132 0 0 25 0 1 0 486311292 161243136 37911 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39366 37911 603 41 0 39325 0
vsize: 157464
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 11458
Raw data (stat): 11401 (minisat+) Z 11400 10720 10719 0 -1 12 39533 0 0 0 119889 140 0 0 25 0 1 0 486311292 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.3
CPU user time (s): 1198.89
CPU system time (s): 1.40279
CPU usage (%): 100.012
Max. virtual memory (Kb): 157464
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####