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-ran10x26.opb
MD5SUM	f8a5d8e99e0f063cb10208b1e5f7bf38
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1277437
Optimality of the best value was proved	NO
Number of terms in the objective function	5460
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	1567797422
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	1567797422
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	1189.04
Number of variables	5460
Total number of constraints	296
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	296
Minimum length of a constraint	21
Maximum length of a constraint	520
Trace number 17672

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        431472 kB
Buffers:         34956 kB
Cached:         545928 kB
SwapCached:        176 kB
Active:         236224 kB
Inactive:       347452 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        431220 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13928 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:34:03 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 19251 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 332 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 330]---> Adder-cost: 538   maxlim: 57062   bits: 16/16
c ---[ 328]---> Adder-cost: 536   maxlim: 52326   bits: 16/16
c ---[ 326]---> Adder-cost: 536   maxlim: 52582   bits: 16/16
c ---[ 324]---> Adder-cost: 536   maxlim: 53094   bits: 16/16
c ---[ 322]---> Adder-cost: 536   maxlim: 53606   bits: 16/16
c ---[ 320]---> Adder-cost: 538   maxlim: 58982   bits: 16/16
c ---[ 318]---> Adder-cost: 522   maxlim: 38502   bits: 16/16
c ---[ 316]---> Adder-cost: 538   maxlim: 57574   bits: 16/16
c ---[ 314]---> Adder-cost: 536   maxlim: 53990   bits: 16/16
c ---[ 312]---> Adder-cost: 538   maxlim: 56806   bits: 16/16
c ---[ 310]---> Adder-cost: 216   maxlim: 36214   bits: 16/16
c ---[ 308]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Adder-cost: 216   maxlim: 35190   bits: 16/16
c ---[ 304]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Adder-cost: 216   maxlim: 35446   bits: 16/16
c ---[ 296]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Adder-cost: 216   maxlim: 35062   bits: 16/16
c ---[ 288]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 280]---> Sorter-cost: 2404     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 2090     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Adder-cost: 216   maxlim: 36470   bits: 16/16
c ---[ 266]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1874     Base: 2 2 2 2 2 2 2 2 2
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   12
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   17
c ---[ 255]---> BDD-cost:   11
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   11
c ---[ 252]---> BDD-cost:   17
c ---[ 251]---> BDD-cost:   12
c ---[ 250]---> BDD-cost:   14
c ---[ 249]---> BDD-cost:   14
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   16
c ---[ 245]---> BDD-cost:   11
c ---[ 244]---> BDD-cost:   12
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   17
c ---[ 240]---> BDD-cost:   17
c ---[ 239]---> BDD-cost:   11
c ---[ 238]---> BDD-cost:   12
c ---[ 237]---> BDD-cost:   17
c ---[ 236]---> BDD-cost:   10
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   12
c ---[ 233]---> BDD-cost:   12
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   12
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   17
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   12
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   12
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   12
c ---[ 221]---> BDD-cost:   14
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:   15
c ---[ 218]---> BDD-cost:   17
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   12
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   17
c ---[ 212]---> BDD-cost:   17
c ---[ 211]---> BDD-cost:   19
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   17
c ---[ 207]---> BDD-cost:   10
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   12
c ---[ 204]---> BDD-cost:   16
c ---[ 203]---> BDD-cost:   15
c ---[ 202]---> BDD-cost:   10
c ---[ 201]---> BDD-cost:   12
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   19
c ---[ 198]---> BDD-cost:   11
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   12
c ---[ 193]---> BDD-cost:   15
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   12
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   12
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   13
c ---[ 184]---> BDD-cost:   15
c ---[ 183]---> BDD-cost:   15
c ---[ 182]---> BDD-cost:   11
c ---[ 181]---> BDD-cost:   12
c ---[ 180]---> BDD-cost:   12
c ---[ 179]---> BDD-cost:   15
c ---[ 178]---> BDD-cost:   10
c ---[ 177]---> BDD-cost:   12
c ---[ 176]---> BDD-cost:   12
c ---[ 175]---> BDD-cost:   15
c ---[ 174]---> BDD-cost:   15
c ---[ 173]---> BDD-cost:   12
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   15
c ---[ 170]---> BDD-cost:   11
c ---[ 169]---> BDD-cost:   16
c ---[ 168]---> BDD-cost:   12
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:   17
c ---[ 165]---> BDD-cost:   12
c ---[ 164]---> BDD-cost:   14
c ---[ 163]---> BDD-cost:   14
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   11
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   15
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   17
c ---[ 154]---> BDD-cost:   18
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:   12
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   12
c ---[ 148]---> BDD-cost:   12
c ---[ 147]---> BDD-cost:   14
c ---[ 146]---> BDD-cost:   12
c ---[ 145]---> BDD-cost:   16
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   12
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:   11
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   11
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   12
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   14
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   16
c ---[ 125]---> BDD-cost:   16
c ---[ 124]---> BDD-cost:   19
c ---[ 123]---> BDD-cost:   11
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   16
c ---[ 120]---> BDD-cost:   10
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   16
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   11
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:   11
c ---[ 110]---> BDD-cost:   12
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   12
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   14
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   17
c ---[ 102]---> BDD-cost:   12
c ---[ 101]---> BDD-cost:   11
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   13
c ---[  97]---> BDD-cost:   17
c ---[  96]---> BDD-cost:   16
c ---[  95]---> BDD-cost:   11
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   15
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   19
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   17
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:   14
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   11
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   13
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   17
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   12
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   17
c ---[  53]---> BDD-cost:   12
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   12
c ---[  49]---> BDD-cost:   14
c ---[  48]---> BDD-cost:   14
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   17
c ---[  39]---> BDD-cost:   17
c ---[  38]---> BDD-cost:   11
c ---[  37]---> BDD-cost:   12
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   12
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   17
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   12
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   12
c ---[  24]---> BDD-cost:   11
c ---[  23]---> BDD-cost:   17
c ---[  22]---> BDD-cost:   12
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   12
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   17
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   12
c ---[   0]---> BDD-cost:   13
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  156471   425391 |   46941       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/43792          
c   -- var.elim.:  2000/43792          
c   -- var.elim.:  3000/43792          
c   -- var.elim.:  4000/43792          
c   -- var.elim.:  5000/43792          
c   -- var.elim.:  6000/43792          
c   -- var.elim.:  7000/43792          
c   -- var.elim.:  8000/43792          
c   -- var.elim.:  9000/43792          
c   -- var.elim.:  10000/43792          
c   -- var.elim.:  11000/43792          
c   -- var.elim.:  12000/43792          
c   -- var.elim.:  13000/43792          
c   -- var.elim.:  14000/43792          
c   -- var.elim.:  15000/43792          
c   -- var.elim.:  16000/43792          
c   -- var.elim.:  17000/43792          
c   -- var.elim.:  18000/43792          
c   -- var.elim.:  19000/43792          
c   -- var.elim.:  20000/43792          
c   -- var.elim.:  21000/43792          
c   -- var.elim.:  22000/43792          
c   -- var.elim.:  23000/43792          
c   -- var.elim.:  24000/43792          
c   -- var.elim.:  25000/43792          
c   -- var.elim.:  26000/43792          
c   -- var.elim.:  27000/43792          
c   -- var.elim.:  28000/43792          
c   -- var.elim.:  29000/43792          
c   -- var.elim.:  30000/43792          
c   -- var.elim.:  31000/43792          
c   -- var.elim.:  32000/43792          
c   -- var.elim.:  33000/43792          
c   -- var.elim.:  34000/43792          
c   -- var.elim.:  35000/43792          
c   -- var.elim.:  36000/43792          
c   -- var.elim.:  37000/43792          
c   -- var.elim.:  38000/43792          
c   -- var.elim.:  39000/43792          
c   -- var.elim.:  40000/43792          
c   -- var.elim.:  41000/43792          
c   -- var.elim.:  42000/43792          
c   -- var.elim.:  43000/43792          
c   -- var.elim.:  43792/43792          
c   -- var.elim.:  1000/21980          
c   -- var.elim.:  2000/21980          
c   -- var.elim.:  3000/21980          
c   -- var.elim.:  4000/21980          
c   -- var.elim.:  5000/21980          
c   -- var.elim.:  6000/21980          
c   -- var.elim.:  7000/21980          
c   -- var.elim.:  8000/21980          
c   -- var.elim.:  9000/21980          
c   -- var.elim.:  10000/21980          
c   -- var.elim.:  11000/21980          
c   -- var.elim.:  12000/21980          
c   -- var.elim.:  13000/21980          
c   -- var.elim.:  14000/21980          
c   -- var.elim.:  15000/21980          
c   -- var.elim.:  16000/21980          
c   -- var.elim.:  17000/21980          
c   -- var.elim.:  18000/21980          
c   -- var.elim.:  19000/21980          
c   -- var.elim.:  20000/21980          
c   -- var.elim.:  21000/21980          
c   -- var.elim.:  21980/21980          
c   -- var.elim.:  324/324          
c   -- subsuming                       
c   -- var.elim.:  1000/3379          
c   -- var.elim.:  2000/3379          
c   -- var.elim.:  3000/3379          
c   -- var.elim.:  3379/3379          
c   -- var.elim.:  1000/2922          
c   -- var.elim.:  2000/2922          
c   -- var.elim.:  2922/2922          
c   -- var.elim.:  12/12          
c   -- subsuming                       
c   -- var.elim.:  408/408          
c   -- var.elim.:  204/204          
c   -- subsuming                       
c   -- var.elim.:  40/40          
c   -- var.elim.:  41/41          
c |         0 |  138739   436921 |      --       0       --      -- |     --   | -13256/26852
c |         0 |  138739   436921 |   55495       0        0     nan |  0.000 % |
c |       100 |  138712   436828 |   61033      99      576     5.8 | 13.802 % |
c |       250 |  138544   436229 |   67055     241     1350     5.6 | 13.871 % |
c |       475 |  138544   436229 |   73760     466     2539     5.4 | 13.871 % |
c |       812 |  138240   435206 |   80958     774     4155     5.4 | 13.996 % |
c |      1318 |  137979   434327 |   88886    1273     7220     5.7 | 14.121 % |
c |      2080 |  137831   433811 |   97670    2015    11550     5.7 | 14.184 % |
c |      3220 |  137569   432866 |  107233    3119    17155     5.5 | 14.293 % |
c |      4928 |  137251   431791 |  117683    4812    27217     5.7 | 14.440 % |
c |      7492 |  136484   429248 |  128728    7299    42443     5.8 | 14.778 % |
c |     11338 |  136393   428875 |  141507   11140    65711     5.9 | 14.816 % |
c |     17104 |  135760   426598 |  154935   16873   102203     6.1 | 15.088 % |
c |     25753 |  134570   422635 |  168935   25466   162768     6.4 | 15.661 % |
c |     38727 |  132610   416311 |  183122   38243   254802     6.7 | 16.722 % |
c |     58188 |  130560   409521 |  198320   57567   490866     8.5 | 17.774 % |
c |     87381 |  128821   403994 |  215246   86625  1340393    15.5 | 18.719 % |
c ==============================================================================
c (current CPU-time: 149.377 s)
c ==============================================================================
c [1mFound solution: 5453858[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 11067   maxlim: 3257484   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    103369 |  206125   680148 |   61837  102576  2107849    20.5 | 18.719 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16714          
c   -- var.elim.:  2000/16714          
c   -- var.elim.:  3000/16714          
c   -- var.elim.:  4000/16714          
c   -- var.elim.:  5000/16714          
c   -- var.elim.:  6000/16714          
c   -- var.elim.:  7000/16714          
c   -- var.elim.:  8000/16714          
c   -- var.elim.:  9000/16714          
c   -- var.elim.:  10000/16714          
c   -- var.elim.:  11000/16714          
c   -- var.elim.:  12000/16714          
c   -- var.elim.:  13000/16714          
c   -- var.elim.:  14000/16714          
c   -- var.elim.:  15000/16714          
c   -- var.elim.:  16000/16714          
c   -- var.elim.:  16714/16714          
c   -- var.elim.:  1000/1833          
c   -- var.elim.:  1833/1833          
c   -- var.elim.:  109/109          
c   -- subsuming                       
c   -- var.elim.:  310/310          
c   -- var.elim.:  103/103          
c |    103369 |  204847   678897 |      --  102576       --      -- |     --   | -1278/-1240
c |    103369 |  204847   678897 |   81938   99909  2064613    20.7 | 18.719 % |
c |    103469 |  204847   678897 |   90132   18455   706904    38.3 | 14.227 % |
c |    103619 |  204847   678897 |   99145   18605   707728    38.0 | 14.227 % |
c |    103846 |  204847   678897 |  109060   18832   709166    37.7 | 14.227 % |
c |    104184 |  204847   678897 |  119966   19170   710718    37.1 | 14.227 % |
c |    104691 |  204847   678897 |  131963   19677   713759    36.3 | 14.227 % |
c |    105451 |  204847   678897 |  145159   20437   718084    35.1 | 14.227 % |
c |    106591 |  204733   678462 |  159586   21571   725198    33.6 | 14.259 % |
c |    108299 |  204733   678462 |  175545   23279   735599    31.6 | 14.259 % |
c |    110861 |  204411   677380 |  192796   25827   750930    29.1 | 14.380 % |
c |    114709 |  204098   676283 |  211751   29659   779057    26.3 | 14.481 % |
c |    120475 |  203861   675396 |  232655   35407   821902    23.2 | 14.561 % |
c |    129125 |  203730   674978 |  255756   44045   890498    20.2 | 14.613 % |
c |    142099 |  203097   672683 |  280458   56919  1112760    19.5 | 14.822 % |
c ==============================================================================
c (current CPU-time: 266.675 s)
c ==============================================================================
c [1mFound solution: 4467151[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4244191   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    160385 |  203092   672677 |   60927   75188  1549296    20.6 | 14.822 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1083          
c   -- var.elim.:  1083/1083          
c   -- var.elim.:  798/798          
c   -- var.elim.:  124/124          
c   -- subsuming                       
c   -- var.elim.:  176/176          
c   -- var.elim.:  76/76          
c |    160385 |  202573   672236 |      --   75188       --      -- |     --   | -519/-434
c |    160385 |  202573   672236 |   81029   74528  1541168    20.7 | 14.822 % |
c |    160486 |  202573   672236 |   89132   74629  1541858    20.7 | 14.978 % |
c |    160637 |  202573   672236 |   98045   74780  1543937    20.6 | 14.978 % |
c |    160862 |  202573   672236 |  107849   75005  1547517    20.6 | 14.978 % |
c |    161199 |  202573   672236 |  118634   75342  1552720    20.6 | 14.978 % |
c |    161705 |  202573   672236 |  130498   75848  1557705    20.5 | 14.978 % |
c |    162464 |  202565   672213 |  143542   76606  1566830    20.5 | 14.980 % |
c |    163605 |  202515   672023 |  157857   77745  1580204    20.3 | 14.992 % |
c |    165314 |  202413   671655 |  173556   79445  1600520    20.1 | 15.023 % |
c |    167876 |  202236   670991 |  190744   81977  1677146    20.5 | 15.068 % |
c |    171721 |  202220   670934 |  209802   85821  1744622    20.3 | 15.072 % |
c |    177490 |  202146   670680 |  230698   91570  1913830    20.9 | 15.096 % |
c |    186139 |  202146   670680 |  253768  100219  2216172    22.1 | 15.096 % |
c |    199114 |  202146   670680 |  279145  113194  4528710    40.0 | 15.096 % |
c ==============================================================================
c (current CPU-time: 378.715 s)
c ==============================================================================
c [1mFound solution: 3724532[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4986810   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    217655 |  201950   670142 |   60584  131708  5114263    38.8 | 15.096 % |
c   -- subsuming                       
c   -- var.elim.:  560/560          
c   -- var.elim.:  384/384          
c   -- var.elim.:  22/22          
c   -- var.elim.:  16/16          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  91/91          
c   -- var.elim.:  45/45          
c |    217655 |  201741   669940 |      --  131708       --      -- |     --   | -209/-190
c |    217655 |  201741   669940 |   80696  131250  5106262    38.9 | 15.096 % |
c |    217755 |  201654   669650 |   88727   23291   506682    21.8 | 15.294 % |
c |    217905 |  201654   669650 |   97600   23441   507434    21.6 | 15.294 % |
c |    218131 |  201638   669584 |  107352   23666   508696    21.5 | 15.299 % |
c |    218468 |  201539   669183 |  118029   24002   510485    21.3 | 15.325 % |
c |    218974 |  201539   669183 |  129832   24508   513040    20.9 | 15.325 % |
c |    219733 |  201442   668857 |  142746   25249   517979    20.5 | 15.355 % |
c |    220872 |  201442   668857 |  157021   26388   524635    19.9 | 15.355 % |
c |    222580 |  201438   668846 |  172720   28095   535186    19.0 | 15.358 % |
c |    225143 |  201409   668741 |  189964   30657   552331    18.0 | 15.367 % |
c |    228987 |  201409   668741 |  208961   34501   576811    16.7 | 15.367 % |
c |    234753 |  201409   668741 |  229857   40267   635271    15.8 | 15.367 % |
c |    243403 |  201233   668021 |  252622   48890   780285    16.0 | 15.422 % |
c |    256377 |  201125   667606 |  277735   61852   934219    15.1 | 15.455 % |
c |    275839 |  201001   667138 |  305320   81280  1716054    21.1 | 15.495 % |
c |    305031 |  200927   666866 |  335728  110466  3190747    28.9 | 15.514 % |
c |    348821 |  200900   666768 |  369252  154243  8985603    58.3 | 15.521 % |
c |    414506 |  200831   666505 |  406037  219918 15411117    70.1 | 15.543 % |
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 -X258_bit_7 -X258_bit_6 X258_bit_5 X258_bit_4 X258_bit_3 -X258_bit_2 X258_bit_1 -X258_bit0 -X258_bit1 -X258_bit2 -X258_bit3 -X258_bit4 -X258_bit5 -X258_bit6 -X258_bit7 -X258_bit8 -X258_bit9 -X258_bit10 -X258_bit11 -X258_bit12 -X259_bit_7 -X259_bit_6 -X259_bit_5 -X259_bit_4 -X259_bit_3 -X259_bit_2 -X259_bit_1 -X259_bit0 -X259_bit1 -X259_bit2 -X259_bit3 -X259_bit4 -X259_bit5 -X259_bit6 -X259_bit7 -X259_bit8 -X259_bit9 -X259_bit10 -X259_bit11 -X259_bit12 -Y0_bit0 -Y1_bit0 -Y2_bit0 Y3_bit0 Y4_bit0 -Y5_bit0 -Y6_bit0 -Y7_bit0 -Y8_bit0 Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 -Y13_bit0 Y14_bit0 -Y15_bit0 Y16_bit0 -Y17_bit0 -Y18_bit0 -Y19_bit0 -Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 -Y24_bit0 -Y25_bit0 Y26_bit0 -Y27_bit0 Y28_bit0 -Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 -Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 -Y37_bit0 -Y38_bit0 Y39_bit0 -Y40_bit0 Y41_bit0 Y42_bit0 -Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 -Y48_bit0 Y49_bit0 Y50_bit0 -Y51_bit0 Y52_bit0 -Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 Y57_bit0 Y58_bit0 Y59_bit0 -Y60_bit0 Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 Y69_bit0 -Y70_bit0 Y71_bit0 Y72_bit0 Y73_bit0 -Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 Y79_bit0 Y80_bit0 Y81_bit0 Y82_bit0 Y83_bit0 Y84_bit0 Y85_bit0 Y86_bit0 Y87_bit0 -Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 -Y92_bit0 Y93_bit0 -Y94_bit0 -Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 Y103_bit0 -Y104_bit0 Y105_bit0 -Y106_bit0 Y107_bit0 Y108_bit0 -Y109_bit0 Y110_bit0 -Y111_bit0 Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 -Y116_bit0 Y117_bit0 Y118_bit0 Y119_bit0 Y120_bit0 -Y121_bit0 Y122_bit0 -Y123_bit0 Y124_bit0 -Y125_bit0 Y126_bit0 Y127_bit0 -Y128_bit0 Y129_bit0 -Y130_bit0 Y131_bit0 Y132_bit0 -Y133_bit0 Y134_bit0 Y135_bit0 Y136_bit0 Y137_bit0 -Y138_bit0 Y139_bit0 Y140_bit0 -Y141_bit0 Y142#### 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.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (runsolver) R 7886 30701 30700 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 486417273 1052672 97 4294967295 134512640 135381576 3221224432 3221219872 134514522 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8699 0 0 0 972 26 0 0 25 0 1 0 486417273 35680256 7428 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8711 7428 603 41 0 8670 0
vsize: 34844
[startup+20.0004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8722 0 0 0 1971 27 0 0 25 0 1 0 486417273 35680256 7451 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8711 7451 603 41 0 8670 0
vsize: 34844
[startup+30.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8730 0 0 0 2971 27 0 0 25 0 1 0 486417273 35680256 7459 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8711 7459 603 41 0 8670 0
vsize: 34844
[startup+40.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8738 0 0 0 3971 27 0 0 25 0 1 0 486417273 35680256 7467 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8711 7467 603 41 0 8670 0
vsize: 34844
[startup+50.0014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8803 0 0 0 4971 27 0 0 25 0 1 0 486417273 36077568 7532 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8808 7532 603 41 0 8767 0
vsize: 35232
[startup+60.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 8894 0 0 0 5972 27 0 0 25 0 1 0 486417273 36474880 7623 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8905 7623 603 41 0 8864 0
vsize: 35620
[startup+70.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 9024 0 0 0 6972 27 0 0 25 0 1 0 486417273 37011456 7753 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9036 7753 603 41 0 8995 0
vsize: 36144
[startup+80.0014 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 9175 0 0 0 7971 27 0 0 25 0 1 0 486417273 37552128 7904 4294967295 134512640 134672761 3221224544 3221223728 134615554 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9168 7904 603 41 0 9127 0
vsize: 36672
[startup+90.0007 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 9261 0 0 0 8971 27 0 0 25 0 1 0 486417273 37949440 7990 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9265 7990 603 41 0 9224 0
vsize: 37060
[startup+100.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 9789 0 0 0 9970 29 0 0 25 0 1 0 486417273 40067072 8518 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 8518 603 41 0 9741 0
vsize: 39128
[startup+110.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 9912 0 0 0 10970 29 0 0 25 0 1 0 486417273 40734720 8641 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9945 8641 603 41 0 9904 0
vsize: 39780
[startup+120.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 10023 0 0 0 11970 29 0 0 25 0 1 0 486417273 41267200 8752 4294967295 134512640 134672761 3221224544 3221223680 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10075 8752 603 41 0 10034 0
vsize: 40300
[startup+130.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 10601 0 0 0 12969 31 0 0 25 0 1 0 486417273 43515904 9330 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10624 9330 603 41 0 10583 0
vsize: 42496
[startup+140 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 11038 0 0 0 13968 31 0 0 25 0 1 0 486417273 45244416 9767 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11046 9768 603 41 0 11005 0
vsize: 44184
[startup+150.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 13111 0 0 0 14963 37 0 0 25 0 1 0 486417273 55160832 11816 4294967295 134512640 134672761 3221224544 3221222980 134542660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13467 11816 603 41 0 13426 0
vsize: 53868
[startup+160.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21422 0 0 0 15942 58 0 0 25 0 1 0 486417273 71983104 16323 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 16323 603 41 0 17533 0
vsize: 70296
[startup+170 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21422 0 0 0 16942 58 0 0 25 0 1 0 486417273 71983104 16323 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 16323 603 41 0 17533 0
vsize: 70296
[startup+180.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21455 0 0 0 17942 58 0 0 25 0 1 0 486417273 72245248 16356 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16356 603 41 0 17597 0
vsize: 70552
[startup+190.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21457 0 0 0 18942 58 0 0 25 0 1 0 486417273 72245248 16358 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16358 603 41 0 17597 0
vsize: 70552
[startup+200.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21462 0 0 0 19942 58 0 0 25 0 1 0 486417273 72245248 16363 4294967295 134512640 134672761 3221224544 3221223728 134616037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16363 603 41 0 17597 0
vsize: 70552
[startup+210.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21462 0 0 0 20943 58 0 0 25 0 1 0 486417273 72245248 16363 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16363 603 41 0 17597 0
vsize: 70552
[startup+220.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21462 0 0 0 21943 58 0 0 25 0 1 0 486417273 72245248 16363 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16363 603 41 0 17597 0
vsize: 70552
[startup+230.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21462 0 0 0 22943 58 0 0 25 0 1 0 486417273 72245248 16363 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16363 603 41 0 17597 0
vsize: 70552
[startup+240.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21463 0 0 0 23943 58 0 0 25 0 1 0 486417273 72245248 16364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16364 603 41 0 17597 0
vsize: 70552
[startup+250.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21463 0 0 0 24943 58 0 0 25 0 1 0 486417273 72245248 16364 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16364 603 41 0 17597 0
vsize: 70552
[startup+260.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 21464 0 0 0 25943 58 0 0 25 0 1 0 486417273 72245248 16365 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17638 16365 603 41 0 17597 0
vsize: 70552
[startup+270.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 23816 0 0 0 26936 65 0 0 25 0 1 0 486417273 72310784 16442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17654 16442 603 41 0 17613 0
vsize: 70616
[startup+280.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 23816 0 0 0 27936 65 0 0 25 0 1 0 486417273 72310784 16442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17654 16442 603 41 0 17613 0
vsize: 70616
[startup+290.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 23816 0 0 0 28936 65 0 0 25 0 1 0 486417273 72310784 16442 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17654 16442 603 41 0 17613 0
vsize: 70616
[startup+300.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 23816 0 0 0 29936 65 0 0 25 0 1 0 486417273 72310784 16442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17654 16442 603 41 0 17613 0
vsize: 70616
[startup+310.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 23818 0 0 0 30936 65 0 0 25 0 1 0 486417273 72441856 16444 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17686 16444 603 41 0 17645 0
vsize: 70744
[startup+320.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 24174 0 0 0 31935 67 0 0 25 0 1 0 486417273 73904128 16800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18043 16800 603 41 0 18002 0
vsize: 72172
[startup+330.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 24800 0 0 0 32934 68 0 0 25 0 1 0 486417273 76423168 17426 4294967295 134512640 134672761 3221224544 3221223584 134612932 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18658 17426 603 41 0 18617 0
vsize: 74632
[startup+340.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 25780 0 0 0 33931 71 0 0 25 0 1 0 486417273 80392192 18406 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19627 18406 603 41 0 19586 0
vsize: 78508
[startup+350.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 26698 0 0 0 34928 74 0 0 25 0 1 0 486417273 84090880 19324 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20530 19324 603 41 0 20489 0
vsize: 82120
[startup+360.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 26821 0 0 0 35928 74 0 0 25 0 1 0 486417273 84627456 19447 4294967295 134512640 134672761 3221224544 3221223696 134614481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20661 19447 603 41 0 20620 0
vsize: 82644
[startup+370.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 27222 0 0 0 36927 75 0 0 25 0 1 0 486417273 86208512 19848 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21047 19848 603 41 0 21006 0
vsize: 84188
[startup+380.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 29381 0 0 0 37921 82 0 0 25 0 1 0 486417273 90652672 20785 4294967295 134512640 134672761 3221224544 3221222776 1075352361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22132 20785 603 41 0 22091 0
vsize: 88528
[startup+390.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 38918 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+400.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 39919 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+410.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 40919 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+420.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 41919 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+430.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 42919 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223720 134565025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+440.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 43919 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+450.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 44920 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+460.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 45920 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+470.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 46920 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+480.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 47920 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+490.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 48920 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+500.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 49921 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+510.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 50921 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+520.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 51921 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+530.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 52921 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+540.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 53921 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223724 134616076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+550.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30444 0 0 0 54922 84 0 0 25 0 1 0 486417273 87941120 20181 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21470 20181 603 41 0 21429 0
vsize: 85880
[startup+560.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 30865 0 0 0 55920 85 0 0 25 0 1 0 486417273 89784320 20602 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21920 20602 603 41 0 21879 0
vsize: 87680
[startup+570.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 31715 0 0 0 56919 87 0 0 25 0 1 0 486417273 93216768 21452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22758 21452 603 41 0 22717 0
vsize: 91032
[startup+580.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 32500 0 0 0 57917 89 0 0 25 0 1 0 486417273 96391168 22237 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23533 22237 603 41 0 23492 0
vsize: 94132
[startup+590.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 33159 0 0 0 58916 91 0 0 25 0 1 0 486417273 99041280 22896 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24180 22896 603 41 0 24139 0
vsize: 96720
[startup+600.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 33835 0 0 0 59914 93 0 0 25 0 1 0 486417273 101818368 23572 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24858 23572 603 41 0 24817 0
vsize: 99432
[startup+610.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 34388 0 0 0 60912 95 0 0 25 0 1 0 486417273 104058880 24125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25405 24125 603 41 0 25364 0
vsize: 101620
[startup+620.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 34680 0 0 0 61911 96 0 0 25 0 1 0 486417273 105263104 24417 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25699 24417 603 41 0 25658 0
vsize: 102796
[startup+630.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 34854 0 0 0 62911 96 0 0 25 0 1 0 486417273 105930752 24591 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25862 24591 603 41 0 25821 0
vsize: 103448
[startup+640.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 35159 0 0 0 63910 97 0 0 25 0 1 0 486417273 107257856 24896 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26186 24896 603 41 0 26145 0
vsize: 104744
[startup+650.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 35497 0 0 0 64909 98 0 0 25 0 1 0 486417273 108593152 25234 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26512 25234 603 41 0 26471 0
vsize: 106048
[startup+660.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 35857 0 0 0 65908 100 0 0 25 0 1 0 486417273 110047232 25594 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26867 25594 603 41 0 26826 0
vsize: 107468
[startup+670.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 36283 0 0 0 66906 102 0 0 25 0 1 0 486417273 111775744 26020 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27289 26020 603 41 0 27248 0
vsize: 109156
[startup+680.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 36945 0 0 0 67904 104 0 0 25 0 1 0 486417273 114405376 26682 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27931 26682 603 41 0 27890 0
vsize: 111724
[startup+690.006 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 37505 0 0 0 68904 105 0 0 25 0 1 0 486417273 116776960 27242 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28510 27242 603 41 0 28469 0
vsize: 114040
[startup+700.006 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 38047 0 0 0 69902 107 0 0 25 0 1 0 486417273 118902784 27784 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29029 27784 603 41 0 28988 0
vsize: 116116
[startup+710.007 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 38547 0 0 0 70901 108 0 0 25 0 1 0 486417273 120901632 28284 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29517 28284 603 41 0 29476 0
vsize: 118068
[startup+720.007 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 39041 0 0 0 71900 109 0 0 25 0 1 0 486417273 123006976 28778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30031 28778 603 41 0 29990 0
vsize: 120124
[startup+730.007 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 39551 0 0 0 72899 111 0 0 25 0 1 0 486417273 125018112 29288 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30522 29288 603 41 0 30481 0
vsize: 122088
[startup+740.007 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 40056 0 0 0 73898 112 0 0 25 0 1 0 486417273 127135744 29793 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31039 29793 603 41 0 30998 0
vsize: 124156
[startup+750.008 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 40538 0 0 0 74897 113 0 0 25 0 1 0 486417273 129114112 30275 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31522 30275 603 41 0 31481 0
vsize: 126088
[startup+760.007 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 40974 0 0 0 75896 114 0 0 25 0 1 0 486417273 130854912 30711 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31947 30711 603 41 0 31906 0
vsize: 127788
[startup+770.007 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 41160 0 0 0 76895 115 0 0 25 0 1 0 486417273 131670016 30897 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32146 30897 603 41 0 32105 0
vsize: 128584
[startup+780.008 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 41437 0 0 0 77895 116 0 0 25 0 1 0 486417273 132857856 31174 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32436 31174 603 41 0 32395 0
vsize: 129744
[startup+790.008 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 41746 0 0 0 78894 117 0 0 25 0 1 0 486417273 134041600 31483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32725 31483 603 41 0 32684 0
vsize: 130900
[startup+800.008 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 41984 0 0 0 79894 117 0 0 25 0 1 0 486417273 135110656 31721 4294967295 134512640 134672761 3221224544 3221223688 134616314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32986 31721 603 41 0 32945 0
vsize: 131944
[startup+810.009 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 42319 0 0 0 80893 118 0 0 25 0 1 0 486417273 136437760 32056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33310 32056 603 41 0 33269 0
vsize: 133240
[startup+820.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 42814 0 0 0 81892 119 0 0 25 0 1 0 486417273 138440704 32551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33799 32551 603 41 0 33758 0
vsize: 135196
[startup+830.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 43601 0 0 0 82890 122 0 0 25 0 1 0 486417273 141611008 33338 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34573 33338 603 41 0 34532 0
vsize: 138292
[startup+840.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 44277 0 0 0 83889 123 0 0 25 0 1 0 486417273 144384000 34014 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35250 34014 603 41 0 35209 0
vsize: 141000
[startup+850.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 44863 0 0 0 84887 125 0 0 25 0 1 0 486417273 146759680 34600 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35830 34600 603 41 0 35789 0
vsize: 143320
[startup+860.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 45361 0 0 0 85885 127 0 0 25 0 1 0 486417273 148869120 35098 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36345 35098 603 41 0 36304 0
vsize: 145380
[startup+870.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 45844 0 0 0 86884 128 0 0 25 0 1 0 486417273 150712320 35581 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36795 35581 603 41 0 36754 0
vsize: 147180
[startup+880.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 46346 0 0 0 87883 129 0 0 25 0 1 0 486417273 152821760 36083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37310 36083 603 41 0 37269 0
vsize: 149240
[startup+890.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 46811 0 0 0 88882 131 0 0 25 0 1 0 486417273 154791936 36548 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37791 36548 603 41 0 37750 0
vsize: 151164
[startup+900.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 47273 0 0 0 89881 132 0 0 25 0 1 0 486417273 156631040 37010 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38240 37010 603 41 0 38199 0
vsize: 152960
[startup+910.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 47746 0 0 0 90880 133 0 0 25 0 1 0 486417273 158490624 37483 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38694 37483 603 41 0 38653 0
vsize: 154776
[startup+920.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 48204 0 0 0 91879 134 0 0 25 0 1 0 486417273 160448512 37941 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39172 37941 603 41 0 39131 0
vsize: 156688
[startup+930.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 48644 0 0 0 92879 135 0 0 25 0 1 0 486417273 162160640 38381 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39590 38381 603 41 0 39549 0
vsize: 158360
[startup+940.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 49097 0 0 0 93878 135 0 0 25 0 1 0 486417273 164016128 38834 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40043 38834 603 41 0 40002 0
vsize: 160172
[startup+950.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 49566 0 0 0 94878 136 0 0 25 0 1 0 486417273 165998592 39303 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40527 39303 603 41 0 40486 0
vsize: 162108
[startup+960.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 50031 0 0 0 95877 137 0 0 25 0 1 0 486417273 167866368 39768 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40983 39768 603 41 0 40942 0
vsize: 163932
[startup+970.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 50451 0 0 0 96876 138 0 0 25 0 1 0 486417273 169578496 40188 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41401 40188 603 41 0 41360 0
vsize: 165604
[startup+980.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 50859 0 0 0 97875 139 0 0 25 0 1 0 486417273 171282432 40596 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41817 40596 603 41 0 41776 0
vsize: 167268
[startup+990.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 51264 0 0 0 98874 140 0 0 25 0 1 0 486417273 172867584 41001 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42204 41001 603 41 0 42163 0
vsize: 168816
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 51658 0 0 0 99874 141 0 0 25 0 1 0 486417273 174583808 41395 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42623 41395 603 41 0 42582 0
vsize: 170492
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 52080 0 0 0 100873 142 0 0 25 0 1 0 486417273 176295936 41817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43041 41817 603 41 0 43000 0
vsize: 172164
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 52468 0 0 0 101872 143 0 0 25 0 1 0 486417273 177876992 42205 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43427 42205 603 41 0 43386 0
vsize: 173708
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 52848 0 0 0 102871 144 0 0 25 0 1 0 486417273 179335168 42585 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43783 42585 603 41 0 43742 0
vsize: 175132
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 53244 0 0 0 103870 145 0 0 25 0 1 0 486417273 181051392 42981 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44202 42981 603 41 0 44161 0
vsize: 176808
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 53646 0 0 0 104870 146 0 0 25 0 1 0 486417273 182644736 43383 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44591 43383 603 41 0 44550 0
vsize: 178364
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 54011 0 0 0 105869 146 0 0 25 0 1 0 486417273 184098816 43748 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44946 43748 603 41 0 44905 0
vsize: 179784
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 54410 0 0 0 106869 147 0 0 25 0 1 0 486417273 185815040 44147 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45365 44147 603 41 0 45324 0
vsize: 181460
[startup+1080.01 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 54794 0 0 0 107868 148 0 0 25 0 1 0 486417273 188387328 44531 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45993 44531 603 41 0 45952 0
vsize: 183972
[startup+1090.01 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 55192 0 0 0 108867 149 0 0 25 0 1 0 486417273 190103552 44929 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46412 44929 603 41 0 46371 0
vsize: 185648
[startup+1100.01 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 55570 0 0 0 109866 150 0 0 25 0 1 0 486417273 191541248 45307 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46763 45307 603 41 0 46722 0
vsize: 187052
[startup+1110.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 55948 0 0 0 110866 151 0 0 25 0 1 0 486417273 193122304 45685 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47149 45685 603 41 0 47108 0
vsize: 188596
[startup+1120.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 56318 0 0 0 111865 152 0 0 25 0 1 0 486417273 194703360 46055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47535 46055 603 41 0 47494 0
vsize: 190140
[startup+1130.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 56678 0 0 0 112864 153 0 0 25 0 1 0 486417273 196165632 46415 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47892 46415 603 41 0 47851 0
vsize: 191568
[startup+1140.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 57038 0 0 0 113864 153 0 0 25 0 1 0 486417273 197619712 46775 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48247 46776 603 41 0 48206 0
vsize: 192988
[startup+1150.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 57391 0 0 0 114863 154 0 0 25 0 1 0 486417273 199065600 47128 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48600 47128 603 41 0 48559 0
vsize: 194400
[startup+1160.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 57778 0 0 0 115862 155 0 0 25 0 1 0 486417273 200658944 47515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48989 47515 603 41 0 48948 0
vsize: 195956
[startup+1170.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 58132 0 0 0 116861 157 0 0 25 0 1 0 486417273 202104832 47869 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49342 47869 603 41 0 49301 0
vsize: 197368
[startup+1180.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 58471 0 0 0 117860 158 0 0 25 0 1 0 486417273 203431936 48208 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49666 48208 603 41 0 49625 0
vsize: 198664
[startup+1190.01 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 58848 0 0 0 118859 159 0 0 25 0 1 0 486417273 205008896 48585 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50051 48585 603 41 0 50010 0
vsize: 200204
[startup+1200.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 7887
Raw data (stat): 7887 (minisat+) R 7886 30701 30700 0 -1 0 59207 0 0 0 119858 160 0 0 25 0 1 0 486417273 206458880 48944 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50405 48944 603 41 0 50364 0
vsize: 201620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.01 1.00 0.93 1/54 7887
Raw data (stat): 7887 (minisat+) Z 7886 30701 30700 0 -1 12 59208 0 0 0 119859 170 0 0 25 0 1 0 486417273 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.13
CPU time (s): 1200.3
CPU user time (s): 1198.6
CPU system time (s): 1.70774
CPU usage (%): 100.015
Max. virtual memory (Kb): 201620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####