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 17621

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        598656 kB
Buffers:         31628 kB
Cached:         383172 kB
SwapCached:          0 kB
Active:         131008 kB
Inactive:       286612 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        598404 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12796 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:16:47 (client local time) WITH STATUS 10 IN 1200.38 SECONDS
stats: 19342 7 1200.38 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  102506   286914 |   30751       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/27446          
c   -- var.elim.:  2000/27446          
c   -- var.elim.:  3000/27446          
c   -- var.elim.:  4000/27446          
c   -- var.elim.:  5000/27446          
c   -- var.elim.:  6000/27446          
c   -- var.elim.:  7000/27446          
c   -- var.elim.:  8000/27446          
c   -- var.elim.:  9000/27446          
c   -- var.elim.:  10000/27446          
c   -- var.elim.:  11000/27446          
c   -- var.elim.:  12000/27446          
c   -- var.elim.:  13000/27446          
c   -- var.elim.:  14000/27446          
c   -- var.elim.:  15000/27446          
c   -- var.elim.:  16000/27446          
c   -- var.elim.:  17000/27446          
c   -- var.elim.:  18000/27446          
c   -- var.elim.:  19000/27446          
c   -- var.elim.:  20000/27446          
c   -- var.elim.:  21000/27446          
c   -- var.elim.:  22000/27446          
c   -- var.elim.:  23000/27446          
c   -- var.elim.:  24000/27446          
c   -- var.elim.:  25000/27446          
c   -- var.elim.:  26000/27446          
c   -- var.elim.:  27000/27446          
c   -- var.elim.:  27446/27446          
c   -- var.elim.:  1000/12163          
c   -- var.elim.:  2000/12163          
c   -- var.elim.:  3000/12163          
c   -- var.elim.:  4000/12163          
c   -- var.elim.:  5000/12163          
c   -- var.elim.:  6000/12163          
c   -- var.elim.:  7000/12163          
c   -- var.elim.:  8000/12163          
c   -- var.elim.:  9000/12163          
c   -- var.elim.:  10000/12163          
c   -- var.elim.:  11000/12163          
c   -- var.elim.:  12000/12163          
c   -- var.elim.:  12163/12163          
c   -- var.elim.:  666/666          
c   -- subsuming                       
c   -- var.elim.:  1000/4760          
c   -- var.elim.:  2000/4760          
c   -- var.elim.:  3000/4760          
c   -- var.elim.:  4000/4760          
c   -- var.elim.:  4760/4760          
c   -- var.elim.:  1000/2634          
c   -- var.elim.:  2000/2634          
c   -- var.elim.:  2634/2634          
c   -- subsuming                       
c |         0 |   87548   277619 |      --       0       --      -- |     --   | -10468/3371
c |         0 |   87548   277619 |   35019       0        0     nan |  0.000 % |
c |       100 |   87548   277619 |   38521     100      278     2.8 | 20.487 % |
c |       251 |   87511   277489 |   42355     247      734     3.0 | 20.514 % |
c |       476 |   87474   277359 |   46571     468     1417     3.0 | 20.541 % |
c |       813 |   87437   277229 |   51206     801     2487     3.1 | 20.568 % |
c |      1319 |   87437   277229 |   56327    1307     4247     3.2 | 20.568 % |
c |      2078 |   87368   276980 |   61911    2059     7935     3.9 | 20.612 % |
c |      3217 |   87368   276980 |   68102    3198    12888     4.0 | 20.612 % |
c |      4925 |   87368   276980 |   74912    4906    21992     4.5 | 20.612 % |
c |      7487 |   87331   276850 |   82368    7466    35689     4.8 | 20.639 % |
c |     11332 |   87257   276590 |   90528   11309    83011     7.3 | 20.692 % |
c |     17100 |   87146   276200 |   99455   17067   254026    14.9 | 20.773 % |
c |     25749 |   87146   276200 |  109400   25716   438718    17.1 | 20.773 % |
c ==============================================================================
c (current CPU-time: 54.7667 s)
c ==============================================================================
c [1mFound solution: 5650972[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10520   maxlim: 2728812   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     35773 |  160553   538448 |   48165   35733   793842    22.2 | 20.773 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13698          
c   -- var.elim.:  2000/13698          
c   -- var.elim.:  3000/13698          
c   -- var.elim.:  4000/13698          
c   -- var.elim.:  5000/13698          
c   -- var.elim.:  6000/13698          
c   -- var.elim.:  7000/13698          
c   -- var.elim.:  8000/13698          
c   -- var.elim.:  9000/13698          
c   -- var.elim.:  10000/13698          
c   -- var.elim.:  11000/13698          
c   -- var.elim.:  12000/13698          
c   -- var.elim.:  13000/13698          
c   -- var.elim.:  13698/13698          
c   -- var.elim.:  252/252          
c   -- var.elim.:  108/108          
c   -- subsuming                       
c   -- var.elim.:  119/119          
c   -- var.elim.:  154/154          
c   -- subsuming                       
c   -- var.elim.:  112/112          
c |     35773 |  160189   537764 |      --   35733       --      -- |     --   | -364/-672
c |     35773 |  160189   537764 |   64075   34358   658550    19.2 | 20.773 % |
c |     35873 |  160170   537691 |   70474   34457   659058    19.1 | 14.317 % |
c |     36024 |  160170   537691 |   77522   34608   660645    19.1 | 14.317 % |
c |     36249 |  160170   537691 |   85274   34833   664057    19.1 | 14.317 % |
c |     36586 |  160170   537691 |   93801   35170   674093    19.2 | 14.317 % |
c |     37092 |  160170   537691 |  103182   35676   678333    19.0 | 14.317 % |
c |     37851 |  160170   537691 |  113500   36435   683418    18.8 | 14.317 % |
c |     38992 |  160170   537691 |  124850   37576   712635    19.0 | 14.317 % |
c ==============================================================================
c (current CPU-time: 67.9287 s)
c ==============================================================================
c [1mFound solution: 5636531[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2743253   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39579 |  160245   538095 |   48073   38163   729825    19.1 | 14.317 % |
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  42/42          
c   -- var.elim.:  10/10          
c |     39579 |  160222   538058 |      --   38163       --      -- |     --   | -23/-27
c |     39579 |  160222   538058 |   64088   38149   729740    19.1 | 14.317 % |
c |     39679 |  160222   538058 |   70497   38249   730214    19.1 | 14.343 % |
c |     39830 |  160222   538058 |   77547   38400   731011    19.0 | 14.343 % |
c |     40055 |  160222   538058 |   85302   38625   732484    19.0 | 14.343 % |
c |     40392 |  160222   538058 |   93832   38962   736582    18.9 | 14.343 % |
c |     40898 |  160222   538058 |  103215   39468   740741    18.8 | 14.343 % |
c |     41658 |  160222   538058 |  113537   40228   746630    18.6 | 14.343 % |
c |     42798 |  160222   538058 |  124890   41368   773228    18.7 | 14.343 % |
c |     44506 |  160222   538058 |  137380   43076   867627    20.1 | 14.343 % |
c |     47068 |  160139   537764 |  151039   45635  1004817    22.0 | 14.382 % |
c |     50912 |  160079   537551 |  166081   49475  1037222    21.0 | 14.407 % |
c ==============================================================================
c (current CPU-time: 108.238 s)
c ==============================================================================
c [1mFound solution: 5347659[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3032125   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55047 |  160124   537825 |   48037   53610  1209541    22.6 | 14.407 % |
c   -- subsuming                       
c   -- var.elim.:  131/131          
c   -- var.elim.:  84/84          
c   -- var.elim.:  24/24          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  34/34          
c   -- var.elim.:  22/22          
c |     55047 |  160015   537459 |      --   53610       --      -- |     --   | -95/-182
c |     55047 |  160015   537459 |   64006   53484  1199857    22.4 | 14.407 % |
c |     55147 |  160015   537459 |   70406   53584  1200604    22.4 | 14.450 % |
c |     55298 |  160015   537459 |   77447   53735  1203324    22.4 | 14.450 % |
c |     55523 |  160002   537413 |   85185   53959  1207567    22.4 | 14.456 % |
c |     55860 |  160002   537413 |   93703   54296  1219398    22.5 | 14.456 % |
c |     56366 |  160002   537413 |  103073   54802  1226838    22.4 | 14.456 % |
c |     57125 |  160002   537413 |  113381   55561  1245105    22.4 | 14.456 % |
c |     58265 |  160002   537413 |  124719   56701  1284893    22.7 | 14.456 % |
c |     59977 |  160002   537413 |  137191   58413  1368937    23.4 | 14.456 % |
c |     62540 |  159978   537329 |  150887   60969  1466804    24.1 | 14.468 % |
c |     66386 |  159978   537329 |  165976   64815  1584882    24.5 | 14.468 % |
c |     72152 |  159897   537034 |  182481   70576  1817184    25.7 | 14.502 % |
c |     80801 |  159860   536904 |  200683   79220  1945945    24.6 | 14.520 % |
c |     93775 |  159860   536904 |  220752   92194  4184204    45.4 | 14.520 % |
c |    113238 |  159860   536904 |  242827  111657  6147599    55.1 | 14.520 % |
c |    142431 |  159860   536904 |  267109  140850  7543136    53.6 | 14.520 % |
c ==============================================================================
c (current CPU-time: 294.321 s)
c ==============================================================================
c [1mFound solution: 5260640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3119144   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    177952 |  159888   537078 |   47966  176371  9587785    54.4 | 14.520 % |
c   -- subsuming                       
c   -- var.elim.:  123/123          
c   -- var.elim.:  90/90          
c   -- var.elim.:  31/31          
c   -- subsuming                       
c   -- var.elim.:  70/70          
c   -- var.elim.:  56/56          
c |    177952 |  159768   536744 |      --  176371       --      -- |     --   | -120/-327
c |    177952 |  159768   536744 |   63907  175053  9476033    54.1 | 14.520 % |
c |    178053 |  159768   536744 |   70297   21135   816118    38.6 | 14.558 % |
c |    178204 |  159768   536744 |   77327   21286   817007    38.4 | 14.558 % |
c |    178429 |  159768   536744 |   85060   21511   819568    38.1 | 14.558 % |
c |    178767 |  159768   536744 |   93566   21849   822859    37.7 | 14.558 % |
c |    179275 |  159768   536744 |  102923   22357   831340    37.2 | 14.558 % |
c |    180035 |  159768   536744 |  113215   23117   835826    36.2 | 14.558 % |
c |    181174 |  159768   536744 |  124537   24256   847406    34.9 | 14.558 % |
c |    182883 |  159768   536744 |  136990   25965   889131    34.2 | 14.558 % |
c |    185445 |  159768   536744 |  150689   28527   902278    31.6 | 14.558 % |
c |    189290 |  159731   536614 |  165720   32371   924325    28.6 | 14.576 % |
c |    195056 |  159731   536614 |  182292   38137  1218330    31.9 | 14.576 % |
c |    203705 |  159731   536614 |  200521   46786  1821635    38.9 | 14.576 % |
c |    216680 |  159731   536614 |  220573   59761  2644002    44.2 | 14.576 % |
c |    236141 |  159700   536507 |  242584   79219  3551641    44.8 | 14.588 % |
c |    265334 |  159626   536247 |  266718  108405  7725518    71.3 | 14.625 % |
c |    309123 |  159589   536117 |  293322  152189 12747147    83.8 | 14.643 % |
c ==============================================================================
c (current CPU-time: 710.193 s)
c ==============================================================================
c [1mFound solution: 4604168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3775616   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    370603 |  159638   536365 |   47891  213669 16321815    76.4 | 14.643 % |
c   -- subsuming                       
c   -- var.elim.:  145/145          
c   -- var.elim.:  79/79          
c   -- var.elim.:  28/28          
c   -- subsuming                       
c   -- var.elim.:  56/56          
c   -- var.elim.:  57/57          
c |    370603 |  159512   535921 |      --  213669       --      -- |     --   | -104/-201
c |    370603 |  159512   535921 |   63804  211855 15807937    74.6 | 14.643 % |
c |    370703 |  159512   535921 |   70185   19243   811157    42.2 | 14.683 % |
c |    370854 |  159512   535921 |   77203   19394   812181    41.9 | 14.683 % |
c |    371079 |  159512   535921 |   84924   19619   814207    41.5 | 14.683 % |
c |    371416 |  159512   535921 |   93416   19956   818426    41.0 | 14.683 % |
c |    371922 |  159512   535921 |  102758   20462   821851    40.2 | 14.683 % |
c |    372682 |  159512   535921 |  113034   21222   827266    39.0 | 14.683 % |
c |    373823 |  159512   535921 |  124337   22363   842333    37.7 | 14.683 % |
c |    375532 |  159512   535921 |  136771   24072   869540    36.1 | 14.683 % |
c |    378094 |  159475   535791 |  150413   26632   908942    34.1 | 14.701 % |
c |    381938 |  159475   535791 |  165454   30476   985463    32.3 | 14.701 % |
c |    387704 |  159419   535588 |  181936   36237  1088609    30.0 | 14.725 % |
c |    396354 |  159405   535536 |  200112   44884  1353347    30.2 | 14.728 % |
c |    409329 |  159405   535536 |  220123   57859  2798704    48.4 | 14.728 % |
c |    428790 |  159405   535536 |  242136   77320  3858401    49.9 | 14.728 % |
c |    457983 |  159405   535536 |  266349  106513  6186033    58.1 | 14.728 % |
c |    501772 |  159368   535406 |  292916  150299  9763530    65.0 | 14.747 % |
c |    567460 |  159368   535406 |  322208  215987 16024330    74.2 | 14.747 % |
c ==============================================================================
c (current CPU-time: 1099.03 s)
c ==============================================================================
c [1mFound solution: 4381028[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3998756   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    578001 |  159388   535543 |   47816  226525 16702595    73.7 | 14.747 % |
c   -- subsuming                       
c   -- var.elim.:  168/168          
c   -- var.elim.:  113/113          
c   -- var.elim.:  51/51          
c   -- subsuming                       
c   -- var.elim.:  78/78          
c   -- var.elim.:  33/33          
c |    578001 |  159275   535320 |      --  226525       --      -- |     --   | -113/-217
c |    578001 |  159275   535320 |   63710  224935 16061438    71.4 | 14.747 % |
c |    578102 |  159275   535320 |   70081   19688   868695    44.1 | 14.783 % |
c |    578252 |  159275   535320 |   77089   19838   869471    43.8 | 14.783 % |
c |    578477 |  159275   535320 |   84798   20063   870662    43.4 | 14.783 % |
c |    578815 |  159275   535320 |   93277   20401   876865    43.0 | 14.783 % |
c |    579321 |  159275   535320 |  102605   20907   880400    42.1 | 14.783 % |
c |    580080 |  159275   535320 |  112866   21666   919362    42.4 | 14.783 % |
c |    581219 |  159238   535190 |  124123   22800   924446    40.5 | 14.801 % |
c |    582927 |  159201   535060 |  136504   24505   935663    38.2 | 14.820 % |
c |    585489 |  159201   535060 |  150155   27067  1050908    38.8 | 14.820 % |
c |    589333 |  159201   535060 |  165170   30911  1092047    35.3 | 14.820 % |
c |    595100 |  159150   534878 |  181629   36674  1261381    34.4 | 14.841 % |
c |    603750 |  159150   534878 |  199792   45324  1663217    36.7 | 14.841 % |
c |    616724 |  159150   534878 |  219771   58298  2591412    44.5 | 14.841 % |
c |    636185 |  159113   534748 |  241692   77756  3292284    42.3 | 14.859 % |
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_b#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 1825
Raw data (stat): 1825 (runsolver) R 1824 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486306964 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0006 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 5620 0 0 0 982 16 0 0 25 0 1 0 486306964 22896640 5009 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5590 5009 603 41 0 5549 0
vsize: 22360
[startup+20 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 5620 0 0 0 1982 16 0 0 25 0 1 0 486306964 22896640 5009 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5590 5009 603 41 0 5549 0
vsize: 22360
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 5633 0 0 0 2982 16 0 0 25 0 1 0 486306964 23031808 5022 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5623 5022 603 41 0 5582 0
vsize: 22492
[startup+40.001 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 5977 0 0 0 3981 17 0 0 25 0 1 0 486306964 24453120 5366 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5970 5366 603 41 0 5929 0
vsize: 23880
[startup+50.0014 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 6404 0 0 0 4980 19 0 0 25 0 1 0 486306964 26316800 5793 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6425 5793 603 41 0 6384 0
vsize: 25700
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 15183 0 0 0 5959 40 0 0 25 0 1 0 486306964 55324672 11883 4294967295 134512640 134672761 3221224544 3221223712 134564493 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13507 11883 603 41 0 13466 0
vsize: 54028
[startup+70.0011 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 17039 0 0 0 6953 46 0 0 25 0 1 0 486306964 56537088 12185 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13803 12185 603 41 0 13762 0
vsize: 55212
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 17041 0 0 0 7953 46 0 0 25 0 1 0 486306964 56537088 12187 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13803 12187 603 41 0 13762 0
vsize: 55212
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 17297 0 0 0 8952 46 0 0 25 0 1 0 486306964 57602048 12443 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14063 12443 603 41 0 14022 0
vsize: 56252
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 17345 0 0 0 9953 46 0 0 25 0 1 0 486306964 57737216 12491 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14096 12491 603 41 0 14055 0
vsize: 56384
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 19193 0 0 0 10947 51 0 0 25 0 1 0 486306964 59379712 12895 4294967295 134512640 134672761 3221224544 3221223792 134593629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14497 12895 603 41 0 14456 0
vsize: 57988
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 19697 0 0 0 11947 52 0 0 25 0 1 0 486306964 59912192 13025 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14627 13025 603 41 0 14586 0
vsize: 58508
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 19973 0 0 0 12946 53 0 0 25 0 1 0 486306964 61112320 13301 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14920 13301 603 41 0 14879 0
vsize: 59680
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 20308 0 0 0 13945 54 0 0 25 0 1 0 486306964 62709760 13636 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15310 13636 603 41 0 15269 0
vsize: 61240
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 20525 0 0 0 14945 55 0 0 25 0 1 0 486306964 63516672 13853 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15507 13853 603 41 0 15466 0
vsize: 62028
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 22397 0 0 0 15940 60 0 0 25 0 1 0 486306964 71172096 15725 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17376 15725 603 41 0 17335 0
vsize: 69504
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 23336 0 0 0 16937 63 0 0 25 0 1 0 486306964 74891264 16664 4294967295 134512640 134672761 3221224544 3221223584 134603522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18284 16664 603 41 0 18243 0
vsize: 73136
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 24029 0 0 0 17934 66 0 0 25 0 1 0 486306964 77811712 17357 4294967295 134512640 134672761 3221224544 3221223584 134614261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18997 17357 603 41 0 18956 0
vsize: 75988
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1825
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 24589 0 0 0 18932 68 0 0 25 0 1 0 486306964 80068608 17917 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17917 603 41 0 19507 0
vsize: 78192
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 1863
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 25156 0 0 0 19930 70 0 0 25 0 1 0 486306964 82313216 18484 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20096 18484 603 41 0 20055 0
vsize: 80384
[startup+210.007 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 25682 0 0 0 20929 72 0 0 25 0 1 0 486306964 84451328 19010 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20618 19010 603 41 0 20577 0
vsize: 82472
[startup+220.007 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 25964 0 0 0 21928 73 0 0 25 0 1 0 486306964 85663744 19292 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20914 19292 603 41 0 20873 0
vsize: 83656
[startup+230.008 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 26614 0 0 0 22926 75 0 0 25 0 1 0 486306964 88711168 19942 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21658 19942 603 41 0 21617 0
vsize: 86632
[startup+240.008 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 27311 0 0 0 23924 77 0 0 25 0 1 0 486306964 91643904 20639 4294967295 134512640 134672761 3221224544 3221223680 134614736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22374 20639 603 41 0 22333 0
vsize: 89496
[startup+250.009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 27885 0 0 0 24924 78 0 0 25 0 1 0 486306964 93904896 21213 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22926 21213 603 41 0 22885 0
vsize: 91704
[startup+260.009 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 28312 0 0 0 25923 79 0 0 25 0 1 0 486306964 95629312 21640 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23347 21640 603 41 0 23306 0
vsize: 93388
[startup+270.009 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 1878
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 28704 0 0 0 26921 80 0 0 25 0 1 0 486306964 97234944 22032 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23739 22032 603 41 0 23698 0
vsize: 94956
[startup+280.01 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 29083 0 0 0 27921 81 0 0 25 0 1 0 486306964 98856960 22411 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24135 22411 603 41 0 24094 0
vsize: 96540
[startup+290.01 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 29390 0 0 0 28920 82 0 0 25 0 1 0 486306964 100073472 22718 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24432 22718 603 41 0 24391 0
vsize: 97728
[startup+300.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 29916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223708 134564518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+310.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 30915 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+320.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 31915 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+330.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 32915 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223692 134614482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+340.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 33916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+350.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 34916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+360.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 35916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+370.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 36916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+380.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 37916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+390.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 38916 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+400.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 39917 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+410.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 40917 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+420.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 41917 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+430.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 42917 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+440.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 43917 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+450.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 44918 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 45918 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 46918 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 47918 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 48918 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+500.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31859 0 0 0 49919 87 0 0 25 0 1 0 486306964 101928960 23083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24885 23083 603 41 0 24844 0
vsize: 99540
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 31923 0 0 0 50919 87 0 0 25 0 1 0 486306964 102195200 23147 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24950 23147 603 41 0 24909 0
vsize: 99800
[startup+520.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 32311 0 0 0 51917 88 0 0 25 0 1 0 486306964 103780352 23535 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25337 23535 603 41 0 25296 0
vsize: 101348
[startup+530.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1880
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 32664 0 0 0 52917 89 0 0 25 0 1 0 486306964 105254912 23888 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25697 23888 603 41 0 25656 0
vsize: 102788
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 33001 0 0 0 53916 90 0 0 25 0 1 0 486306964 106700800 24225 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26050 24225 603 41 0 26009 0
vsize: 104200
[startup+550.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 33358 0 0 0 54916 91 0 0 25 0 1 0 486306964 108150784 24582 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26404 24582 603 41 0 26363 0
vsize: 105616
[startup+560.126 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 33697 0 0 0 55926 91 0 0 25 0 1 0 486306964 109617152 24921 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26762 24921 603 41 0 26721 0
vsize: 107048
[startup+570.126 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 34093 0 0 0 56925 92 0 0 25 0 1 0 486306964 111206400 25317 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27150 25317 603 41 0 27109 0
vsize: 108600
[startup+580.127 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 34668 0 0 0 57925 93 0 0 25 0 1 0 486306964 113590272 25892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27732 25892 603 41 0 27691 0
vsize: 110928
[startup+590.126 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 35067 0 0 0 58923 95 0 0 25 0 1 0 486306964 115191808 26291 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28123 26291 603 41 0 28082 0
vsize: 112492
[startup+600.127 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 35518 0 0 0 59922 96 0 0 25 0 1 0 486306964 117063680 26742 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28580 26742 603 41 0 28539 0
vsize: 114320
[startup+610.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 35707 0 0 0 60922 97 0 0 25 0 1 0 486306964 117866496 26931 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28776 26931 603 41 0 28735 0
vsize: 115104
[startup+620.127 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 35972 0 0 0 61921 98 0 0 25 0 1 0 486306964 118927360 27196 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29035 27196 603 41 0 28994 0
vsize: 116140
[startup+630.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 36414 0 0 0 62920 99 0 0 25 0 1 0 486306964 120791040 27638 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29490 27638 603 41 0 29449 0
vsize: 117960
[startup+640.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 36818 0 0 0 63919 100 0 0 25 0 1 0 486306964 122404864 28042 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29884 28042 603 41 0 29843 0
vsize: 119536
[startup+650.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 37162 0 0 0 64919 101 0 0 25 0 1 0 486306964 123863040 28386 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30240 28386 603 41 0 30199 0
vsize: 120960
[startup+660.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 37591 0 0 0 65917 103 0 0 25 0 1 0 486306964 125587456 28815 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30661 28815 603 41 0 30620 0
vsize: 122644
[startup+670.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 37985 0 0 0 66917 103 0 0 25 0 1 0 486306964 127176704 29209 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31049 29209 603 41 0 31008 0
vsize: 124196
[startup+680.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 38468 0 0 0 67916 104 0 0 25 0 1 0 486306964 129163264 29692 4294967295 134512640 134672761 3221224544 3221223728 134615761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31534 29692 603 41 0 31493 0
vsize: 126136
[startup+690.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 38867 0 0 0 68915 105 0 0 25 0 1 0 486306964 130785280 30091 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31930 30091 603 41 0 31889 0
vsize: 127720
[startup+700.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 39148 0 0 0 69915 106 0 0 25 0 1 0 486306964 131862528 30372 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32193 30372 603 41 0 32152 0
vsize: 128772
[startup+710.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 39796 0 0 0 70912 109 0 0 25 0 1 0 486306964 134533120 31020 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32845 31020 603 41 0 32804 0
vsize: 131380
[startup+720.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 71906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223776 134564429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+730.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 72905 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+740.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 73906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+750.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 74906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+760.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 75906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+770.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 76906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+780.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 77906 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+790.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 78907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+800.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 79907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+810.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 80907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+820.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 81907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+830.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 82907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+840.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 83907 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+850.143 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 84908 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+860.143 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 85908 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+870.143 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 86908 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223800 134618007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+880.143 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 87908 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+890.143 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 88908 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+900.144 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 89909 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223536 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+910.146 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 90909 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+920.145 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 91909 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+930.145 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 92909 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+940.146 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 93909 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+950.146 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 94910 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+960.149 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 95910 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+970.148 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 96910 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+980.149 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 97910 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+990.149 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 98911 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1000.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 99911 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1010.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 100911 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1020.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 101911 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1030.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 102911 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1040.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 103912 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1050.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42018 0 0 0 104912 115 0 0 25 0 1 0 486306964 135004160 31189 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32960 31189 603 41 0 32919 0
vsize: 131840
[startup+1060.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42297 0 0 0 105911 116 0 0 25 0 1 0 486306964 136282112 31468 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33272 31468 603 41 0 33231 0
vsize: 133088
[startup+1070.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42645 0 0 0 106910 117 0 0 25 0 1 0 486306964 137748480 31816 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33630 31816 603 41 0 33589 0
vsize: 134520
[startup+1080.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42803 0 0 0 107910 117 0 0 25 0 1 0 486306964 138416128 31974 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33793 31974 603 41 0 33752 0
vsize: 135172
[startup+1090.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 42941 0 0 0 108910 117 0 0 25 0 1 0 486306964 138948608 32112 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33923 32112 603 41 0 33882 0
vsize: 135692
[startup+1100.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 44108 0 0 0 109908 120 0 0 25 0 1 0 486306964 144801792 33279 4294967295 134512640 134672761 3221224544 3221222664 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35352 33279 603 41 0 35311 0
vsize: 141408
[startup+1110.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 110903 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1120.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 111903 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1130.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 112903 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1140.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 113903 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1150.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 114904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1160.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 115904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1170.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 116904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 117904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 118904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 1882
Raw data (stat): 1825 (minisat+) R 1824 32461 32460 0 -1 0 45701 0 0 0 119904 124 0 0 25 0 1 0 486306964 141553664 32772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32772 603 41 0 34518 0
vsize: 138236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 1882
Raw data (stat): 1825 (minisat+) Z 1824 32461 32460 0 -1 12 45702 0 0 0 119905 131 0 0 25 0 1 0 486306964 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.24
CPU time (s): 1200.38
CPU user time (s): 1199.06
CPU system time (s): 1.3168
CPU usage (%): 100.011
Max. virtual memory (Kb): 141408
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####