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-ran6x43.opb
MD5SUM	795a1eda830447df9b9714fdf1d66b4e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2795888
Optimality of the best value was proved	NO
Number of terms in the objective function	5418
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	1537450315
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	1537450315
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	1224.65
Number of variables	5418
Total number of constraints	307
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	307
Minimum length of a constraint	21
Maximum length of a constraint	860
Trace number 17607

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        385736 kB
Buffers:         32628 kB
Cached:         585468 kB
SwapCached:         24 kB
Active:         171812 kB
Inactive:       448956 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        385484 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22548 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:11:41 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 19355 7 1200.32 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 356 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 354]---> Adder-cost: 894   maxlim: 78677   bits: 17/17
c ---[ 352]---> Adder-cost: 894   maxlim: 84309   bits: 17/17
c ---[ 350]---> Adder-cost: 886   maxlim: 78933   bits: 17/17
c ---[ 348]---> Adder-cost: 894   maxlim: 93141   bits: 17/17
c ---[ 346]---> Adder-cost: 818   maxlim: 37973   bits: 16/16
c ---[ 344]---> Adder-cost: 894   maxlim: 84437   bits: 17/17
c ---[ 342]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost:  778     Base: 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost:  912     Base: 2 2 2 2 2 2 2 2 2
c ---[ 257]---> BDD-cost:   12
c ---[ 256]---> BDD-cost:   12
c ---[ 255]---> BDD-cost:   14
c ---[ 254]---> BDD-cost:   11
c ---[ 253]---> BDD-cost:   15
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   14
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   12
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   12
c ---[ 246]---> BDD-cost:   10
c ---[ 245]---> BDD-cost:   15
c ---[ 244]---> BDD-cost:   17
c ---[ 243]---> BDD-cost:   12
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   11
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   17
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   12
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   10
c ---[ 230]---> BDD-cost:   14
c ---[ 229]---> BDD-cost:   17
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:   15
c ---[ 225]---> BDD-cost:   14
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   12
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   12
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   14
c ---[ 216]---> BDD-cost:   14
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   12
c ---[ 212]---> BDD-cost:   14
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   13
c ---[ 208]---> BDD-cost:   12
c ---[ 207]---> BDD-cost:   11
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   19
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   10
c ---[ 202]---> BDD-cost:   12
c ---[ 201]---> BDD-cost:   15
c ---[ 200]---> BDD-cost:   15
c ---[ 199]---> BDD-cost:   12
c ---[ 198]---> BDD-cost:   10
c ---[ 197]---> BDD-cost:   15
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   11
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   17
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   11
c ---[ 189]---> BDD-cost:   19
c ---[ 188]---> BDD-cost:   12
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   17
c ---[ 181]---> BDD-cost:   19
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   13
c ---[ 174]---> BDD-cost:   12
c ---[ 173]---> BDD-cost:   13
c ---[ 172]---> BDD-cost:   11
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   12
c ---[ 155]---> BDD-cost:   10
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   13
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   11
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   13
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   13
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   17
c ---[ 122]---> BDD-cost:   10
c ---[ 121]---> BDD-cost:   14
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   11
c ---[ 118]---> BDD-cost:   11
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   14
c ---[ 115]---> BDD-cost:   17
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:   19
c ---[ 108]---> BDD-cost:   14
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   12
c ---[ 105]---> BDD-cost:   19
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   15
c ---[ 101]---> BDD-cost:   12
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   12
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   13
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   17
c ---[  85]---> BDD-cost:   19
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   11
c ---[  79]---> BDD-cost:   15
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   11
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:   11
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   19
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:   17
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   11
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:   11
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   12
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:   15
c ---[  44]---> BDD-cost:   19
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   12
c ---[  39]---> BDD-cost:   19
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   12
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   17
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   17
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   19
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   14
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   11
c ---[  10]---> BDD-cost:   12
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   12
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  135576   364454 |   40672       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/38026          
c   -- var.elim.:  2000/38026          
c   -- var.elim.:  3000/38026          
c   -- var.elim.:  4000/38026          
c   -- var.elim.:  5000/38026          
c   -- var.elim.:  6000/38026          
c   -- var.elim.:  7000/38026          
c   -- var.elim.:  8000/38026          
c   -- var.elim.:  9000/38026          
c   -- var.elim.:  10000/38026          
c   -- var.elim.:  11000/38026          
c   -- var.elim.:  12000/38026          
c   -- var.elim.:  13000/38026          
c   -- var.elim.:  14000/38026          
c   -- var.elim.:  15000/38026          
c   -- var.elim.:  16000/38026          
c   -- var.elim.:  17000/38026          
c   -- var.elim.:  18000/38026          
c   -- var.elim.:  19000/38026          
c   -- var.elim.:  20000/38026          
c   -- var.elim.:  21000/38026          
c   -- var.elim.:  22000/38026          
c   -- var.elim.:  23000/38026          
c   -- var.elim.:  24000/38026          
c   -- var.elim.:  25000/38026          
c   -- var.elim.:  26000/38026          
c   -- var.elim.:  27000/38026          
c   -- var.elim.:  28000/38026          
c   -- var.elim.:  29000/38026          
c   -- var.elim.:  30000/38026          
c   -- var.elim.:  31000/38026          
c   -- var.elim.:  32000/38026          
c   -- var.elim.:  33000/38026          
c   -- var.elim.:  34000/38026          
c   -- var.elim.:  35000/38026          
c   -- var.elim.:  36000/38026          
c   -- var.elim.:  37000/38026          
c   -- var.elim.:  38000/38026          
c   -- var.elim.:  38026/38026          
c   -- var.elim.:  1000/19170          
c   -- var.elim.:  2000/19170          
c   -- var.elim.:  3000/19170          
c   -- var.elim.:  4000/19170          
c   -- var.elim.:  5000/19170          
c   -- var.elim.:  6000/19170          
c   -- var.elim.:  7000/19170          
c   -- var.elim.:  8000/19170          
c   -- var.elim.:  9000/19170          
c   -- var.elim.:  10000/19170          
c   -- var.elim.:  11000/19170          
c   -- var.elim.:  12000/19170          
c   -- var.elim.:  13000/19170          
c   -- var.elim.:  14000/19170          
c   -- var.elim.:  15000/19170          
c   -- var.elim.:  16000/19170          
c   -- var.elim.:  17000/19170          
c   -- var.elim.:  18000/19170          
c   -- var.elim.:  19000/19170          
c   -- var.elim.:  19170/19170          
c   -- var.elim.:  676/676          
c   -- subsuming                       
c   -- var.elim.:  1000/3211          
c   -- var.elim.:  2000/3211          
c   -- var.elim.:  3000/3211          
c   -- var.elim.:  3211/3211          
c   -- var.elim.:  1000/2531          
c   -- var.elim.:  2000/2531          
c   -- var.elim.:  2531/2531          
c   -- var.elim.:  210/210          
c   -- var.elim.:  250/250          
c   -- var.elim.:  130/130          
c   -- subsuming                       
c   -- var.elim.:  744/744          
c   -- var.elim.:  344/344          
c   -- subsuming                       
c   -- var.elim.:  163/163          
c   -- var.elim.:  80/80          
c |         0 |  116907   368985 |      --       0       --      -- |     --   | -13352/19500
c |         0 |  116907   368985 |   46762       0        0     nan |  0.000 % |
c |       102 |  116871   368855 |   51423     100      420     4.2 | 16.928 % |
c |       252 |  116871   368855 |   56565     250     1038     4.2 | 16.928 % |
c |       478 |  116871   368855 |   62222     476     1957     4.1 | 16.928 % |
c |       816 |  116824   368683 |   68416     809     3246     4.0 | 16.950 % |
c |      1322 |  116778   368500 |   75228    1312     5292     4.0 | 16.974 % |
c |      2081 |  116726   368312 |   82714    2067     8466     4.1 | 16.999 % |
c |      3221 |  116508   367506 |   90816    3190    13272     4.2 | 17.102 % |
c |      4929 |  116358   366964 |   99769    4882    20495     4.2 | 17.173 % |
c |      7491 |  115971   365590 |  109381    7423    35588     4.8 | 17.371 % |
c |     11335 |  115575   364214 |  119908   11233    65446     5.8 | 17.584 % |
c |     17101 |  115261   363085 |  131541   16970   196686    11.6 | 17.740 % |
c |     25752 |  114644   360883 |  143920   25572   294025    11.5 | 18.076 % |
c |     38726 |  114008   358715 |  157434   38494   688852    17.9 | 18.424 % |
c |     58187 |  113680   357582 |  172679   57923  1709911    29.5 | 18.601 % |
c |     87379 |  113624   357398 |  189854   87111  3213011    36.9 | 18.643 % |
c |    131170 |  113586   357265 |  208769  130890  6421780    49.1 | 18.665 % |
c ==============================================================================
c (current CPU-time: 266.559 s)
c ==============================================================================
c [1mFound solution: 5239055[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10631   maxlim: 3248188   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    186906 |  187592   621679 |   56277  186596  9593490    51.4 | 18.665 % |
c   -- subsuming                       
c   -- var.elim.:  1000/15101          
c   -- var.elim.:  2000/15101          
c   -- var.elim.:  3000/15101          
c   -- var.elim.:  4000/15101          
c   -- var.elim.:  5000/15101          
c   -- var.elim.:  6000/15101          
c   -- var.elim.:  7000/15101          
c   -- var.elim.:  8000/15101          
c   -- var.elim.:  9000/15101          
c   -- var.elim.:  10000/15101          
c   -- var.elim.:  11000/15101          
c   -- var.elim.:  12000/15101          
c   -- var.elim.:  13000/15101          
c   -- var.elim.:  14000/15101          
c   -- var.elim.:  15000/15101          
c   -- var.elim.:  15101/15101          
c   -- var.elim.:  1000/1244          
c   -- var.elim.:  1244/1244          
c   -- var.elim.:  352/352          
c   -- var.elim.:  56/56          
c   -- var.elim.:  21/21          
c   -- var.elim.:  22/22          
c   -- subsuming                       
c   -- var.elim.:  377/377          
c   -- var.elim.:  274/274          
c   -- var.elim.:  68/68          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  139/139          
c   -- var.elim.:  53/53          
c |    186906 |  186092   618524 |      --  186596       --      -- |     --   | -1500/-3145
c |    186906 |  186092   618524 |   74436  152816  5559293    36.4 | 18.665 % |
c |    187007 |  186092   618524 |   81880   15908   416669    26.2 | 14.104 % |
c |    187157 |  186092   618524 |   90068   16058   417323    26.0 | 14.104 % |
c |    187382 |  186031   618313 |   99042   16282   418278    25.7 | 14.125 % |
c |    187719 |  185985   618165 |  108920   16613   419746    25.3 | 14.149 % |
c |    188225 |  185967   618099 |  119800   17115   424695    24.8 | 14.154 % |
c |    188984 |  185967   618099 |  131780   17874   428401    24.0 | 14.154 % |
c |    190126 |  185925   617955 |  144926   19010   445165    23.4 | 14.172 % |
c |    191834 |  185925   617955 |  159418   20718   453961    21.9 | 14.172 % |
c |    194398 |  185836   617660 |  175276   23278   477085    20.5 | 14.203 % |
c |    198243 |  185748   617333 |  192712   27102   510250    18.8 | 14.229 % |
c |    204009 |  185662   617035 |  211886   32858   565177    17.2 | 14.253 % |
c |    212660 |  185662   617035 |  233074   41509  1087367    26.2 | 14.253 % |
c ==============================================================================
c (current CPU-time: 333.628 s)
c ==============================================================================
c [1mFound solution: 4764228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3723015   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    216117 |  185706   617260 |   55711   44963  1130535    25.1 | 14.253 % |
c   -- subsuming                       
c   -- var.elim.:  399/399          
c   -- var.elim.:  255/255          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  89/89          
c   -- var.elim.:  20/20          
c |    216117 |  185593   617078 |      --   44963       --      -- |     --   | -113/-174
c |    216117 |  185593   617078 |   74237   44885  1130061    25.2 | 14.253 % |
c |    216217 |  185569   616992 |   81650   44983  1130574    25.1 | 14.298 % |
c |    216367 |  185569   616992 |   89815   45133  1131584    25.1 | 14.298 % |
c |    216592 |  185569   616992 |   98796   45358  1134407    25.0 | 14.298 % |
c |    216929 |  185465   616591 |  108615   45687  1136731    24.9 | 14.330 % |
c |    217435 |  185465   616591 |  119477   46193  1140821    24.7 | 14.330 % |
c |    218194 |  185465   616591 |  131425   46952  1149851    24.5 | 14.330 % |
c |    219335 |  185379   616295 |  144500   48074  1186957    24.7 | 14.361 % |
c |    221043 |  185379   616295 |  158950   49782  1239086    24.9 | 14.361 % |
c |    223608 |  185352   616200 |  174820   52345  1281032    24.5 | 14.371 % |
c |    227452 |  185286   615963 |  192233   56186  1351373    24.1 | 14.397 % |
c |    233218 |  185259   615869 |  211426   61947  1465968    23.7 | 14.408 % |
c |    241867 |  185240   615800 |  232544   70595  1695612    24.0 | 14.413 % |
c |    254842 |  185240   615800 |  255799   83570  3129616    37.4 | 14.413 % |
c |    274303 |  185134   615429 |  281218  103025  3908537    37.9 | 14.449 % |
c |    303497 |  185134   615429 |  309340  132219  6973309    52.7 | 14.449 % |
c |    347286 |  185126   615390 |  340259  176000 14813696    84.2 | 14.452 % |
c |    412970 |  185080   615224 |  374192  241678 21904403    90.6 | 14.470 % |
c ==============================================================================
c (current CPU-time: 813.28 s)
c ==============================================================================
c [1mFound solution: 4368800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4118443   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    488189 |  185045   615186 |   55513  316892 27459386    86.7 | 14.470 % |
c   -- subsuming                       
c   -- var.elim.:  470/470          
c   -- var.elim.:  360/360          
c   -- var.elim.:  29/29          
c   -- subsuming                       
c   -- var.elim.:  111/111          
c   -- var.elim.:  42/42          
c |    488189 |  184806   614662 |      --  316892       --      -- |     --   | -239/-512
c |    488189 |  184806   614662 |   73922  307389 23390840    76.1 | 14.470 % |
c |    488290 |  184806   614662 |   81314   16951  1651549    97.4 | 14.586 % |
c |    488440 |  184806   614662 |   89446   17101  1652246    96.6 | 14.586 % |
c |    488665 |  184806   614662 |   98390   17326  1653277    95.4 | 14.586 % |
c |    489002 |  184806   614662 |  108229   17663  1654821    93.7 | 14.586 % |
c |    489508 |  184806   614662 |  119052   18169  1657266    91.2 | 14.586 % |
c |    490268 |  184781   614559 |  130940   18927  1660698    87.7 | 14.591 % |
c |    491407 |  184763   614482 |  144020   20064  1666976    83.1 | 14.596 % |
c |    493115 |  184763   614482 |  158422   21772  1674912    76.9 | 14.596 % |
c |    495677 |  184639   614042 |  174147   24326  1687517    69.4 | 14.635 % |
c |    499521 |  184596   613901 |  191517   28168  1709860    60.7 | 14.654 % |
c |    505287 |  184442   613304 |  210493   33909  1752708    51.7 | 14.706 % |
c |    513936 |  184398   613141 |  231487   42550  2016245    47.4 | 14.721 % |
c |    526910 |  184265   612667 |  254453   55510  2259716    40.7 | 14.768 % |
c |    546373 |  184242   612583 |  279863   74960  3995399    53.3 | 14.776 % |
c |    575567 |  184233   612554 |  307834  104152  6120154    58.8 | 14.781 % |
c |    619356 |  184233   612554 |  338618  147941 11166170    75.5 | 14.781 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 X2_bit_1 -X2_bit0 -X2_bit1 X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 X6_bit0 X6_bit1 X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 X7_bit0 X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 X8_bit_6 X8_bit_5 X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 X9_bit_6 X9_bit_5 -X9_bit_4 X9_bit_3 X9_bit_2 X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 X10_bit_4 -X10_bit_3 X10_bit_2 X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 X12_bit_6 -X12_bit_5 X12_bit_4 -X12_bit_3 X12_bit_2 -X12_bit_1 X12_bit0 X12_bit1 X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 X14_bit_2 -X14_bit_1 -X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 X16_bit_6 X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 -X17_bit_6 X17_bit_5 -X17_bit_4 -X17_bit_3 X17_bit_2 -X17_bit_1 X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 -X19_bit_5 X19_bit_4 -X19_bit_3 X19_bit_2 X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 X20_bit_6 X20_bit_5 X20_bit_4 -X20_bit_3 -X20_bit_2 X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 X20_bit3 X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 X21_bit_6 -X21_bit_5 X21_bit_4 X21_bit_3 -X21_bit_2 -X21_bit_1 X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X23_bit_7 X23_bit_6 X23_bit_5 X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 X23_bit0 X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 X24_bit_5 X24_bit_4 -X24_bit_3 X24_bit_2 -X24_bit_1 -X24_bit0 X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 X25_bit_5 X25_bit_4 X25_bit_3 X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 X27_bit_6 X27_bit_5 X27_bit_4 -X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 X27_bit2 X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 X29_bit_5 X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 -X34_bit_5 -X34_bit_4 -X34_bit_3 X34_bit_2 X34_bit_1 X34_bit0 X34_bit1 X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 X36_bit_5 -X36_bit_4 X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 X37_bit2 X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 X38_bit1 X38_bit2 X38_bit3 X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 X40_bit_6 X40_bit_5 X40_bit_4 X40_bit_3 X40_bit_2 X40_bit_1 -X40_bit0 -X40_bit1 X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 X42_bit_5 -X42_bit_4 X42_bit_3 X42_bit_2 -X42_bit_1 -X42_bit0 X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 X44_bit_5 X44_bit_4 X44_bit_3 X44_bit_2 X44_bit_1 X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 X47_bit_5 X47_bit_4 X47_bit_3 X47_bit_2 X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 X47_bit3 X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 X48_bit_5 X48_bit_4 X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 X49_bit_1 X49_bit0 X49_bit1 X49_bit2 X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 X51_bit_6 X51_bit_5 X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 X52_bit_6 X52_bit_5 X52_bit_4 X52_bit_3 X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 X54_bit_3 -X54_bit_2 X54_bit_1 -X54_bit0 -X54_bit1 X54_bit2 X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 X55_bit_7 X55_bit_6 X55_bit_5 X55_bit_4 X55_bit_3 X55_bit_2 -X55_bit_1 X55_bit0 X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 X57_bit_5 X57_bit_4 X57_bit_3 -X57_bit_2 X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 X59_bit_6 X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 -X60_bit_6 X60_bit_5 X60_bit_4 X60_bit_3 X60_bit_2 -X60_bit_1 -X60_bit0 X60_bit1 X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 X61_bit_6 X61_bit_5 X61_bit_4 X61_bit_3 X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 X62_bit_3 X62_bit_2 X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 X63_bit_6 X63_bit_5 X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 X66_bit_6 X66_bit_5 X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 X68_bit_5 X68_bit_4 X68_bit_3 X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 X70_bit_7 X70_bit_6 X70_bit_5 X70_bit_4 -X70_bit_3 X70_bit_2 X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 X74_bit_6 -X74_bit_5 X74_bit_4 X74_bit_3 X74_bit_2 -X74_bit_1 X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 X75_bit_6 X75_bit_5 X75_bit_4 -X75_bit_3 X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 X77_bit_3 X77_bit_2 X77_bit_1 X77_bit0 -X77_bit1 X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 -X79_bit_6 X79_bit_5 -X79_bit_4 X79_bit_3 X79_bit_2 X79_bit_1 -X79_bit0 -X79_bit1 X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 X80_bit_7 -X80_bit_6 X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 X80_bit0 X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 X81_bit_4 X81_bit_3 -X81_bit_2 X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 X82_bit_4 -X82_bit_3 X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 X83_bit_5 X83_bit_4 X83_bit_3 X83_bit_2 X83_bit_1 X83_bit0 X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 X84_bit_5 -X84_bit_4 X84_bit_3 X84_bit_2 X84_bit_1 X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 -X89_bit_6 -X89_bit_5 -X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 X94_bit_6 X94_bit_5 X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 X95_bit_6 -X95_bit_5 -X95_bit_4 X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 X98_bit_6 X98_bit_5 -X98_bit_4 X98_bit_3 X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 X99_bit_6 X99_bit_5 -X99_bit_4 X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 X102_bit_6 X102_bit_5 -X102_bit_4 X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 X104_bit_6 X104_bit_5 X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 X105_bit_2 X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 X106_bit_6 X106_bit_5 X106_bit_4 X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 X110_bit_7 X110_bit_6 X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 X113_bit_3 X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 X118_bit_6 -X118_bit_5 -X118_bit_4 X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 X120_bit_6 -X120_bit_5 -X120_bit_4 X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 X124_bit_6 -X124_bit_5 X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 X126_bit_6 -X126_bit_5 -X126_bit_4 X126_bit_3 X126_bit_2 X126_bit_1 X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 X127_bit_3 -X127_bit_2 -X127_bit_1 X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 X131_bit_3 X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 -X132_bit_6 -X132_bit_5 X132_bit_4 X132_bit_3 X132_bit_2 X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 X134_bit_4 X134_bit_3 -X134_bit_2 X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 X136_bit_2 X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 X137_bit_6 X137_bit_5 X137_bit_4 -X137_bit_3 X137_bit_2 X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 X138_bit_6 -X138_bit_5 X138_bit_4 X138_bit_3 X138_bit_2 X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 X141_bit_6 -X141_bit_5 X141_bit_4 X141_bit_3 X141_bit_2 -X141_bit_1 X141_bit0 X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 X142_bit_3 X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 X145_bit_6 X145_bit_5 -X145_bit_4 X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 X146_bit_5 -X146_bit_4 X146_bit_3 X146_bit_2 -X146_bit_1 X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 X147_bit_5 X147_bit_4 -X147_bit_3 X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 X149_bit_5 X149_bit_4 X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 -X150_bit_5 X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 X152_bit0 -X152_bit1 X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 X153_bit_7 -X153_bit_6 X153_bit_5 -X153_bit_4 X153_bit_3 X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 X154_bit_7 X154_bit_6 X154_bit_5 X154_bit_4 X154_bit_3 X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 X156_bit_5 X156_bit_4 X156_bit_3 X156_bit_2 X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 X157_bit_2 X157_bit_1 -X157_bit0 X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 X158_bit_5 -X158_bit_4 X158_bit_3 X158_bit_2 -X158_bit_1 -X158_bit0 X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 X159_bit_5 X159_bit_4 X159_bit_3 X159_bit_2 X159_bit_1 X159_bit0 X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 X160_bit_1 X160_bit0 X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 X165_bit_5 -X165_bit_4 X165_bit_3 X165_bit_2 X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 X166_bit_5 X166_bit_4 -X166_bit_3 -X166_bit_2 X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 X167_bit_2 X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 X168_bit_4 -X168_bit_3 X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 X169_bit_6 -X169_bit_5 X169_bit_4 X169_bit_3 X169_bit_2 X169_bit_1 X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 X181_bit_1 X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 X184_bit_5 X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 X189_bit_6 -X189_bit_5 X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 X190_bit_6 -X190_bit_5 X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 -X191_bit_5 X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 X192_bit_6 -X192_bit_5 X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 X195_bit_7 -X195_bit_6 -X195_bit_5 X195_bit_4 X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 X197_bit_7 -X197_bit_6 -X197_bit_5 -X197_bit_4 -X197_bit_3 -X197_bit_2 X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 -X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 -X208_bit_6 -X208_bit_5 -X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 X212_bit_4 X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 X216_bit_6 X216_bit_5 X216_bit_4 X216_bit_3 X216_bit_2 X216_bit_1 X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 X218_bit_7 X218_bit_6 X218_bit_5 X218_bit_4 X218_bit_3 X218_bit_2 X218_bit_1 -X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 X220_bit_5 X220_bit_4 X220_bit_3 X220_bit_2 X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 -X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 X221_bit_1 X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 X222_bit_7 -X222_bit_6 X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 X223_bit_7 X223_bit_6 X223_bit_5 X223_bit_4 X223_bit_3 -X223_bit_2 X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 X224_bit_7 X224_bit_6 X224_bit_5 X224_bit_4 X224_bit_3 X224_bit_2 X224_bit_1 X224_bit0 X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 X225_bit_4 X225_bit_3 X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 X226_bit_6 X226_bit_5 X226_bit_4 -X226_bit_3 X226_bit_2 -X226_bit_1 X226_bit0 -X226_bit1 X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 X227_bit_7 X227_bit_6 -X227_bit_5 X227_bit_4 X227_bit_3 -X227_bit_2 -X227_bit_1 X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 X228_bit_5 -X228_bit_4 X228_bit_3 X228_bit_2 X228_bit_1 -X228_bit0 -X228_bit1 X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 -X230_bit_5 X230_bit_4 X230_bit_3 -X230_bit_2 X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 X231_bit_7 X231_bit_6 X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 X231_bit_1 -X231_bit0 -X231_bit1 X231_bit2 X231_bit3 X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 X232_bit_7 X232_bit_6 X232_bit_5 X232_bit_4 X232_bit_3 -X232_bit_2 X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 -X233_bit_6 X233_bit_5 X233_bit_4 X233_bit_3 X233_bit_2 X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 X234_bit_7 -X234_bit_6 -X234_bit_5 X234_bit_4 -X234_bit_3 X234_bit_2 -X234_bit_1 X234_bit0 -X234_bit1 X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 X235_bit_6 X235_bit_5 X235_bit_4 X235_bit_3 -X235_bit_2 X235_bit_1 X235_bit0 X235_bit1 -X235_bit2 X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 X236_bit_7 -X236_bit_6 X236_bit_5 -X236_bit_4 X236_bit_3 -X236_bit_2 X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 X238_bit_7 X238_bit_6 X238_bit_5 X238_bit_4 X238_bit_3 X238_bit_2 -X238_bit_1 X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 X239_bit_4 X239_bit_3 -X239_bit_2 -X239_bit_1 X239_bit0 X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 X240_bit_7 X240_bit_6 -X240_bit_5 X240_bit_4 X240_bit_3 X240_bit_2 X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 X242_bit_5 X242_bit_4 -X242_bit_3 X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 -X244_bit_6 X244_bit_5 X244_bit_4 -X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 X247_bit_7 X247_bit_6 X247_bit_5 X247_bit_4 X247_bit_3 X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 X249_bit_7 X249_bit_6 -X249_bit_5 X249_bit_4 X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 -X250_bit_3 -X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 -X251_bit_4 -X251_bit_3 -X251_bit_2 -X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 X252_bit_7 X252_bit_6 -X252_bit_5 -X252_bit_4 X252_bit_3 -X252_bit_2 -X252_bit_1 X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 X253_bit_6 X253_bit_5 -X253_bit_4 X253_bit_3 X253_bit_2 -X253_bit_1 X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 X254_bit_6 X254_bit_5 X254_bit_4 -X254_bit_3 X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 -X255_bit_6 -X255_bit_5 -X255_bit_4 -X255_bit_3 -X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -X256_bit_7 -X256_bit_6 X256_bit_5 X256_bit_4 X256_bit_3 X256_bit_2 X256_bit_1 -X256_bit0 X256_bit1 X256_bit2 -X256_bit3 -X256_bit4 -X256_bit5 -X256_bit6 -X256_bit7 -X256_bit8 -X256_bit9 -X256_bit10 -X256_bit11 -X256_bit12 X257_bit_7 X257_bit_6 X257_bit_5 -X257_bit_4 X257_bit_3 X257_bit_2 -X257_bit_1 -X257_bit0 -X257_bit1 -X257_bit2 -X257_bit3 -X257_bit4 -X257_bit5 -X257_bit6 -X257_bit7 -X257_bit8 -X257_bit9 -X257_bit10 -X257_bit11 -X257_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 -Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 -Y11_bit0 Y12_bit0 -Y13_bit0 Y14_bit0 -Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 Y25_bit0 -Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 -Y30_bit0 Y31_bit0 -Y32_bit0 Y33_bit0 Y34_bit0 -Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 -Y41_bit0 Y42_bit0 Y43_bit0 Y44_bit0 -Y45_bit0 -Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 Y57_bit0 Y58_bit0 Y59_bit0 Y60_bit0 Y61_bit0 Y62_bit0 Y63_bit0 -Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 Y69_bit0 Y70_bit0 -Y71_bit0 Y72_bit0 -Y73_bit0 Y74_bit0 Y75_bit0 -Y76_bit0 Y77_bit0 -Y78_bit0 Y79_bit0 Y80_bit0 Y81_bit0 Y82_bit0 Y83_bit0 Y84_bit0 -Y85_bit0 -Y86_bit0 -Y87_bit0 Y88_bit0 -Y89_bit0 -#### 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.83 0.94 0.94 2/54 1262
Raw data (stat): 1262 (runsolver) R 1261 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544498645 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.86 0.94 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7639 0 0 0 976 22 0 0 25 0 1 0 544498645 32673792 6628 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7977 6628 603 41 0 7936 0
vsize: 31908
[startup+20.001 s]
Raw data (loadavg): 0.88 0.94 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7651 0 0 0 1975 23 0 0 25 0 1 0 544498645 32673792 6640 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7977 6640 603 41 0 7936 0
vsize: 31908
[startup+30.0021 s]
Raw data (loadavg): 0.90 0.94 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7670 0 0 0 2975 23 0 0 25 0 1 0 544498645 32673792 6659 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7977 6659 603 41 0 7936 0
vsize: 31908
[startup+40.0021 s]
Raw data (loadavg): 0.91 0.94 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7723 0 0 0 3975 23 0 0 25 0 1 0 544498645 32980992 6712 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8052 6712 603 41 0 8011 0
vsize: 32208
[startup+50.0032 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7800 0 0 0 4975 24 0 0 25 0 1 0 544498645 33251328 6789 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8118 6789 603 41 0 8077 0
vsize: 32472
[startup+60.0032 s]
Raw data (loadavg): 0.94 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 7932 0 0 0 5975 24 0 0 25 0 1 0 544498645 33787904 6921 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8249 6921 603 41 0 8208 0
vsize: 32996
[startup+70.003 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 8634 0 0 0 6972 27 0 0 25 0 1 0 544498645 36827136 7623 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8991 7623 603 41 0 8950 0
vsize: 35964
[startup+80.0033 s]
Raw data (loadavg): 0.95 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 9275 0 0 0 7971 29 0 0 25 0 1 0 544498645 39358464 8264 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9609 8264 603 41 0 9568 0
vsize: 38436
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 9846 0 0 0 8969 31 0 0 25 0 1 0 544498645 41639936 8835 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10166 8835 603 41 0 10125 0
vsize: 40664
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 10448 0 0 0 9966 33 0 0 25 0 1 0 544498645 44302336 9437 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10816 9437 603 41 0 10775 0
vsize: 43264
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 11137 0 0 0 10964 36 0 0 25 0 1 0 544498645 47099904 10126 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11499 10126 603 41 0 11458 0
vsize: 45996
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 11599 0 0 0 11963 37 0 0 25 0 1 0 544498645 48951296 10588 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11951 10588 603 41 0 11910 0
vsize: 47804
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 12361 0 0 0 12961 40 0 0 25 0 1 0 544498645 52146176 11350 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12731 11350 603 41 0 12690 0
vsize: 50924
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 12935 0 0 0 13959 41 0 0 25 0 1 0 544498645 54411264 11924 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13284 11924 603 41 0 13243 0
vsize: 53136
[startup+150.007 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 13463 0 0 0 14958 42 0 0 25 0 1 0 544498645 56541184 12452 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13804 12453 603 41 0 13763 0
vsize: 55216
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 14170 0 0 0 15955 46 0 0 25 0 1 0 544498645 59334656 13159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14486 13159 603 41 0 14445 0
vsize: 57944
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 14747 0 0 0 16953 48 0 0 25 0 1 0 544498645 61702144 13736 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15064 13736 603 41 0 15023 0
vsize: 60256
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 15348 0 0 0 17951 50 0 0 25 0 1 0 544498645 64745472 14337 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15807 14337 603 41 0 15766 0
vsize: 63228
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 15634 0 0 0 18950 52 0 0 25 0 1 0 544498645 65810432 14623 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16067 14623 603 41 0 16026 0
vsize: 64268
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 16110 0 0 0 19948 54 0 0 25 0 1 0 544498645 67813376 15099 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16556 15099 603 41 0 16515 0
vsize: 66224
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 16708 0 0 0 20946 56 0 0 25 0 1 0 544498645 70197248 15697 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17138 15697 603 41 0 17097 0
vsize: 68552
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 17214 0 0 0 21944 58 0 0 25 0 1 0 544498645 72179712 16203 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17622 16203 603 41 0 17581 0
vsize: 70488
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 17699 0 0 0 22942 60 0 0 25 0 1 0 544498645 74186752 16688 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18112 16688 603 41 0 18071 0
vsize: 72448
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 18079 0 0 0 23941 61 0 0 25 0 1 0 544498645 75792384 17068 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18504 17068 603 41 0 18463 0
vsize: 74016
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 18586 0 0 0 24940 63 0 0 25 0 1 0 544498645 77783040 17575 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18990 17575 603 41 0 18949 0
vsize: 75960
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 19084 0 0 0 25938 65 0 0 25 0 1 0 544498645 79773696 18073 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19476 18073 603 41 0 19435 0
vsize: 77904
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 28167 0 0 0 26917 86 0 0 25 0 1 0 544498645 106815488 24549 4294967295 134512640 134672761 3221224544 3221223184 134622879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26078 24549 603 41 0 26037 0
vsize: 104312
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29221 0 0 0 27914 89 0 0 25 0 1 0 544498645 105492480 24249 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25755 24249 603 41 0 25714 0
vsize: 103020
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29221 0 0 0 28914 89 0 0 25 0 1 0 544498645 105492480 24249 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25755 24249 603 41 0 25714 0
vsize: 103020
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29253 0 0 0 29914 90 0 0 25 0 1 0 544498645 105754624 24281 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 24281 603 41 0 25778 0
vsize: 103276
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29254 0 0 0 30914 90 0 0 25 0 1 0 544498645 105754624 24282 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 24282 603 41 0 25778 0
vsize: 103276
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29255 0 0 0 31914 90 0 0 25 0 1 0 544498645 105754624 24283 4294967295 134512640 134672761 3221224544 3221223728 134615843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 24283 603 41 0 25778 0
vsize: 103276
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 29259 0 0 0 32914 91 0 0 25 0 1 0 544498645 105754624 24287 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25819 24287 603 41 0 25778 0
vsize: 103276
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 33907 97 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 34907 98 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 35907 98 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 36907 99 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 37906 99 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 38906 99 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 39906 100 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 40906 100 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 41905 101 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 42905 101 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 43905 101 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 44905 101 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223584 134612883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 45905 102 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 46905 102 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31437 0 0 0 47905 102 0 0 25 0 1 0 544498645 105799680 24331 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25830 24331 603 41 0 25789 0
vsize: 103320
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31555 0 0 0 48904 103 0 0 25 0 1 0 544498645 106328064 24449 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25959 24449 603 41 0 25918 0
vsize: 103836
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1262
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 31934 0 0 0 49903 104 0 0 25 0 1 0 544498645 107921408 24828 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26348 24828 603 41 0 26307 0
vsize: 105392
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 32990 0 0 0 50896 111 0 0 25 0 1 0 544498645 112287744 25884 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27414 25884 603 41 0 27373 0
vsize: 109656
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 34329 0 0 0 51893 114 0 0 25 0 1 0 544498645 117706752 27223 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28737 27223 603 41 0 28696 0
vsize: 114948
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 35589 0 0 0 52891 117 0 0 25 0 1 0 544498645 122880000 28483 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30000 28483 603 41 0 29959 0
vsize: 120000
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 36909 0 0 0 53889 119 0 0 25 0 1 0 544498645 128294912 29803 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31322 29803 603 41 0 31281 0
vsize: 125288
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 37678 0 0 0 54887 121 0 0 25 0 1 0 544498645 131452928 30572 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32093 30572 603 41 0 32052 0
vsize: 128372
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 38142 0 0 0 55885 123 0 0 25 0 1 0 544498645 133300224 31036 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32544 31036 603 41 0 32503 0
vsize: 130176
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1317
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 38588 0 0 0 56884 124 0 0 25 0 1 0 544498645 135147520 31482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32995 31482 603 41 0 32954 0
vsize: 131980
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 39002 0 0 0 57883 125 0 0 25 0 1 0 544498645 136859648 31896 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33413 31896 603 41 0 33372 0
vsize: 133652
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 39248 0 0 0 58883 126 0 0 25 0 1 0 544498645 137797632 32142 4294967295 134512640 134672761 3221224544 3221223712 134564752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33642 32142 603 41 0 33601 0
vsize: 134568
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 39790 0 0 0 59881 128 0 0 25 0 1 0 544498645 140054528 32684 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34193 32684 603 41 0 34152 0
vsize: 136772
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 40823 0 0 0 60879 130 0 0 25 0 1 0 544498645 144150528 33717 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35193 33717 603 41 0 35152 0
vsize: 140772
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 41982 0 0 0 61876 134 0 0 25 0 1 0 544498645 149008384 34876 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36379 34876 603 41 0 36338 0
vsize: 145516
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 42867 0 0 0 62874 135 0 0 25 0 1 0 544498645 152604672 35761 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37257 35761 603 41 0 37216 0
vsize: 149028
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 43376 0 0 0 63873 137 0 0 25 0 1 0 544498645 154636288 36270 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37753 36270 603 41 0 37712 0
vsize: 151012
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 43853 0 0 0 64872 138 0 0 25 0 1 0 544498645 156639232 36747 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38242 36747 603 41 0 38201 0
vsize: 152968
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 44316 0 0 0 65871 140 0 0 25 0 1 0 544498645 158498816 37210 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38696 37210 603 41 0 38655 0
vsize: 154784
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 44796 0 0 0 66869 142 0 0 25 0 1 0 544498645 160481280 37690 4294967295 134512640 134672761 3221224544 3221223548 134619845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39180 37690 603 41 0 39139 0
vsize: 156720
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 45228 0 0 0 67868 143 0 0 25 0 1 0 544498645 162254848 38122 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39613 38122 603 41 0 39572 0
vsize: 158452
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 45464 0 0 0 68867 143 0 0 25 0 1 0 544498645 163188736 38358 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39841 38358 603 41 0 39800 0
vsize: 159364
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 45769 0 0 0 69866 144 0 0 25 0 1 0 544498645 164384768 38663 4294967295 134512640 134672761 3221224544 3221223728 134615469 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40133 38663 603 41 0 40092 0
vsize: 160532
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 46360 0 0 0 70865 146 0 0 25 0 1 0 544498645 166768640 39254 4294967295 134512640 134672761 3221224544 3221223796 134618481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40715 39254 603 41 0 40674 0
vsize: 162860
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 47053 0 0 0 71863 148 0 0 25 0 1 0 544498645 170622976 39947 4294967295 134512640 134672761 3221224544 3221223680 134614551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41656 39947 603 41 0 41615 0
vsize: 166624
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 47516 0 0 0 72862 150 0 0 25 0 1 0 544498645 172638208 40410 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42148 40410 603 41 0 42107 0
vsize: 168592
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 47929 0 0 0 73860 151 0 0 25 0 1 0 544498645 174276608 40823 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42548 40823 603 41 0 42507 0
vsize: 170192
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 48362 0 0 0 74860 152 0 0 25 0 1 0 544498645 176017408 41256 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42973 41256 603 41 0 42932 0
vsize: 171892
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 48728 0 0 0 75859 153 0 0 25 0 1 0 544498645 177610752 41622 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43362 41622 603 41 0 43321 0
vsize: 173448
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 49057 0 0 0 76859 154 0 0 25 0 1 0 544498645 178880512 41951 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43672 41951 603 41 0 43631 0
vsize: 174688
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 49398 0 0 0 77857 155 0 0 25 0 1 0 544498645 180400128 42292 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44043 42292 603 41 0 44002 0
vsize: 176172
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 49897 0 0 0 78856 157 0 0 25 0 1 0 544498645 182407168 42791 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44533 42791 603 41 0 44492 0
vsize: 178132
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 50659 0 0 0 79854 159 0 0 25 0 1 0 544498645 185462784 43553 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45279 43553 603 41 0 45238 0
vsize: 181116
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 51449 0 0 0 80851 162 0 0 25 0 1 0 544498645 188796928 44343 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46093 44343 603 41 0 46052 0
vsize: 184372
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54624 0 0 0 81843 170 0 0 25 0 1 0 544498645 192753664 45136 4294967295 134512640 134672761 3221224544 3221223488 134645588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47059 45136 603 41 0 47018 0
vsize: 188236
[startup+830.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 82843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 83843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 84843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223696 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1319
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 85843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 86843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 87843 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 88844 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 89844 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 90844 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 91844 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 92845 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 93846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 94846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 95846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 96846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 97846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223488 1075351051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 98846 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223584 134612835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 99847 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54751 0 0 0 100847 170 0 0 25 0 1 0 544498645 191705088 44962 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44962 603 41 0 46762 0
vsize: 187212
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 101847 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 102847 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 103847 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 104848 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 105848 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 106848 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 107848 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 108848 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 109849 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 110849 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 111849 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 112849 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 113849 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 114850 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 115850 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 116850 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 117850 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 118850 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 1321
Raw data (stat): 1262 (minisat+) R 1261 26298 26297 0 -1 0 54752 0 0 0 119851 170 0 0 25 0 1 0 544498645 191705088 44963 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46803 44963 603 41 0 46762 0
vsize: 187212
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 1321
Raw data (stat): 1262 (minisat+) Z 1261 26298 26297 0 -1 12 54753 0 0 0 119852 179 0 0 25 0 1 0 544498645 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.32
CPU user time (s): 1198.52
CPU system time (s): 1.79473
CPU usage (%): 100.014
Max. virtual memory (Kb): 188236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####